open import 1Lab.HLevel.Closure
open import 1Lab.Path
open import 1Lab.Type

open import Meta.Idiom

module Data.Irr where

Strict propositional truncationsπŸ”—

private variable
  β„“ : Level
  A : Type β„“

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
    .lower : A

The most important property of this type is that, given any in the constant path refl checks at type 

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) }