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
In intensional type theory such as homotopy type theory a pregroupoid is a precategory $C$ with a family of functions $(-)^{{-1}_{a, b}}:Mor_C(a, b) \to Mor_C(b, a)$ for objects $a:Ob(C)$ and $b:Ob(C)$ and identifications $\lambda(a, b, f):f^{{-1}_{a, b}} \circ_{a, b, a} f = id_a$ and $\rho(a, b, f):f \circ_{b, a, b} f^{{-1}_{a, b}} = id_b$ for objects $a:Ob(C)$ and $b:Ob(C)$ and morphisms $f:Mor_C(a, b)$.
Equivalently, it is a dagger precategory with identifications $\lambda(a, b, f):f^{\dagger_{a, b}} \circ_{a, b, a} f = id_a$ and $\rho(a, b, f):f \circ_{b, a, b} f^{\dagger_{a, b}} = id_b$ for objects $a:Ob(C)$ and $b:Ob(C)$ and morphisms $f:Mor_C(a, b)$.
A pregroupoid whose sets of morphisms are all subsingletons is a symmetric proset.
A pregroupoid whose object type is a set is a strict groupoid.
A pregroupoid whose canonical functions
are equivalences of types for all objects $a:Ob(C)$ and $b:Ob(C)$ is a skeletal groupoid.
A pregroupoid whose canonical functions
are equivalences of types for all objects $a:Ob(C)$ and $b:Ob(C)$ is a univalent groupoid. Every 1-truncated type is equivalent to a univalent groupoid.
Every gaunt pregroupoid is a set.
Last revised on September 22, 2022 at 18:57:27. See the history of this page for a list of all contributions to it.