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)