nLab preset

Presets

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Category theory

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

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

(∞,1)-topos theory

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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, an equivalence prerelation on XX which satisfies the principle of substitution and the identity of indiscernibles.

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.

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.) In particular, the principle of substitution and identity of indiscernibles together imply that any two equality relations on a preset are equal to each other, so equality is unique if it exists.

We define a relation between sets to be a prerelation that respects equality; such a prefunction is said to be extensional.

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.

In general, prerelations are

Presets, types, sets, and setoids

Presets do not have equality. However, the types in many type theories come equipped with some kind of identity type, where the only difference from equality is that they are not predicates. Thus, strictly speaking, the types in the type theories are not presets.

The sets defined by Bishop do not have quotient sets, so there is still a distinction between Bishop sets and the quotient set of an object with an equivalence relation: this is the difference between a set and a setoid. Some people call a set with no quotient sets a “preset”, however, this use of “preset” is at odds with preset as something that does not have equality.

While there is at most one equality on a preset due to the principle of substitution and the identity of indiscernibles, a given preset may have many different equivalence relations, giving rise to setoids. For example, the setoid Q +Q^+ of positive rational numbers may be defined using the same underlying set as the setoid Z +×Z +Z^+ \times Z^+ of ordered pairs of positive integers, but the equivalence relation is different; two pairs (a,b)(a,b) and (c,d)(c,d) of positive integers are equivalent iff a=ca = c and b=db = d, while two positive rational numbers a/ba/b and c/dc/d are equivalent iff ad=bca d = b c. (Of course, these definitions require that one already has the set Z +Z^+ of positive integers with its equality relation, and the operation of multiplication on it. Additionally, the cartesian product of two sets is itself a set.)

Formalisation

In category theory

One may hope to formalise the category of presets and prefunctions between presets, but unfortunately, presets and prefunctions do not form a category. Instead, they only form a magmoid.

In type theory

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. Unlike the case for types with identity relations, 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).

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.

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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 July 16, 2023 at 14:18:36. See the history of this page for a list of all contributions to it.