The dependent binomial theorem for types (Distributivity of dependent function types over coproduct types)

module foundation.dependent-binomial-theorem where
Imports
open import foundation.contractible-types
open import foundation.coproduct-decompositions
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.identity-types
open import foundation.raising-universe-levels
open import foundation.type-theoretic-principle-of-choice
open import foundation.universal-property-coproduct-types
open import foundation.universal-property-dependent-pair-types

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.univalence
open import foundation-core.universe-levels

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

Idea

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  fam-coprod :
    Fin 2  UU (l1  l2)
  fam-coprod (inl (inr star)) = raise l2 A
  fam-coprod (inr star) = raise l1 B

  map-compute-total-fam-coprod :
    Σ (Fin 2) fam-coprod  A + B
  map-compute-total-fam-coprod (pair (inl (inr star)) y) = inl (map-inv-raise y)
  map-compute-total-fam-coprod (pair (inr star) y) = inr (map-inv-raise y)

  map-inv-compute-total-fam-coprod :
    A + B  Σ (Fin 2) fam-coprod
  pr1 (map-inv-compute-total-fam-coprod (inl x)) = zero-Fin 1
  pr2 (map-inv-compute-total-fam-coprod (inl x)) = map-raise x
  pr1 (map-inv-compute-total-fam-coprod (inr x)) = one-Fin 1
  pr2 (map-inv-compute-total-fam-coprod (inr x)) = map-raise x

  issec-map-inv-compute-total-fam-coprod :
    (map-compute-total-fam-coprod  map-inv-compute-total-fam-coprod) ~ id
  issec-map-inv-compute-total-fam-coprod (inl x) =
    ap inl (isretr-map-inv-raise {l2} x)
  issec-map-inv-compute-total-fam-coprod (inr x) =
    ap inr (isretr-map-inv-raise {l1} x)

  isretr-map-inv-compute-total-fam-coprod :
    (map-inv-compute-total-fam-coprod  map-compute-total-fam-coprod) ~ id
  isretr-map-inv-compute-total-fam-coprod (pair (inl (inr star)) y) =
    ap (pair (zero-Fin 1)) (issec-map-inv-raise y)
  isretr-map-inv-compute-total-fam-coprod (pair (inr star) y) =
    ap (pair (one-Fin 1)) (issec-map-inv-raise y)

  is-equiv-map-compute-total-fam-coprod :
    is-equiv map-compute-total-fam-coprod
  is-equiv-map-compute-total-fam-coprod =
    is-equiv-has-inverse
      map-inv-compute-total-fam-coprod
      issec-map-inv-compute-total-fam-coprod
      isretr-map-inv-compute-total-fam-coprod

  compute-total-fam-coprod :
    (Σ (Fin 2) fam-coprod)  (A + B)
  pr1 compute-total-fam-coprod = map-compute-total-fam-coprod
  pr2 compute-total-fam-coprod = is-equiv-map-compute-total-fam-coprod

  inv-compute-total-fam-coprod :
    (A + B)  Σ (Fin 2) fam-coprod
  inv-compute-total-fam-coprod =
    inv-equiv compute-total-fam-coprod

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : X  UU l2} {B : X  UU l3}
  where

  type-distributive-Π-coprod : UU (l1  l2  l3)
  type-distributive-Π-coprod =
    Σ ( X  Fin 2)
      ( λ f  ((x : X) (p : is-zero-Fin 2 (f x))  A x) ×
              ((x : X) (p : is-one-Fin 2 (f x))  B x))

  distributive-Π-coprod :
    ((x : X)  A x + B x)  type-distributive-Π-coprod
  distributive-Π-coprod =
    ( ( equiv-tot
        ( λ f 
          ( ( equiv-prod
              ( equiv-map-Π
                ( λ x 
                  equiv-map-Π
                    ( λ p 
                      ( inv-equiv (compute-raise l3 (A x))) ∘e
                      ( equiv-tr (fam-coprod (A x) (B x)) p))))
              ( equiv-map-Π
                ( λ x 
                  equiv-map-Π
                    ( λ p 
                      ( inv-equiv (compute-raise l2 (B x))) ∘e
                      ( equiv-tr (fam-coprod (A x) (B x)) p))))) ∘e
            ( distributive-Π-Σ)) ∘e
          ( equiv-map-Π
            ( λ x 
              ( equiv-universal-property-coprod
                ( fam-coprod (A x) (B x) (f x))) ∘e
              ( equiv-diagonal-is-contr
                ( fam-coprod (A x) (B x) (f x))
                ( is-contr-is-zero-or-one-Fin-two-ℕ (f x))))))) ∘e
      ( distributive-Π-Σ)) ∘e
    ( equiv-map-Π
      ( λ x  inv-compute-total-fam-coprod (A x) (B x)))

  type-distributive-Π-coprod-binary-coproduct-Decomposition :
    UU (l1  l2  l3  lsuc l1  lsuc l1)
  type-distributive-Π-coprod-binary-coproduct-Decomposition =
    Σ ( binary-coproduct-Decomposition l1 l1 X)
      ( λ d 
        ( ( (u : left-summand-binary-coproduct-Decomposition d) 
            ( A
              ( map-inv-equiv
                ( matching-correspondence-binary-coproduct-Decomposition d)
                ( inl u)))) ×
          ( ( v : right-summand-binary-coproduct-Decomposition d) 
            ( B
              ( map-inv-equiv
                ( matching-correspondence-binary-coproduct-Decomposition d)
                ( inr v))))))

  equiv-type-distributive-Π-coprod-binary-coproduct-Decomposition :
    type-distributive-Π-coprod 
    type-distributive-Π-coprod-binary-coproduct-Decomposition
  equiv-type-distributive-Π-coprod-binary-coproduct-Decomposition =
    equiv-Σ
    ( λ d 
      ( (u : left-summand-binary-coproduct-Decomposition d) 
        A
          ( map-inv-equiv
            ( matching-correspondence-binary-coproduct-Decomposition d)
            ( inl u))) ×
      ( (v : right-summand-binary-coproduct-Decomposition d) 
        B
          ( map-inv-equiv
            ( matching-correspondence-binary-coproduct-Decomposition d)
            ( inr v))))
      ( equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ X)
      ( λ f 
        equiv-prod
          ( equiv-Π
              ( λ z 
                  A
                  ( map-inv-equiv
                    ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                      ( X)
                      ( f))
                    ( inl z)))
              ( id-equiv)
              ( λ a 
                equiv-eq
                  ( ap
                      ( A)
                      ( compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ
                        ( X)
                        ( f)
                        ( a)))) ∘e
            inv-equiv equiv-ev-pair)
          ( equiv-Π
              ( λ z 
                  B
                  ( map-inv-equiv
                    ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                      X f)
                    ( inr z)))
              ( id-equiv)
              ( λ a 
                equiv-eq
                  ( ap
                      ( B)
                      ( compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ
                        ( X)
                        ( f)
                        ( a)))) ∘e
            inv-equiv equiv-ev-pair))

  distributive-Π-coprod-binary-coproduct-Decomposition :
    ((x : X)  A x + B x) 
    type-distributive-Π-coprod-binary-coproduct-Decomposition
  distributive-Π-coprod-binary-coproduct-Decomposition =
    equiv-type-distributive-Π-coprod-binary-coproduct-Decomposition ∘e
    distributive-Π-coprod