Propositions Properties

Table of Contents

1 Propositions properties

module Lib.Prop.Proposition where

This file shows some properties related to the fact that a type A is a proposition. For instance, it states the 4 equivalent ways of stating that a type is a proposition, and gives maps for each situation.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Stdlib.Prelude
import Lib.Data.Decidability
import Lib.Data.Map
import Lib.Data.Unit
import Lib.Prop.Contr
import Lib.Prop.Coprod
import Lib.Prop.Equiv
import Lib.Prop.Unit

1.2 Equivalent statements for is-prop

In our formalisation, a type A has a witness is-prop A whenever all its elements are equal. However, there are 3 other ways to state this:

  • whenever A is inhabited, it is contractible ;
  • the identity elements of A are contractible ;
  • the map A is equivalent to Unit.

Note that the second point is also part of a more general theorem – if A is k-truncated, then the identity on A is also k-truncated.

1.2.1 Definitions of conditions

is-proof-irrelevant (A : U) : U =
  A → is-contr A

is-subterminal (A : U) : U =
  Equiv A Unit

has-contr-eq (A : U) : U =
  (x y : A) → is-contr (Path A x y)

1.2.2 Maps between conditions

  1. A proposition is proof irrelevant
    is-prop/is-proof-irrelevant (A : U) (p : is-prop A) : is-proof-irrelevant A =
  λx. (x, p x)
  2. A type is subterminal whenever its proofs are irrelevant

    First, we define the function that erases every a : A to star. 

    const-star (A : U) : A → Unit = λ_. star

    The center of contraction of the fibration is given by the center of contraction of A, and the fact that Unit is a proposition (that is, all its elements are equal). 

    is-proof-irrelevant/contr-center (A : U) (x : A) (f : is-proof-irrelevant A) (y : Unit) : Fib A Unit (const-star A) y =
  ((f x).1, Unit/is-prop y (const-star A (f x).1))

    Using the fact that there is a path between a dependent pair whenever there are two paths p and q between both its elements, we exhibit p using the contraction of A (as the center's fibration first element is defined as the center of the contraction of A, it is easy) and q using the fact that Unit is a set, that is, its identity types are a proposition – i.e., they are all equal. 

    is-proof-irrelevant/contr-contr (A : U) (x : A) (f : is-proof-irrelevant A) (y : Unit) (v : Fib A Unit (const-star A) y)
  : Path (Fib A Unit (const-star A) y) (is-proof-irrelevant/contr-center A x f y) v =
      let u : Fib A Unit (const-star A) y = (is-proof-irrelevant/contr-center A x f y)
          p : Path A u.1 v.1 = (f x).2 v.1
          r : (Path Unit y (const-star A v.1)) = (tr A u.1 v.1 p (λz. Path Unit y (const-star A z)) u.2)
          q : Path (Path Unit y (const-star A v.1)) r v.2 =
                    Unit/is-set y (const-star A v.1) r v.2
      in
      SgPathO→PathΣ A (λz. Path Unit y (const-star A z)) u v (p, q)

    Finally, we use these two lemmas to build a contraction between the fibers of const-star, i.e., to show that const-star is an equivalence whenever A is an inhabited proposition. 

    is-proof-irrelevant/is-equiv-const-star (A : U) (x : A) (f : is-proof-irrelevant A) : is-equiv A Unit (const-star A) =
  λy.
    let c : Fib A Unit (const-star A) y = is-proof-irrelevant/contr-center A x f y
        contr : (H : Fib A Unit (const-star A) y) → Path (Fib A Unit (const-star A) y) c H =
                    is-proof-irrelevant/contr-contr A x f y
    in (c, contr)

is-proof-irrelevant/is-subterminal (A : U) (x : A) (f : is-proof-irrelevant A) : is-subterminal A =
  (const-star A, is-proof-irrelevant/is-equiv-const-star A x f)
  3. A subterminal type has a contractible identity

    If A is subterminal, then the identity types of A are equivalent to contractible types, hence, by the 3-for-2 property of contraction, the identity types of A are contractible. 

    is-subterminal/has-contr-eq (A : U) (e : is-subterminal A) : has-contr-eq A =
  λx y. is-contr/is-contr-equiv (Path A x y) (Path Unit (Equiv/map A Unit e x) (Equiv/map A Unit e y))
                                (Equiv/Equiv-id A Unit e x y)
                                (Unit/id-is-contr (Equiv/map A Unit e x) (Equiv/map A Unit e y))
  4. All the elements of a type are equal whenever it has a contractible equality

    To complete the equivalence proofs, we use the center of contraction of the equality to show that any two elements are equal. 

    has-contr-eq/is-prop (A : U) (c : has-contr-eq A) : is-prop A =
  λx y. (center (Path A x y) (c x y))
  5. Equivalences

    Thus, we can define back-and-forth maps between all the conditions.

    1. is-prop
      is-prop/is-subterminal (A : U) (p : is-prop A) (x : A) : is-subterminal A =
  is-proof-irrelevant/is-subterminal A x (is-prop/is-proof-irrelevant A p)

is-prop/has-contr-eq' (A : U) (p : is-prop A) (x : A) : has-contr-eq A =
  is-subterminal/has-contr-eq A (is-prop/is-subterminal A p x)

is-prop/has-contr-eq (A : U) (p : is-prop A) : has-contr-eq A =
  λx y. (p x y,
         λq. 
          let H : is-contr (Path A x y) = is-prop/has-contr-eq' A p x x y in
          comp (Path A x y) (p x y) (H.1) (inv (Path A x y) (H.1) (p x y) (H.2 (p x y)))
                            q (H.2 q))
    2. is-proof-irrelevant
      is-proof-irrelevant/has-contr-eq (A : U) (x : A) (f : is-proof-irrelevant A) : has-contr-eq A =
  is-subterminal/has-contr-eq A (is-proof-irrelevant/is-subterminal A x f)

is-proof-irrelevant/is-prop (A : U) (x : A) (f : is-proof-irrelevant A) : is-prop A =
  has-contr-eq/is-prop A (is-proof-irrelevant/has-contr-eq A x f)
    3. is-subterminal
      is-subterminal/is-prop (A : U) (e : is-subterminal A) : is-prop A =
  has-contr-eq/is-prop A (is-subterminal/has-contr-eq A e)

is-subterminal/is-proof-irrelevant (A : U) (e : is-subterminal A) : is-proof-irrelevant A =
  is-prop/is-proof-irrelevant A (is-subterminal/is-prop A e)
    4. has-contr-eq
      has-contr-eq/is-proof-irrelevant (A : U) (c : has-contr-eq A) : is-proof-irrelevant A =
  is-prop/is-proof-irrelevant A (has-contr-eq/is-prop A c)

has-contr-eq/is-subterminal (A : U) (x : A) (c : has-contr-eq A) : is-subterminal A =
  is-proof-irrelevant/is-subterminal A x (has-contr-eq/is-proof-irrelevant A c)

1.3 The Prop universe

UU-Prop : U = Σ U is-prop

Prop/type (A : UU-Prop) : U = A.1

Prop/is-prop (A : UU-Prop) : is-prop (Prop/type A) = A.2  

Prop/hom (A B : UU-Prop) : U = (Prop/type A) → (Prop/type B)

1.4 Empty is a proposition

Empty/is-prop : is-prop (Empty) =
  λx y. ex-falso (Path Empty x y) x

Empty/Prop : UU-Prop =
  ( Empty,
    Empty/is-prop)

1.5 Equiv when inverse

A map between two propositions is an equivalence as soon as there is a map back and forth between these two propositions. 

Prop/is-equiv (A B : UU-Prop) (f : Prop/hom A B) (g : Prop/hom B A) : is-equiv (Prop/type A) (Prop/type B) f =
  let H : Htpy' (Prop/type B) (Prop/type B) (λz. f (g z)) (id (Prop/type B)) = λx. Prop/is-prop B (f (g x)) x
      K : Htpy' (Prop/type A) (Prop/type A) (λz. g (f z)) (id (Prop/type A)) = λx. Prop/is-prop A (g (f x)) x
  in
  has-inverse/is-equiv (Prop/type A) (Prop/type B) f (g, (H, K))

Prop/Equiv (A B : UU-Prop) (f : Prop/hom A B) (g : Prop/hom B A) : Equiv (Prop/type A) (Prop/type B) =
  (f, Prop/is-equiv A B f g)

1.6 Closure under type-formers

The product of propositions is a proposition 

is-prop/prod (A B : U) (p : is-prop A) (q : is-prop B) : is-prop (A * B) =
  is-prop/sg A (λ_. B) p (λ_. q)

Prop/Prod (A B : UU-Prop) : UU-Prop =
  ( Prop/type A * Prop/type B,
    is-prop/prod
    ( Prop/type A)
    ( Prop/type B)
    ( Prop/is-prop A)
    ( Prop/is-prop B))

The dependent product of propositions is a proposition 

Pi/is-prop (A : U) (B : A → UU-Prop) : is-prop ((x : A) → Prop/type (B x)) =
  is-prop/pi A
    ( λx. Prop/type (B x))
    ( λx. Prop/is-prop (B x))

Prop/Pi (A : U) (B : A → UU-Prop) : UU-Prop =
  ( (x : A) → Prop/type (B x),
    Pi/is-prop A B)

The coproduct of P and Q is a proposition under the condition that P implies ¬ Q. 

Coprod/is-prop/inl (P Q : UU-Prop) (H : Prop/type P → neg (Prop/type Q)) (p : Prop/type P)
                        : (v : (Coprod (Prop/type P) (Prop/type Q)))
                         → Path (Coprod (Prop/type P) (Prop/type Q)) (inl p) v = split
  inl p' → Coprod/Eq/map (Prop/type P) (Prop/type Q) (inl p) (inl p') (Prop/is-prop P p p')
  inr q  →
    ex-falso
      ( Path (Coprod (Prop/type P) (Prop/type Q)) (inl p) (inr q))
      ( H p q)

Coprod/is-prop/inr (P Q : UU-Prop) (H : Prop/type P → neg (Prop/type Q)) (q : Prop/type Q)
                        : (v : Coprod (Prop/type P) (Prop/type Q))
                         → Path (Coprod (Prop/type P) (Prop/type Q)) (inr q) v = split
  inl p →
    ex-falso
      ( Path (Coprod (Prop/type P) (Prop/type Q)) (inr q) (inl p))
      ( H p q)
  inr q' → Coprod/Eq/map (Prop/type P) (Prop/type Q) (inr q) (inr q') (Prop/is-prop Q q q')

Coprod/is-prop (P Q : UU-Prop) (H : Prop/type P → neg (Prop/type Q)) : is-prop (Coprod (Prop/type P) (Prop/type Q)) = split 
  inl p → Coprod/is-prop/inl P Q H p
  inr q → Coprod/is-prop/inr P Q H q

Coprod/Prop (P Q : UU-Prop) (H : Prop/type P → neg (Prop/type Q)) : UU-Prop =
  ( Coprod (Prop/type P) (Prop/type Q),
    Coprod/is-prop P Q H)

1.7 Path of proposition is proposition

is-prop/path (A : UU-Prop) (x y : Prop/type A) : is-prop (Path (Prop/type A) x y) =
  is-contr→is-prop
    ( Path (Prop/type A) x y)
    ( is-prop/has-contr-eq
      ( Prop/type A)
      ( Prop/is-prop A) x y)

is-prop/Prop-path (A : UU-Prop) (x y : Prop/type A) : UU-Prop =
  ( Path (Prop/type A) x y,
    is-prop/path A x y)

1.8 Consequence that is-prop implies subterminal: Σ A B is A if B is contractible

Equiv/Sg-target (A : U) (B : A → U) (f : (x : A) → is-contr (B x)) : Equiv (Σ A B) A =
  Equiv/trans
    ( Σ A B)
    ( Σ A (λ_. Unit)) A
    ( Equiv/Sg-fam A B (λ_. Unit)
      ( λx. is-prop/is-subterminal
            ( B x)
            ( is-contr/all-elements-equal
              ( B x)
              ( f x))
            ( f x).1))
    ( Equiv/Sg-base-unit A)

1.9 Σ(z: B(x))(x, y) = (a, z) ≃ x = a

Equiv/Path-tot (A : U) (B : A → U) (a : A) (x : A) (y : B x) : Equiv (Σ (B a) (λz. Path (Σ A B) (x, y) (a, z))) (Path A x a) =
  Equiv/comp two-Nat
    ( Σ (B a) (λz. Path (Σ A B) (x, y) (a, z)))
    ( Σ (B a) (λz. SgPathO A B (x, y) (a, z)))
    ( Equiv/Sg-fam
      ( B a)
      ( λz. Path (Σ A B) (x, y) (a, z))
      ( λz. SgPathO A B (x, y) (a, z))
      ( λz. PathSg/Equiv A B (x, y) (a, z)))
    ( Σ (Path A x a) (λp. Σ (B a) (λz. Path (B a) (tr A x a p B y) z)))
    ( Equiv/assoc-non-dep-Sg
      ( B a)
      ( Path A x a)
      ( λz p. Path (B a) (tr A x a p B y) z))
    ( Path A x a)
    ( Equiv/Sg-target
      ( Path A x a)
      ( λp. Σ (B a) (λz. Path (B a) (tr A x a p B y) z))
      ( λp. is-contr/Sg-path-is-contr
            ( B a)
            ( tr A x a p B y)))

Equiv/Path-tot' (A : U) (B : A → U) (a : A) (x : A) (y : B x) : Equiv (Path A x a) (Σ (B a) (λz. Path (Σ A B) (x, y) (a, z))) =
  Equiv/sym
    ( Σ (B a) (λz. Path (Σ A B) (x, y) (a, z)))
    ( Path A x a)
    ( Equiv/Path-tot A B a x y)

Author: Johann Rosain

Created: 2024-07-23 Tue 13:51

Validate