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)