$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) → σ ＝ σ₀

$f$ is an equivalence if it has a section and also has a retraction:

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

open import MLTT.Spartan
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties

is-equiv : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (f : X → Y) → 𝓤 ⊔ 𝓥 ̇
is-equiv f =
  (Σ s ꞉ (codomain f → domain f) , f ∘ s ∼ id) × (Σ r ꞉ (codomain f → domain f) , r ∘ f ∼ id)