Composition of Cauchy series of species of types

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-04-25.
Last modified on 2024-02-06.

module species.composition-cauchy-series-species-of-types where
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


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


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)


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)

    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 =
        ( λ (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-composition-species-types S T)
      ( X) 
    composition-cauchy-series-species-types S T X
  equiv-cauchy-series-composition-species-types =
    ( equiv-tot
      ( λ U 
        ( equiv-product
          ( id-equiv)
          ( inv-equiv distributive-Π-Σ)) ∘e
        ( ( inv-equiv left-distributive-product-Σ) ∘e
          ( equiv-tot
            ( λ V 
              ( equiv-product
                ( id-equiv)
                ( ( inv-equiv equiv-up-product) ∘e
                  ( equiv-product id-equiv equiv-ev-pair))) ∘e
              ( left-unit-law-Σ-is-contr
                ( is-torsorial-equiv' (Σ U V))
                ( Σ U V , id-equiv))))))) ∘e
      ( reassociate)

Recent changes