Propositional Truncation

1. Propositional Truncation

1 Propositional Truncation

module Lib.PropTrunc where

This file defines the propositional truncation as a higher inductive type. It is useful when wanting to show that a certain type is inhabited, without exhibiting its inhabitant.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.EquivalenceRelations
import Lib.Prop.Proposition

1.2 Specification

Let A be a type and P a proposition. A map f : A → P is a propositional truncation whenever its precomposition is an equivalence.

precomp-Prop (A : U) (P : UU-Prop) (f : A → (Prop/type P)) (Q : UU-Prop) (g : Prop/hom P Q) : A → Prop/type Q =
  λz. g (f z)

is-prop-trunc (A : U) (P : UU-Prop) (f : A → (Prop/type P)) : U =
  (Q : UU-Prop) → is-equiv (Prop/hom P Q) (A → Prop/type Q) (precomp-Prop A P f Q)

We can extract the underlying map of a propositional truncation.

is-prop-trunc/map (A : U) (P : UU-Prop) (f : A → Prop/type P) (H : is-prop-trunc A P f) (Q : UU-Prop) (g : A → Prop/type Q) : Prop/hom P Q =
  (H Q g).1.1

Note that a map A → P is a proposition whenever P is a proposition. Moreover, a map between two propositions is an equivalence as soon as there is a map back and forth between these two propositions.

prop-trunc/has-ext-prop (A : U) (P : UU-Prop) (f : A → Prop/type P) : U =
  (Q : UU-Prop) → (A → Prop/type Q) → (Prop/hom P Q)

That is, to show that f : A → P is a propositional truncation, it suffices to show that precomp-Prop has an inverse.

has-ext-property/is-prop-trunc (A : U) (P : UU-Prop) (f : A → Prop/type P) (H : prop-trunc/has-ext-prop A P f) : is-prop-trunc A P f =
  λQ.
    Prop/is-equiv
      (Prop/hom P Q, is-prop/pi (Prop/type P) (λ_. Prop/type Q) (λ_. Prop/is-prop Q))
      (A → Prop/type Q, is-prop/pi A (λ_. Prop/type Q) (λ_. Prop/is-prop Q))
      (precomp-Prop A P f Q)
      (H Q)

1.3 Definition as an higher inductive type

Sadly, we are not able to show that there exists a propositional truncation for every types. But we can define propositional truncation as higher inductive types!

data Prop-trunc (A : U) : U
  = Prop-trunc/unit (a : A)
  | Prop-trunc/squash (u v : Prop-trunc A) <i> [(i=0) → u, (i=1) → v]

We can remark that the second constructor makes Prop-trunc a proposition.

Prop-trunc/is-prop (A : U) : is-prop (Prop-trunc A) =
  λx y i. Prop-trunc/squash x y i

Thus, Prop-trunc A is in UU-Prop.

Prop-trunc/Prop (A : U) : UU-Prop =
  (Prop-trunc A, Prop-trunc/is-prop A)

Of course, as it is an inductive type, it has a recurrence principle.

rec-Prop-trunc (A : U) (P : UU-Prop) (f : A → Prop/type P) : Prop-trunc A → Prop/type P = split
  Prop-trunc/unit a → f a
  Prop-trunc/squash x y i → (Prop/is-prop P) (rec-Prop-trunc A P f x) (rec-Prop-trunc A P f y) i

1.4 Induction principle

It also has an induction principle.

ind-Prop-trunc (A : U) (P : Prop-trunc A → UU-Prop) (f : (x : A) → Prop/type (P (Prop-trunc/unit x))) : (x : Prop-trunc A) → Prop/type (P x) = split
  Prop-trunc/unit a → f a
  Prop-trunc/squash x y i →
    J ( Prop-trunc A) x
      ( λz q. PathP (j. Prop/type (P (q j))) (ind-Prop-trunc A P f x) (ind-Prop-trunc A P f z))
      ( Prop/is-prop (P x) (ind-Prop-trunc A P f x) (ind-Prop-trunc A P f x)) y
      ( Prop-trunc/is-prop A x y) i

1.5 `unit` is a propositional truncation

Of course, the unit constructor of Prop-trunc satisfies the is-prop-trunc property.

Prop-trunc/is-prop-trunc (A : U) : is-prop-trunc A (Prop-trunc/Prop A) (λa. Prop-trunc/unit a) =
  has-ext-property/is-prop-trunc A (Prop-trunc/Prop A) (λa. Prop-trunc/unit a) (λQ. rec-Prop-trunc A Q)

This makes the eval fail (in coe). See how to report that with a concise file?

1.6 Map between truncations

If there is a map between A and B, then there is a map between the propositional truncations of A and B.

Prop-trunc/map (A B : U) (f : A → B) : (Prop-trunc A) → Prop-trunc B =
  rec-Prop-trunc A
    ( Prop-trunc/Prop B)
    ( λx. Prop-trunc/unit (f x))

As such, when there is an equivalence between A and B, there is an equivalence between the propositional truncation of A and the propositional truncation of B (as well as the associated maps).

