## Definition ## Given a function $f:A \to B$ over a term $b:B$, the [[homotopy fiber]] $hfiber(f, b)$ is a __homotopy equivalence__ if $hfiber(f, b)$ is [[contractible]] for all terms $b:B$ $$p:\prod_{b:B} isContr(hfiber(f))$$ The type of homotopy equivalences $A \cong B$ is defined as $$A \cong B \coloneqq \sum_{f:A \to B} \prod_{b:B} isContr(hfiber(f))$$ ## See also ## * [[homotopy fiber]] * [[univalence axiom]]