Coproduct decompositions in a subuniverse

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

Created on 2023-04-08.

module foundation.coproduct-decompositions-subuniverse where

Imports
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.functoriality-coproduct-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.structure-identity-principle
open import foundation.subuniverses
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-empty-type
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equality-dependent-pair-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.propositions
open import foundation-core.torsorial-type-families


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-coproduct (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-coproduct
( 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-torsorial-equiv-binary-coproduct-Decomposition-subuniverse :
is-torsorial (equiv-binary-coproduct-Decomposition-subuniverse P A X)
is-torsorial-equiv-binary-coproduct-Decomposition-subuniverse =
is-torsorial-Eq-structure
( is-torsorial-equiv-subuniverse P
( left-summand-binary-coproduct-Decomposition-subuniverse P A X))
( left-summand-binary-coproduct-Decomposition-subuniverse P A X ,
id-equiv)
( is-torsorial-Eq-structure
( is-torsorial-equiv-subuniverse P
( right-summand-binary-coproduct-Decomposition-subuniverse P A X))
( right-summand-binary-coproduct-Decomposition-subuniverse P A X ,
id-equiv)
( is-torsorial-htpy-equiv
( equiv-coproduct 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-torsorial-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-product)
( λ x →
equiv-postcomp-equiv
( commutative-coproduct
( 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-is-invertible
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-coproduct _ _)
( inclusion-subuniverse P X)) ∘e
( ( left-unit-law-Σ-is-contr
( is-torsorial-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-is-invertible
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-torsorial-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-coproduct-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 (equiv-is-empty is-empty-raise-empty (pr2 x)))
( eq-is-prop (is-prop-type-Prop (P _))))
( eq-is-prop is-property-is-empty)))
( ( raise-empty l1 , C1) , is-empty-raise-empty)) ∘e
( ( inv-associative-Σ _ _ _) ∘e
( ( equiv-tot (λ _ → commutative-product)) ∘e
( ( associative-Σ _ _ _))))))) ∘e
( ( associative-Σ _ _ _))