Homotopy Type Theory quotient set > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

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

Definition

In set theory

Let SS be a set and let \equiv be an equivalence relation on SS . Then Let the us quotient define set aS/S/\equivquotient set algebra of SS and \equiv is to be a set with a function ι A(S/) S \iota A \in {(S/\equiv)}^{S} 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 TT be a type, and let \equiv be an equivalence relation on TT.

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

References

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