nLab quotient equivalence relation

Idea

Similar to the construction of a quotient set from a set (i.e. h-set) with an equivalence relation as a higher inductive type in homotopy type theory, there is a construction of a “quotient equivalence relation” from a type with two equivalence relations, as an higher inductive type family.

This construction is reminiscent of the quotient set construction in set theory, because equality in set theory is defined in the foundations as a equivalence relation. The difference is that here we treat both equivalence relations on the same level, while in set theory one of the equivalence relations is given primacy as the default equality of the foundations.

Definition

Recall that an equivalence relation on a type $A$ is a type family $\sim$ consisting of dependent types $a \sim b$ indexed by objects $a:A$ and $b:A$, with witnesses of reflexivity, symmetry, and transitivity, and (-1)-truncatedness

$$a:A \vdash \mathrm{refl}(a):(a \sim a)$$

$$a:A, b:A \vdash \mathrm{sym}(a, b):(a \sim b) \to (b \sim a)$$

$$a:A, b:A, c:A \vdash \mathrm{trans}(a, b, c):(a \sim b) \times (b \sim c) \to (a \sim c)$$

$$a:A, b:A \vdash \mathrm{proptrunc}(a, b):\prod_{p:a \sim b} \prod_{q: a \sim b} p =_{a \sim b} q$$

Given a type $A$ with two equivalence relations $\equiv_A$ and $\sim_{A}$, the quotient equivalence relation on $(A, \equiv_{A}, \sim_{A})$ is the higher inductive type family $\equiv^{'}_{A}$ inductively generated by the following constructors:

• For each element $a:A$ and $b:A$, a function

  $$f_{\equiv_A}(a, b):(a \equiv_{A} b) \to (a \equiv^{'}_{A} b)$$

• For each element $a:A$ and $b:A$, a function

  $$f_{\sim_A}(a, b):(a \sim_{A} b) \to (a \equiv^{'}_{A} b)$$

• For each element $a:A$, a witness

  $$\mathrm{refl}(a):(a \equiv^{'}_{A} a)$$

• For each element $a:A$ and $b:A$, a witness

  $$\mathrm{sym}(a, b, c):(a \equiv^{'}_{A} b) \to (b \equiv^{'}_{A} a)$$

• For each element $a:A$, $b:A$, and $c:A$, a witness

  $$\mathrm{trans}(a, b, c):(a \equiv^{'}_{A} b) \times (b \equiv^{'}_{A} c) \to (a \equiv^{'}_{A} c)$$

• For each element $a:A$ and $b:A$, a witness

  $$\mathrm{proptrunc}(a, b):\prod_{p:a \equiv^{'}_{A} b} \prod_{q: a \equiv^{'}_{A} b} p =_{a \equiv^{'}_{A} b} q$$

See also

• higher inductive type
• inductive-inductive type
• quotient set
• equivalence relation