Cauchy composition of species of types in a subuniverse

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2024-10-29.

module species.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.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.global-subuniverses
open import foundation.homotopies
open import foundation.propositions
open import foundation.relaxed-sigma-decompositions
open import foundation.sigma-closed-subuniverses
open import foundation.sigma-decomposition-subuniverse
open import foundation.subuniverses
open import foundation.transport-along-identifications
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
open import species.unit-cauchy-composition-species-of-types-in-subuniverses

Idea

A species S : type-subuniverse P → type-subuniverse Q induces its Cauchy series

  X ↦ Σ (A : type-subuniverse P), (S A) × (A → X)

The Cauchy composition of species S and T is obtained from the coefficients of the composite of the Cauchy series of S and T.

Definition

Cauchy composition of species

module _
  {l1 l2 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  where

  type-cauchy-composition-species-subuniverse :
    {l3 l4 : Level} →
    (S : species-subuniverse P (subuniverse-global-subuniverse Q l3)) →
    (T : species-subuniverse P (subuniverse-global-subuniverse Q l4)) →
    type-subuniverse P → UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
  type-cauchy-composition-species-subuniverse {l3} {l4} S T X =
    Σ ( Σ-Decomposition-Subuniverse P X)
      ( λ D →
        ( inclusion-subuniverse
          ( subuniverse-global-subuniverse Q l3)
          ( S (subuniverse-indexing-type-Σ-Decomposition-Subuniverse P X D))) ×
        ( (x : indexing-type-Σ-Decomposition-Subuniverse P X D) →
          inclusion-subuniverse
          ( subuniverse-global-subuniverse Q l4)
          ( T (subuniverse-cotype-Σ-Decomposition-Subuniverse P X D x))))

  is-closed-under-cauchy-composition-species-subuniverse : UUω
  is-closed-under-cauchy-composition-species-subuniverse =
    { l3 l4 : Level}
    ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
    ( T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
    ( X : type-subuniverse P) →
    is-in-global-subuniverse Q
      ( type-cauchy-composition-species-subuniverse S T X)

module _
  {l1 l2 l3 l4 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
  (C2 : is-closed-under-Σ-subuniverse P)
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  where

  cauchy-composition-species-subuniverse :
    species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
  cauchy-composition-species-subuniverse X =
    ( type-cauchy-composition-species-subuniverse P Q S T X , C1 S T X)

Properties

Σ-extension of species of types in a subuniverse preserves cauchy composition

module _
  {l1 l2 l3 l4 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
  (C2 : is-closed-under-Σ-subuniverse P)
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  where

  preserves-cauchy-composition-Σ-extension-species-subuniverse :
    ( X : UU l1) →
    Σ-extension-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
      ( cauchy-composition-species-subuniverse P Q C1 C2 S T)
      ( X) ≃
    ( cauchy-composition-species-types
      ( Σ-extension-species-subuniverse P
        ( subuniverse-global-subuniverse Q l3)
        ( S))
      ( Σ-extension-species-subuniverse P
        ( subuniverse-global-subuniverse Q l4)
        ( T))
      ( X))
  preserves-cauchy-composition-Σ-extension-species-subuniverse X =
    ( ( equiv-tot
        ( λ D →
          ( ( equiv-product id-equiv (inv-equiv distributive-Π-Σ)) ∘e
          ( ( inv-equiv right-distributive-product-Σ) ∘e
          ( ( equiv-tot (λ _ → inv-equiv (left-distributive-product-Σ)))))) ∘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
                        ( inv-equiv
                          ( matching-correspondence-Relaxed-Σ-Decomposition
                            ( pr1 D))))
                      ( C2
                          ( indexing-type-Relaxed-Σ-Decomposition (pr1 D) ,
                              pr1 (pr2 D))
                          ( λ x →
                            ( cotype-Relaxed-Σ-Decomposition (pr1 D) x ,
                                pr2 (pr2 D) x)))))) ∘e
              ( commutative-product ∘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))
              ( _))))))

Unit laws for Cauchy composition of species-subuniverse

