Spahn univalence axiom

Homotopy pullback

For two function types $f:A\to C$, $g:B\to C$, their dependent sum over the identity type of the evaluations interprets in categorical semantics as the homotopy pullback of $f$ and $g$ depicted as the right hand side of

$$\sum_{a:A,b:B} (f(a)=g(b))=\{a:A|f(a)=g(b)\}$$

Homotopy fiber

$$hfiber(f,b):=\sum_{a:A}f(a)=b$$

(homotopy-type-theoretical) Equivalence

$$is Equiv(f):=\prod_{b:B}is Contr(h fiber(f))$$

$f$ is called to be an equivalence if $is Equiv(f)$ is inhabited.

$$Equiv_C(x,y):=\sum_{f:x\to y} is Equiv(f)$$

Identity types

The categorical semantics of an identity type $Id_C$ is given by the path-object fibration $C^I\stackrel{Id_C}{\to}C\times C$ and

$$a:A,b:B\dashv f(x)=g(y)$$

interprets as the homotopy pullback

$$\array{ (f,g)^* C^I&\to &C^I \\ \downarrow&&\downarrow^{Id_C} \\ A\times B&\stackrel{(f,g)}{\to}&C\times C }$$

The univalence axiom

The univalence axiom is defined to be the assertion that

$$Id_C(x,y)\stackrel{\sim}{\to}Equiv_C(x,y)$$

Is an equivalence for all type $x, y$.