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)