open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Retracts
open import 1Lab.Type.Sigma
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HIT.Truncation where

Propositional TruncationπŸ”—

Let AA be a type. The propositional truncation of AA is a type which represents the proposition β€œA is inhabited”. In MLTT, propositional truncations can not be constructed without postulates, even in the presence of impredicative prop. However, Cubical Agda provides a tool to define them: higher inductive types.

data βˆ₯_βˆ₯ {β„“} (A : Type β„“) : Type β„“ where
  inc    : A β†’ βˆ₯ A βˆ₯
  squash : is-prop βˆ₯ A βˆ₯

The two constructors that generate βˆ₯_βˆ₯ state precisely that the truncation is inhabited when A is (inc), and that it is a proposition (squash).

is-prop-βˆ₯-βˆ₯ : βˆ€ {β„“} {A : Type β„“} β†’ is-prop βˆ₯ A βˆ₯
is-prop-βˆ₯-βˆ₯ = squash

instance
  H-Level-truncation : βˆ€ {n} {β„“} {A : Type β„“} β†’ H-Level βˆ₯ A βˆ₯ (suc n)
  H-Level-truncation = hlevel-instance (is-prop→is-hlevel-suc squash)

The eliminator for βˆ₯_βˆ₯ says that you can eliminate onto PP whenever it is a family of propositions, by providing a case for inc.