Equiv/Prop-trunc-map (A B : U) (e : Equiv A B) : (Prop-trunc A) → Prop-trunc B =
  Prop-trunc/map A B (Equiv/map A B e)

Equiv/Prop-trunc-inv-map (A B : U) (e : Equiv A B) : (Prop-trunc B) → Prop-trunc A =
  Prop-trunc/map B A (Equiv/inv-map A B e)  

Equiv/Prop-trunc (A B : U) (e : Equiv A B) : Equiv (Prop-trunc A) (Prop-trunc B) =
  Prop/Equiv (Prop-trunc/Prop A) (Prop-trunc/Prop B) (Equiv/Prop-trunc-map A B e) (Equiv/Prop-trunc-inv-map A B e)

1.7 Mere equality

A mere equality is the propositional truncation of an equality.

mere-eq (A : U) (x y : A) : U =
  Prop-trunc (Path A x y)

mere-eq/Prop (A : U) (x y : A) : UU-Prop =
  Prop-trunc/Prop (Path A x y)

Of course, mere equality is still an equivalence relation.

mere-eq/refl (A : U) (x : A) : mere-eq A x x =
  Prop-trunc/unit (refl A x)

mere-eq/sym (A : U) (x y : A) : (p : mere-eq A x y) → mere-eq A y x =
  rec-Prop-trunc
    ( Path A x y)
    ( mere-eq/Prop A y x)
    ( λp. Prop-trunc/unit (inv A x y p))

