Coproduct decompositions

module foundation.coproduct-decompositions where
Imports
open import foundation.coproduct-decompositions-subuniverse
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functoriality-coproduct-types
open import foundation.structure-identity-principle
open import foundation.transport
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type
open import foundation.univalence

open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.standard-finite-types

Definitions

Binary coproduct decomposition

module _
  {l1 : Level} (l2 l3 : Level) (X : UU l1)
  where

  binary-coproduct-Decomposition : UU (l1  lsuc l2  lsuc l3)
  binary-coproduct-Decomposition =
    Σ ( UU l2) ( λ A  Σ ( UU l3) ( λ B  (X  (A + B))))

module _
  {l1 l2 l3 : Level} {X : UU l1}
  (d : binary-coproduct-Decomposition l2 l3 X)
  where

  left-summand-binary-coproduct-Decomposition : UU l2
  left-summand-binary-coproduct-Decomposition = pr1 d

  right-summand-binary-coproduct-Decomposition : UU l3
  right-summand-binary-coproduct-Decomposition = pr1 (pr2 d)

  matching-correspondence-binary-coproduct-Decomposition :
    X 
    ( left-summand-binary-coproduct-Decomposition +
      right-summand-binary-coproduct-Decomposition)
  matching-correspondence-binary-coproduct-Decomposition = pr2 (pr2 d)

Propositions

Coproduct decomposition is equivalent to coproduct decomposition of a full subuniverse

equiv-coproduct-Decomposition-full-subuniverse :
  {l1 : Level}  (X : UU l1) 
  binary-coproduct-Decomposition l1 l1 X 
  binary-coproduct-Decomposition-subuniverse  _  unit-Prop) (X , star)
pr1 (equiv-coproduct-Decomposition-full-subuniverse X) d =
  ( left-summand-binary-coproduct-Decomposition d , star) ,
  ( right-summand-binary-coproduct-Decomposition d , star) ,
  ( matching-correspondence-binary-coproduct-Decomposition d)
pr2 (equiv-coproduct-Decomposition-full-subuniverse X) =
  is-equiv-has-inverse
    ( λ d 
      type-left-summand-binary-coproduct-Decomposition-subuniverse
        ( λ _  unit-Prop)
        ( X , star)
        ( d) ,
     type-right-summand-binary-coproduct-Decomposition-subuniverse
       ( λ _  unit-Prop)
       ( X , star)
       ( d) ,
     matching-correspondence-binary-coproduct-Decomposition-subuniverse
       ( λ _  unit-Prop)
       ( X , star)
       ( d))
    ( λ d 
      eq-equiv-binary-coproduct-Decomposition-subuniverse
        ( λ _  unit-Prop)
        ( X , star)
        ( _)
        ( d)
        ( id-equiv ,
          ( id-equiv ,
            htpy-right-whisk
              ( id-map-coprod _ _)
              ( map-equiv
                ( matching-correspondence-binary-coproduct-Decomposition-subuniverse
                  ( λ _  unit-Prop)
                  ( X , star)
                  ( d))))))
    ( refl-htpy)

Characterization of equality of binary coproduct Decomposition

equiv-binary-coproduct-Decomposition :
  {l1 l2 l3 l4 l5 : Level} {A : UU l1}
  (X : binary-coproduct-Decomposition l2 l3 A)
  (Y : binary-coproduct-Decomposition l4 l5 A) 
  UU (l1  l2  l3  l4  l5)
equiv-binary-coproduct-Decomposition X Y =
  Σ ( left-summand-binary-coproduct-Decomposition X 
      left-summand-binary-coproduct-Decomposition Y)
    ( λ el 
      Σ ( right-summand-binary-coproduct-Decomposition X 
          right-summand-binary-coproduct-Decomposition Y)
        ( λ er 
          ( map-coprod (map-equiv el) (map-equiv er) 
            map-equiv
              ( matching-correspondence-binary-coproduct-Decomposition X)) ~
          ( map-equiv
            ( matching-correspondence-binary-coproduct-Decomposition Y))))

