Small Cauchy composition of species types in subuniverses
module species.small-cauchy-composition-species-of-types-in-subuniverses where
Imports
open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.equivalences open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.relaxed-sigma-decompositions open import foundation.sigma-decomposition-subuniverse open import foundation.small-types open import foundation.subuniverses open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type open import foundation.univalence open import foundation.universe-levels open import species.cauchy-composition-species-of-types open import species.species-of-types-in-subuniverses open import species.unit-cauchy-composition-species-of-types
Idea
A species S : Inhabited-Type → UU l can be thought of as the analytic
endofunctor
X ↦ Σ (A : Inhabited-Type) (S A) × (A → X)
Using the formula for composition of analytic endofunctors, we obtain a way to compose species.
Definition
Cauchy composition of species
module _ {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : subuniverse l3 l4) (S : species-subuniverse P Q) (T : species-subuniverse P Q) where small-cauchy-composition-species-subuniverse' : type-subuniverse P → UU (lsuc l1 ⊔ l2 ⊔ l3) small-cauchy-composition-species-subuniverse' X = Σ ( Σ-Decomposition-Subuniverse P X) ( λ D → ( inclusion-subuniverse ( Q) ( S (subuniverse-indexing-type-Σ-Decomposition-Subuniverse P X D))) × ( (x : indexing-type-Σ-Decomposition-Subuniverse P X D) → inclusion-subuniverse ( Q) ( T (subuniverse-cotype-Σ-Decomposition-Subuniverse P X D x)))) module _ {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : subuniverse l3 l4) (C1 : ( S T : species-subuniverse P Q) → (X : type-subuniverse P) → is-small l3 (small-cauchy-composition-species-subuniverse' P Q S T X)) (C2 : ( S T : species-subuniverse P Q) → (X : type-subuniverse P) → ( is-in-subuniverse Q (type-is-small (C1 S T X)))) (C3 : is-closed-under-Σ-subuniverse P) where small-cauchy-composition-species-subuniverse : species-subuniverse P Q → species-subuniverse P Q → species-subuniverse P Q small-cauchy-composition-species-subuniverse S T X = type-is-small (C1 S T X) , C2 S T X
Properties
Equivalent form with species of types
equiv-small-cauchy-composition-Σ-extension-species-subuniverse : ( S : species-subuniverse P Q) ( T : species-subuniverse P Q) ( X : UU l1) → Σ-extension-species-subuniverse P Q ( small-cauchy-composition-species-subuniverse S T) ( X) ≃ ( cauchy-composition-species-types ( Σ-extension-species-subuniverse P Q S) ( Σ-extension-species-subuniverse P Q T) ( X)) equiv-small-cauchy-composition-Σ-extension-species-subuniverse S T X = ( ( equiv-tot ( λ D → ( ( equiv-prod id-equiv (inv-equiv distributive-Π-Σ)) ∘e ( ( inv-equiv right-distributive-prod-Σ) ∘e ( ( equiv-tot (λ _ → inv-equiv (left-distributive-prod-Σ)))))) ∘e ( ( associative-Σ _ _ _)))) ∘e ( ( associative-Σ ( Relaxed-Σ-Decomposition l1 l1 X) ( λ D → is-in-subuniverse P (indexing-type-Relaxed-Σ-Decomposition D) × ((x : indexing-type-Relaxed-Σ-Decomposition D) → is-in-subuniverse P (cotype-Relaxed-Σ-Decomposition D x))) ( _)) ∘e ( ( equiv-Σ-equiv-base ( _) ( ( inv-equiv ( equiv-add-redundant-prop ( is-prop-type-Prop (P X)) ( λ D → ( tr ( is-in-subuniverse P) ( eq-equiv ( Σ (indexing-type-Relaxed-Σ-Decomposition (pr1 D)) (cotype-Relaxed-Σ-Decomposition (pr1 D))) ( X) ( inv-equiv ( matching-correspondence-Relaxed-Σ-Decomposition (pr1 D)))) ( C3 ( indexing-type-Relaxed-Σ-Decomposition (pr1 D) , pr1 (pr2 D)) ( λ x → ( cotype-Relaxed-Σ-Decomposition (pr1 D) x , pr2 (pr2 D) x)))))) ∘e ( commutative-prod ∘e ( equiv-tot ( λ p → equiv-total-is-in-subuniverse-Σ-Decomposition ( P) (X , p))))))) ∘e ( ( inv-associative-Σ ( is-in-subuniverse P X) ( λ p → Σ-Decomposition-Subuniverse P (X , p)) ( _)) ∘e ( ( equiv-tot ( λ p → inv-equiv (equiv-is-small (C1 S T (X , p))))))))))
Unit laws for Cauchy composition of species-subuniverse
module _ (C4 : is-in-subuniverse P (raise-unit l1)) (C5 : (X : UU l1) → is-small l3 (is-contr (X))) (C6 : ( X : type-subuniverse P) → ( is-in-subuniverse ( Q) ( type-is-small (C5 (inclusion-subuniverse P X))))) where small-cauchy-composition-unit-species-subuniverse : species-subuniverse P Q small-cauchy-composition-unit-species-subuniverse X = type-is-small (C5 (inclusion-subuniverse P X)) , C6 X equiv-Σ-extension-small-cauchy-composition-unit-subuniverse : (X : UU l1) → Σ-extension-species-subuniverse ( P) ( Q) ( small-cauchy-composition-unit-species-subuniverse) ( X) ≃ unit-species-types X pr1 (equiv-Σ-extension-small-cauchy-composition-unit-subuniverse X) S = map-inv-equiv-is-small ( C5 X) ( pr2 S) pr2 (equiv-Σ-extension-small-cauchy-composition-unit-subuniverse X) = is-equiv-has-inverse ( λ S → ( tr ( is-in-subuniverse P) ( eq-equiv ( raise-unit l1) ( X) ( ( inv-equiv ( terminal-map , is-equiv-terminal-map-is-contr S)) ∘e inv-equiv (compute-raise-unit l1))) ( C4), map-equiv-is-small (C5 X) S)) ( λ x → eq-is-prop is-property-is-contr) ( λ x → eq-pair ( eq-is-prop (is-prop-type-Prop (P X))) ( eq-is-prop ( is-prop-equiv ( inv-equiv (equiv-is-small (C5 X))) is-property-is-contr))) htpy-left-unit-law-small-cauchy-composition-species-subuniverse : ( S : species-subuniverse P Q) ( X : type-subuniverse P) → inclusion-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( small-cauchy-composition-unit-species-subuniverse) ( S) X) ≃ inclusion-subuniverse Q (S X) htpy-left-unit-law-small-cauchy-composition-species-subuniverse S X = ( ( inv-equiv ( equiv-Σ-extension-species-subuniverse P Q S X)) ∘e ( ( left-unit-law-cauchy-composition-species-types ( Σ-extension-species-subuniverse P Q S) ( inclusion-subuniverse P X)) ∘e ( ( equiv-tot ( λ D → equiv-prod ( equiv-Σ-extension-small-cauchy-composition-unit-subuniverse ( indexing-type-Relaxed-Σ-Decomposition D)) ( id-equiv))) ∘e ( ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse ( small-cauchy-composition-unit-species-subuniverse) ( S) ( inclusion-subuniverse P X)) ∘e ( ( equiv-Σ-extension-species-subuniverse P Q ( small-cauchy-composition-species-subuniverse ( small-cauchy-composition-unit-species-subuniverse) ( S)) ( X))))))) left-unit-law-small-cauchy-composition-species-subuniverse : ( S : species-subuniverse P Q) → small-cauchy-composition-species-subuniverse small-cauchy-composition-unit-species-subuniverse S ＝ S left-unit-law-small-cauchy-composition-species-subuniverse S = eq-equiv-fam-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( small-cauchy-composition-unit-species-subuniverse) ( S)) ( S) ( htpy-left-unit-law-small-cauchy-composition-species-subuniverse S) htpy-right-unit-law-small-cauchy-composition-species-subuniverse : ( S : species-subuniverse P Q) ( X : type-subuniverse P) → inclusion-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( S) ( small-cauchy-composition-unit-species-subuniverse) X) ≃ inclusion-subuniverse Q (S X) htpy-right-unit-law-small-cauchy-composition-species-subuniverse S X = ( ( inv-equiv (equiv-Σ-extension-species-subuniverse P Q S X)) ∘e ( ( right-unit-law-cauchy-composition-species-types ( Σ-extension-species-subuniverse P Q S) ( inclusion-subuniverse P X)) ∘e ( ( equiv-tot ( λ D → equiv-prod ( id-equiv) ( equiv-Π ( _) ( id-equiv) ( λ x → equiv-Σ-extension-small-cauchy-composition-unit-subuniverse ( cotype-Relaxed-Σ-Decomposition D x))))) ∘e ( ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse ( S) ( small-cauchy-composition-unit-species-subuniverse) ( inclusion-subuniverse P X)) ∘e ( ( equiv-Σ-extension-species-subuniverse P Q ( small-cauchy-composition-species-subuniverse S small-cauchy-composition-unit-species-subuniverse) ( X))))))) right-unit-law-small-cauchy-composition-species-subuniverse : ( S : species-subuniverse P Q) → small-cauchy-composition-species-subuniverse S small-cauchy-composition-unit-species-subuniverse ＝ S right-unit-law-small-cauchy-composition-species-subuniverse S = eq-equiv-fam-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( S) ( small-cauchy-composition-unit-species-subuniverse)) ( S) ( htpy-right-unit-law-small-cauchy-composition-species-subuniverse S)
Associativity of composition of species of types in subuniverse
htpy-associative-small-cauchy-composition-species-subuniverse : (S : species-subuniverse P Q) (T : species-subuniverse P Q) (U : species-subuniverse P Q) (X : type-subuniverse P) → inclusion-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( S) ( small-cauchy-composition-species-subuniverse T U) ( X)) ≃ inclusion-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( small-cauchy-composition-species-subuniverse S T) ( U) ( X)) htpy-associative-small-cauchy-composition-species-subuniverse S T U X = ( ( inv-equiv ( equiv-Σ-extension-species-subuniverse P Q ( small-cauchy-composition-species-subuniverse ( small-cauchy-composition-species-subuniverse S T) U) ( X))) ∘e ( ( inv-equiv ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse ( small-cauchy-composition-species-subuniverse S T) ( U) ( inclusion-subuniverse P X))) ∘e ( ( equiv-tot λ D → equiv-prod ( inv-equiv ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse ( S) ( T) ( indexing-type-Relaxed-Σ-Decomposition D))) ( id-equiv)) ∘e ( ( equiv-associative-cauchy-composition-species-types ( Σ-extension-species-subuniverse P Q S) ( Σ-extension-species-subuniverse P Q T) ( Σ-extension-species-subuniverse P Q U) ( inclusion-subuniverse P X)) ∘e ( ( equiv-tot ( λ D → equiv-prod ( id-equiv) ( equiv-Π ( λ y → ( cauchy-composition-species-types ( Σ-extension-species-subuniverse P Q T) ( Σ-extension-species-subuniverse P Q U) ( cotype-Relaxed-Σ-Decomposition D y))) ( id-equiv) ( λ y → ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse ( T) ( U) ( cotype-Relaxed-Σ-Decomposition D y)))))) ∘e ( ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse ( S) ( small-cauchy-composition-species-subuniverse T U) ( inclusion-subuniverse P X)) ∘e ( ( equiv-Σ-extension-species-subuniverse P Q ( small-cauchy-composition-species-subuniverse ( S) ( small-cauchy-composition-species-subuniverse T U)) ( X))))))))) associative-small-cauchy-composition-species-subuniverse : (S : species-subuniverse P Q) (T : species-subuniverse P Q) (U : species-subuniverse P Q)→ small-cauchy-composition-species-subuniverse ( S) ( small-cauchy-composition-species-subuniverse T U) ＝ small-cauchy-composition-species-subuniverse ( small-cauchy-composition-species-subuniverse S T) ( U) associative-small-cauchy-composition-species-subuniverse S T U = eq-equiv-fam-subuniverse ( Q) ( small-cauchy-composition-species-subuniverse ( S) ( small-cauchy-composition-species-subuniverse T U)) ( small-cauchy-composition-species-subuniverse ( small-cauchy-composition-species-subuniverse S T) ( U)) ( htpy-associative-small-cauchy-composition-species-subuniverse S T U)