nLab univalent reflexive graph

Definition

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:

1. For each $x:A$ the type of elements $y:A$ such that $R(x, y)$ is a contractible type.

   $$x:A \vdash \mathrm{ua}(x):\mathrm{isContr}\left(\sum_{y:A} R(x, y)\right)$$

2. There is a family of equivalences

   $$x:A, y:A \vdash \mathrm{ua}(x, y):(x =_A y) \simeq R(x, y)$$

3. $R(x, y)$ is an identity system.

4. For each $x:A$ and $y:A$, the function $\mathrm{idtofam}(x, y)$ is an equivalence of types

   $$x:A, y:A, \vdash \mathrm{ua}(x, y):\mathrm{isEquiv}(\mathrm{idtofam}(x, y))$$

5. $\mathrm{idtofam}(x, y)$ has a retraction

   $$x:A, y:A \vdash \mathrm{ua}(x, y):R(x, y) \to (x =_A y)$$
   $$x:A, y:A, r:R(x, y) \vdash G(x, y):\mathrm{idtofam}(x, y, \mathrm{ua}(x, y, r)) =_{R(x, y)} r$$

6. That $R(x, y)$ with the function $\mathrm{idtofam}(x, y)$ satisfies the universal property of the unary sum of $x =_A y$.

Examples

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.

See also

• reflexive graph

• fundamental theorem of identity types

 References

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)