```------------------------------------------------------------------------
-- The Agda standard library
--
-- Some basic properties of equivalences. This file is designed to be
-- imported qualified.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Function.Properties.Equivalence where

open import Function.Bundles using (Equivalence; _⇔_)
open import Level
open import Relation.Binary using (Setoid; IsEquivalence)
import Relation.Binary.PropositionalEquality as Eq using (setoid)

import Function.Construct.Identity as Identity
import Function.Construct.Symmetry as Symmetry
import Function.Construct.Composition as Composition

private
variable
a ℓ : Level

------------------------------------------------------------------------
-- Setoid bundles

isEquivalence : IsEquivalence (Equivalence {a} {ℓ})
isEquivalence = record
{ refl = λ {x} → Identity.equivalence x
; sym = Symmetry.equivalence
; trans = Composition.equivalence
}

------------------------------------------------------------------------
-- Propositional bundles

⇔-isEquivalence : IsEquivalence {ℓ = ℓ} _⇔_
⇔-isEquivalence = record
{ refl = λ {x} → Identity.equivalence (Eq.setoid x)
; sym = Symmetry.equivalence
; trans = Composition.equivalence
}

------------------------------------------------------------------------
-- Setoids

setoid : (s₁ s₂ : Level) → Setoid (suc (s₁ ⊔ s₂)) (s₁ ⊔ s₂)
setoid s₁ s₂ = record
{ Carrier       = Setoid s₁ s₂
; _≈_           = Equivalence
; isEquivalence = isEquivalence
}

⇔-setoid : (ℓ : Level) → Setoid (suc ℓ) ℓ
⇔-setoid ℓ = record
{ Carrier       = Set ℓ
; _≈_           = _⇔_
; isEquivalence = ⇔-isEquivalence
}
```