nLab
preset

Presets

Context

Foundations

Category theory

(,1)(\infty,1)-Category theory

(,1)(\infty,1)-Topos Theory

(∞,1)-topos theory

Background

Definitions

Characterization

Morphisms

Extra stuff, structure and property

Models

Constructions

structures in a cohesive (∞,1)-topos

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Presets

Idea

A preset is a set without an equality relation. Conversely, a set may be defined as a preset XX equipped with an equality relation (technically an equivalence prerelation on XX).

In his seminal work The Foundations of Constructive Analysis (1967), Errett Bishop explained what you must do to define a set (see also Bishop set) in three steps:

  1. You must state what one must do to construct an element of the set;
  2. Given two elements constructed as in (1), you must state what one must do to prove that the elements are equal;
  3. You must prove that the relation defined in (2) is reflexive, symmetric, and transitive (which can be phrased in similar ‘what one must do’ terms, but that's kind of wordy).

If you only do (1), then you don't have a set, according to Bishop; you only have a preset.

A given preset may define many different sets, depending on the equality relation. For example, the set Q +Q^+ of positive rational numbers may be defined using the same preset as the set Z +×Z +Z^+ \times Z^+ of ordered pairs of positive integers, but the equality relation is different; two pairs (a,b)(a,b) and (c,d)(c,d) of positive integers are equal iff a=ca = c and b=db = d, while two positive rational numbers a/ba/b and c/dc/d are equal iff ad=bca d = b c. (Of course, these definitions require that one already has the set Z +Z^+ of positive integers, including its equality relation, and the operation of multiplication on it.)

Prefunctions and prerelations

As functions go between sets, so prefunctions go between presets. (Bishop used the term ‘operation’ instead of ‘prefunction’, but ‘operation’ has many other meanings.) Even if XX and YY are sets, a prefunction from XX to YY is not the same as a function from XX to YY, because a prefunction need not preserve equality; that is, we may have a=ba = b without f(a)=f(b)f(a) = f(b). Conversely, we may define a function as a prefunction (between sets) that preserves equality; such a prefunction is said to be extensional.

For example, consider the identity prefunction on the underlying preset of both Q +Q^+ and Z +×Z +Z^+ \times Z^+, as defined above. From Z +×Z +Z^+ \times Z^+ to Q +Q^+, this is a function, since a/b=c/da/b = c/d if (a,b)=(c,d)(a,b) = (c,d). But from Q +Q^+ to Z +×Z +Z^+ \times Z^+, it is not a function, since (for example) 2/4=3/62/4 = 3/6 but (2,4)(3,6)(2,4) \neq (3,6). A related example is the operation of taking the numerator of a (positive) rational number; from Q +Q^+ to Z +Z^+, we may view this as a prefunction but not as a function, although it is a function on Z +×Z +Z^+ \times Z^+.

In general, the prefunctions from XX to YY form a preset, since there is no way to compare them for equality. (Of course, it is still impredicative, at least in the classical sense, to form this preset.) However, if YY is a set, then these prefunctions do form a set, with f=gf = g defined to mean that f(a)=g(a)f(a) = g(a) for every aa in XX. If XX is also a set, then the function set from XX to YY is a subset of this set of prefunctions.

Composition of prefunctions is also possible, but likewise does not preserve equality.

A (say binary) prerelation between XX and YY may be thought of as a prefunction from X×YX \times Y to truth values. Even if one is too predicative to allow a (pre)set of truth values, still one may have a notion of prerelation, by fiat if nothing else. Note that one can compare prerelations for equality; R=SR = S means that a Rba \sim_R b if and only if a Sba \sim_S b. (In other words, a preset of truth values becomes a set under the biconditional, so we can compare functions to it.) We define a relation between sets to be a prerelation that respects equality.

Many properties of relations can also be predicated of prerelations, but not all. In particular, prerelations may be reflexive, symmetric, and transitive, so we have a notion of equivalence prerelation, which completes the definition of sets in terms of presets. A prerelation may also be entire, but it makes no sense to ask if it is functional unless YY is a set. In that case, there is a correspondence between prefunctions and functional entire prerelations as usual. In general, however, there is no way to define the prerelation corresponding to a given prefunction (which would be a sort of pre-graph). In other words, the idea that functions are certain relations (namely the functional entire ones) does not extended to prefunctions and prerelations unless YY is a set.

Formalisation

In category theory

One definition of the category PresetPreset of presets is a weak category that is finitely complete, infinitary extensive, and well-pointed (i.e. whose terminal object is a extremal generating object).

The category Set Set of sets is the full subcategory of PresetPreset where all equivalence prerelations have effective quotients, and the category SetoidSetoid of setoids and is the ex/lex completion of PresetPreset. This means both SetSet and SetoidSetoid are Grothendieck topoi over the point satisfying Giraud's axioms. As the ex/lex completion is a free completion, there is a free functor F:PresetSetF: Preset \rightarrow Set that is the left adjoint of the forgetful functor U:SetPresetU: Set \rightarrow Preset, and SetoidSetoid could also be thought of as a subcategory of SetSet, as the category of free sets. (Note that the cofree set on a preset always exists; it is a subsingleton.)

If the presentation axiom (a weak form of the full axiom of choice) holds in SetoidSetoid, as a subcategory of SetSet, SetoidSetoid could be thought of as the category of completely presented sets, the category of sets with a projective presentation. If the axiom of choice holds in PresetPreset, then PresetPreset is equivalent to SetoidSetoid, as the axiom of choice implies that PresetPreset is its own free exact completion, and PresetPreset is equivalent to SetSet because the free functor from PresetPreset to SetSet is an equivalence of categories.

However, these presets still have an equality defined, due to the fact that the hom-object of a weak category is still a set, which means that the morphisms are functions and elements, and function composition preserves equality, so that these ‘presets’ are still sets in some sense; see preset for a discussion of this issue. Commonly, these ‘presets’ are the categorical semantics of an extensional type theory without quotient types (see below) such as Martin-Löf type theory, so are more accurately called ‘extensional types’ instead, belonging to the category ExTypeExType of extensional types instead of PresetPreset.

Instead, it would be more faithful to the original definition of preset for the category PresetPreset of presets and prefunctions to be a weak preset-enriched category whose objects are presets as well, as prefunctions form a preset. But without equality, one has to replace the associative identity and identity morphism axioms for a category with a 2-morphism called the associator that satisfies the pentagon identity and 2-morphisms called the left and right unitors that satisfy the triangle identities, resulting in a preset-enriched (2,1)-category. However, the pentagon identity also involves equalities and so would have to be replaced with a 3-morphism called the pentagonator, and so on, creating a preset-enriched (3,1)-category, a preset-enriched (4,1)-categoy, and so on. In the limit of this process, a preset-enriched category turns out to be an preset-enriched (infinity,1)-category of presets, or a infinity-groupoid-enriched (infinity,1)-category, whose objects are infinity-groupoids as well. This means that PresetPreset is actually equivalent to Grpd \infty Grpd , the (infinity,1)-topos of infinity-groupoids. While every preset still has an equivalence prerelation, these equivalence prerelations represent path space objects instead of equality, and so are still not sets. This means that sets have to be defined using a different definition; indeed, a set is defined as a preset with a path space object where all n-morphisms for n1n\geq 1 are trivial, such that the set is 0-truncated. Sets as defined have quotients, as quotients of sets can be constructed as an (infinity,1)-colimit. These ‘presets’ are the categorical semantics for homotopy type theory.

In type theory

Many foundations based on type theory, such as those of Per Martin-Löf and Thierry Coquand, use types (sometimes called ‘sets’, but they don't have quotients) which behave something like presets (and are sometimes even called ‘presets’). Then a set (sometimes called ‘setoid’) is defined as above, as a type with an equality relation. However, these types usually come equipped with ‘identity’ relations, which are equality relations in all but name; this amounts to saying that every preset has a free set. They usually also adopt an axiom of choice for prefunctions that, together with the identity relations, proves the presentation axiom for general sets, which means that free sets are completely presented sets.

It is possible to develop type-theoretic foundations in which presets are not equipped with identity relations (only metamathematical identity or interconvertibilty judgements); see preset for some discussion. The presentation axiom is not provable in the base theory, although it is provable in the impredicative version (where identity relations can be defined, following Leibniz's definition of equality). A similar result holds for SEAR+ ϵ \epsilon .

In homotopy type theory, a preset is called an homotopy type and a prefunction is simply called a function, and the identity type represents homotopy equivalence instead of equality. In homotopy type theory, there is a truncation operation that allows homotopy types to be turned into n-types, and for n=0n=0, the 0-type is a set and the identity type for a 0-type is equality.

If you are willing to accept the presentation axiom, then you can define a notion of preset internal to a given theory of sets: as a projective set. (With the full axiom of choice, therefore, a preset is simply a set.) Alternatively, you might forgo presets as such but define a prefunction between sets to be an entire relation; although not everything translates, some of the properties are similar.

In logic

If an untyped first-order logic does not have equality of propositions or equality of predicates, then the domain of discourse is a preset instead of a set. This remains true for typed first-order logic with multiple types, which are presets if each type does not have local equality.

The sorts in Michael Makkai's FOLDS are presets. FOLDS is very different from the other foundations considered above, since it is based strictly on prerelations and has no notion of prefunction. As far as I can tell, it therefore does not prove the presentation axiom.

Applications

To make the principle of equivalence hold automatically, a category should have only a preset of objects and only its hom-sets as sets. Then a category whose set of objects is a set may be called a strict category, which is really a special case of a strict ∞-category. Alternatively, one may keep sets as sets but adopt preclasses; then a small category is strict but a large category is not.

In constructive mathematics, we want the real numbers to form a linearly ordered Heyting field RR with completeness for located Dedekind cuts. Using power sets and a set NN of natural numbers, one may form RR directly as a subset of 𝒫N\mathcal{P}N (or something equivalent), but what if you wish to be (at least weakly) predicative? Using function sets, one may form the Cauchy reals as a subquotient of N NN^N, but these are complete in the desired sense only if a weak form of countable choice (which follows from either the presentation axiom or excluded middle) holds. (Essentially, there may not be enough sequences of natural numbers.) Alternatively, if you have them, you can use prefunction sets and form RR as a subquotient of the set of presequences of natural numbers.

The construction of RR above may also be done with entire relations if the axiom of fullness holds (see also real numbers object). Conversely, the axiom of fullness follows from the existence of presets of prefunctions; in addition to defining a functional entire prerelation, a prefunction between sets also defines an entire relation, and the set of these satisfies fullness. (This is related to the idea that prefunctions between sets may be formalised as entire relations.)

See also the discussion at net about how to force the domain of a net to be partial order, by using either entire relations or prefunctions as nets.

Fixing inadequate foundations

Sometimes one finds a foundation of predicative mathematics in which it appears to be impossible to construct quotient sets, leading to much hand-wringing. (For a simple example, simply remove the axiom of power sets from ZFC as normally presented.) However, if you reinterpret the nominal ‘sets’ as presets and define a set as a preset equipped with an equivalence prerelation, then quotient sets exist after all. (In impredicative mathematics, there is a more familiar construction of a quotient set available, as a subset of a power set.)

Assuming (as usual) that the original foundation had equality relations on its sets, there will be identity prerelations on the presets, leading to a special class of sets (those which arise from equipping a preset with its identity prerelation) which we may again call the completely presented sets.

When you do this, the new kind of set is usually called a ‘setoid’, and then there may be hand-wringing about the need to use setoids instead of sets as one would like. But if you didn't have quotient sets originally, then you shouldn't have been talking about ‘sets’ in the first place; theories of sets without quotient sets are really theories of presets. (You can also use the term ‘type’ if it seems appropriate.)

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

Last revised on March 1, 2021 at 18:08:45. See the history of this page for a list of all contributions to it.