Composition of Cauchy series of species of types

module species.composition-cauchy-series-species-of-types 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.homotopies
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-cartesian-product-types
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import species.cauchy-composition-species-of-types
open import species.cauchy-series-species-of-types
open import species.species-of-types

Idea

The composition of Cauchy series of two species of types S and T at X is defined as the Cauchy series of S applied to the Cauchy series of T at X

Definition

composition-cauchy-series-species-types :
  {l1 l2 l3 l4 : Level} → species-types l1 l2 → species-types l1 l3 →
  UU l4 → UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
composition-cauchy-series-species-types S T X =
  cauchy-series-species-types S (cauchy-series-species-types T X)

Property

The Cauchy series associated to the composition of the species `S` and `T` is the composition of their Cauchy series

module _
  {l1 l2 l3 l4 : Level}
  (S : species-types l1 l2)
  (T : species-types l1 l3)
  (X : UU l4)
  where

  private
    reassociate :
      cauchy-series-species-types (cauchy-composition-species-types S T) X ≃
      Σ ( UU l1)
        ( λ U →
           Σ ( U → UU l1)
             ( λ V →
               Σ ( Σ ( UU l1) (λ F → F ≃ Σ U V))
                 ( λ F → (S U) × (((y : U) → T (V y)) × (pr1 F → X)))))
    pr1 reassociate (F , ((U , V , e) , s , fs) , ft) =
      (U , V , (F , e) , s , fs , ft)
    pr2 reassociate =
      is-equiv-has-inverse
        ( λ (U , V , (F , e) , s , fs , ft) →
          (F , ((U , V , e) , s , fs) , ft))
        ( refl-htpy)
        ( refl-htpy)

  equiv-cauchy-series-composition-species-types :
    cauchy-series-species-types
      ( cauchy-composition-species-types S T)
      ( X) ≃
    composition-cauchy-series-species-types S T X
  equiv-cauchy-series-composition-species-types =
    ( equiv-tot
      ( λ U →
        ( equiv-prod
          ( id-equiv)
          ( inv-equiv distributive-Π-Σ)) ∘e
        ( ( inv-equiv left-distributive-prod-Σ) ∘e
          ( equiv-tot
            ( λ V →
              ( equiv-prod
                ( id-equiv)
                ( ( inv-equiv universal-property-product) ∘e
                  ( equiv-prod id-equiv equiv-ev-pair))) ∘e
              ( left-unit-law-Σ-is-contr
                ( is-contr-total-equiv' (Σ U V))
                ( Σ U V , id-equiv))))))) ∘e
      ( reassociate)