For two function types , , their dependent sum over the identity type of the evaluations interprets in categorical semantics as the homotopy pullback of and depicted as the right hand side of
Homotopy fiber
(homotopy-type-theoretical) Equivalence
is called to be an equivalence if is inhabited.
Identity types
The categorical semantics of an identity type is given by the path-object fibration and
interprets as the homotopy pullback
The univalence axiom
The univalence axiom is defined to be the assertion that