Homotopy Type Theory homotopy equivalence > history (Rev #1)

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))

Homotopy Type Theory homotopy equivalence > history (Rev #1)

Definition

See also