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
There are two ways to show that two objects of a presetoid are identified with each other: by way of the identity type, and by way of the type of isomorphisms in the core pregroupoid of a presetoid. Univalent setoids are precisely the presetoids which the two notions of identifying objects with each other coincide.
For each object $a:Ob(A)$ and $b:Ob(A)$ of a presetoid $A$, there is a function
from the identity type to the type of isomorphisms in the core pregroupoid $\mathrm{Core}(A)$ of $A$. A presetoid is a univalent setoid or a saturated setoid if for each object $a:Ob(A)$ and $b:Ob(A)$ the function
is an equivalence of types.
Since every type of morphisms in the core of the presetoid is a h-set, this means that every univalent setoid is a h-groupoid.
Last revised on September 22, 2022 at 11:47:51. See the history of this page for a list of all contributions to it.