module _
  {l1 l2 l3 l4 l5 : Level} {A : UU l1}
  (X : binary-coproduct-Decomposition l2 l3 A)
  (Y : binary-coproduct-Decomposition l4 l5 A)
  (e : equiv-binary-coproduct-Decomposition X Y)
  where

  equiv-left-summand-equiv-binary-coproduct-Decomposition :
    left-summand-binary-coproduct-Decomposition X 
    left-summand-binary-coproduct-Decomposition Y
  equiv-left-summand-equiv-binary-coproduct-Decomposition = pr1 e

  map-equiv-left-summand-equiv-binary-coproduct-Decomposition :
    left-summand-binary-coproduct-Decomposition X 
    left-summand-binary-coproduct-Decomposition Y
  map-equiv-left-summand-equiv-binary-coproduct-Decomposition =
    map-equiv equiv-left-summand-equiv-binary-coproduct-Decomposition

  equiv-right-summand-equiv-binary-coproduct-Decomposition :
    right-summand-binary-coproduct-Decomposition X 
    right-summand-binary-coproduct-Decomposition Y
  equiv-right-summand-equiv-binary-coproduct-Decomposition = pr1 (pr2 e)

  map-equiv-right-summand-equiv-binary-coproduct-Decomposition :
    right-summand-binary-coproduct-Decomposition X 
    right-summand-binary-coproduct-Decomposition Y
  map-equiv-right-summand-equiv-binary-coproduct-Decomposition =
    map-equiv (equiv-right-summand-equiv-binary-coproduct-Decomposition)

module _
  {l1 l2 l3 : Level} {A : UU l1} (X : binary-coproduct-Decomposition l2 l3 A)
  where

  id-equiv-binary-coproduct-Decomposition :
    equiv-binary-coproduct-Decomposition X X
  pr1 id-equiv-binary-coproduct-Decomposition = id-equiv
  pr1 (pr2 id-equiv-binary-coproduct-Decomposition) = id-equiv
  pr2 (pr2 id-equiv-binary-coproduct-Decomposition) x =
    id-map-coprod
      ( left-summand-binary-coproduct-Decomposition X)
      ( right-summand-binary-coproduct-Decomposition X)
      ( map-equiv
        ( matching-correspondence-binary-coproduct-Decomposition X)
        ( x))

  is-contr-total-equiv-binary-coproduct-Decomposition :
    is-contr
      ( Σ ( binary-coproduct-Decomposition l2 l3 A)
          ( equiv-binary-coproduct-Decomposition X))
  is-contr-total-equiv-binary-coproduct-Decomposition =
    is-contr-total-Eq-structure
      ( _)
      ( is-contr-total-equiv ( left-summand-binary-coproduct-Decomposition X))
      ( left-summand-binary-coproduct-Decomposition X , id-equiv)
      ( is-contr-total-Eq-structure
        ( _)
        ( is-contr-total-equiv (right-summand-binary-coproduct-Decomposition X))
        ( right-summand-binary-coproduct-Decomposition X , id-equiv)
        ( is-contr-total-htpy-equiv
          ( equiv-coprod id-equiv id-equiv ∘e
            matching-correspondence-binary-coproduct-Decomposition X)))

  equiv-eq-binary-coproduct-Decomposition :
    (Y : binary-coproduct-Decomposition l2 l3 A)  (X  Y) 
    equiv-binary-coproduct-Decomposition X Y
  equiv-eq-binary-coproduct-Decomposition .X refl =
    id-equiv-binary-coproduct-Decomposition

  is-equiv-equiv-eq-binary-coproduct-Decomposition :
    (Y : binary-coproduct-Decomposition l2 l3 A) 
    is-equiv (equiv-eq-binary-coproduct-Decomposition Y)
  is-equiv-equiv-eq-binary-coproduct-Decomposition =
    fundamental-theorem-id
      is-contr-total-equiv-binary-coproduct-Decomposition
      equiv-eq-binary-coproduct-Decomposition

  extensionality-binary-coproduct-Decomposition :
    (Y : binary-coproduct-Decomposition l2 l3 A) 
    (X  Y)  equiv-binary-coproduct-Decomposition X Y
  pr1 (extensionality-binary-coproduct-Decomposition Y) =
    equiv-eq-binary-coproduct-Decomposition Y
  pr2 (extensionality-binary-coproduct-Decomposition Y) =
    is-equiv-equiv-eq-binary-coproduct-Decomposition Y

  eq-equiv-binary-coproduct-Decomposition :
    (Y : binary-coproduct-Decomposition l2 l3 A) 
    equiv-binary-coproduct-Decomposition X Y  (X  Y)
  eq-equiv-binary-coproduct-Decomposition Y =
    map-inv-equiv (extensionality-binary-coproduct-Decomposition Y)