βˆ₯-βˆ₯-elim : βˆ€ {β„“ β„“'} {A : Type β„“}
             {P : βˆ₯ A βˆ₯ β†’ Type β„“'}
         β†’ ((x : _) β†’ is-prop (P x))
         β†’ ((x : A) β†’ P (inc x))
         β†’ (x : βˆ₯ A βˆ₯) β†’ P x
βˆ₯-βˆ₯-elim pprop incc (inc x) = incc x
βˆ₯-βˆ₯-elim pprop incc (squash x y i) =
  is-propβ†’pathp (Ξ» j β†’ pprop (squash x y j)) (βˆ₯-βˆ₯-elim pprop incc x)
                                             (βˆ₯-βˆ₯-elim pprop incc y)
                                             i

βˆ₯-βˆ₯-elimβ‚‚ : βˆ€ {β„“ ℓ₁ β„“β‚‚} {A : Type β„“} {B : Type ℓ₁}
              {P : βˆ₯ A βˆ₯ β†’ βˆ₯ B βˆ₯ β†’ Type β„“β‚‚}
          β†’ (βˆ€ x y β†’ is-prop (P x y))
          β†’ (βˆ€ x y β†’ P (inc x) (inc y))
          β†’ βˆ€ x y β†’ P x y
βˆ₯-βˆ₯-elimβ‚‚ {A = A} {B} {P} pprop work x y = go x y where
  go : βˆ€ x y β†’ P x y
  go (inc x) (inc x₁) = work x x₁
  go (inc x) (squash y y₁ i) =
    is-propβ†’pathp (Ξ» i β†’ pprop (inc x) (squash y y₁ i))
                  (go (inc x) y) (go (inc x) y₁) i

  go (squash x x₁ i) z =
    is-propβ†’pathp (Ξ» i β†’ pprop (squash x x₁ i) z)
                  (go x z) (go x₁ z) i

βˆ₯-βˆ₯-rec : βˆ€ {β„“ β„“'} {A : Type β„“} {P : Type β„“'}
         β†’ is-prop P
         β†’ (A β†’ P)
         β†’ (x : βˆ₯ A βˆ₯) β†’ P
βˆ₯-βˆ₯-rec pprop = βˆ₯-βˆ₯-elim (Ξ» _ β†’ pprop)

βˆ₯-βˆ₯-recβ‚‚ : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : Type β„“''} {P : Type β„“'}
         β†’ is-prop P
         β†’ (A β†’ B β†’ P)
         β†’ (x : βˆ₯ A βˆ₯) (y : βˆ₯ B βˆ₯) β†’ P
βˆ₯-βˆ₯-recβ‚‚ pprop = βˆ₯-βˆ₯-elimβ‚‚ (Ξ» _ _ β†’ pprop)

βˆ₯-βˆ₯-rec!
  : βˆ€ {β„“ β„“'} {A : Type β„“} {P : Type β„“'}
  β†’ {@(tactic hlevel-tactic-worker) pprop : is-prop P}
  β†’ (A β†’ P)
  β†’ (x : βˆ₯ A βˆ₯) β†’ P
βˆ₯-βˆ₯-rec! {pprop = pprop} = βˆ₯-βˆ₯-elim (Ξ» _ β†’ pprop)

βˆ₯-βˆ₯-proj : βˆ€ {β„“} {A : Type β„“} β†’ {@(tactic hlevel-tactic-worker) ap : is-prop A} β†’ βˆ₯ A βˆ₯ β†’ A
βˆ₯-βˆ₯-proj {ap = ap} = βˆ₯-βˆ₯-rec ap Ξ» x β†’ x

The propositional truncation can be called the free proposition on a type, because it satisfies the universal property that a left adjoint would have. Specifically, let B be a proposition. We have:

βˆ₯-βˆ₯-univ : βˆ€ {β„“} {A : Type β„“} {B : Type β„“}
         β†’ is-prop B β†’ (βˆ₯ A βˆ₯ β†’ B) ≃ (A β†’ B)
βˆ₯-βˆ₯-univ {A = A} {B = B} bprop = Isoβ†’Equiv (inc' , iso rec (Ξ» _ β†’ refl) beta) where
  inc' : (x : βˆ₯ A βˆ₯ β†’ B) β†’ A β†’ B
  inc' f x = f (inc x)

  rec : (f : A β†’ B) β†’ βˆ₯ A βˆ₯ β†’ B
  rec f (inc x) = f x
  rec f (squash x y i) = bprop (rec f x) (rec f y) i

  beta : _
  beta f = funext (βˆ₯-βˆ₯-elim (Ξ» _ β†’ is-propβ†’is-set bprop _ _) (Ξ» _ β†’ refl))

Furthermore, as required of a free construction, the propositional truncation extends to a functor:

βˆ₯-βˆ₯-map : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
        β†’ (A β†’ B) β†’ βˆ₯ A βˆ₯ β†’ βˆ₯ B βˆ₯
βˆ₯-βˆ₯-map f (inc x)        = inc (f x)
βˆ₯-βˆ₯-map f (squash x y i) = squash (βˆ₯-βˆ₯-map f x) (βˆ₯-βˆ₯-map f y) i

βˆ₯-βˆ₯-mapβ‚‚ : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : Type β„“'} {C : Type β„“''}
         β†’ (A β†’ B β†’ C) β†’ βˆ₯ A βˆ₯ β†’ βˆ₯ B βˆ₯ β†’ βˆ₯ C βˆ₯
βˆ₯-βˆ₯-mapβ‚‚ f (inc x) (inc y)  = inc (f x y)
βˆ₯-βˆ₯-mapβ‚‚ f (squash x y i) z = squash (βˆ₯-βˆ₯-mapβ‚‚ f x z) (βˆ₯-βˆ₯-mapβ‚‚ f y z) i
βˆ₯-βˆ₯-mapβ‚‚ f x (squash y z i) = squash (βˆ₯-βˆ₯-mapβ‚‚ f x y) (βˆ₯-βˆ₯-mapβ‚‚ f x z) i

Using the propositional truncation, we can define the existential quantifier as a truncated Ξ£.

βˆƒ : βˆ€ {a b} (A : Type a) (B : A β†’ Type b) β†’ Type _
βˆƒ A B = βˆ₯ Ξ£ A B βˆ₯

syntax βˆƒ A (Ξ» x β†’ B) = βˆƒ[ x ∈ A ] B

Note that if PP is already a proposition, then truncating it does nothing:

is-propβ†’equivβˆ₯-βˆ₯ : βˆ€ {β„“} {P : Type β„“} β†’ is-prop P β†’ P ≃ βˆ₯ P βˆ₯
is-propβ†’equivβˆ₯-βˆ₯ pprop = prop-ext pprop squash inc (βˆ₯-βˆ₯-elim (Ξ» x β†’ pprop) Ξ» x β†’ x)

In fact, an alternative definition of is-prop is given by β€œbeing equivalent to your own truncation”:

is-prop≃equivβˆ₯-βˆ₯ : βˆ€ {β„“} {P : Type β„“}
               β†’ is-prop P ≃ (P ≃ βˆ₯ P βˆ₯)
is-prop≃equivβˆ₯-βˆ₯ {P = P} =
  prop-ext is-prop-is-prop eqv-prop is-propβ†’equivβˆ₯-βˆ₯ inv
  where
    inv : (P ≃ βˆ₯ P βˆ₯) β†’ is-prop P
    inv eqv = equivβ†’is-hlevel 1 ((eqv e⁻¹) .fst) ((eqv e⁻¹) .snd) squash

    eqv-prop : is-prop (P ≃ βˆ₯ P βˆ₯)
    eqv-prop x y = Ξ£-path (Ξ» i p β†’ squash (x .fst p) (y .fst p) i)
                          (is-equiv-is-prop _ _ _)

Maps into SetsπŸ”—

The elimination principle for βˆ₯Aβˆ₯\| A \| says that we can only use the AA inside in a way that doesn’t matter: the motive of elimination must be a family of propositions, so our use of AA must not matter in a very strong sense. Often, it’s useful to relax this requirement slightly: Can we map out of βˆ₯Aβˆ₯\| A \| using a constant function?

The answer is yes! However, the witness of constancy we use must be very coherent indeed. In particular, we need enough coherence on top of a family of paths (xΒ y:A)β†’fx≑Bfy(x\ y : A) \to f x \equiv_B f y to ensure that the image of ff is a proposition; Then we can map from βˆ₯Aβˆ₯β†’im⁑fβ†’B\| A \| \to \operatorname*{im}f \to B.

From the discussion in 1Lab.Counterexamples.Sigma, we know the definition of image, or more properly of (βˆ’1)(-1)-image:

image : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ (A β†’ B) β†’ Type _
image {A = A} {B = B} f = Ξ£[ b ∈ B ] βˆƒ[ a ∈ A ] (f a ≑ b)

To see that the image indeed implements the concept of image, we define a way to factor any map through its image. By the definition of image, we have that the map f-image is always surjective, and since βˆƒ is a family of props, the first projection out of image is an embedding. Thus we factor a map ff as Aβ† im⁑fβ†ͺBA \twoheadrightarrow \operatorname*{im}f \hookrightarrow B.

f-image
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ (f : A β†’ B) β†’ A β†’ image f
f-image f x = f x , inc (x , refl)

We now prove the theorem that will let us map out of a propositional truncation using a constant function into sets: if BB is a set, and f:Aβ†’Bf : A \to B is a constant function, then im⁑f\operatorname*{im}f is a proposition.

is-constant→image-is-prop
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ is-set B
  β†’ (f : A β†’ B) β†’ (βˆ€ x y β†’ f x ≑ f y) β†’ is-prop (image f)

This is intuitively true (if the function is constant, then there is at most one thing in the image!), but formalising it turns out to be slightly tricky, and the requirement that BB be a set is perhaps unexpected.

A sketch of the proof is as follows. Suppose that we have some (a,x)(a, x) and (b,y)(b, y) in the image. We know, morally, that xx (respectively yy) give us some fβˆ—(a):Af^*(a) : A and p:f(fβˆ—a)=ap : f(f^*a) = a (resp q:f(fβˆ—(b))=bq : f(f^*(b)) = b) β€” which would establish that a≑ba \equiv b, as we need, since we have a=f(fβˆ—(a))=f(fβˆ—(b))=ba = f(f^*(a)) = f(f^*(b)) = b, where the middle equation is by constancy of ff β€” but crucially, the

is-constant→image-is-prop bset f f-const (a , x) (b , y) =
  Ξ£-prop-path (Ξ» _ β†’ squash)
    (βˆ₯-βˆ₯-elimβ‚‚ (Ξ» _ _ β†’ bset _ _)
      (Ξ» { (f*a , p) (f*b , q) β†’ sym p Β·Β· f-const f*a f*b Β·Β· q }) x y)

Using the image factorisation, we can project from a propositional truncation onto a set using a constant map.

βˆ₯-βˆ₯-rec-set : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
            β†’ (f : A β†’ B)
            β†’ (βˆ€ x y β†’ f x ≑ f y)
            β†’ is-set B
            β†’ βˆ₯ A βˆ₯ β†’ B
βˆ₯-βˆ₯-rec-set {A = A} {B} f f-const bset x =
  βˆ₯-βˆ₯-elim {P = Ξ» _ β†’ image f}
    (λ _ → is-constant→image-is-prop bset f f-const) (f-image f) x .fst

open import Meta.Idiom
open import Meta.Bind

instance
  Map-βˆ₯βˆ₯ : Map (eff βˆ₯_βˆ₯)
  Map-βˆ₯βˆ₯ .Map._<$>_ = βˆ₯-βˆ₯-map

  {-# TERMINATING #-}
  Idiom-βˆ₯βˆ₯ : Idiom (eff βˆ₯_βˆ₯)
  Idiom-βˆ₯βˆ₯ .Idiom.pure = inc
  Idiom-βˆ₯βˆ₯ .Idiom._<*>_ {A = A} {B = B} = go where
    go : βˆ₯ (A β†’ B) βˆ₯ β†’ βˆ₯ A βˆ₯ β†’ βˆ₯ B βˆ₯
    go (inc f) (inc x) = inc (f x)
    go (inc f) (squash x y i) = squash (go (inc f) x) (go (inc f) y) i
    go (squash f g i) (inc y) = squash (go f (inc y)) (go g (inc y)) i
    go (squash f g i) (squash x y j) = hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
      k (i = i0) β†’ squash (go f x) (go f (squash x y j)) k
      k (i = i1) β†’ squash (go f x) (go g (squash x y j)) k
      k (j = i0) β†’ squash (go f x) (go (squash f g i) x) k
      k (j = i1) β†’ squash (go f x) (go (squash f g i) y) k
      k (k = i0) β†’ go f x

  Bind-βˆ₯βˆ₯ : Bind (eff βˆ₯_βˆ₯)
  Bind-βˆ₯βˆ₯ .Bind._>>=_ {A = A} {B = B} = go where
    go : βˆ₯ A βˆ₯ β†’ (A β†’ βˆ₯ B βˆ₯) β†’ βˆ₯ B βˆ₯
    go (inc x) f = f x
    go (squash x y i) f = squash (go x f) (go y f) i