nLab set-like structures in homotopy type theory

Contents

Context

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

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Graph theory

Contents

Idea

Historically, there have been foundations which do not take the notion of set to be the fundamental notion. These include preset theories over first order logic such as certain presentations of SEAR, as well as type theories like MLTT and cubical type theory. In such theories, there have been multiple proposed definitions of what a set should be. These include:

In homotopy type theory (and more generally in any intensional type theory), all these definitions are valid, but they lead to different structures which behave differently from each other. This article is dedicated to distinguishing between the different set-like structures which have popped up throughout history, in the context of homotopy type theory.

Definitions

A proposition is a type AA such that for all elements a:Aa:A and b:Ab:A there is an element p(a,b):a= Abp(a, b):a =_A b. An h-set is a type AA where every identity type a= Aba =_A b is an proposition for all elements a:Aa:A and b:Ab:A.

We take the approach in CapriottiKraus17 in defining a graph A(A 0,A 1)A \coloneqq (A_0, A_1) to be a type A 0A_0 with a type family A 1(a,b)A_1(a, b) indexed by elements a:A 0a:A_0 and b:A 0b:A_0. While not defined in CapriottiKraus17, we could continue to borrow from graph theory terminology and call the type family A 1A_1 the edge type family of a graph.

The edge type family A 1A_1 is

  • transitive if it comes with a family of functions

    trans(a,b,c):(A 1(a,b)×A 1(b,c))A 1(a,c)\mathrm{trans}(a, b, c):(A_1(a, b) \times A_1(b, c)) \to A_1(a, c)
  • symmetric if it comes with a family of functions

    sym(a,b):A 1(a,b)A 1(b,a)\mathrm{sym}(a, b):A_1(a, b)\to A_1(b, a)
  • reflexive if it comes with a family of elements

    refl(a):A 1(a,a)\mathrm{refl}(a):A_1(a, a)

The graph (A 0,A 1)(A_0, A_1) is similarly called

  • transitive if its edge type family is transitive

  • symmetric if its edge type family is symmetric

  • reflexive if its edge type family is reflexive

In analogy with similar concepts in category theory (wild category, precategory, strict category, and univalent category), we define the following:

A wild set (A 0,A 1,trans,sym,refl)(A_0, A_1,\mathrm{trans}, \mathrm{sym}, \mathrm{refl}) is a reflexive, symmetric, transitive graph.

A preset is a wild set whose hom-types are h-propositions. This is the same as a type with an equivalence relation. Note that “preset” used here is different from the notion of preset in preset theories like SEAR without equality, which correspond more to bare types in homotopy type theory.

A strict set or strict preset is a preset whose object type is also an h-set.

A univalent set is a preset which satisfies the Rezk completion condition

idToArr:a= A 0bA 1(a,b)\mathrm{idToArr}:a =_{A_0} b \simeq A_1(a, b)

Univalent sets are the same as h-sets, and so they are typically just called sets.

We do the same for the notion of setoids/Bishop set:

A wild setoid (A 0,A 1,trans,sym,refl)(A_0, A_1,\mathrm{trans}, \mathrm{sym}, \mathrm{refl}) is the same as a wild set, a reflexive, symmetric, transitive graph. These are the setoids/Bishop sets talked about in general intensional type theory.

A presetoid is a wild setoid whose hom-types are h-sets. This is the same as a type with a pseudo-equivalence relation.

A strict setoid is a presetoid whose object type is also an h-set. These are the setoids/Bishop sets talked about in set-level foundations.

A univalent setoid is a presetoid which satisfies the Rezk completion condition

idToIso:a= A 0bab\mathrm{idToIso}:a =_{A_0} b \simeq a \cong b

where aba \cong b are the hom-sets of the core pregroupoid of the presetoid.

Bijections, isomorphisms, and equivalences

We begin with wild sets

A(A 0,A 1,trans A,refl A,sym A)A \coloneqq (A_0, A_1, \mathrm{trans}_A, \mathrm{refl}_A, \mathrm{sym}_A)
B(B 0,B 1,trans B,refl B,sym B)B \coloneqq (B_0, B_1, \mathrm{trans}_B, \mathrm{refl}_B, \mathrm{sym}_B)
C(C 0,C 1,trans C,refl C,sym C)C \coloneqq (C_0, C_1, \mathrm{trans}_C, \mathrm{refl}_C, \mathrm{sym}_C)

An extensional function between two wild sets f:ABf:A \to B consists of a function f 0:A 0B 0f_0:A_0 \to B_0 and for each object a:A 0a:A_0 and b:B 0b:B_0 a function f 1(a,b):A 1(a,b)B 1(a,b)f_1(a, b):A_1(a, b) \to B_1(a, b).

