Coproduct decompositions in a subuniverse
module foundation.coproduct-decompositions-subuniverse where
Imports
open import foundation.coproduct-types open import foundation.empty-types open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.functoriality-coproduct-types open import foundation.structure-identity-principle open import foundation.subuniverses open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-empty-type open import foundation.univalence open import foundation-core.cartesian-product-types open import foundation-core.contractible-types open import foundation-core.dependent-pair-types open import foundation-core.equality-dependent-pair-types 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-cartesian-product-types open import foundation-core.type-arithmetic-dependent-pair-types open import foundation-core.universe-levels
Idea
Let P be a subuniverse and X a type in P. A binary coproduct decomposition
of X is defined to be two types A and B in P and an equivalence from X
to A+B.
Definitions
Binary coproduct decomposition
module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) where binary-coproduct-Decomposition-subuniverse : UU (lsuc l1 ⊔ l2) binary-coproduct-Decomposition-subuniverse = Σ ( type-subuniverse P) ( λ k1 → Σ ( type-subuniverse P) ( λ k2 → ( inclusion-subuniverse P X) ≃ ( inclusion-subuniverse P k1 + inclusion-subuniverse P k2))) module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) (d : binary-coproduct-Decomposition-subuniverse P X) where left-summand-binary-coproduct-Decomposition-subuniverse : type-subuniverse P left-summand-binary-coproduct-Decomposition-subuniverse = pr1 d type-left-summand-binary-coproduct-Decomposition-subuniverse : UU l1 type-left-summand-binary-coproduct-Decomposition-subuniverse = inclusion-subuniverse P left-summand-binary-coproduct-Decomposition-subuniverse right-summand-binary-coproduct-Decomposition-subuniverse : type-subuniverse P right-summand-binary-coproduct-Decomposition-subuniverse = pr1 (pr2 d) type-right-summand-binary-coproduct-Decomposition-subuniverse : UU l1 type-right-summand-binary-coproduct-Decomposition-subuniverse = inclusion-subuniverse P right-summand-binary-coproduct-Decomposition-subuniverse matching-correspondence-binary-coproduct-Decomposition-subuniverse : inclusion-subuniverse P X ≃ ( type-left-summand-binary-coproduct-Decomposition-subuniverse + type-right-summand-binary-coproduct-Decomposition-subuniverse) matching-correspondence-binary-coproduct-Decomposition-subuniverse = pr2 (pr2 d)
Iterated binary coproduct decompositions
module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) where left-iterated-binary-coproduct-Decomposition-subuniverse : UU (lsuc l1 ⊔ l2) left-iterated-binary-coproduct-Decomposition-subuniverse = Σ ( binary-coproduct-Decomposition-subuniverse P X) ( λ d → binary-coproduct-Decomposition-subuniverse P ( left-summand-binary-coproduct-Decomposition-subuniverse P X d)) right-iterated-binary-coproduct-Decomposition-subuniverse : UU (lsuc l1 ⊔ l2) right-iterated-binary-coproduct-Decomposition-subuniverse = Σ ( binary-coproduct-Decomposition-subuniverse P X) ( λ d → binary-coproduct-Decomposition-subuniverse P ( right-summand-binary-coproduct-Decomposition-subuniverse P X d))
Ternary coproduct Decomposition-subuniverses
module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) where ternary-coproduct-Decomposition-subuniverse : UU (lsuc l1 ⊔ l2) ternary-coproduct-Decomposition-subuniverse = Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → inclusion-subuniverse P X ≃ ( inclusion-subuniverse P (pr1 x) + ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) module _ (d : ternary-coproduct-Decomposition-subuniverse) where types-ternary-coproduct-Decomposition-subuniverse : type-subuniverse P × (type-subuniverse P × type-subuniverse P) types-ternary-coproduct-Decomposition-subuniverse = pr1 d first-summand-ternary-coproduct-Decomposition-subuniverse : type-subuniverse P first-summand-ternary-coproduct-Decomposition-subuniverse = ( pr1 types-ternary-coproduct-Decomposition-subuniverse) second-summand-ternary-coproduct-Decomposition-subuniverse : type-subuniverse P second-summand-ternary-coproduct-Decomposition-subuniverse = ( pr1 (pr2 types-ternary-coproduct-Decomposition-subuniverse)) third-summand-ternary-coproduct-Decomposition-subuniverse : type-subuniverse P third-summand-ternary-coproduct-Decomposition-subuniverse = ( pr2 (pr2 types-ternary-coproduct-Decomposition-subuniverse)) matching-correspondence-ternary-coproductuct-Decomposition-subuniverse : ( inclusion-subuniverse P X) ≃ ( ( inclusion-subuniverse P first-summand-ternary-coproduct-Decomposition-subuniverse) + ( ( inclusion-subuniverse P second-summand-ternary-coproduct-Decomposition-subuniverse) + ( inclusion-subuniverse P third-summand-ternary-coproduct-Decomposition-subuniverse))) matching-correspondence-ternary-coproductuct-Decomposition-subuniverse = pr2 d
Propositions
Characterization of equality of binary coproduct Decomposition of subuniverse
equiv-binary-coproduct-Decomposition-subuniverse : {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) (X : binary-coproduct-Decomposition-subuniverse P A) (Y : binary-coproduct-Decomposition-subuniverse P A) → UU (l1) equiv-binary-coproduct-Decomposition-subuniverse P A X Y = Σ ( type-left-summand-binary-coproduct-Decomposition-subuniverse P A X ≃ type-left-summand-binary-coproduct-Decomposition-subuniverse P A Y) ( λ el → Σ ( type-right-summand-binary-coproduct-Decomposition-subuniverse P A X ≃ type-right-summand-binary-coproduct-Decomposition-subuniverse P A Y) ( λ er → ( map-coprod (map-equiv el) (map-equiv er) ∘ map-equiv ( matching-correspondence-binary-coproduct-Decomposition-subuniverse P A X)) ~ ( map-equiv ( matching-correspondence-binary-coproduct-Decomposition-subuniverse P A Y)))) module _ {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) (X : binary-coproduct-Decomposition-subuniverse P A) (Y : binary-coproduct-Decomposition-subuniverse P A) (e : equiv-binary-coproduct-Decomposition-subuniverse P A X Y) where equiv-left-summand-equiv-binary-coproduct-Decomposition-subuniverse : type-left-summand-binary-coproduct-Decomposition-subuniverse P A X ≃ type-left-summand-binary-coproduct-Decomposition-subuniverse P A Y equiv-left-summand-equiv-binary-coproduct-Decomposition-subuniverse = pr1 e map-equiv-left-summand-equiv-binary-coproduct-Decomposition-subuniverse : type-left-summand-binary-coproduct-Decomposition-subuniverse P A X → type-left-summand-binary-coproduct-Decomposition-subuniverse P A Y map-equiv-left-summand-equiv-binary-coproduct-Decomposition-subuniverse = map-equiv equiv-left-summand-equiv-binary-coproduct-Decomposition-subuniverse equiv-right-summand-equiv-binary-coproduct-Decomposition-subuniverse : type-right-summand-binary-coproduct-Decomposition-subuniverse P A X ≃ type-right-summand-binary-coproduct-Decomposition-subuniverse P A Y equiv-right-summand-equiv-binary-coproduct-Decomposition-subuniverse = pr1 (pr2 e) map-equiv-right-summand-equiv-binary-coproduct-Decomposition-subuniverse : type-right-summand-binary-coproduct-Decomposition-subuniverse P A X → type-right-summand-binary-coproduct-Decomposition-subuniverse P A Y map-equiv-right-summand-equiv-binary-coproduct-Decomposition-subuniverse = map-equiv equiv-right-summand-equiv-binary-coproduct-Decomposition-subuniverse module _ {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) (X : binary-coproduct-Decomposition-subuniverse P A) where id-equiv-binary-coproduct-Decomposition-subuniverse : equiv-binary-coproduct-Decomposition-subuniverse P A X X pr1 id-equiv-binary-coproduct-Decomposition-subuniverse = id-equiv pr1 (pr2 id-equiv-binary-coproduct-Decomposition-subuniverse) = id-equiv pr2 (pr2 id-equiv-binary-coproduct-Decomposition-subuniverse) x = id-map-coprod ( type-left-summand-binary-coproduct-Decomposition-subuniverse P A X) ( type-right-summand-binary-coproduct-Decomposition-subuniverse P A X) ( map-equiv ( matching-correspondence-binary-coproduct-Decomposition-subuniverse P A X) ( x)) is-contr-total-equiv-binary-coproduct-Decomposition-subuniverse : is-contr ( Σ ( binary-coproduct-Decomposition-subuniverse P A) ( equiv-binary-coproduct-Decomposition-subuniverse P A X)) is-contr-total-equiv-binary-coproduct-Decomposition-subuniverse = is-contr-total-Eq-structure ( _) ( is-contr-total-equiv-subuniverse P ( left-summand-binary-coproduct-Decomposition-subuniverse P A X)) ( left-summand-binary-coproduct-Decomposition-subuniverse P A X , id-equiv) ( is-contr-total-Eq-structure ( _) ( is-contr-total-equiv-subuniverse P ( right-summand-binary-coproduct-Decomposition-subuniverse P A X)) ( right-summand-binary-coproduct-Decomposition-subuniverse P A X , id-equiv) ( is-contr-total-htpy-equiv ( equiv-coprod id-equiv id-equiv ∘e matching-correspondence-binary-coproduct-Decomposition-subuniverse P A X))) equiv-eq-binary-coproduct-Decomposition-subuniverse : (Y : binary-coproduct-Decomposition-subuniverse P A) → (X ＝ Y) → equiv-binary-coproduct-Decomposition-subuniverse P A X Y equiv-eq-binary-coproduct-Decomposition-subuniverse .X refl = id-equiv-binary-coproduct-Decomposition-subuniverse is-equiv-equiv-eq-binary-coproduct-Decomposition-subuniverse : (Y : binary-coproduct-Decomposition-subuniverse P A) → is-equiv (equiv-eq-binary-coproduct-Decomposition-subuniverse Y) is-equiv-equiv-eq-binary-coproduct-Decomposition-subuniverse = fundamental-theorem-id is-contr-total-equiv-binary-coproduct-Decomposition-subuniverse equiv-eq-binary-coproduct-Decomposition-subuniverse extensionality-binary-coproduct-Decomposition-subuniverse : (Y : binary-coproduct-Decomposition-subuniverse P A) → (X ＝ Y) ≃ equiv-binary-coproduct-Decomposition-subuniverse P A X Y pr1 (extensionality-binary-coproduct-Decomposition-subuniverse Y) = equiv-eq-binary-coproduct-Decomposition-subuniverse Y pr2 (extensionality-binary-coproduct-Decomposition-subuniverse Y) = is-equiv-equiv-eq-binary-coproduct-Decomposition-subuniverse Y eq-equiv-binary-coproduct-Decomposition-subuniverse : (Y : binary-coproduct-Decomposition-subuniverse P A) → equiv-binary-coproduct-Decomposition-subuniverse P A X Y → (X ＝ Y) eq-equiv-binary-coproduct-Decomposition-subuniverse Y = map-inv-equiv (extensionality-binary-coproduct-Decomposition-subuniverse Y)
Equivalence between binary coproduct Decomposition-subuniverse induce by commutativiy of coproduct
module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) where equiv-commutative-binary-coproduct-Decomposition-subuniverse : binary-coproduct-Decomposition-subuniverse P X ≃ binary-coproduct-Decomposition-subuniverse P X equiv-commutative-binary-coproduct-Decomposition-subuniverse = ( associative-Σ ( type-subuniverse P) ( λ _ → type-subuniverse P) ( _)) ∘e ( ( equiv-Σ ( _) ( commutative-prod) ( λ x → equiv-postcomp-equiv ( commutative-coprod ( inclusion-subuniverse P (pr1 x)) ( inclusion-subuniverse P (pr2 x))) (inclusion-subuniverse P X))) ∘e ( ( inv-associative-Σ ( type-subuniverse P) ( λ _ → type-subuniverse P) ( _))))
Equivalence between iterated coproduct and ternary coproduct decomposition
module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) (C1 : is-closed-under-coproducts-subuniverse P) where private map-reassociate-left-iterated-coproduct-Decomposition-subuniverse : left-iterated-binary-coproduct-Decomposition-subuniverse P X → Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → Σ ( Σ ( type-subuniverse P) ( λ A → ( inclusion-subuniverse P A) ≃ ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) ( λ A → ( inclusion-subuniverse P X) ≃ ( inclusion-subuniverse P (pr1 A) + inclusion-subuniverse P (pr1 x)))) map-reassociate-left-iterated-coproduct-Decomposition-subuniverse ( (A , B , e) , C , D , f) = ( (B , C , D) , (A , f) , e) map-inv-reassociate-left-iterated-coproduct-Decomposition-subuniverse : Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → Σ ( Σ ( type-subuniverse P) ( λ A → inclusion-subuniverse P A ≃ ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) ( λ A → inclusion-subuniverse P X ≃ ( inclusion-subuniverse P (pr1 A) + inclusion-subuniverse P (pr1 x)))) → left-iterated-binary-coproduct-Decomposition-subuniverse P X map-inv-reassociate-left-iterated-coproduct-Decomposition-subuniverse ( (B , C , D) , (A , f) , e) = ( (A , B , e) , C , D , f) equiv-reassociate-left-iterated-coproduct-Decomposition-subuniverse : left-iterated-binary-coproduct-Decomposition-subuniverse P X ≃ Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → Σ ( Σ ( type-subuniverse P) ( λ A → inclusion-subuniverse P A ≃ ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) ( λ A → inclusion-subuniverse P X ≃ ( inclusion-subuniverse P (pr1 A) + inclusion-subuniverse P (pr1 x)))) pr1 equiv-reassociate-left-iterated-coproduct-Decomposition-subuniverse = map-reassociate-left-iterated-coproduct-Decomposition-subuniverse pr2 equiv-reassociate-left-iterated-coproduct-Decomposition-subuniverse = is-equiv-has-inverse map-inv-reassociate-left-iterated-coproduct-Decomposition-subuniverse refl-htpy refl-htpy equiv-ternary-left-iterated-coproduct-Decomposition-subuniverse : left-iterated-binary-coproduct-Decomposition-subuniverse P X ≃ ternary-coproduct-Decomposition-subuniverse P X equiv-ternary-left-iterated-coproduct-Decomposition-subuniverse = ( equiv-tot ( λ x → ( ( equiv-postcomp-equiv ( commutative-coprod _ _) ( inclusion-subuniverse P X)) ∘e ( ( left-unit-law-Σ-is-contr ( is-contr-total-equiv-subuniverse' P ( ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))) , ( C1 (pr2 (pr1 (pr2 x))) (pr2 (pr2 (pr2 x))))))) ( ( ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))) , ( C1 (pr2 (pr1 (pr2 x))) (pr2 (pr2 (pr2 x))))) , ( id-equiv)))))) ∘e ( equiv-reassociate-left-iterated-coproduct-Decomposition-subuniverse) private map-reassociate-right-iterated-coproduct-Decomposition-subuniverse : right-iterated-binary-coproduct-Decomposition-subuniverse P X → Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → Σ ( Σ ( type-subuniverse P) ( λ B → ( inclusion-subuniverse P B) ≃ ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) ( λ B → ( inclusion-subuniverse P X) ≃ ( inclusion-subuniverse P (pr1 x) + inclusion-subuniverse P (pr1 B)))) map-reassociate-right-iterated-coproduct-Decomposition-subuniverse ( (A , B , e) , C , D , f) = ( (A , C , D) , (B , f) , e) map-inv-reassociate-right-iterated-coproduct-Decomposition-subuniverse : Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → Σ ( Σ ( type-subuniverse P) ( λ B → ( inclusion-subuniverse P B) ≃ ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) ( λ B → ( inclusion-subuniverse P X) ≃ ( inclusion-subuniverse P (pr1 x) + inclusion-subuniverse P (pr1 B)))) → right-iterated-binary-coproduct-Decomposition-subuniverse P X map-inv-reassociate-right-iterated-coproduct-Decomposition-subuniverse ( (A , C , D) , (B , f) , e) = ( (A , B , e) , C , D , f) equiv-reassociate-right-iterated-coproduct-Decomposition-subuniverse : right-iterated-binary-coproduct-Decomposition-subuniverse P X ≃ Σ ( type-subuniverse P × (type-subuniverse P × type-subuniverse P)) ( λ x → Σ ( Σ ( type-subuniverse P) ( λ B → ( inclusion-subuniverse P B) ≃ ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))))) ( λ B → ( inclusion-subuniverse P X) ≃ ( inclusion-subuniverse P (pr1 x) + inclusion-subuniverse P (pr1 B)))) pr1 equiv-reassociate-right-iterated-coproduct-Decomposition-subuniverse = map-reassociate-right-iterated-coproduct-Decomposition-subuniverse pr2 equiv-reassociate-right-iterated-coproduct-Decomposition-subuniverse = is-equiv-has-inverse map-inv-reassociate-right-iterated-coproduct-Decomposition-subuniverse refl-htpy refl-htpy equiv-ternary-right-iterated-coproduct-Decomposition-subuniverse : right-iterated-binary-coproduct-Decomposition-subuniverse P X ≃ ternary-coproduct-Decomposition-subuniverse P X equiv-ternary-right-iterated-coproduct-Decomposition-subuniverse = ( equiv-tot ( λ x → left-unit-law-Σ-is-contr ( is-contr-total-equiv-subuniverse' P ( ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))) , ( C1 (pr2 (pr1 (pr2 x))) (pr2 (pr2 (pr2 x)))))) ( ( ( inclusion-subuniverse P (pr1 (pr2 x)) + inclusion-subuniverse P (pr2 (pr2 x))) , ( C1 (pr2 (pr1 (pr2 x))) (pr2 (pr2 (pr2 x))))) , ( id-equiv)))) ∘e ( equiv-reassociate-right-iterated-coproduct-Decomposition-subuniverse)
Coproduct-decomposition with empty right summand
module _ {l1 l2 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) (C1 : is-in-subuniverse P (raise-empty l1)) where equiv-is-empty-right-summand-binary-coproduct-Decomposition-subuniverse : Σ ( binary-coproduct-Decomposition-subuniverse P X) ( λ d → is-empty ( inclusion-subuniverse P ( right-summand-binary-coproduct-Decomposition-subuniverse P X d))) ≃ Σ ( type-subuniverse P) ( λ Y → inclusion-subuniverse P X ≃ pr1 Y) equiv-is-empty-right-summand-binary-coproduct-Decomposition-subuniverse = ( equiv-tot ( λ x → ( equiv-postcomp-equiv ( right-unit-law-coprod-is-empty ( inclusion-subuniverse P x) ( raise-empty l1) ( is-empty-raise-empty)) ( inclusion-subuniverse P X)) ∘e ( ( left-unit-law-Σ-is-contr ( ( ( raise-empty l1 , C1) , is-empty-raise-empty) , ( λ x → eq-pair-Σ ( eq-pair-Σ ( eq-equiv ( raise-empty l1) ( inclusion-subuniverse P (pr1 x)) ( equiv-is-empty is-empty-raise-empty ( pr2 x))) ( eq-is-prop (is-prop-type-Prop (P _)))) ( eq-is-prop is-prop-is-empty))) ( ( raise-empty l1 , C1) , is-empty-raise-empty)) ∘e ( ( inv-associative-Σ _ _ _) ∘e ( ( equiv-tot (λ _ → commutative-prod)) ∘e ( ( associative-Σ _ _ _))))))) ∘e ( ( associative-Σ _ _ _))