[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] The fiber of the identity function $\lambda(t:A).t$ at an element $a:A$ is the type $\sum_{b:A} a =_A b$. This type is always contractible for all elements $a:A$; the center of contraction is the dependent pair $(a, \mathrm{refl}_A(a)):\sum_{b:A} a =_A b$ and the contraction $$\prod_{y:\sum_{b:A} a =_A b} (a, \mathrm{refl}_A(a)) =_{\sum_{b:A} a =_A b} y$$ is inductively defined by induction on the identity type and induction on dependent product types: there is an identification $$\mathrm{refl}_{\sum_{b:A} a =_A b}((a, \mathrm{refl}_A(a))):(a, \mathrm{refl}_A(a)) =_{\sum_{b:A} a =_A b} (a, \mathrm{refl}_A(a))$$ See Theorem 10.1.4 and Proposition 5.5.1 of: * [[Egbert Rijke]], *[[Introduction to Homotopy Type Theory]]*, Cambridge Studies in Advanced Mathematics, Cambridge University Press ([arXiv:2212.11082](https://arxiv.org/abs/2212.11082)) category: redirected to nlab