## 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$.