[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] the problem with contractible fibers is that without weak function extensionality, $$\prod_{y:B} \sum_{p:\sum_{x:A} \mathrm{Id}_B(f(x), y)} \prod_{q:\sum_{x:A} \mathrm{Id}_B(f(x), y)} \mathrm{Id}_{\sum_{x:A} \mathrm{Id}_B(f(x), y)}(p, q)$$ cannot be proven to be contractible. This means half adjoint equivalences are the proper definition of equivalence: $$\sum_{g:B \to A} \sum_{G:\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)} \sum_{H:\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)} \prod_{x:A} G(f(x)) =_{f(g(f(x))) =_B f(x)} \mathrm{ap}(f, g(f(x)), x, H(x)))$$ $$x:A \mathrm{cohdefisContr}_A(x):\mathrm{Id}_{\mathrm{Id}_B(\mathrm{defisContr}_A(\mathrm{defisContr}_A^{-1}(\mathrm{defisContr}_A(x))), \mathrm{defisContr}_A(x))}\left(\mathrm{secdefisContr}_A(\mathrm{defisContr}_A(x)), \mathrm{ap}(\mathrm{defisContr}_A, \mathrm{defisContr}_A^{-1}(\mathrm{defisContr}_A(x)), x, \mathrm{retdefisContr}_A(x)))\right)$$ category: redirected to nlab