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 set theory, a setoid is usually described as a set with a pseudo-equivalence relation. However, in homotopy type theory or more generally in intensional type theory, there are multiple different ways to define the concept of a “collection with a pseudo-equivalence relation”. Presetoids arise from the most general possible notion of “collection with a pseudo-equivalence relation” in homotopy type theory , in the same way that the notion of precategory and pregroupoid arise when defining categories and groupoids.
A pseudo-equivalence relation on a type $A$ is a family of sets $Hom(a, b)$ of morphisms for each element $a:A$ and $b:A$, which comes with the following additional structure
for each element $a:A$ a family of morphisms
for each object $a:A$ and $b:A$ a family of functions
for each object $a:A$, $b:A$, and $c:A$, a family of functions
A presetoid $A$ consists of a type $Ob(A)$ of objects and a pseudo-equivalence relation $(\mathrm{Hom}, \mathrm{id}, \mathrm{dagger}, \mathrm{comp})$.
The structure-preserving maps between two presetoids are called dagger-functors. A dagger-functor $F:A \to B$ between two presetoids $A$ and $B$ consists of
a function $f_{Ob}:\mathrm{Ob}(A) \to \mathrm{Ob}(B)$
a family of functions $f_{hom}(a, b):\mathrm{Hom}_A(a, b) \to \mathrm{Hom}_B(f_{Ob}(a), f_{Ob}(b))$
and identifications indicating that the identity morphism, dagger, and the composition operation are preserved:
An dagger functor between two presetoids is faithful if every morphism function $f_{Hom}(a, b):\mathrm{Hom}_A(a, b) \to \mathrm{Hom}_B(f_{Ob}(a), f_{Ob}(b))$ is an injection. A dagger functor is embedding-on-objects if the object function $f_V:V_A \to V_B$ is an embedding, and equivalent-on-objects if the object function is a equivalence of types.
A subpresetoid $G$ of a presetoid $A$ is a presetoid $G$ with an faithful embedding-on-objects dagger functor $f:G \to A$. A subpresetoid $G$ of $A$ is a subpregroupoid if the pseudo-equivalence relation of $G$ additionally come with:
for every object $a:Ob(G)$, $b:Ob(G)$, $c:Ob(G)$, and $d:Ob(G)$ and morphism $f:Hom_G(a, b)$, $g:Hom_G(b, c)$, and $h:Hom_G(c, d)$, an identification
for every object $a:Ob(G)$, $b:Ob(G)$ and morphism $f:Hom_G(a, b)$, an identification
for every object $a:Ob(G)$, $b:Ob(G)$ and morphism $f:Hom_G(a, b)$, an identification
for every object $a:Ob(G)$, $b:Ob(G)$ and morphism $f:Hom_G(a, b)$, an identification
for every object $a:Ob(G)$, $b:Ob(G)$ and morphism $f:Hom_G(a, b)$, an identification
A subpregroupoid $G$ of a presetoid $A$ is a maximal subpregroupoid if the dagger functor $f:G \to A$ is equivalent-on-objects, and additionally if, for every other subgroupoid $H$ of $A$ with a faithful embedding-on-objects dagger functor $g:H \to A$, the type of faithful embedding-on-objects dagger functors $h:H \to G$ with an identification $\mathrm{up}(f, g, h):h \circ f = g$ is contractible.
The core pregroupoid $Core(A)$ of a setoid $A$ is the maximal subpregroupoid of $A$. Since the core is a pregroupoid, every morphism in the core is an isomorphism, and the type of morphisms between two objects $a$ and $b$ in the core of $A$ is denoted as $a \cong_A b$.
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 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 an h-groupoid.
Last revised on September 22, 2022 at 07:47:18. See the history of this page for a list of all contributions to it.