mere-eq/trans (A : U) (x y : A) (p : mere-eq A x y) (z : A) (q : mere-eq A y z) : mere-eq A x z =
  rec-Prop-trunc
    ( Path A x y)
    ( mere-eq/Prop A x z)
    ( λp'. rec-Prop-trunc
            ( Path A y z)
            ( mere-eq/Prop A x z)
            ( λq'. Prop-trunc/unit (comp A x y p' z q')) q) p

In fact, it is an equivalence relation.

mere-eq/Eq-Rel (A : U) : Eq-Rel A =
  ( mere-eq/Prop A,
    ( mere-eq/refl A,
      ( mere-eq/sym A,
        λx y z p. mere-eq/trans A x y p z)))

1.8 Back-and-forth map between prop and prop trunc

If P is a proposition, then there is a map out of Prop-trunc P.

Prop-trunc/map-out (P : UU-Prop) : Prop-trunc (Prop/type P) → Prop/type P =
  rec-Prop-trunc
    ( Prop/type P) P
    ( id (Prop/type P))

And so, mere equality is equivalent to equality.

Prop-trunc/mere-eq (A : UU-Prop) (x y : (Prop/type A)) : Equiv (Path (Prop/type A) x y) (mere-eq (Prop/type A) x y) =
  Prop/Equiv
    ( is-prop/Prop-path A x y)
    ( mere-eq/Prop
      ( Prop/type A) x y)
    ( λp. Prop-trunc/unit p)
    ( Prop-trunc/map-out
      ( is-prop/Prop-path A x y))

1.9 Mere equivalence

A mere equivalence is the propositional truncation of an equivalence.

mere-equiv (X Y : U) : U =
  Prop-trunc
    ( Equiv X Y)

Utilitary accessor of UU-Prop:

mere-equiv/is-prop (X Y : U) : is-prop (mere-equiv X Y) =
  Prop-trunc/is-prop
    ( Equiv X Y)

mere-equiv/Prop (X Y : U) : UU-Prop =
  ( mere-equiv X Y,
    mere-equiv/is-prop X Y)

Of course, it satisfies the equivalence properties of equivalence.

mere-equiv/refl (X : U) : mere-equiv X X =
  rec-Prop-trunc
    ( Equiv X X)
    ( mere-equiv/Prop X X)
    ( λe. Prop-trunc/unit e)
    ( Prop-trunc/unit (Equiv/refl X))

mere-equiv/sym (X Y : U) (e : mere-equiv X Y) : mere-equiv Y X =
  rec-Prop-trunc
    ( Equiv X Y)
    ( mere-equiv/Prop Y X)
    ( λe'. Prop-trunc/unit (Equiv/sym X Y e')) e    

Pi/Prop (A : U) (B : A → U) (q : is-prop/fam A B) : UU-Prop =
  ( Pi A B,
    is-prop/pi A B q)

mere-equiv/trans (X Y : U) (e : mere-equiv X Y) (Z : U) (e' : mere-equiv Y Z) : mere-equiv X Z =
  rec-Prop-trunc
    ( Equiv X Y)
    ( mere-equiv/Prop X Z)
    ( λeX.
        rec-Prop-trunc
          ( Equiv Y Z)
          ( mere-equiv/Prop X Z)
          ( λeY. Prop-trunc/unit
                  ( Equiv/trans X Y Z eX eY)) e') e

1.10 Closure under product

The following equivalence holds: ||A|| × ||B|| ≅ ||A × B||.

Prop-trunc/closed-Prod/map (A B : U) : (Prop-trunc A * Prop-trunc B) → Prop-trunc (A * B) =
  λt.
    rec-Prop-trunc A
      ( Prop-trunc/Prop (A * B))
      ( λx. rec-Prop-trunc B
            ( Prop-trunc/Prop (A * B))
            ( λy. Prop-trunc/unit (x, y)) t.2) t.1

Prop-trunc/closed-Prod/inv-map (A B : U) : Prop-trunc (A * B) → Prop-trunc A * Prop-trunc B =
  rec-Prop-trunc
    ( A * B)
    ( Prop/Prod
      ( Prop-trunc/Prop A)
      ( Prop-trunc/Prop B))
    ( λu. (Prop-trunc/unit u.1, Prop-trunc/unit u.2))  

Prop-trunc/closed-Prod (A B : U) : Equiv (Prop-trunc A * Prop-trunc B) (Prop-trunc (A * B)) =
  Prop/Equiv
    ( Prop/Prod
      ( Prop-trunc/Prop A)
      ( Prop-trunc/Prop B))
    ( Prop-trunc/Prop (A * B))
    ( Prop-trunc/closed-Prod/map A B)
    ( Prop-trunc/closed-Prod/inv-map A B)

1.11 Closure under Σ-type

We have that || Σ_{(x: A)}B(x) || is equivalent to || Σ_{x: A} ||B(x)|| ||.

Prop-trunc/closed-Sg/map (A : U) (B : A → U) : Prop-trunc (Σ A (λx. Prop-trunc (B x))) → Prop-trunc (Σ A B) =
  rec-Prop-trunc
    ( Σ A (λx. Prop-trunc (B x)))
    ( Prop-trunc/Prop (Σ A B))
    ( λt. rec-Prop-trunc
          ( B t.1)
          ( Prop-trunc/Prop (Σ A B))
          ( λb. Prop-trunc/unit (t.1, b)) t.2)

Prop-trunc/closed-Sg/inv-map (A : U) (B : A → U) : Prop-trunc (Σ A B) → Prop-trunc (Σ A (λx. Prop-trunc (B x))) =
  rec-Prop-trunc
    ( Σ A B)
    ( Prop-trunc/Prop (Σ A (λx. Prop-trunc (B x))))
    ( λt. Prop-trunc/unit (t.1, Prop-trunc/unit t.2))

Prop-trunc/closed-Sg/right-htpy (A : U) (B : A → U) : (t : Prop-trunc (Σ A B))
                                    → Path (Prop-trunc (Σ A B))
                                           (Prop-trunc/closed-Sg/map A B (Prop-trunc/closed-Sg/inv-map A B t)) t =
  ind-Prop-trunc
    ( Σ A B)
    ( λt. is-prop/Prop-path
          ( Prop-trunc/Prop (Σ A B))
          ( Prop-trunc/closed-Sg/map A B (Prop-trunc/closed-Sg/inv-map A B t)) t)
    ( λt. refl (Prop-trunc (Σ A B)) (Prop-trunc/unit t))

Prop-trunc/closed-Sg/left-htpy (A : U) (B : A → U) : (t : Prop-trunc (Σ A (λx. Prop-trunc (B x))))
                                   → Path (Prop-trunc (Σ A (λx. Prop-trunc (B x))))
                                          (Prop-trunc/closed-Sg/inv-map A B (Prop-trunc/closed-Sg/map A B t)) t =
  ind-Prop-trunc
    ( Σ A (λx. Prop-trunc (B x)))
    ( λt. is-prop/Prop-path
          ( Prop-trunc/Prop (Σ A (λx. Prop-trunc (B x))))
          ( Prop-trunc/closed-Sg/inv-map A B (Prop-trunc/closed-Sg/map A B t)) t)
    ( λt. ind-Prop-trunc
          ( B t.1)
          ( λb. is-prop/Prop-path
                ( Prop-trunc/Prop (Σ A (λx. Prop-trunc (B x))))
                ( Prop-trunc/closed-Sg/inv-map A B (Prop-trunc/closed-Sg/map A B (Prop-trunc/unit (t.1, b)))) (Prop-trunc/unit (t.1, b)))
          ( λb. refl (Prop-trunc (Σ A (λx. Prop-trunc (B x)))) (Prop-trunc/unit (t.1, Prop-trunc/unit b))) t.2)

Prop-trunc/closed-Σ (A : U) (B : A → U) : Equiv (Prop-trunc (Σ A (λx. Prop-trunc (B x)))) (Prop-trunc (Σ A B)) =
  has-inverse/Equiv
    ( Prop-trunc (Σ A (λx. Prop-trunc (B x))))
    ( Prop-trunc (Σ A B))
    ( Prop-trunc/closed-Sg/map A B)
    ( Prop-trunc/closed-Sg/inv-map A B,
      ( Prop-trunc/closed-Sg/right-htpy A B,
        Prop-trunc/closed-Sg/left-htpy A B))

1.12 Map out of Π-type

Prop-trunc/Pi/map-out (A : U) (B : A → U) (g : Prop-trunc ((x : A) → B x)) (x : A) : Prop-trunc (B x) =
  rec-Prop-trunc
    ( (y : A) → B y)
    ( Prop-trunc/Prop (B x))
    ( λf. Prop-trunc/unit (f x)) g