Homotopy Type Theory quotient set > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

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

Definition

In set theory

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

$\forall a \in S. \forall b \in S. (a \equiv b) \implies (\iota(a) = \iota(b))$

A quotient set algebra homomorphism of $S$ and $\equiv$ is a function $f \in B^A$ between two quotient set algebras $A$ and $B$ such that

$\forall a \in S. f(\iota_A(a)) = \iota_B(a)$

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

In homotopy type theory

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

• a function $\iota: T \to T/\equiv$

• a family of dependent terms

$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/\equiv, b:T/\equiv \vdash \tau(a, b): isProp(a =_{T/\equiv} b)$