natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
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.
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
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
For each element $a:A$ and $b:A$, a function
For each element $a:A$, a witness
For each element $a:A$ and $b:A$, a witness
For each element $a:A$, $b:A$, and $c:A$, a witness
For each element $a:A$ and $b:A$, a witness
Last revised on September 20, 2022 at 22:17:11. See the history of this page for a list of all contributions to it.