Typal equivalence

Let $𝐴, 𝐵$ be types. A function $𝑓 : 𝐴 \to 𝐵$ is said to be an equivalence iff it has contractible fibres, #m/def/type i.e.

i s E q u i v (𝑓) : = \prod 𝑥 : 𝐵 i s C o n t r (\sum 𝑦 : 𝐴 (𝑓 𝑦 \equiv 𝐵 𝑥))

Intuitively, this says that for every $𝑥 : 𝐵$ there exists a unique $𝑦 : 𝐴$ in its fibre. We also refer to the type $𝐴 ≃ 𝐵$ of equivalences between $𝐴$ and $𝐵$ , so

𝐴 ≃ 𝐵 : = \sum 𝑓 : 𝐴 \to 𝐵 i s E q u i v (𝑓)

#state/develop | #lang/en | #SemBr