The identity function id A:AAid_A:A \to A is an extensional function which consists of the identity function id A 0:A 0A 0id_{A_0}:A_0 \to A_0 for all elements a:A 0a:A_0 and b:A 0b:A_0, the identity function id (a,b):(a Ab)(a Ab))id_\equiv(a, b):(a \equiv_A b) \to (a \equiv_A b)).

The composition gf:ACg \circ f:A \to C of extensional functions f:ABf:A \to B and g:BCg:B \to C is defined as

(gf) 0g 0f 0(g \circ f)_0 \coloneqq g_0 \circ f_0

and for all objects a:A 0a:A_0 and b:A 0b:A_0,

(gf) (a,b)g equiv(f 0(a),f 0(b))f equiv(a,b)(g \circ f)_\equiv(a, b) \coloneqq g_equiv(f_0(a), f_0(b)) \circ f_equiv(a, b)

We naively copy the set-theoretic definitions of injection, surjection, and bijection over to type theory

An extensional function f:ABf:A \to B is a injection if for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):B 1(f 0(a),b)p(a, b):B_1(f_0(a), b) is a subsingleton.

isInj(f) b:B 0isProp( a:AB 1(f 0(a),b))\mathrm{isInj}(f) \coloneqq \prod_{b:B_0} \mathrm{isProp}\left(\sum_{a:A} B_1(f_0(a), b)\right)

An extensional function f:ABf:A \to B is a surjection if for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):B 1(f 0(a),b)p(a, b):B_1(f_0(a), b) is inhabited.

isSurj(f) b:B 0| a:AB 1(f 0(a),b)|\mathrm{isSurj}(f) \coloneqq \prod_{b:B_0} \left|\sum_{a:A} B_1(f_0(a), b)\right|

An extensional function f:ABf:A \to B is a bijection if for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):B 1(f 0(a),b)p(a, b):B_1(f_0(a), b) is a singleton.

isBij(f) b:B 0isContr( a:AB 1(f 0(a),b))\mathrm{isBij}(f) \coloneqq \prod_{b:B_0} \mathrm{isContr}\left(\sum_{a:A} B_1(f_0(a), b)\right)

We also naively copy the categorical-theoretic definition of isomorphism over to type theory

An extensional function f:ABf:A \to B is an isomorphism if there exist an extensional function g:BAg:B \to A with witnesses

ret 0(f,g):(gf) 0=id A 0\mathrm{ret}_0(f, g):(g \circ f)_0 = id_{A_0}
sec 0(f,g):(fg) 0=id B 0\mathrm{sec}_0(f, g):(f \circ g)_0 = id_{B_0}
ret 1(f,g)(a,b):(gf) 1(a,b)=id A 1(a,b)\mathrm{ret}_1(f, g)(a, b):(g \circ f)_1(a, b) = id_{A_1}(a, b)
sec 1(f,g)(a,b):(fg) 1(a,b)=id B 1(a,b)\mathrm{sec}_1(f, g)(a, b):(f \circ g)_1(a, b) = id_{B_1}(a, b)

An extensional function f:ABf:A \to B is an equivalence if the function f 0:A 0B 0f_0:A_0 \to B_0 is an equivalence of types and for all elements a:A 0a:A_0 and b:A 0b:A_0 the function f 1(a,b):A 1(a,b)B 1(f 0(a),f 0(b))f_1(a, b):A_1(a, b) \to B_1(f_0(a), f_0(b)) is an equivalence of types.

The only notion of wild sets for which the set-theoretic notions of bijection, isomorphism, and equivalence are all the same is an h-set: a transitive, reflexive, and symmetric graph whose hom-types are propositionally truncated, and which satisfy the Rezk completion condition

idToArr:a= A 0bA 1(a,b)\mathrm{idToArr}:a =_{A_0} b \simeq A_1(a, b)

Isomorphism and equivalence of wild sets are the same only when both the object type and the hom-types are h-sets. Bijection and equivalence of wild sets are the same only in the presence of the Rezk completion condition on the structure. Combined with the requirement that the object type is an h-set, this automatically means that the hom-types are h-propositions, which makes the entire structure an h-set.

This is why h-sets are simply called sets in homotopy type theory and more generally in intensional type theory.

 See also

For a similar phenomenon in defining preorders and posets, see

And for defining a category in homotopy type theory, see

References

Last revised on September 26, 2022 at 19:40:49. See the history of this page for a list of all contributions to it.