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 σ₀ : fiber f y such that σ = σ₀ for all σ : fiber f y.

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