Strict propositional truncations🔗

In Agda, it’s possible to turn any type into one that definitionally has at most one inhabitant. We do this using a record containing an irrelevant field.

record Irr {ℓ} (A : Type ℓ) : Type ℓ where
  constructor forget
  field
    @irr lower : A

The most important property of this type is that, given any $x,y$ in $\mathrm{Irr}(A)\text{,}$ the constant path refl checks at type $x\equiv y\text{.}$

instance
  H-Level-Irr : ∀ {n} → H-Level (Irr A) (suc n)
  H-Level-Irr {n} = prop-instance λ _ _ → refl

instance
  make-irr : ∀ {ℓ} {A : Type ℓ} ⦃ _ : A ⦄ → Irr A
  make-irr ⦃ x ⦄ = forget x
  {-# INCOHERENT make-irr #-}

  Map-Irr : Map (eff Irr)
  Map-Irr = record { map = λ where f (forget x) → forget (f x) }

  Idiom-Irr : Idiom (eff Irr)
  Idiom-Irr = record { pure = λ x → forget x ; _<*>_ = λ where (forget f) (forget x) → forget (f x) }