module _
  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
  ( C3 : is-in-subuniverse P (raise-unit l1))
  ( C4 :
    is-closed-under-is-contr-subuniverses P
      ( subuniverse-global-subuniverse Q l1))
  (X : UU l1)
  where

  map-equiv-Σ-extension-cauchy-composition-unit-subuniverse :
    Σ-extension-species-subuniverse P
      ( subuniverse-global-subuniverse Q l1)
      ( cauchy-composition-unit-species-subuniverse P Q C4)
      ( X) →
    unit-species-types X
  map-equiv-Σ-extension-cauchy-composition-unit-subuniverse (p , H) = H

  map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse :
    unit-species-types X →
    Σ-extension-species-subuniverse P
      ( subuniverse-global-subuniverse Q l1)
      ( cauchy-composition-unit-species-subuniverse P Q C4)
      ( X)
  pr1 (map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse H) =
    is-in-subuniverse-equiv P (equiv-is-contr is-contr-raise-unit H) C3
  pr2 (map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse H) = H

  is-section-map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse :
    ( map-equiv-Σ-extension-cauchy-composition-unit-subuniverse ∘
      map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse) ~ id
  is-section-map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse =
    refl-htpy

  is-retraction-map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse :
    ( map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse ∘
      map-equiv-Σ-extension-cauchy-composition-unit-subuniverse) ~ id
  is-retraction-map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse
    x =
    eq-pair
      ( eq-is-prop (is-prop-type-Prop (P X)))
      ( eq-is-prop is-property-is-contr)

  is-equiv-map-equiv-Σ-extension-cauchy-composition-unit-subuniverse :
    is-equiv map-equiv-Σ-extension-cauchy-composition-unit-subuniverse
  is-equiv-map-equiv-Σ-extension-cauchy-composition-unit-subuniverse =
    is-equiv-is-invertible
      map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse
      is-section-map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse
      is-retraction-map-inv-equiv-Σ-extension-cauchy-composition-unit-subuniverse

  equiv-Σ-extension-cauchy-composition-unit-subuniverse :
    Σ-extension-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q l1)
      ( cauchy-composition-unit-species-subuniverse P Q C4)
      ( X) ≃
    unit-species-types X
  pr1 equiv-Σ-extension-cauchy-composition-unit-subuniverse =
    map-equiv-Σ-extension-cauchy-composition-unit-subuniverse
  pr2 equiv-Σ-extension-cauchy-composition-unit-subuniverse =
    is-equiv-map-equiv-Σ-extension-cauchy-composition-unit-subuniverse

module _
  { l1 l2 l3 : Level}
  ( P : subuniverse l1 l2)
  ( Q : global-subuniverse (λ l → l))
  ( C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
  ( C2 : is-closed-under-Σ-subuniverse P)
  ( C3 : is-in-subuniverse P (raise-unit l1))
  ( C4 :
    is-closed-under-is-contr-subuniverses P
      ( subuniverse-global-subuniverse Q l1))
  ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  where

  equiv-left-unit-law-cauchy-composition-species-subuniverse :
    ( X : type-subuniverse P) →
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3))
      ( cauchy-composition-species-subuniverse P Q C1 C2
        ( cauchy-composition-unit-species-subuniverse P Q C4)
        ( S)
        ( X)) ≃
    inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
  equiv-left-unit-law-cauchy-composition-species-subuniverse X =
    ( ( inv-equiv
        ( equiv-Σ-extension-species-subuniverse
          ( P)
          ( subuniverse-global-subuniverse Q l3)
          ( S)
          ( X))) ∘e
      ( ( left-unit-law-cauchy-composition-species-types
          ( Σ-extension-species-subuniverse
            ( P)
            ( subuniverse-global-subuniverse Q l3)
            ( S))
          ( inclusion-subuniverse P X)) ∘e
        ( ( equiv-tot
            ( λ D →
              equiv-product
                ( equiv-Σ-extension-cauchy-composition-unit-subuniverse
                  ( P)
                  ( Q)
                  ( C3)
                  ( C4)
                  ( indexing-type-Relaxed-Σ-Decomposition D))
                ( id-equiv))) ∘e
          ( ( preserves-cauchy-composition-Σ-extension-species-subuniverse
              ( P)
              ( Q)
              ( C1)
              ( C2)
              ( cauchy-composition-unit-species-subuniverse P Q C4)
              ( S)
              ( inclusion-subuniverse P X)) ∘e
            ( ( equiv-Σ-extension-species-subuniverse
                ( P)
                ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3))
                ( cauchy-composition-species-subuniverse
                  ( P)
                  ( Q)
                  ( C1)
                  ( C2)
                  ( cauchy-composition-unit-species-subuniverse P Q C4)
                  ( S))
                  ( X)))))))

  equiv-right-unit-law-cauchy-composition-species-subuniverse :
    ( X : type-subuniverse P) →
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3))
      ( cauchy-composition-species-subuniverse P Q C1 C2 S
        ( cauchy-composition-unit-species-subuniverse P Q C4)
        ( X)) ≃
    inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
  equiv-right-unit-law-cauchy-composition-species-subuniverse X =
    ( inv-equiv
      ( equiv-Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l3)
        ( S)
        ( X))) ∘e
    ( ( right-unit-law-cauchy-composition-species-types
        ( Σ-extension-species-subuniverse
          ( P)
          ( subuniverse-global-subuniverse Q l3)
          ( S))
        ( inclusion-subuniverse P X)) ∘e
      ( ( equiv-tot
          ( λ D →
            equiv-product
              ( id-equiv)
              ( equiv-Π-equiv-family
                ( λ x →
                  equiv-Σ-extension-cauchy-composition-unit-subuniverse
                    ( P)
                    ( Q)
                    ( C3)
                    ( C4)
                    ( cotype-Relaxed-Σ-Decomposition D x))))) ∘e
        ( ( preserves-cauchy-composition-Σ-extension-species-subuniverse
            ( P)
            ( Q)
            ( C1)
            ( C2)
            ( S)
            ( cauchy-composition-unit-species-subuniverse P Q C4)
            ( inclusion-subuniverse P X)) ∘e
          ( ( equiv-Σ-extension-species-subuniverse
              ( P)
              ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3))
              ( cauchy-composition-species-subuniverse P Q C1 C2 S
                ( cauchy-composition-unit-species-subuniverse P Q C4))
              ( X))))))

