Propositional truncation

module foundations.propositional-truncation where

open import foundations.universe
open import foundations.identity-type
open import foundations.proposition

Propositional truncationは素のAgdaでは構成できないので、その型のみを定義する。

private variable
  ℓ : Level
  A : Type ℓ

record PropTrunc : Typeω where
  field
    ∥_∥ : Type ℓ → Type ℓ
    isProp∥∥ : isProp ∥ A ∥
    ∣_∣ : A → ∥ A ∥
    rec : ∀ {P : Type ℓ} → isProp P → (A → P) → ∥ A ∥ → P

  β : ∀ (P : Type ℓ) (isPropP : isProp P) (x : A) (f : A → P)
    → rec isPropP f ∣ x ∣ ＝ f x
  β P isPropP x f = isPropP _ (f x)

βがjudgmental equalityではないので、これはweak propositional truncationとも呼ばれる。