Equivalence between X → Fin 2 and binary-coproduct-Decomposition l1 l1 X

module _
  {l1 : Level}
  (X : UU l1)
  where

  module _
    (f : X  Fin 2)
    where

    matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
      (X  ((fib f (inl (inr star))) + (fib f (inr star))))
    matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ =
      ( ( equiv-coprod
          ( left-unit-law-Σ-is-contr ( is-contr-Fin-one-ℕ) ( inr star))
          ( left-unit-law-Σ-is-contr is-contr-unit star)) ∘e
        ( ( right-distributive-Σ-coprod ( Fin 1) unit  x  fib f x) ∘e
            ( inv-equiv-total-fib f))))

    compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
      (x : X) 
      (inl (inr star)  f x) 
      Σ ( Σ ( fib f (inl (inr star)))
            ( λ y 
              inl y 
              ( map-equiv
                ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
                ( x))))
        ( λ z  pr1 (pr1 z)  x)
    compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
      x p =
      tr
        ( λ a 
          Σ ( Σ ( fib f (inl (inr star)))
              ( λ y 
                inl y 
                ( map-coprod
                  ( map-left-unit-law-Σ-is-contr
                    ( is-contr-Fin-one-ℕ)
                    ( inr star))
                  ( map-left-unit-law-Σ-is-contr is-contr-unit star))
                  ( map-right-distributive-Σ-coprod
                    ( Fin 1)
                    ( unit)
                    ( λ x  fib f x)
                    ( pr1 a , x , pr2 a))))
            ( λ z  pr1 (pr1 z)  x))
        ( eq-pair-Σ p ( tr-Id p (inv p)  left-inv p))
        ( ( ( x , (inv p)) ,
            ( ap
              ( inl)
              ( inv
                ( inv-map-eq-transpose-equiv
                  ( left-unit-law-Σ-is-contr is-contr-Fin-one-ℕ (inr star))
                  ( refl))))),
          refl)

    compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ :
      (y : fib f (inl (inr star))) 
      pr1 y 
      map-inv-equiv
        ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
        ( inl y)
    compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ
      y =
      map-eq-transpose-equiv
        ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
        ( inv
          ( pr2
            ( pr1
              ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( pr1 y)
                ( inv (pr2 y))))) 
          ap
            inl
            ( eq-pair-Σ
              ( pr2
                ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                  ( pr1 y)
                  ( inv (pr2 y))))
              ( eq-is-prop (is-set-Fin 2 _ _))))

    compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
      (x : X) 
      (inr star  f x) 
      Σ ( Σ ( fib f (inr star))
            ( λ y 
              inr y 
              ( map-equiv
                ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
                ( x))))
        ( λ z  pr1 (pr1 z)  x)
    compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
      x p =
      tr
        ( λ a 
          Σ ( Σ ( fib f (inr star))
                ( λ y 
                  inr y 
                  ( map-coprod
                    ( map-left-unit-law-Σ-is-contr
                      ( is-contr-Fin-one-ℕ)
                      ( inr star))
                    ( map-left-unit-law-Σ-is-contr is-contr-unit star))
                    ( map-right-distributive-Σ-coprod
                      ( Fin 1)
                      ( unit)
                      ( λ x  fib f x)
                      ( pr1 a , x , pr2 a))))
            ( λ z  pr1 (pr1 z)  x))
        ( eq-pair-Σ p ( tr-Id p (inv p)  left-inv p))
        ( ( ( x , (inv p)) ,
            ( ap
              ( inr)
              ( inv
                  ( inv-map-eq-transpose-equiv
                    ( left-unit-law-Σ-is-contr is-contr-unit star)
                    ( refl))))),
          refl)

    compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ :
      (y : fib f (inr star)) 
      pr1 y 
      map-inv-equiv
        ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
        ( inr y)
    compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ
      y =
      map-eq-transpose-equiv
        ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
        ( inv
          ( pr2
            ( pr1
              ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( pr1 y)
                ( inv (pr2 y))))) 
          ap
            inr
            ( eq-pair-Σ
              ( pr2
                ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                  ( pr1 y)
                  ( inv (pr2 y))))
              ( eq-is-prop (is-set-Fin 2 _ _))))

    map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
      binary-coproduct-Decomposition l1 l1 X
    pr1 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) =
      fib f (inl (inr star))
    pr1 (pr2 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)) =
      fib f (inr star)
    pr2 (pr2 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)) =
      matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ

  map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    ( left-summand-binary-coproduct-Decomposition d +
      right-summand-binary-coproduct-Decomposition d) 
    Fin 2
  map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    d (inl _) =
    inl (inr star)
  map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    d (inr _) =
    inr star

  map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    X  Fin 2
  map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d x =
    map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
      ( d)
      ( map-equiv
        ( matching-correspondence-binary-coproduct-Decomposition d)
        ( x))

  compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    (t :
      ( left-summand-binary-coproduct-Decomposition d) +
      ( right-summand-binary-coproduct-Decomposition d)) 
    ( inl (inr star) 
      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
        ( d)
        ( t)) 
    Σ ( left-summand-binary-coproduct-Decomposition d)
      ( λ a  inl a  t)
  compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    d (inl y) x =
    y , refl

  compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    (x : X) 
    ( inl (inr star) 
      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d x) 
    Σ ( left-summand-binary-coproduct-Decomposition d)
      ( λ a 
        inl a 
        map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x)
  compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d x p =
    compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
      ( d)
      ( map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x)
      ( p)

  compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    (t :
      ( left-summand-binary-coproduct-Decomposition d) +
      ( right-summand-binary-coproduct-Decomposition d)) 
    ( inr star 
      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
        ( d)
        ( t)) 
    Σ ( right-summand-binary-coproduct-Decomposition d)
      ( λ a  inr a  t)
  compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    d (inr y) x =
    y , refl

  compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    (x : X) 
    ( inr star 
      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d x) 
    Σ ( right-summand-binary-coproduct-Decomposition d)
      ( λ a 
        inr a 
        map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x)
  compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d x p =
    compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
      ( d)
      ( map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x)
      ( p)

  isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper :
    (f : X  Fin 2) 
    (x : X) 
    (v : (inl (inr star)  f x) + (inr star  f x)) 
    ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
        ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f) x 
      f x)
  isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    f x (inl y) =
    ( inv
      ( ap
          ( λ p 
            map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
              ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f)
              ( p))
          ( pr2
            ( pr1
              ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                f
                x
                y)))) 
      y)
  isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    f x (inr y) =
    ( inv
      ( ap
          ( λ p 
            map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
              ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f)
              ( p))
          ( pr2
            ( pr1
              ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                f
                x
                y)))) 
      y)

  isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ 
      map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) ~
    id
  isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f =
    eq-htpy
      ( λ x 
        isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
          ( f)
          ( x)
          ( map-coprod
            ( map-left-unit-law-Σ-is-contr is-contr-Fin-one-ℕ ( inr star))
            ( map-left-unit-law-Σ-is-contr is-contr-unit star)
            ( map-right-distributive-Σ-coprod
              ( Fin 1)
              ( unit)
              ( λ y  y  f x)
              ( f x , refl))))

  equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    left-summand-binary-coproduct-Decomposition
      ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
        ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d)) 
    left-summand-binary-coproduct-Decomposition d
  equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d =
    ( ( right-unit-law-coprod
          ( left-summand-binary-coproduct-Decomposition d)) ∘e
      ( ( equiv-coprod
          ( right-unit-law-Σ-is-contr  _  is-contr-unit) ∘e
            equiv-tot
              ( λ _  extensionality-Fin 2 (inl (inr star)) (inl (inr star))))
          ( right-absorption-Σ
              (right-summand-binary-coproduct-Decomposition d) ∘e
            equiv-tot
              ( λ _  extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e
        ( ( right-distributive-Σ-coprod
            ( left-summand-binary-coproduct-Decomposition d)
            ( right-summand-binary-coproduct-Decomposition d)
            ( λ y 
              map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
                d y  inl (inr star))) ∘e
          ( equiv-Σ-equiv-base
            ( λ y 
              map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
                d y  inl (inr star))
            ( matching-correspondence-binary-coproduct-Decomposition d)))))

  equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    (d : binary-coproduct-Decomposition l1 l1 X) 
    right-summand-binary-coproduct-Decomposition
      ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
        ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d)) 
    right-summand-binary-coproduct-Decomposition d
  equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d =
   ( ( left-unit-law-coprod
        ( right-summand-binary-coproduct-Decomposition d)) ∘e
      ( ( equiv-coprod
          ( right-absorption-Σ
              ( left-summand-binary-coproduct-Decomposition d) ∘e
            equiv-tot
              ( λ _  extensionality-Fin 2 (inl (inr star)) (inr star)))
          ( right-unit-law-Σ-is-contr  _  is-contr-unit) ∘e
            equiv-tot
              ( λ _  extensionality-Fin 2 (inr star) (inr star)))) ∘e
        ( ( right-distributive-Σ-coprod
            ( left-summand-binary-coproduct-Decomposition d)
            ( right-summand-binary-coproduct-Decomposition d)
            ( λ y 
              map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
                d y  inr star)) ∘e
          ( equiv-Σ-equiv-base
            ( λ y 
              ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
                d y) 
              ( inr star))
            ( matching-correspondence-binary-coproduct-Decomposition d)))))

  compute-equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    ( d : binary-coproduct-Decomposition l1 l1 X) 
    ( inl 
      ( map-equiv
        ( equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          ( d)))) ~
    ( ( map-equiv
        ( matching-correspondence-binary-coproduct-Decomposition d))  pr1)
  compute-equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d (x , p) =
    ap
      ( λ x 
        inl
        ( map-equiv
            ( ( right-unit-law-coprod
                ( left-summand-binary-coproduct-Decomposition d)) ∘e
              ( ( equiv-coprod
                  ( right-unit-law-Σ-is-contr  _  is-contr-unit) ∘e
                    equiv-tot
                      ( λ _ 
                        extensionality-Fin 2 (inl (inr star)) (inl (inr star))))
                  ( right-absorption-Σ
                      (right-summand-binary-coproduct-Decomposition d) ∘e
                    equiv-tot
                      ( λ _ 
                        extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e
                ( ( right-distributive-Σ-coprod
                    ( left-summand-binary-coproduct-Decomposition d)
                    ( right-summand-binary-coproduct-Decomposition d)
                    ( λ y 
                      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
                        d y 
                      inl (inr star))))))
            ( x)))
      ( eq-pair-Σ
        {t =
          pair
            ( inl
              ( pr1
                ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                    d x (inv p))))
            ( refl)}
          ( inv
            ( pr2
              ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d)
                ( x)
                ( inv p))))
          ( eq-is-prop
            ( is-set-Fin 2 _ _))) 
    ( pr2
        ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          ( d)
          ( x)
          ( inv p)))

  compute-equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    ( d : binary-coproduct-Decomposition l1 l1 X) 
    ( inr 
      ( map-equiv
        ( equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          ( d)))) ~
    ( map-equiv
      ( matching-correspondence-binary-coproduct-Decomposition d)  pr1)
  compute-equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d (x , p) =
    ap
      ( λ x 
        inr
          ( map-equiv
            ( ( left-unit-law-coprod
                ( right-summand-binary-coproduct-Decomposition d)) ∘e
              ( ( equiv-coprod
                  ( right-absorption-Σ
                      ( left-summand-binary-coproduct-Decomposition d) ∘e
                    equiv-tot
                      ( λ _ 
                        extensionality-Fin 2 (inl (inr star)) (inr star)))
                  ( right-unit-law-Σ-is-contr  _  is-contr-unit) ∘e
                    equiv-tot
                      ( λ _  extensionality-Fin 2 (inr star) (inr star)))) ∘e
                ( ( right-distributive-Σ-coprod
                    ( left-summand-binary-coproduct-Decomposition d)
                    ( right-summand-binary-coproduct-Decomposition d)
                    ( λ y 
                      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
                        d y  inr star)))))
           ( x)))
      ( eq-pair-Σ
        {t =
          ( inr
             ( pr1
               ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                 ( d)
                 ( x)
                 ( inv p))),
            refl)}
          ( inv
            ( pr2
              ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d)
                ( x)
                ( inv p))))
          ( eq-is-prop
            ( is-set-Fin 2 _ _))) 
    ( pr2
        ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          ( d)
          ( x)
          ( inv p)))

  matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper :
    ( d : binary-coproduct-Decomposition l1 l1 X) 
    ( x : X) 
    ( ( inl (inr star) 
        ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          ( d)
          ( x))) +
      ( inr star 
        ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          ( d)
          ( x)))) 
    ( map-coprod
        ( map-equiv
          ( equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d)))
        ( map-equiv
          ( equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d))) 
      map-equiv
        ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          (map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d)))
      ( x) 
    map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x
  matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    d x (inl p) =
    ap
      ( map-coprod
        ( map-equiv
          ( equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d)))
        ( map-equiv
          ( equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d))))
      ( inv
        ( pr2
          ( pr1
            ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
              ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d))
              ( x)
              ( p))))) 
    ( compute-equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
      ( d)
      ( pr1
         ( pr1
           ( pr1
             ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
               ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                  ( d))
               ( x)
               ( p)))) ,
        pr2
          ( pr1
            ( pr1
              ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                  ( d))
                ( x)
                ( p))))) 
      ap
        ( map-equiv
          ( matching-correspondence-binary-coproduct-Decomposition d))
        ( pr2
            ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
              ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d))
              ( x)
              ( p))))
  matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
    d x (inr p) =
    ap
      ( map-coprod
        ( map-equiv
          ( equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d)))
        ( map-equiv
          ( equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d))))
      ( inv
        ( pr2
          ( pr1
            ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
              ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d))
              ( x)
              ( p))))) 
    ( compute-equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
      ( d)
      ( pr1
        ( pr1
          ( pr1
            ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
              ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d))
              ( x)
              ( p)))) ,
        pr2
          ( pr1
            ( pr1
              ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                  ( d))
                ( x)
                ( p))))) 
      ap
        ( map-equiv
          ( matching-correspondence-binary-coproduct-Decomposition d))
        ( pr2
            ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
              ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                ( d))
              ( x)
              ( p))))

  value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper :
    (y : Fin 2)  (inl (inr star)  y) + (inr star  y)
  value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper (inl x) =
    inl (ap inl (eq-is-contr is-contr-Fin-one-ℕ))
  value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper (inr x) =
    inr (ap inr (eq-is-contr is-contr-unit))

  value-map-into-Fin-Two-ℕ-eq-zero-or-one :
    (f : X  Fin 2) 
    (x : X) 
    (inl (inr star)  f x) + (inr star  f x)
  value-map-into-Fin-Two-ℕ-eq-zero-or-one f x =
    value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper (f x)

  matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    ( d : binary-coproduct-Decomposition l1 l1 X) 
    ( map-coprod
        ( map-equiv
          ( equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d)))
        ( map-equiv
          ( equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d))) 
      map-equiv
        ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
          (map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
            ( d)))) ~
    map-equiv (matching-correspondence-binary-coproduct-Decomposition d)
  matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
    d x =
    matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper
      ( d)
      ( x)
      ( value-map-into-Fin-Two-ℕ-eq-zero-or-one
        ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d)
        ( x))

  issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ 
      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) ~
    id
  issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d =
    eq-equiv-binary-coproduct-Decomposition
      ( ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ 
          map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
        ( d))
      ( d)
      ( equiv-left-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
        ( d) ,
        equiv-right-summand-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
        ( d) ,
        matching-correspondence-htpy-issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
        ( d))

  is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    is-equiv map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
  is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ =
    is-equiv-has-inverse
      map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
      ( issec-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)
      ( isretr-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)

  equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ :
    (X  Fin 2)  binary-coproduct-Decomposition l1 l1 X
  pr1 equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ =
    map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
  pr2 equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ =
    is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