Associativity of composition of species of types in subuniverse

module _
  { l1 l2 l3 l4 l5 : Level}
  ( P : subuniverse l1 l2)
  ( Q : global-subuniverse (λ l → l))
  ( C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
  ( C2 : is-closed-under-Σ-subuniverse P)
  ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  ( T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  ( U : species-subuniverse P (subuniverse-global-subuniverse Q l5))
  where

  equiv-associative-cauchy-composition-species-subuniverse :
    (X : type-subuniverse P) →
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
      ( cauchy-composition-species-subuniverse P Q C1 C2 S
        ( cauchy-composition-species-subuniverse P Q C1 C2 T U)
        ( X)) ≃
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
      ( cauchy-composition-species-subuniverse P Q C1 C2
        ( cauchy-composition-species-subuniverse P Q C1 C2 S T)
        ( U)
        ( X))
  equiv-associative-cauchy-composition-species-subuniverse X =
    ( inv-equiv
      ( equiv-Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
        ( cauchy-composition-species-subuniverse P Q C1 C2
          ( cauchy-composition-species-subuniverse P Q C1 C2 S T)
          ( U))
        ( X))) ∘e
    ( ( inv-equiv
        ( preserves-cauchy-composition-Σ-extension-species-subuniverse P Q C1 C2
          ( cauchy-composition-species-subuniverse P Q C1 C2 S T)
          ( U)
          ( inclusion-subuniverse P X))) ∘e
      ( ( equiv-tot
          ( λ D →
            equiv-product
              ( inv-equiv
                ( preserves-cauchy-composition-Σ-extension-species-subuniverse
                  ( P)
                  ( Q)
                  ( C1)
                  ( C2)
                  ( S)
                  ( T)
                  ( indexing-type-Relaxed-Σ-Decomposition D)))
              ( id-equiv))) ∘e
        ( ( equiv-associative-cauchy-composition-species-types
            ( Σ-extension-species-subuniverse P
              ( subuniverse-global-subuniverse Q l3)
              ( S))
            ( Σ-extension-species-subuniverse P
              ( subuniverse-global-subuniverse Q l4)
              ( T))
            ( Σ-extension-species-subuniverse P
              ( subuniverse-global-subuniverse Q l5)
              ( U))
            ( inclusion-subuniverse P X)) ∘e
          ( equiv-tot
            ( λ D →
              equiv-product
                ( id-equiv)
                ( equiv-Π
                  ( λ y →
                    cauchy-composition-species-types
                      ( Σ-extension-species-subuniverse
                        ( P)
                        ( subuniverse-global-subuniverse Q l4)
                        ( T))
                      ( Σ-extension-species-subuniverse
                        ( P)
                        ( subuniverse-global-subuniverse Q l5)
                        ( U))
                      ( cotype-Relaxed-Σ-Decomposition D y))
                  ( id-equiv)
                  ( λ y →
                    preserves-cauchy-composition-Σ-extension-species-subuniverse
                      ( P)
                      ( Q)
                      ( C1)
                      ( C2)
                      ( T)
                      ( U)
                      ( cotype-Relaxed-Σ-Decomposition D y)))) ∘e
            ( ( preserves-cauchy-composition-Σ-extension-species-subuniverse
                ( P)
                ( Q)
                ( C1)
                ( C2)
                ( S)
                ( cauchy-composition-species-subuniverse P Q C1 C2 T U)
                ( inclusion-subuniverse P X)) ∘e
              ( equiv-Σ-extension-species-subuniverse P
                ( subuniverse-global-subuniverse Q
                  ( lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
                ( cauchy-composition-species-subuniverse P Q C1 C2 S
                  ( cauchy-composition-species-subuniverse P Q C1 C2 T U))
                ( X)))))))

Recent changes