Cauchy series of species of types in subuniverses
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-04-27.
Last modified on 2025-08-30.
module species.cauchy-series-species-of-types-in-subuniverses where
Imports
open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.global-subuniverses open import foundation.postcomposition-functions open import foundation.propositions open import foundation.subuniverses open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import species.cauchy-series-species-of-types open import species.species-of-types-in-subuniverses
Idea
The
Cauchy series¶
of a species S
of types in
subuniverse from P
to Q
at X
is defined as
Σ (U : type-subuniverse P) (S(U) × (U → X)).
Definition
module _ {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2) (Q : subuniverse l3 l4) (S : species-subuniverse P Q) (X : UU l5) where cauchy-series-species-subuniverse : UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l5) cauchy-series-species-subuniverse = Σ ( type-subuniverse P) ( λ U → inclusion-subuniverse Q (S U) × (inclusion-subuniverse P U → X))
Property
Equivalent form with species of types
equiv-cauchy-series-Σ-extension-species-subuniverse : cauchy-series-species-subuniverse ≃ cauchy-series-species-types (Σ-extension-species-subuniverse P Q S) X equiv-cauchy-series-Σ-extension-species-subuniverse = (equiv-tot (λ U → inv-associative-Σ _ _ _)) ∘e (associative-Σ _ _ _)
Equivalences
module _ {α : Level → Level} {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse α) (S : species-subuniverse P (subuniverse-global-subuniverse Q l3)) (T : species-subuniverse P (subuniverse-global-subuniverse Q l4)) (f : (F : type-subuniverse P) → inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S F) ≃ inclusion-subuniverse (subuniverse-global-subuniverse Q l4) (T F)) (X : UU l5) where equiv-cauchy-series-equiv-species-subuniverse : cauchy-series-species-subuniverse ( P) ( subuniverse-global-subuniverse Q l3) ( S) ( X) ≃ cauchy-series-species-subuniverse ( P) ( subuniverse-global-subuniverse Q l4) ( T) ( X) equiv-cauchy-series-equiv-species-subuniverse = equiv-tot (λ X → equiv-product-left (f X)) module _ {l1 l2 l3 l4 l5 l6 : Level} (P : subuniverse l1 l2) (Q : subuniverse l3 l4) (S : species-subuniverse P Q) (X : UU l5) (Y : UU l6) (e : X ≃ Y) where equiv-cauchy-series-species-subuniverse : cauchy-series-species-subuniverse P Q S X ≃ cauchy-series-species-subuniverse P Q S Y equiv-cauchy-series-species-subuniverse = equiv-tot ( λ F → equiv-product-right (equiv-postcomp (inclusion-subuniverse P F) e))
Recent changes
- 2025-08-30. Fredrik Bakke. Some cleanup of species (#1502).
- 2024-10-29. Fredrik Bakke. chore: Replace strange whitespace (#1215).
- 2024-02-06. Fredrik Bakke. Rename
(co)prod
to(co)product
(#1017). - 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).