Defintion. Voevodsky's [ag-000T]

$f$ is an equivalence if its fibers are contractible (or singletons): For every $y : Y$, the type

{-# OPTIONS --safe --without-K #-}
module ag-000T where

open import MLTT.Spartan hiding (fiber)

fiber : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → Y → 𝓤 ⊔ 𝓥 ̇
fiber f y = Σ x ꞉ domain f , f x ＝ y

has the property that there is a distinguished element $\sigma_0 : \text{fiber f } y$ such that $\sigma = \sigma_0$ for all $\sigma : \text{fiber f } y$.

is-equiv : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (f : X → Y) → 𝓤 ⊔ 𝓥 ̇
is-equiv f = ∀ (y : codomain f) → Σ σ₀ ꞉ fiber f y , ∀ (σ : fiber f y) → σ ＝ σ₀