open import 1Lab.Reflection.Induction
open import 1Lab.Function.Embedding
open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Closure
open import 1Lab.Path.Reasoning
open import 1Lab.Type.Sigma
open import 1Lab.Inductive
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base

module 1Lab.HIT.Truncation where

Propositional truncationπŸ”—

Let be a type. The propositional truncation of 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 = prop-instance squash

The eliminator for βˆ₯_βˆ₯ says that you can eliminate onto 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)

βˆ₯-βˆ₯-out : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A β†’ βˆ₯ A βˆ₯ β†’ A
βˆ₯-βˆ₯-out ap = βˆ₯-βˆ₯-rec ap Ξ» x β†’ x

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

βˆ₯-βˆ₯-out! : βˆ€ {β„“} {A : Type β„“} ⦃ _ : H-Level A 1 ⦄ β†’ βˆ₯ A βˆ₯ β†’ A
βˆ₯-βˆ₯-out! = βˆ₯-βˆ₯-out (hlevel 1)

instance
  Inductive-βˆ₯βˆ₯
    : βˆ€ {β„“ β„“' β„“m} {A : Type β„“} {P : βˆ₯ A βˆ₯ β†’ Type β„“'} ⦃ i : Inductive (βˆ€ x β†’ P (inc x)) β„“m ⦄
    β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (P x) 1 ⦄
    β†’ Inductive (βˆ€ x β†’ P x) β„“m
  Inductive-βˆ₯βˆ₯ ⦃ i ⦄ = record
    { methods = i .Inductive.methods
    ; from    = Ξ» f β†’ βˆ₯-βˆ₯-elim (Ξ» x β†’ hlevel 1) (i .Inductive.from f)
    }

  Dec-βˆ₯βˆ₯ : βˆ€ {β„“} {A : Type β„“} β†’ ⦃ Dec A ⦄ β†’ Dec βˆ₯ A βˆ₯
  Dec-βˆ₯βˆ₯ ⦃ yes a ⦄ = yes (inc a)
  Dec-βˆ₯βˆ₯ ⦃ no Β¬a ⦄ = no (rec! Β¬a)

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 b} (A : Type a) (B : A β†’ Type b) β†’ Type _
βˆƒ-syntax = βˆƒ

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

Note that if 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 (βˆ₯-βˆ₯-out pprop)

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

Throughout the 1Lab, we use the words β€œmere” and β€œmerely” to modify a type to mean its propositional truncation. This terminology is adopted from the HoTT book. For example, a type is said merely equivalent to if the type is inhabited.

Maps into setsπŸ”—

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

The answer is yes, provided we’re mapping into a set! In that case, the image of is a proposition, so that we can map from In the next section, we’ll see a more general method for mapping into types that aren’t sets.

From the discussion in 1Lab.Counterexamples.Sigma, we know the definition of image, or more properly of 

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 image-inc is always surjective, and since βˆƒ is a family of props, the first projection out of image is an embedding. Thus we factor a map as 

image-inc
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ (f : A β†’ B) β†’ A β†’ image f
image-inc 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 is a set, and is a constant function, then 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 be a set is perhaps unexpected.

