🔍

Equations Inline Footnotes

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

open import Data.Dec.Base

open import Meta.Idiom
open import Meta.Bind

module Data.Irr where

Strict propositional truncations🔗

private variable
  ℓ : Level
  A : Type ℓ

As with how the propositional truncation freely generates a proposition from a type, we can define a strict truncation modality which freely generates a definitionally irrelevant type from a type.

This is a secondary notion in our type theory, since this type former does not have a well-behaved elimination principle. However, its presence in the theory allows defining record types with finer control over definitional equality, which can be a notable optimisation; and the resulting types are essentially well-behaved as long as we only wrap decidable propositions.

The construction proceeds in two stages: first, we define Irrˢ, living in SProp, generated by $A\text{.}$ This type is then wrapped in the record Irr to bring it back to the correct universe of fibrant types.

data Irrˢ {ℓ} (A : Type ℓ) : SProp ℓ where
  forgetˢ : A → Irrˢ A

record Irr {ℓ} (A : Type ℓ) : Type ℓ where
  constructor liftˢ
  field lowerˢ : Irrˢ A

open Irr public
pattern forget s = liftˢ (forgetˢ s)

As promised, Irr is definitionally irrelevant, as can be demonstrated by checking that the reflexive path connects the a priori distinct variables $x$ and $y\text{.}$

instance
  H-Level-Irr : ∀ {n} → H-Level (Irr A) (suc n)
  H-Level-Irr {n} = prop-instance λ x y → 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 = λ f x → liftˢ (mapˢ f (x .lowerˢ)) } where
    mapˢ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → Irrˢ A → Irrˢ B
    mapˢ f (forgetˢ x) = forgetˢ (f x)

  Idiom-Irr : Idiom (eff Irr)
  Idiom-Irr = record { pure = λ x → forget x ; _<*>_ = λ f x → liftˢ (apˢ (f .lowerˢ) (x .lowerˢ)) } where
    apˢ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Irrˢ (A → B) → Irrˢ A → Irrˢ B
    apˢ (forgetˢ f) (forgetˢ x) = forgetˢ (f x)

  Bind-Irr : Bind (eff Irr)
  Bind-Irr = record { _>>=_ = λ x f → liftˢ (joinˢ (map f x .lowerˢ)) } where
    joinˢ : ∀ {ℓ} {A : Type ℓ} → Irrˢ (Irr A) → Irrˢ A
    joinˢ (forgetˢ (forget x)) = forgetˢ x

Recovering decidable propositions🔗

As mentioned above, Irr does not have a well-behaved elimination principle. However, since ⊥ is a strict proposition, we can show that $\mathrm{Irr}(A)$ implies $\neg \neg A\text{.}$

Irr→not-not : ∀ {ℓ} {A : Type ℓ} → Irr A → ¬ ¬ A
Irr→not-not {A = A} (liftˢ aˢ) f = liftˢ (go aˢ f) where
  go : Irrˢ A → (A → ⊥) → ⊥ˢ
  go (forgetˢ a) ¬a = ¬a a .⊥.lowerˢ

Therefore, if the type being truncated is decidable, we can recover a legitimate $A$ given only knowledge of $\mathrm{Irr}(A)\text{,}$ using the result above to refute the no case.

recover : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → Irr A → A
recover ⦃ yes x ⦄ _   = x
recover ⦃ no ¬x ⦄ ¬¬x = absurd (Irr→not-not ¬¬x ¬x)