Arithmetic law for coproduct decomposition and Σ-decomposition

module foundation.arithmetic-law-coproduct-and-sigma-decompositions where
Imports
open import foundation.coproduct-decompositions
open import foundation.equivalences
open import foundation.functoriality-coproduct-types
open import foundation.relaxed-sigma-decompositions
open import foundation.type-arithmetic-coproduct-types
open import foundation.univalence
open import foundation.universal-property-coproduct-types

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

Idea

Let X be a type, we have the following equivalence :

  Σ ( (U , V , e) : Relaxed-Σ-Decomposition X)
    ( binary-coproduct-Decomposition U) ≃
  Σ ( (A , B , e) : binary-coproduct-Decomposition X)
    ( Relaxed-Σ-Decomposition A ×
      Relaxed-Σ-Decomposition B )

We also show a computational rule to simplify the use of this equivalence.

Propositions

Coproduct decomposition of the indexing type of a relaxed Σ-decomposition are equivalent to relaxed Σ-decomposition of the left and right summand of a coproduct decomposition.

module _
  {l : Level} {X : UU l}
  where

  private
    reassociate :
      Σ (Relaxed-Σ-Decomposition l l X)
        ( λ d  binary-coproduct-Decomposition l l
          ( indexing-type-Relaxed-Σ-Decomposition d)) 
        Σ ( UU l)
          ( λ A 
            Σ ( UU l)
              ( λ B 
                Σ ( Σ ( UU l) λ U  ( U  (A + B)))
                  ( λ U  Σ (pr1 U  UU l)  Y  X  Σ (pr1 U) Y))))
    pr1 reassociate ((U , V , f) , A , B , e) = (A , B , (U , e) , V , f)
    pr2 reassociate =
      is-equiv-has-inverse
        ( λ (A , B , (U , e) , V , f)  ((U , V , f) , A , B , e))
        ( refl-htpy)
        ( refl-htpy)

    reassociate' :
      Σ ( UU l)
        ( λ A 
          Σ ( UU l)
            ( λ B 
              Σ ( (A  UU l) × (B  UU l))
                ( λ (YA , YB) 
                  Σ ( Σ (UU l)  A'  A'  Σ A YA))
                    ( λ A' 
                      Σ ( Σ (UU l)  B'  B'  Σ B YB))
                        ( λ B'  X  (pr1 A' + pr1 B')))))) 
      Σ ( binary-coproduct-Decomposition l l X)
      ( λ d 
        Relaxed-Σ-Decomposition l l
          ( left-summand-binary-coproduct-Decomposition d) ×
        Relaxed-Σ-Decomposition l l
          ( right-summand-binary-coproduct-Decomposition d))
    pr1 reassociate' (A , B , (YA , YB) , (A' , eA) , (B' , eB) , e) =
      (A' , B' , e) , ((A , YA , eA) , B , YB , eB)
    pr2 reassociate' =
      is-equiv-has-inverse
        ( λ ((A' , B' , e) , ((A , YA , eA) , B , YB , eB)) 
          (A , B , (YA , YB) , (A' , eA) , (B' , eB) , e))
        ( refl-htpy)
        ( refl-htpy)

  equiv-binary-coproduct-Decomposition-Σ-Decomposition :
    Σ ( Relaxed-Σ-Decomposition l l X)
      ( λ d 
        binary-coproduct-Decomposition l l
          ( indexing-type-Relaxed-Σ-Decomposition d)) 
    Σ ( binary-coproduct-Decomposition l l X)
      ( λ d 
        Relaxed-Σ-Decomposition l l
          ( left-summand-binary-coproduct-Decomposition d) ×
        Relaxed-Σ-Decomposition l l
          ( right-summand-binary-coproduct-Decomposition d))

  equiv-binary-coproduct-Decomposition-Σ-Decomposition =
    ( ( reassociate') ∘e
      ( ( equiv-tot
            ( λ A 
              equiv-tot
                ( λ B 
                  ( ( equiv-tot
                        ( λ ( YA , YB) 
                          ( ( equiv-tot
                              ( λ A' 
                                equiv-tot
                                  ( λ B' 
                                    equiv-postcomp-equiv
                                      ( equiv-coprod
                                        ( inv-equiv (pr2 A'))
                                        ( inv-equiv (pr2 B')))
                                      ( X))) ∘e
                            ( ( inv-left-unit-law-Σ-is-contr
                                  ( is-contr-total-equiv' (Σ A YA))
                                  ( Σ A YA , id-equiv)) ∘e
                              ( inv-left-unit-law-Σ-is-contr
                                  ( is-contr-total-equiv' (Σ B YB))
                                  ( Σ B YB , id-equiv)))))) ∘e
                    ( ( equiv-Σ-equiv-base
                          ( λ (YA , YB)  X  (Σ A YA + Σ B YB))
                          ( equiv-universal-property-coprod (UU l))) ∘e
                      ( ( equiv-tot
                            ( λ Y 
                              equiv-postcomp-equiv
                                ( right-distributive-Σ-coprod A B Y)
                                ( X))) ∘e
                          ( left-unit-law-Σ-is-contr
                              ( is-contr-total-equiv' (A + B))
                              ((A + B) , id-equiv))))))))) ∘e
      ( reassociate)))

  module _
    ( D : Σ ( Relaxed-Σ-Decomposition l l X)
            ( λ D 
              binary-coproduct-Decomposition
                l l
                ( indexing-type-Relaxed-Σ-Decomposition D)))
    where

    private
      tr-total-equiv :
        {l1 l3 l4 : Level} {X Y : UU l1} (e : Y  X) 
        (h : Id {A = Σ (UU l1) λ Y  Y  X} (X , id-equiv) (Y , e)) 
        {C : (X : UU l1)  (X  UU l3)  UU l4} 
        {f : Σ (Y  UU l3)  Z  C Y Z)} 
        (x : X) 
        pr1
          ( tr
            ( λ Y 
              ( Σ ( pr1 Y  UU l3)
                  ( λ Z  C (pr1 Y) Z) 
                Σ ( X  UU l3)
                  ( λ Z  C X Z)))
            ( h)
            ( id)
            ( f))
          ( x) 
        pr1 f (map-inv-equiv e x)
      tr-total-equiv e refl x = refl

    compute-left-equiv-binary-coproduct-Decomposition-Σ-Decomposition :
      ( a : left-summand-binary-coproduct-Decomposition (pr2 D)) 
      cotype-Relaxed-Σ-Decomposition
        ( pr1
          ( pr2
            ( map-equiv equiv-binary-coproduct-Decomposition-Σ-Decomposition
              ( D))))
        ( a) 
      cotype-Relaxed-Σ-Decomposition
        ( pr1 D)
        ( map-inv-equiv
          ( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
          ( inl a))
    compute-left-equiv-binary-coproduct-Decomposition-Σ-Decomposition a =
      tr-total-equiv
        ( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
        ( inv
            ( contraction
                ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
                ( (pr1 (pr2 D) + pr1 (pr2 (pr2 D))) , id-equiv)) 
          contraction
            ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
                ( pr1 (pr1 D) , pr2 (pr2 (pr2 D))))
        ( inl a)

    compute-right-equiv-binary-coproduct-Decomposition-Σ-Decomposition :
      ( b : right-summand-binary-coproduct-Decomposition (pr2 D)) 
      cotype-Relaxed-Σ-Decomposition
        ( pr2
          ( pr2
            ( map-equiv equiv-binary-coproduct-Decomposition-Σ-Decomposition
              ( D))))
        ( b) 
      cotype-Relaxed-Σ-Decomposition (pr1 D)
        ( map-inv-equiv
          ( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
          ( inr b))
    compute-right-equiv-binary-coproduct-Decomposition-Σ-Decomposition b =
      tr-total-equiv
          ( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
          ( inv
              ( contraction
                  ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
                  ( (pr1 (pr2 D) + pr1 (pr2 (pr2 D))) , id-equiv)) 
            contraction
              ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
                  ( pr1 (pr1 D) , pr2 (pr2 (pr2 D))))
          ( inr b)