Homotopy Type Theory quotient set > history (Rev #4)


Whenever editing is allowed on the nLab again, this article should be ported over there.


In set theory

Let SS be a set and let \equiv be an equivalence relation on SS. Let us define a quotient set algebra of SS and \equiv to be a set AA with a function ιA S\iota \in A^S such that

aS.bS.(ab)(ι(a)=ι(b))\forall a \in S. \forall b \in S. (a \equiv b) \implies (\iota(a) = \iota(b))

A quotient set algebra homomorphism of SS and \equiv is a function fB Af \in B^A between two quotient set algebras AA and BB such that

aS.f(ι A(a))=ι B(a)\forall a \in S. f(\iota_A(a)) = \iota_B(a)

The category of quotient set algebras of SS and \equiv is the category QSA(S,)QSA(S, \equiv) whose objects Ob(QSA(S,))Ob(QSA(S, \equiv)) are quotient set algebras of SS and \equiv and whose morphisms Mor(QSA(S,))Mor(QSA(S, \equiv)) are quotient set algebra homomorphisms of SS and \equiv. The quotient set of SS and \equiv, denoted S/S/\equiv, is defined as the initial object in the category of quotient set algebras of SS and \equiv.

In homotopy type theory

Let (T,)(T,\equiv) be a setoid. The quotient set T/T/\equiv is inductively generated by the following:

  • a function ι:TT/\iota: T \to T/\equiv

  • a family of dependent terms

    a:T,b:Teq T/(a,b):(ab)(ι(a)= T/ι(b))a:T, b:T \vdash eq_{T/\equiv}(a, b): (a \equiv b) \to (\iota(a) =_{T/\equiv} \iota(b))
  • a family of dependent terms

    a:T/,b:T/τ(a,b):isProp(a= T/b)a:T/\equiv, b:T/\equiv \vdash \tau(a, b): isProp(a =_{T/\equiv} b)

See also


Revision on April 27, 2022 at 15:38:10 by Anonymous?. See the history of this page for a list of all contributions to it.