# Arithmetic law for product decomposition and Π-decomposition

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-05-25.

module foundation.arithmetic-law-product-and-pi-decompositions where

Imports
open import foundation.coproduct-decompositions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-cartesian-product-types
open import foundation.pi-decompositions
open import foundation.product-decompositions
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universal-property-coproduct-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.transport-along-identifications


## Idea

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

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


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

## Propositions

### Product decompositions of the indexing type of a Π-decomposition are equivalent to Π-decomposition of the left and right summand of a product decomposition

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

private
reassociate :
Σ (Π-Decomposition l l X)
( λ d → binary-coproduct-Decomposition l l
( indexing-type-Π-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-is-invertible
( λ (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-product-Decomposition l l X)
( λ d →
Π-Decomposition l l
( left-summand-binary-product-Decomposition d) ×
Π-Decomposition l l
( right-summand-binary-product-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-is-invertible
( λ ((A' , B' , e) , ((A , YA , eA) , B , YB , eB)) →
(A , B , (YA , YB) , (A' , eA) , (B' , eB) , e))
( refl-htpy)
( refl-htpy)

equiv-binary-product-Decomposition-Π-Decomposition :
Σ ( Π-Decomposition l l X)
( λ d →
binary-coproduct-Decomposition l l (indexing-type-Π-Decomposition d)) ≃
Σ ( binary-product-Decomposition l l X)
( λ d →
Π-Decomposition l l
( left-summand-binary-product-Decomposition d) ×
Π-Decomposition l l
( right-summand-binary-product-Decomposition d))

equiv-binary-product-Decomposition-Π-Decomposition =
( ( reassociate') ∘e
( ( equiv-tot
( λ A →
equiv-tot
( λ B →
( ( equiv-tot
( λ ( YA , YB) →
( ( equiv-tot
( λ A' →
equiv-tot
( λ B' →
equiv-postcomp-equiv
( equiv-product
( inv-equiv (pr2 A'))
( inv-equiv (pr2 B')))
( X))) ∘e
( ( inv-left-unit-law-Σ-is-contr
( is-torsorial-equiv' (Π A YA))
( Π A YA , id-equiv)) ∘e
( inv-left-unit-law-Σ-is-contr
( is-torsorial-equiv' (Π B YB))
( Π B YB , id-equiv)))))) ∘e
( ( equiv-Σ-equiv-base
( λ z → X ≃ (Π A (pr1 z) × Π B (pr2 z)))
( equiv-universal-property-coproduct (UU l))) ∘e
( ( equiv-tot
( λ Y →
equiv-postcomp-equiv
( equiv-dependent-universal-property-coproduct
( Y))
( X))) ∘e
( left-unit-law-Σ-is-contr
( is-torsorial-equiv' (A + B))
((A + B) , id-equiv))))))))) ∘e
( reassociate)))

module _
( D : Σ ( Π-Decomposition l l X)
( λ D →
binary-coproduct-Decomposition
l l
( indexing-type-Π-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-product-Decomposition-Π-Decomposition :
( a : left-summand-binary-coproduct-Decomposition (pr2 D)) →
cotype-Π-Decomposition
( pr1
( pr2
( map-equiv equiv-binary-product-Decomposition-Π-Decomposition
( D))))
( a) ＝
cotype-Π-Decomposition
( pr1 D)
( map-inv-equiv
( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
( inl a))
compute-left-equiv-binary-product-Decomposition-Π-Decomposition a =
tr-total-equiv
( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
( inv
( contraction
( is-torsorial-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
( (pr1 (pr2 D) + pr1 (pr2 (pr2 D))) , id-equiv)) ∙
contraction
( is-torsorial-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
( pr1 (pr1 D) , pr2 (pr2 (pr2 D))))
( inl a)

compute-right-equiv-binary-product-Decomposition-Π-Decomposition :
( b : right-summand-binary-coproduct-Decomposition (pr2 D)) →
cotype-Π-Decomposition
( pr2
( pr2
( map-equiv equiv-binary-product-Decomposition-Π-Decomposition
( D))))
( b) ＝
cotype-Π-Decomposition (pr1 D)
( map-inv-equiv
( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
( inr b))
compute-right-equiv-binary-product-Decomposition-Π-Decomposition b =
tr-total-equiv
( matching-correspondence-binary-coproduct-Decomposition (pr2 D))
( inv
( contraction
( is-torsorial-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
( (pr1 (pr2 D) + pr1 (pr2 (pr2 D))) , id-equiv)) ∙
contraction
( is-torsorial-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D))))
( pr1 (pr1 D) , pr2 (pr2 (pr2 D))))
( inr b)