Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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
Similar to how equality is stable if its double negation implies equality, an equivalence relation ought is stable if its double negation implies equality.
In set theory, an equivalence relation $\equiv$ on a set $S$ is stable if for all $a \in S$ and $b \in S$, if $\neg\neg(a \equiv b)$ then $a \equiv b$.
In type theory, a (proposition-valued) equivalence relation $\equiv$ on a type $T$ is stable if for all $a:T$ and $b:T$, there is a function $p(a, b):\neg\neg(a \equiv b) \to (a \equiv b)$.
Last revised on September 22, 2022 at 16:20:46. See the history of this page for a list of all contributions to it.