Cauchy composition of species of types
module species.cauchy-composition-species-of-types where
Imports
open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.discrete-relaxed-sigma-decompositions open import foundation.equivalences open import foundation.function-extensionality open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.relaxed-sigma-decompositions open import foundation.trivial-relaxed-sigma-decompositions open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-function-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice open import foundation.univalence open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels open import species.species-of-types open import species.unit-cauchy-composition-species-of-types
Idea
A species of types S : UU l1 → UU l2 can be thought of as the polynomial
endofunctor
X ↦ Σ (A : UU l1) (S A) × (A → X)
Using the formula for composition of analytic endofunctors, we obtain a way to compose species, which is called the Cauchy composition of species.
Definition
Cauchy composition of species
cauchy-composition-species-types : {l1 l2 l3 : Level} → species-types l1 l2 → species-types l1 l3 → species-types l1 (lsuc l1 ⊔ l2 ⊔ l3) cauchy-composition-species-types {l1} {l2} {l3} S T X = Σ ( Relaxed-Σ-Decomposition l1 l1 X) ( λ D → ( S (indexing-type-Relaxed-Σ-Decomposition D)) × ( ( y : indexing-type-Relaxed-Σ-Decomposition D) → T (cotype-Relaxed-Σ-Decomposition D y)))
Properties
Unit laws for Cauchy composition of species
left-unit-law-cauchy-composition-species-types : {l1 l2 : Level} (F : species-types l1 l2) → (A : UU l1) → cauchy-composition-species-types unit-species-types F A ≃ F A left-unit-law-cauchy-composition-species-types {l1} F A = ( left-unit-law-Σ-is-contr ( is-contr-type-trivial-Relaxed-Σ-Decomposition) ( trivial-Relaxed-Σ-Decomposition l1 A , is-trivial-trivial-Relaxed-Σ-Decomposition {l1} {l1} {A})) ∘e ( ( inv-associative-Σ ( Relaxed-Σ-Decomposition l1 l1 A) ( λ D → is-contr (indexing-type-Relaxed-Σ-Decomposition D)) ( λ C → F (cotype-Relaxed-Σ-Decomposition (pr1 C) (center (pr2 C))))) ∘e ( ( equiv-Σ ( _) ( id-equiv) ( λ D → equiv-Σ ( λ z → F (cotype-Relaxed-Σ-Decomposition D (center z))) ( id-equiv) ( λ C → ( left-unit-law-Π-is-contr C (center C))))))) right-unit-law-cauchy-composition-species-types : {l1 l2 : Level} (F : species-types l1 l2) → (A : UU l1) → cauchy-composition-species-types F unit-species-types A ≃ F A right-unit-law-cauchy-composition-species-types {l1} F A = ( left-unit-law-Σ-is-contr ( is-contr-type-discrete-Relaxed-Σ-Decomposition) ( ( discrete-Relaxed-Σ-Decomposition l1 A) , is-discrete-discrete-Relaxed-Σ-Decomposition)) ∘e ( ( inv-associative-Σ ( Relaxed-Σ-Decomposition l1 l1 A) ( λ D → ( y : indexing-type-Relaxed-Σ-Decomposition D) → is-contr (cotype-Relaxed-Σ-Decomposition D y)) ( λ D → F (indexing-type-Relaxed-Σ-Decomposition (pr1 D)))) ∘e ( ( equiv-Σ ( λ D → ( ( y : indexing-type-Relaxed-Σ-Decomposition D) → unit-species-types ( cotype-Relaxed-Σ-Decomposition D y)) × F ( indexing-type-Relaxed-Σ-Decomposition D)) ( id-equiv) ( λ _ → commutative-prod))))
Associativity of composition of species
module _ {l1 l2 l3 l4 : Level} (S : species-types l1 l2) (T : species-types l1 l3) (U : species-types l1 l4) where equiv-associative-cauchy-composition-species-types : (A : UU l1) → cauchy-composition-species-types ( S) ( cauchy-composition-species-types T U) ( A) ≃ cauchy-composition-species-types ( cauchy-composition-species-types S T) ( U) ( A) equiv-associative-cauchy-composition-species-types A = ( equiv-Σ ( _) ( id-equiv) ( λ D1 → ( ( inv-equiv right-distributive-prod-Σ) ∘e ( ( equiv-Σ ( _) ( id-equiv) ( λ D2 → ( inv-associative-Σ ( S (indexing-type-Relaxed-Σ-Decomposition D2)) ( λ _ → ( x : indexing-type-Relaxed-Σ-Decomposition D2) → T ( cotype-Relaxed-Σ-Decomposition D2 x)) _))) ∘e ( ( equiv-Σ ( _) ( id-equiv) ( λ D2 → ( equiv-prod ( id-equiv) ( ( equiv-prod ( id-equiv) ( ( inv-equiv ( equiv-precomp-Π ( inv-equiv ( matching-correspondence-Relaxed-Σ-Decomposition D2)) ( λ x → U ( cotype-Relaxed-Σ-Decomposition D1 x)))) ∘e ( inv-equiv equiv-ev-pair))) ∘e ( distributive-Π-Σ)))))))))) ∘e ( ( associative-Σ ( Relaxed-Σ-Decomposition l1 l1 A) ( λ D → Relaxed-Σ-Decomposition l1 l1 ( indexing-type-Relaxed-Σ-Decomposition D)) ( _)) ∘e ( ( inv-equiv ( equiv-Σ-equiv-base ( _) ( equiv-displayed-fibered-Relaxed-Σ-Decomposition))) ∘e ( ( inv-associative-Σ ( Relaxed-Σ-Decomposition l1 l1 A) ( λ D → ( x : indexing-type-Relaxed-Σ-Decomposition D) → Relaxed-Σ-Decomposition l1 l1 ( cotype-Relaxed-Σ-Decomposition D x)) ( _)) ∘e ( ( equiv-Σ ( _) ( id-equiv) ( λ D → left-distributive-prod-Σ)) ∘e ( ( equiv-Σ ( _) ( id-equiv) ( λ D → equiv-prod id-equiv distributive-Π-Σ))))))) htpy-associative-cauchy-composition-species-types : cauchy-composition-species-types ( S) ( cauchy-composition-species-types T U) ~ cauchy-composition-species-types (cauchy-composition-species-types S T) U htpy-associative-cauchy-composition-species-types A = eq-equiv ( cauchy-composition-species-types S ( cauchy-composition-species-types T U) ( A)) ( cauchy-composition-species-types ( cauchy-composition-species-types S T) ( U) ( A)) ( equiv-associative-cauchy-composition-species-types A) associative-cauchy-composition-species-types : ( cauchy-composition-species-types ( S) ( cauchy-composition-species-types T U)) ＝ ( cauchy-composition-species-types (cauchy-composition-species-types S T) U) associative-cauchy-composition-species-types = eq-htpy htpy-associative-cauchy-composition-species-types