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 dependent type theory, a reflexive graph is a type $A$ with a type family $x:A, y:A \vdash R(x, y)$ and a family of functions $x:A, y:A \vdash \mathrm{idtofam}(x, y):(x =_A y) \to R(x, y)$.
Such a reflexive graph is a univalent reflexive graph if the following conditions hold, which are all equivalent by the fundamental theorem of identity types:
For each $x:A$ the type of elements $y:A$ such that $R(x, y)$ is a contractible type.
There is a family of equivalences
$R(x, y)$ is an identity system.
For each $x:A$ and $y:A$, the function $\mathrm{idtofam}(x, y)$ is an equivalence of types
$\mathrm{idtofam}(x, y)$ has a retraction
That $R(x, y)$ with the function $\mathrm{idtofam}(x, y)$ satisfies the universal property of the unary sum of $x =_A y$.
There are many examples of univalent reflexive graphs in mathematics. These include posets, T0-spaces, metric spaces, univalent categories, univalent groupoids, univalent dagger categories, univalent bicategories, univalent setoids, and univalent universes.
The definitions and proofs are generalized to general univalent reflexive graphs from the various definitions of univalent universes found in the homotopy type theory literature:
Univalent Foundations Project, p. 4 & Sec. 2.10 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
Dan Licata, weak univalence with “beta” implies full univalence (web)
Last revised on January 13, 2023 at 17:09:19. See the history of this page for a list of all contributions to it.