A sketch of the proof is as follows. Suppose that we have some and in the image. We know, morally, that (respectively give us some and (resp β€” which would establish that as we need, since we have where the middle equation is by constancy of β€” but and are hidden under propositional truncations, so we crucially need to use the fact that is a set so that is a proposition.

is-constant→image-is-prop bset f fconst (a , x) (b , y) =
  Ξ£-prop-path (Ξ» _ β†’ squash)
    (βˆ₯-βˆ₯-elimβ‚‚ (Ξ» _ _ β†’ bset _ _)
      (Ξ» { (f*a , p) (f*b , q) β†’ sym p Β·Β· fconst 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 β„“'}
            β†’ is-set B
            β†’ (f : A β†’ B)
            β†’ (βˆ€ x y β†’ f x ≑ f y)
            β†’ βˆ₯ A βˆ₯ β†’ B
βˆ₯-βˆ₯-rec-set {A = A} {B} bset f fconst x =
  βˆ₯-βˆ₯-elim {P = Ξ» _ β†’ image f}
    (λ _ → is-constant→image-is-prop bset f fconst) (image-inc f) x .fst

βˆ₯-βˆ₯-rec-set!
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} ⦃ _ : H-Level B 2 ⦄
  β†’ (f : A β†’ B) (c : βˆ€ x y β†’ f x ≑ f y)
  β†’ βˆ₯ A βˆ₯ β†’ B
βˆ₯-βˆ₯-rec-set! {A = A} f c x = go x .fst where
  go : βˆ₯ A βˆ₯ β†’ image f
  go (inc x)        = f x , inc (x , refl)
  go (squash x y i) = is-constant→image-is-prop (hlevel 2) f c (go x) (go y) i

Maps into groupoidsπŸ”—

We can push this idea further: as discussed in (Kraus 2015), in general, functions are equivalent to coherently constant functions This involves an infinite tower of conditions, each relating to the previous one, which isn’t something we can easily formulate in the language of type theory.

However, when is an it is enough to ask for the first levels of the tower. In the case of sets, we’ve seen that the naΓ―ve notion of constancy is enough. We now deal with the case of groupoids, which requires an additional step: we ask for a function equipped with a witness of constancy and a coherence

This time, we cannot hope to show that the image of is a proposition: the image of a map is Instead, we use the following higher inductive type, which can be thought of as the β€œcodiscrete groupoid” on 

data βˆ₯_βˆ₯Β³ {β„“} (A : Type β„“) : Type β„“ where
  inc : A β†’ βˆ₯ A βˆ₯Β³
  iconst : βˆ€ a b β†’ inc a ≑ inc b
  icoh : βˆ€ a b c β†’ PathP (Ξ» i β†’ inc a ≑ iconst b c i) (iconst a b) (iconst a c)
  squash : is-groupoid βˆ₯ A βˆ₯Β³

The recursion principle for this type says exactly that any coherently constant function into a groupoid factors through 

βˆ₯-βˆ₯Β³-rec
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ is-groupoid B
  β†’ (f : A β†’ B)
  β†’ (fconst : βˆ€ x y β†’ f x ≑ f y)
  β†’ (βˆ€ x y z β†’ fconst x y βˆ™ fconst y z ≑ fconst x z)
  β†’ βˆ₯ A βˆ₯Β³ β†’ B
βˆ₯-βˆ₯Β³-rec {A = A} {B} bgrpd f fconst fcoh = go where
  go : βˆ₯ A βˆ₯Β³ β†’ B
  go (inc x) = f x
  go (iconst a b i) = fconst a b i
  go (icoh a b c i j) = βˆ™β†’square (sym (fcoh a b c)) i j
  go (squash x y a b p q i j k) = bgrpd
    (go x) (go y)
    (Ξ» i β†’ go (a i)) (Ξ» i β†’ go (b i))
    (Ξ» i j β†’ go (p i j)) (Ξ» i j β†’ go (q i j))
    i j k

All that remains to show is that is a proposition1, which mainly requires writing more elimination principles.

βˆ₯-βˆ₯Β³-elim-set
  : βˆ€ {β„“} {A : Type β„“} {β„“'} {P : βˆ₯ A βˆ₯Β³ β†’ Type β„“'}
  β†’ (βˆ€ a β†’ is-set (P a))
  β†’ (f : (a : A) β†’ P (inc a))
  β†’ (βˆ€ a b β†’ PathP (Ξ» i β†’ P (iconst a b i)) (f a) (f b))
  β†’ βˆ€ a β†’ P a
unquoteDef βˆ₯-βˆ₯Β³-elim-set = make-elim-n 2 βˆ₯-βˆ₯Β³-elim-set (quote βˆ₯_βˆ₯Β³)

βˆ₯-βˆ₯Β³-elim-prop
  : βˆ€ {β„“} {A : Type β„“} {β„“'} {P : βˆ₯ A βˆ₯Β³ β†’ Type β„“'}
  β†’ (βˆ€ a β†’ is-prop (P a))
  β†’ (f : (a : A) β†’ P (inc a))
  β†’ βˆ€ a β†’ P a
unquoteDef βˆ₯-βˆ₯Β³-elim-prop = make-elim-n 1 βˆ₯-βˆ₯Β³-elim-prop (quote βˆ₯_βˆ₯Β³)

βˆ₯-βˆ₯Β³-is-prop : βˆ€ {β„“} {A : Type β„“} β†’ is-prop βˆ₯ A βˆ₯Β³
βˆ₯-βˆ₯Β³-is-prop = is-contr-if-inhabitedβ†’is-prop $
  βˆ₯-βˆ₯Β³-elim-prop (Ξ» _ β†’ hlevel 1)
    (Ξ» a β†’ contr (inc a) (βˆ₯-βˆ₯Β³-elim-set (Ξ» _ β†’ squash _ _) (iconst a) (icoh a)))

Hence we get the desired recursion principle for the usual propositional truncation.

βˆ₯-βˆ₯-rec-groupoid
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ is-groupoid B
  β†’ (f : A β†’ B)
  β†’ (fconst : βˆ€ x y β†’ f x ≑ f y)
  β†’ (βˆ€ x y z β†’ fconst x y βˆ™ fconst y z ≑ fconst x z)
  β†’ βˆ₯ A βˆ₯ β†’ B
βˆ₯-βˆ₯-rec-groupoid bgrpd f fconst fcoh =
  βˆ₯-βˆ₯Β³-rec bgrpd f fconst fcoh ∘ βˆ₯-βˆ₯-rec βˆ₯-βˆ₯Β³-is-prop inc
As we hinted at above, this method generalises (externally) to we sketch the details of the next level for the curious reader.

The next coherence involves a tetrahedron all of whose faces are or, since we’re doing cubical type theory, a β€œcubical tetrahedron”:

data βˆ₯_βˆ₯⁴ {β„“} (A : Type β„“) : Type β„“ where
  inc : A β†’ βˆ₯ A βˆ₯⁴
  iconst : βˆ€ a b β†’ inc a ≑ inc b
  icoh : βˆ€ a b c β†’ PathP (Ξ» i β†’ inc a ≑ iconst b c i) (iconst a b) (iconst a c)
  iassoc : βˆ€ a b c d β†’ PathP (Ξ» i β†’ PathP (Ξ» j β†’ inc a ≑ icoh b c d i j)
                                          (iconst a b) (icoh a c d i))
                             (icoh a b c) (icoh a b d)
  squash : is-hlevel βˆ₯ A βˆ₯⁴ 4

βˆ₯-βˆ₯⁴-rec
  : βˆ€ {β„“} {A : Type β„“} {β„“'} {B : Type β„“'}
  β†’ is-hlevel B 4
  β†’ (f : A β†’ B)
  β†’ (fconst : βˆ€ a b β†’ f a ≑ f b)
  β†’ (fcoh : βˆ€ a b c β†’ PathP (Ξ» i β†’ f a ≑ fconst b c i) (fconst a b) (fconst a c))
  β†’ (βˆ€ a b c d β†’ PathP (Ξ» i β†’ PathP (Ξ» j β†’ f a ≑ fcoh b c d i j)
                                    (fconst a b) (fcoh a c d i))
                       (fcoh a b c) (fcoh a b d))
  β†’ βˆ₯ A βˆ₯⁴ β†’ B
unquoteDef βˆ₯-βˆ₯⁴-rec = make-rec-n 4 βˆ₯-βˆ₯⁴-rec (quote βˆ₯_βˆ₯⁴)

open import Meta.Idiom
open import Meta.Bind

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

  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) y = squash (go f y) (go g y) i

  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

is-embedding→image-inc-is-equiv
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} {f : A β†’ B}
  β†’ is-embedding f
  β†’ is-equiv (image-inc f)
is-embedding→image-inc-is-equiv {f = f} f-emb =
  is-iso→is-equiv $
  iso (Ξ» im β†’ fst $ βˆ₯-βˆ₯-out (f-emb _) (im .snd))
    (Ξ» im β†’ Ξ£-prop-path! (snd $ βˆ₯-βˆ₯-out (f-emb _) (im .snd)))
    (Ξ» _ β†’ refl)

is-embedding→image-equiv
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} {f : A β†’ B}
  β†’ is-embedding f
  β†’ A ≃ image f
is-embedding→image-equiv {f = f} f-emb =
  image-inc f , is-embedding→image-inc-is-equiv f-emb

  1. in fact, it’s even a propositional truncation of in that it satisfies the same universal property as β†©οΈŽ

References