`h`-Levels

1. Truncation levels properties

1 Truncation levels properties

module Lib.Prop.Levels where

This file is a collection of lemmas about Voevodsky's h-levels.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Stdlib.Prelude
import Lib.Univalence
import Lib.Prop.Proposition
import Lib.Prop.Set

1.2 Closure under equivalence for propositions and sets

is-prop/closed-equiv (A B : U) (e : Equiv A B) (H : is-prop B) : is-prop A =
  has-contr-eq/is-prop A (is-of-lvl/closed-equiv A B e one-Nat (is-prop/has-contr-eq B H))

is-prop/closed-equiv' (A B : U) (e : Equiv A B) (H : is-prop A) : is-prop B =
  has-contr-eq/is-prop B (is-of-lvl/closed-equiv' A B e one-Nat (is-prop/has-contr-eq A H))

is-set/closed-equiv (A B : U) (e : Equiv A B) (H : is-set B) : is-set A =
  let f : A → B = Equiv/map A B e in
  λx y. is-prop/closed-equiv (Path A x y) (Path B (f x) (f y)) (Equiv/Equiv-id A B e x y) (H (f x) (f y))

is-set/closed-equiv' (A B : U) (e : Equiv A B) (H : is-set A) : is-set B =
  is-set/closed-equiv B A (Equiv/sym A B e) H

1.3 `is-prop` is a proposition

is-prop/is-set (A : U) (is-prop-A : is-prop A) : is-set A =
  λx y. is-contr→is-prop (Path A x y) (is-prop/has-contr-eq A is-prop-A x y)

is-prop/is-prop (A : U) : is-prop (is-prop A) =
  is-prop/ass-inh
    ( is-prop A)
    ( λis-prop-A.
        is-prop/pi-2 A
          ( λ_. A)
          ( λx y. Path A x y)
          ( is-prop/is-set A is-prop-A))

TODO: the thing above has really long eval time, find out why.

1.4 `UU-Prop` is a set

Equiv is a proposition whenever B is a proposition.

Equiv/is-prop (A : U) (B : UU-Prop) : is-prop (Equiv A (Prop/type B)) =
  λe e'.
    SgPath-prop
      ( A → Prop/type B)
      ( is-equiv A
        ( Prop/type B))
      ( is-equiv/is-prop A
        ( Prop/type B)) e e'
      ( is-prop/pi A
        ( λ_. Prop/type B)
        ( λ_. Prop/is-prop B) e.1 e'.1)

By univalence, the path between the underlying type of propositions is equivalent to a proposition, so it is also a proposition.

Prop/eq-Prop (A B : UU-Prop) : is-prop (Path U (Prop/type A) (Prop/type B)) =
  is-prop/closed-equiv'
    ( Equiv (Prop/type A) (Prop/type B))
    ( Path U (Prop/type A) (Prop/type B))
    ( univalence (Prop/type A) (Prop/type B))
    ( Equiv/is-prop (Prop/type A) B)

Moreover, path between propositions is equivalent to path between their underlying type.

UU-Prop/eq/map (A B : UU-Prop) : Path U (Prop/type A) (Prop/type B) → Path UU-Prop A B =
  SgPath-prop U is-prop
    ( is-prop/is-prop) A B    

UU-Prop/eq (A B : UU-Prop) : Path UU-Prop A B → Path U (Prop/type A) (Prop/type B) =
  λp i. (p i).1

UU-Prop/is-equiv (A : UU-Prop) : (B : UU-Prop) → is-equiv (Path UU-Prop A B) (Path U (Prop/type A) (Prop/type B)) (UU-Prop/eq A B) =
  fundamental-theorem-id UU-Prop
    ( λB. Path U (Prop/type A) (Prop/type B)) A
    ( UU-Prop/eq A)
    ( ( A, refl U (Prop/type A)),
      ( λt. SgPath-prop UU-Prop
            ( λB. Path U (Prop/type A) (Prop/type B))
            ( Prop/eq-Prop A)
            ( A, refl U (Prop/type A)) t
            ( UU-Prop/eq/map A t.1 t.2)))

UU-Prop/Eq/Equiv (A B : UU-Prop) : Equiv (Path UU-Prop A B) (Path U (Prop/type A) (Prop/type B)) =
  ( UU-Prop/eq A B,
    UU-Prop/is-equiv A B)

UU-Prop/is-set (A B : UU-Prop) : is-prop (Path UU-Prop A B) =
  is-prop/closed-equiv
    ( Path UU-Prop A B)
    ( Path U (Prop/type A) (Prop/type B))
    ( UU-Prop/Eq/Equiv A B)
    ( Prop/eq-Prop A B)

UU-Prop/Set : UU-Set =
  ( UU-Prop,
    UU-Prop/is-set)

1.5 Lifting prop universe to set universe

Prop/Set (A : UU-Prop) : UU-Set =
  (Prop/type A, is-prop/is-set (Prop/type A) (Prop/is-prop A))

1.6 `is-set` is a proposition

is-set/is-prop (A : U) : is-prop (is-set A) =
  is-prop/ass-inh
    ( is-set A)
    ( λis-set-A.
        is-prop/pi-2 A
          ( λ_. A)
          ( λx y. is-prop (Path A x y))
          ( λx y. is-prop/is-prop (Path A x y)))

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

1.7 Closure of sets under product

If A and B are both sets, then A * B is also a set.

Set/closed-Prod/is-set (A B : UU-Set) : is-set ((Set/type A) * (Set/type B)) =
  λt u.
    is-prop/closed-equiv
      ( Path ((Set/type A) * (Set/type B)) t u)
      ( Eq-prod
        ( Set/type A)
        ( Set/type B) t u)
      ( Eq-prod/Equiv
        ( Set/type A)
        ( Set/type B) t u)
      ( is-prop/prod
        ( Path (Set/type A) t.1 u.1)
        ( Path (Set/type B) t.2 u.2)
        ( Set/is-set A t.1 u.1)
        ( Set/is-set B t.2 u.2))


Set/closed-Prod (A B : UU-Set) : UU-Set =
  ( (Set/type A) * (Set/type B),
    Set/closed-Prod/is-set A B)

1.8 Closure of sets under Σ-types

Set/closed-Sg/is-set (A : UU-Set) (B : (Set/type A) → UU-Set) : is-set (Σ (Set/type A) (λx. Set/type (B x))) =
  λt u p q.
    let p' : PathP (i. Set/type (B (p i).1)) t.2 u.2 = λi. (p i).2
        q' : PathP (i. Set/type (B (q i).1)) t.2 u.2 = λi. (q i).2
        spq : Path (Path (Set/type A) t.1 u.1) (λi. (p i).1) (λi. (q i).1) = Set/is-set A t.1 u.1 ( λi. (p i).1) ( λi. (q i).1)
        r  : PathP (i. PathP (j. Set/type (B (spq i j))) t.2 u.2) p' q' = 
                    square/dependent-fill
                      ( Set/type A) B t.1 u.1
                      ( λi. (p i).1)
                      ( λi. (q i).1) spq t.2 u.2 p' q'
    in
    λi. SgPathP→PathSg
        ( Set/type A)
        ( λx. Set/type (B x)) t u
        ( spq i, r i)

Set/closed-Σ (A : UU-Set) (B : (Set/type A) → UU-Set) : UU-Set =
  ( Σ (Set/type A) (λx. Set/type (B x)),
    Set/closed-Sg/is-set A B)

1.9 Closure of sets under coproducts

Set/closed-Coprod/is-set/inl (A B : UU-Set) (x : Set/type A)
                                  : (v : Coprod (Set/type A) (Set/type B))
                                    → is-prop (Path (Coprod (Set/type A) (Set/type B)) (inl x) v)  = split
  inl a →
    is-prop/closed-equiv
      ( Path (Coprod (Set/type A) (Set/type B)) (inl x) (inl a))
      ( Path (Set/type A) x a)
      ( Coprod/Eq/Equiv (Set/type A) (Set/type B) (inl x) (inl a))
      ( Set/is-set A x a)
  inr y →
    is-prop/closed-equiv
      ( Path (Coprod (Set/type A) (Set/type B)) (inl x) (inr y))
      ( Empty)
      ( Coprod/Eq/Equiv (Set/type A) (Set/type B) (inl x) (inr y))
      ( Empty/is-prop)

Set/closed-Coprod/is-set/inr (A B : UU-Set) (y : Set/type B)
                                  : (v : Coprod (Set/type A) (Set/type B))
                                    → is-prop (Path (Coprod (Set/type A) (Set/type B)) (inr y) v)  = split
  inl a →
    is-prop/closed-equiv
      ( Path (Coprod (Set/type A) (Set/type B)) (inr y) (inl a))
      ( Empty)
      ( Coprod/Eq/Equiv (Set/type A) (Set/type B) (inr y) (inl a))
      ( Empty/is-prop)
  inr b →
    is-prop/closed-equiv
      ( Path (Coprod (Set/type A) (Set/type B)) (inr y) (inr b))
      ( Path (Set/type B) y b)
      ( Coprod/Eq/Equiv (Set/type A) (Set/type B) (inr y) (inr b))
      ( Set/is-set B y b)

Set/closed-Coprod/is-set (A B : UU-Set) : is-set (Coprod (Set/type A) (Set/type B)) = split
  inl x → Set/closed-Coprod/is-set/inl A B x
  inr y → Set/closed-Coprod/is-set/inr A B y

Set/closed-Coprod (A B : UU-Set) : UU-Set =
  ( Coprod (Set/type A) (Set/type B),
    Set/closed-Coprod/is-set A B)

1.10 (x, y) = (x', y') is x = x' if the type of y, y' is proposition

The back-and-forth maps are already defined; one is Sg-Path/left and the other is SgPath-prop. We show that they are inverses to each other.

PathPath/Equiv (A : U) (B : A → U) (u v : Σ A B) (p q : Path (Σ A B) u v) 
                  : Equiv (Path (Path (Σ A B) u v) p q) (Path (SgPathP A B u v) (PathSg→SgPathP A B u v p) (PathSg→SgPathP A B u v q))  =
  Equiv/Equiv-id
    ( Path (Σ A B) u v)
    ( SgPathP A B u v)
    ( PathSg-equiv-SgPathP A B u v) p q

PathPath/map (A : U) (B : A → U) (u v : Σ A B) (p q : Path (Σ A B) u v) (spq : Path (SgPathP A B u v) (PathSg→SgPathP A B u v p) (PathSg→SgPathP A B u v q))
         : Path (Path (Σ A B) u v) p q =
  Equiv/inv-map
    ( Path (Path (Σ A B) u v) p q)
    ( Path (SgPathP A B u v) (PathSg→SgPathP A B u v p) (PathSg→SgPathP A B u v q))
    ( PathPath/Equiv A B u v p q) spq

SgPath-prop' (A : U) (B : A → U) (H : (x : A) → is-prop (B x)) (u v : Σ A B) (p : Path A u.1 v.1) : Path (Σ A B) u v =
  SgPathP→PathΣ A B u v (p, J A u.1 (λz q. (y : B z) → PathP (i. B (q i)) u.2 y) (λy. H u.1 u.2 y) v.1 p v.2)

SgPath-prop/right-htpy (A : U) (B : A → U) (H : (x : A) → is-prop (B x)) (u v : Σ A B) (p : Path (Σ A B) u v)
                          : Path (Path (Σ A B) u v) (SgPath-prop' A B H u v (Sg-path/left A B u v p)) p =
  PathPath/map A B u v 
    ( SgPath-prop' A B H u v (Sg-path/left A B u v p)) p
    ( SgPathP→PathSg
      ( Path A u.1 v.1)
      ( λr. PathP (i. B (r i)) u.2 v.2)
      ( PathSg→SgPathP A B u v
        ( SgPath-prop' A B H u v (Sg-path/left A B u v p)))
      ( PathSg→SgPathP A B u v p)
      ( refl (Path A u.1 v.1) (PathSg→SgPathP A B u v p).1 ,
        J A u.1
        ( λz q. (y :B z) → (r s : PathP (i. B (q i)) u.2 y) → Path (PathP (i. B (q i)) u.2 y) r s)
        ( λy r s. is-prop/is-set
                  ( B u.1)
                  ( H u.1) u.2 y r s) v.1 (λi. (p i).1) v.2
                  ( PathSg→SgPathP A B u v
                    ( SgPath-prop' A B H u v (Sg-path/left A B u v p))).2
                    (PathSg→SgPathP A B u v p).2))

SgPath-prop/left-htpy (A : U) (B : A → U) (H : (x : A) → is-prop (B x)) (u v : Σ A B) (p : Path A u.1 v.1)
                         : Path (Path A u.1 v.1) (Sg-path/left A B u v (SgPath-prop' A B H u v p)) p =
  refl (Path A u.1 v.1) p

SgPath-prop/Equiv (A : U) (B : A → U) (H : (x : A) → is-prop (B x)) (u v : Σ A B)
                     : Equiv (Path A u.1 v.1) (Path (Σ A B) u v) =
  has-inverse/Equiv
    ( Path A u.1 v.1)
    ( Path (Σ A B) u v)
    ( SgPath-prop' A B H u v)
    ( Sg-path/left A B u v,
      ( SgPath-prop/right-htpy A B H u v,
        SgPath-prop/left-htpy A B H u v))

SgPath-prop/Equiv' (A : U) (B : A → U) (H : (x : A) → is-prop (B x)) (u v : Σ A B)
                      : Equiv (Path (Σ A B) u v) (Path A u.1 v.1) =
  has-inverse/Equiv
    ( Path (Σ A B) u v)
    ( Path A u.1 v.1)
    ( Sg-path/left A B u v)
    ( SgPath-prop' A B H u v,
      ( SgPath-prop/left-htpy A B H u v,
        SgPath-prop/right-htpy A B H u v))

1.11 Proposition of equality between elements of set

Set/eq/Prop (X : UU-Set) (x y : Set/type X) : UU-Prop =
  ( Path (Set/type X) x y,
    Set/is-set X x y)

1.12 Fiber inclusion is injective whenever A is a set

is-set-is-inj-fib (A : U) (B : A → U) (a : A) (H : is-set A)
                  (y z : B a) (p : Path (Σ A B) (a, y) (a, z))
                       : Path (B a) y z =
  let axiom-K-A : axiom-K A = is-set/axiom-K A H
      p' : SgPathO A B (a, y) (a, z) = PathSg→SgPathO A B (a, y) (a, z) p in
  tr
    ( B a)
    ( tr A a a p'.1 B y) y
    ( comp
      ( B a)
      ( tr A a a p'.1 B y)
      ( tr A a a (refl A a) B y)
      ( ap (Path A a a) (B a) (λq. tr A a a q B y) p'.1 (refl A a) (inv (Path A a a) (refl A a) p'.1 (axiom-K-A a p'.1))) y
      ( tr/refl-path A a B y))
    ( λu. Path (B a) u z) p'.2

h-Levels

Table of Contents