Coproduct Properties

Table of Contents

1 Coproduct properties

module Lib.Prop.Coprod where

This file shows additional properties on coproducts.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Stdlib.Prelude
import Lib.FundamentalTheorem
import Lib.FunExt
import Lib.Data.Coprod
import Lib.Prop.Equiv
import Lib.Prop.Htpy

1.2 If A ≅ A' and B ≅ B', then A + B ≅ A' + B'

1.2.1 Identity

Coprod/id-htpy (A B : U) : Htpy' (Coprod A B) (Coprod A B) (Coprod/map A B A B (id A) (id B)) (id (Coprod A B)) = split
  inl x → refl (Coprod A B) (inl x)
  inr y → refl (Coprod A B) (inr y)

1.2.2 Pair of composable functions

Coprod/comp-fun-htpy (A A' A'' : U) (B B' B'' : U) (f : A → A') (f' : A' → A'') (g : B → B') (g' : B' → B'')
                               : Htpy' (Coprod A B) (Coprod A'' B'')
                                       (Coprod/map A B A'' B'' (λz. f' (f z)) (λz. g' (g z)))
                                       (λz. (Coprod/map A' B' A'' B'' f' g') (Coprod/map A B A' B' f g z)) = split
  inl x → refl (Coprod A'' B'') (inl (f' (f x)))
  inr y → refl (Coprod A'' B'') (inr (g' (g y)))

1.2.3 Homotopies

Coprod/copr-htpy (A A' : U) (B B' : U) (f f' : A → A') (g g' : B → B') (H : Htpy' A A' f f') (K : Htpy' B B' g g')
                       : Htpy' (Coprod A B) (Coprod A' B') (Coprod/map A B A' B' f g) (Coprod/map A B A' B' f' g') = split
  inl x → ap A' (Coprod A' B') (λz. inl z) (f x) (f' x) (H x)
  inr y → ap B' (Coprod A' B') (λz. inr z) (g y) (g' y) (K y)

1.2.4 Result

If f and g are equivalences, then they have inverses.

  1. Inverse

    Thus, the inverse of f + g is f-1 + g-1. Indeed, we have (f + g) ˆ (f-1 + g-1) ∼ (f ˆ f-1) + (g ˆ g-1) ∼ (id A') + (id B') ∼ id (A' + B'). The other homotopy is symmetric. 

    Coprod/closed-is-equiv-map (A A' B B' : U) (f : A → A') (g : B → B') : Coprod A B → Coprod A' B' =
  Coprod/map A B A' B' f g  

Coprod/closed-is-equiv-inv-map (A A' B B' : U) (f : A → A') (g : B → B') (e : is-equiv A A' f) (e' : is-equiv B B' g)
                                          : Coprod A' B' → Coprod A B =
  let f' : A' → A = is-equiv/inv-map A A' f e
      g' : B' → B = is-equiv/inv-map B B' g e'
  in Coprod/map A' B' A B f' g'

Coprod/closed-is-equiv-right-htpy (A A' B B' : U) (f : A → A') (g : B → B') (e : is-equiv A A' f) (e' : is-equiv B B' g)
                                             : Htpy' (Coprod A' B') (Coprod A' B')
                                                     (λz. (Coprod/closed-is-equiv-map A A' B B' f g) (Coprod/closed-is-equiv-inv-map A A' B B' f g e e' z))
                                                     (id (Coprod A' B')) =
  let f' : A' → A = is-equiv/inv-map A A' f e
      g' : B' → B = is-equiv/inv-map B B' g e'
      H : Htpy' A' A' (λz. f (f' z)) (id A') = is-equiv/inv-right-htpy A A' f e
      H' : Htpy' B' B' (λz. g (g' z)) (id B') = is-equiv/inv-right-htpy B B' g e'
  in
  Htpy'/comp (Coprod A' B') (Coprod A' B') (λz. (Coprod/closed-is-equiv-map A A' B B' f g) (Coprod/closed-is-equiv-inv-map A A' B B' f g e e' z))
                                           (Coprod/map A' B' A' B' (λz. f (f' z)) (λz. g (g' z))) (id (Coprod A' B'))
                                           (Htpy'/inv (Coprod A' B') (Coprod A' B') (Coprod/map A' B' A' B' (λz. f (f' z)) (λz. g (g' z)))
                                                      (λz. (Coprod/closed-is-equiv-map A A' B B' f g) (Coprod/closed-is-equiv-inv-map A A' B B' f g e e' z))
                                                      (Coprod/comp-fun-htpy A' A A' B' B B' f' f g' g))
                                           (Htpy'/comp (Coprod A' B') (Coprod A' B')
                                                       (Coprod/map A' B' A' B' (λz. f (f' z)) (λz. g (g' z)))
                                                       (Coprod/map A' B' A' B' (id A') (id B')) (id (Coprod A' B'))
                                                       (Coprod/copr-htpy A' A' B' B' (λz. f (f' z)) (id A') (λz. g (g' z)) (id B') H H')
                                                       (Coprod/id-htpy A' B'))

Coprod/closed-is-equiv-left-htpy (A A' B B' : U) (f : A → A') (g : B → B') (e : is-equiv A A' f) (e' : is-equiv B B' g)
                                            : Htpy' (Coprod A B) (Coprod A B)
                                                     (λz. (Coprod/closed-is-equiv-inv-map A A' B B' f g e e') (Coprod/closed-is-equiv-map A A' B B' f g z))
                                                     (id (Coprod A B)) =
  let f' : A' → A = is-equiv/inv-map A A' f e
      g' : B' → B = is-equiv/inv-map B B' g e'
      K : Htpy' A A (λz. f' (f z)) (id A) = is-equiv/inv-left-htpy A A' f e
      K' : Htpy' B B (λz. g' (g z)) (id B) = is-equiv/inv-left-htpy B B' g e'
  in
  Htpy'/comp (Coprod A B) (Coprod A B) (λz. (Coprod/closed-is-equiv-inv-map A A' B B' f g e e') (Coprod/closed-is-equiv-map A A' B B' f g z))
                                       (Coprod/map A B A B (λz. f' (f z)) (λz. g' (g z))) (id (Coprod A B))
                                           (Htpy'/inv (Coprod A B) (Coprod A B) (Coprod/map A B A B (λz. f' (f z)) (λz. g' (g z)))
                                                      (λz. (Coprod/closed-is-equiv-inv-map A A' B B' f g e e') (Coprod/closed-is-equiv-map A A' B B' f g z))
                                                      (Coprod/comp-fun-htpy A A' A B B' B f f' g g'))
                                           (Htpy'/comp (Coprod A B) (Coprod A B)
                                                       (Coprod/map A B A B (λz. f' (f z)) (λz. g' (g z)))
                                                       (Coprod/map A B A B (id A) (id B)) (id (Coprod A B))
                                                       (Coprod/copr-htpy A A B B (λz. f' (f z)) (id A) (λz. g' (g z)) (id B) K K')
                                                       (Coprod/id-htpy A B))
  2. Equiv
    Coprod/closed-is-equiv (A A' B B' : U) (f : A → A') (g : B → B') (e : is-equiv A A' f) (e' : is-equiv B B' g)
                                  : is-equiv (Coprod A B) (Coprod A' B') (Coprod/closed-is-equiv-map A A' B B' f g) =
  has-inverse/is-equiv (Coprod A B) (Coprod A' B') (Coprod/closed-is-equiv-map A A' B B' f g)
    (Coprod/closed-is-equiv-inv-map A A' B B' f g e e',
      (Coprod/closed-is-equiv-right-htpy A A' B B' f g e e',
       Coprod/closed-is-equiv-left-htpy A A' B B' f g e e'))

Coprod/closed-Equiv (A A' B B' : U) (e : Equiv A A') (e' : Equiv B B') : Equiv (Coprod A B) (Coprod A' B') =
  (Coprod/closed-is-equiv-map A A' B B' (Equiv/map A A' e) (Equiv/map B B' e'),
    Coprod/closed-is-equiv A A' B B' (Equiv/map A A' e) (Equiv/map B B' e') (Equiv/is-equiv A A' e) (Equiv/is-equiv B B' e'))

1.3 Coprod is associative, that is, (A + B) + C ≅ A + (B + C)

Coprod/assoc-map (A B C : U) : (Coprod (Coprod A B) C) → (Coprod A (Coprod B C)) = split
  inl c → ind-Coprod A B (λ_. Coprod A (Coprod B C)) (λx. inl x) (λy. inr (inl y)) c
  inr z → inr (inr z)

Coprod/assoc-inv-map (A B C : U) : (Coprod A (Coprod B C)) → Coprod (Coprod A B) C = split
  inl x → inl (inl x)
  inr a → ind-Coprod B C (λ_. Coprod (Coprod A B) C) (λy. inl (inr y)) (λz. inr z) a

Coprod/assoc-right-htpy (A B C : U) : Htpy' (Coprod A (Coprod B C)) (Coprod A (Coprod B C))
                                            (λz. (Coprod/assoc-map A B C) (Coprod/assoc-inv-map A B C z))
                                            (id (Coprod A (Coprod B C))) = split
  inl x → refl (Coprod A (Coprod B C)) (inl x)
  inr a → ind-Coprod B C (λx. Path (Coprod A (Coprod B C)) ((Coprod/assoc-map A B C) (Coprod/assoc-inv-map A B C (inr x))) (inr x))
                         (λy. refl (Coprod A (Coprod B C)) (inr (inl y))) (λz. refl (Coprod A (Coprod B C)) (inr (inr z))) a

Coprod/assoc-left-htpy (A B C : U) : Htpy' (Coprod (Coprod A B) C) (Coprod (Coprod A B) C)
                                           (λz. (Coprod/assoc-inv-map A B C) (Coprod/assoc-map A B C z))
                                           (id (Coprod (Coprod A B) C)) = split
  inl c → ind-Coprod A B (λz. Path (Coprod (Coprod A B) C) ((Coprod/assoc-inv-map A B C) (Coprod/assoc-map A B C (inl z))) (inl z))
                         (λx. refl (Coprod (Coprod A B) C) (inl (inl x))) (λy. refl (Coprod (Coprod A B) C) (inl (inr y))) c
  inr z → refl (Coprod (Coprod A B) C) (inr z)

Coprod/assoc-is-equiv (A B C : U) : is-equiv (Coprod (Coprod A B) C) (Coprod A (Coprod B C)) (Coprod/assoc-map A B C) =
  has-inverse/is-equiv (Coprod (Coprod A B) C) (Coprod A (Coprod B C)) (Coprod/assoc-map A B C)
    (Coprod/assoc-inv-map A B C, (Coprod/assoc-right-htpy A B C, Coprod/assoc-left-htpy A B C))

Coprod/assoc (A B C : U) : Equiv (Coprod (Coprod A B) C) (Coprod A (Coprod B C)) =
  (Coprod/assoc-map A B C, Coprod/assoc-is-equiv A B C)

1.4 Observational equality of coprod

We define equality for coproducts. 

Coprod/Eq-inl (A B : U) (a : A) : Coprod A B → U = split
  inl x → Path A a x
  inr _ → Empty

Coprod/Eq-inr (A B : U) (b : B) : Coprod A B → U = split
  inl _ → Empty
  inr y → Path B b y

Coprod/Eq (A B : U) : Coprod A B → Coprod A B → U = split
  inl a → Coprod/Eq-inl A B a
  inr b → Coprod/Eq-inr A B b

Coprod/Eq/refl (A B : U) : (x : Coprod A B) → Coprod/Eq A B x x = split
  inl y → refl A y
  inr z → refl B z

We use the fundamental theorem to show that this observational equality is indeed an equality. First, we show that for any s : A + B, Σ (t : A + B) Coprod/Eq s t is contractible. 

Coprod/Eq/is-contr (A B : U) : (s : Coprod A B) → is-contr (Σ (Coprod A B) (Coprod/Eq A B s)) = split
  inl x → is-contr/is-contr-equiv (Σ (Coprod A B) (Coprod/Eq A B (inl x))) (Σ A (λy. Path A x y))
            (Equiv/trans (Σ (Coprod A B) (Coprod/Eq A B (inl x))) (Coprod (Σ A (λy. Path A x y)) (B * Empty)) (Σ A (λy. Path A x y))
              (Equiv/Sg-distr-over-coprod A B (Coprod/Eq A B (inl x)))
              (Equiv/trans (Coprod (Σ A (λy. Path A x y)) (B * Empty)) (Coprod (Σ A (λy. Path A x y)) Empty) (Σ A (λy. Path A x y))
                (Coprod/closed-Equiv (Σ A (λy. Path A x y)) (Σ A (λy. Path A x y)) (B * Empty) Empty (Equiv/refl (Σ A (λy. Path A x y))) (Equiv/Sg-empty B))
                (Equiv/Equiv-copr-type-empty (Σ A (λy. Path A x y)))))
            (is-contr/Sg-path-is-contr A x)
  inr y → is-contr/is-contr-equiv (Σ (Coprod A B) (Coprod/Eq A B (inr y))) (Σ B (λz. Path B y z))
            (Equiv/trans (Σ (Coprod A B) (Coprod/Eq A B (inr y))) (Coprod (A * Empty) (Σ B (λz. Path B y z))) (Σ B (λz. Path B y z))
              (Equiv/Sg-distr-over-coprod A B (Coprod/Eq A B (inr y)))
              (Equiv/trans (Coprod (A * Empty) (Σ B (λz. Path B y z))) (Coprod Empty (Σ B (λz. Path B y z))) (Σ B (λz. Path B y z))
                (Coprod/closed-Equiv (A * Empty) Empty (Σ B (λz. Path B y z)) (Σ B (λz. Path B y z))
                  (Equiv/Sg-empty A) (Equiv/refl (Σ B (λz. Path B y z))))
                (Equiv/Equiv-copr-empty-type (Σ B (λz. Path B y z)))))
            (is-contr/Sg-path-is-contr B y)

That is, using the fundamental theorem, the following family of maps is a family of equivalences. 

Coprod/Eq/eq-map (A B : U) (s : Coprod A B) : (t : Coprod A B) → Path (Coprod A B) s t → Coprod/Eq A B s t = split
  inl x → λp. J (Coprod A B) (inl x) (λt _. Coprod/Eq A B t (inl x)) (refl A x) s (inv (Coprod A B) s (inl x) p)
  inr y → λp. J (Coprod A B) (inr y) (λt _. Coprod/Eq A B t (inr y)) (refl B y) s (inv (Coprod A B) s (inr y) p)

Coprod/Eq/is-equiv-eq-map (A B : U) (s t : Coprod A B) : is-equiv (Path (Coprod A B) s t) (Coprod/Eq A B s t) (Coprod/Eq/eq-map A B s t) =
  fundamental-theorem-id (Coprod A B) (Coprod/Eq A B s) s (Coprod/Eq/eq-map A B s) (Coprod/Eq/is-contr A B s) t

Coprod/Eq/Equiv (A B : U) (s t : Coprod A B) : Equiv (Path (Coprod A B) s t) (Coprod/Eq A B s t) =
  ( Coprod/Eq/eq-map A B s t,
    Coprod/Eq/is-equiv-eq-map A B s t)

Coprod/Eq/Equiv' (A B : U) (s t : Coprod A B) : Equiv (Coprod/Eq A B s t) (Path (Coprod A B) s t) =
  Equiv/sym 
    ( Path (Coprod A B) s t)
    ( Coprod/Eq A B s t)
    ( Coprod/Eq/Equiv A B s t)

Coprod/Eq/map (A B : U) (s t : Coprod A B) : Coprod/Eq A B s t → Path (Coprod A B) s t =
  is-equiv/inv-map (Path (Coprod A B) s t) (Coprod/Eq A B s t) (Coprod/Eq/eq-map A B s t) (Coprod/Eq/is-equiv-eq-map A B s t)

1.5 inl and inr are injective

Coprod/inl-inj (A B : U) (x y : A) (p : Path (Coprod A B) (inl x) (inl y)) : Path A x y =
  Coprod/Eq/eq-map A B (inl x) (inl y) p

Coprod/inr-inj (A B : U) (x y : B) (p : Path (Coprod A B) (inr x) (inr y)) : Path B x y =
  Coprod/Eq/eq-map A B (inr x) (inr y) p

1.6 Dependent universal property of the coproduct

The map Πz: A + BP(z) → Πx: AP(inl(x)) + Πy: BP(inr(y)) is an equivalence. 

Coprod/dependent-universal-property/map (A B : U) (P : Coprod A B → U) : ((z : Coprod A B) → P z) → ((x : A) → P (inl x)) * ((y : B) → P (inr y)) =
  λf. (λx. f (inl x), λy. f (inr y))

Coprod/dependent-universal-property/inv-map (A B : U) (P : Coprod A B → U) (t : ((x : A) → P (inl x)) * ((y : B) → P (inr y))) : (z : Coprod A B) → P z = split
  inl x → t.1 x
  inr y → t.2 y

Coprod/dependent-universal-property/right-htpy' (A B : U) (P : Coprod A B → U) (f : ((x : A) → P (inl x))) (g : ((y : B) → P (inr y))) 
                                                     : Path (((x : A) → P (inl x)) * ((y : B) → P (inr y)))
                                                            (Coprod/dependent-universal-property/map A B P (Coprod/dependent-universal-property/inv-map A B P (f, g))) (f, g) =
  let u : ((x : A) → P (inl x)) * ((y : B) → P (inr y)) = Coprod/dependent-universal-property/map A B P (Coprod/dependent-universal-property/inv-map A B P (f, g)) in
  Eq-prod/eq
    ( (x : A) → P (inl x))
    ( (y : B) → P (inr y))
    ( Coprod/dependent-universal-property/map A B P (Coprod/dependent-universal-property/inv-map A B P (f, g))) (f, g)
    ( eq-htpy A
      ( λx. P (inl x)) u.1 f
      ( λx. refl (P (inl x)) (f x)),
      eq-htpy B
      ( λy. P (inr y)) u.2 g
      ( λy. refl (P (inr y)) (g y)))      

Coprod/dependent-universal-property/right-htpy (A B : U) (P : Coprod A B → U) (t : ((x : A) → P (inl x)) * ((y : B) → P (inr y)))
                                                    : Path (((x : A) → P (inl x)) * ((y : B) → P (inr y)))
                                                           (Coprod/dependent-universal-property/map A B P (Coprod/dependent-universal-property/inv-map A B P t)) t =
  Coprod/dependent-universal-property/right-htpy' A B P t.1 t.2

Coprod/dependent-universal-property/left-htpy/Coprod (A B : U) (P : Coprod A B → U) (f : (z : Coprod A B) → P z)
                                                          : (z : Coprod A B)
                                                          → Path (P z) (Coprod/dependent-universal-property/inv-map A B P (Coprod/dependent-universal-property/map A B P f) z) (f z) = split
  inl x → refl (P (inl x)) (f (inl x))
  inr y → refl (P (inr y)) (f (inr y))

Coprod/dependent-universal-property/left-htpy (A B : U) (P : Coprod A B → U) (f : (z : Coprod A B) → P z)
                                                    : Path ((z : Coprod A B) → P z)
                                                           (Coprod/dependent-universal-property/inv-map A B P (Coprod/dependent-universal-property/map A B P f)) f =
  eq-htpy
    ( Coprod A B) P
    ( Coprod/dependent-universal-property/inv-map A B P (Coprod/dependent-universal-property/map A B P f)) f
    ( Coprod/dependent-universal-property/left-htpy/Coprod A B P f)

Coprod/dependent-universal-property/is-equiv (A B : U) (P : Coprod A B → U)
                                                  : is-equiv ((z : Coprod A B) → P z) (((x : A) → P (inl x)) * ((y : B) → P (inr y))) (Coprod/dependent-universal-property/map A B P) =
  has-inverse/is-equiv
    ( (z : Coprod A B) → P z)
    ( ((x : A) → P (inl x)) * ((y : B) → P (inr y)))
    ( Coprod/dependent-universal-property/map A B P)
    ( Coprod/dependent-universal-property/inv-map A B P,
      ( Coprod/dependent-universal-property/right-htpy A B P,
        Coprod/dependent-universal-property/left-htpy A B P))

Coprod/dependent-universal-property (A B : U) (P : Coprod A B → U) : Equiv ((z : Coprod A B) → P z) (((x : A) → P (inl x)) * ((y : B) → P (inr y))) =
  ( Coprod/dependent-universal-property/map A B P,
    Coprod/dependent-universal-property/is-equiv A B P)

Author: Johann Rosain

Created: 2024-07-23 Tue 13:51

Validate