Cauchy composition of species of types

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

Created on 2023-04-25.

module species.cauchy-composition-species-of-types where
Imports
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.discrete-relaxed-sigma-decompositions
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.relaxed-sigma-decompositions
open import foundation.trivial-relaxed-sigma-decompositions
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-function-types
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-dependent-pair-types
open import foundation.universe-levels

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

Idea

A species of types S : UU l1 → UU l2 can be thought of as the polynomial endofunctor

X ↦ Σ (A : UU l1) (S A) × (A → X)

Using the formula for composition of analytic endofunctors, we obtain a way to compose species, which is called the Cauchy composition of species.

Definition

Cauchy composition of species

cauchy-composition-species-types :
{l1 l2 l3 : Level}  species-types l1 l2  species-types l1 l3
species-types l1 (lsuc l1  l2  l3)
cauchy-composition-species-types {l1} {l2} {l3} S T X =
Σ ( Relaxed-Σ-Decomposition l1 l1 X)
( λ D
( S (indexing-type-Relaxed-Σ-Decomposition D)) ×
( ( y : indexing-type-Relaxed-Σ-Decomposition D)
T (cotype-Relaxed-Σ-Decomposition D y)))

Properties

Unit laws for Cauchy composition of species

left-unit-law-cauchy-composition-species-types :
{l1 l2 : Level}
(F : species-types l1 l2)  (A : UU l1)
cauchy-composition-species-types unit-species-types F A  F A
left-unit-law-cauchy-composition-species-types {l1} F A =
( left-unit-law-Σ-is-contr
( is-contr-type-trivial-Relaxed-Σ-Decomposition)
( trivial-Relaxed-Σ-Decomposition l1 A ,
is-trivial-trivial-Relaxed-Σ-Decomposition {l1} {l1} {A})) ∘e
( ( inv-associative-Σ
( Relaxed-Σ-Decomposition l1 l1 A)
( λ D  is-contr (indexing-type-Relaxed-Σ-Decomposition D))
( λ C  F (cotype-Relaxed-Σ-Decomposition (pr1 C) (center (pr2 C))))) ∘e
( ( equiv-Σ
( _)
( id-equiv)
( λ D
equiv-Σ
( λ z  F (cotype-Relaxed-Σ-Decomposition D (center z)))
( id-equiv)
( λ C
( left-unit-law-Π-is-contr C (center C)))))))

right-unit-law-cauchy-composition-species-types :
{l1 l2 : Level}
(F : species-types l1 l2)  (A : UU l1)
cauchy-composition-species-types F unit-species-types A  F A
right-unit-law-cauchy-composition-species-types {l1} F A =
( left-unit-law-Σ-is-contr
( is-contr-type-discrete-Relaxed-Σ-Decomposition)
( ( discrete-Relaxed-Σ-Decomposition l1 A) ,
is-discrete-discrete-Relaxed-Σ-Decomposition)) ∘e
( ( inv-associative-Σ
( Relaxed-Σ-Decomposition l1 l1 A)
( λ D
( y : indexing-type-Relaxed-Σ-Decomposition D)
is-contr (cotype-Relaxed-Σ-Decomposition D y))
( λ D  F (indexing-type-Relaxed-Σ-Decomposition (pr1 D)))) ∘e
( ( equiv-Σ
( λ D
( ( y : indexing-type-Relaxed-Σ-Decomposition D)
unit-species-types
( cotype-Relaxed-Σ-Decomposition D y)) ×
F ( indexing-type-Relaxed-Σ-Decomposition D))
( id-equiv)
( λ _  commutative-product))))

Associativity of composition of species

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

equiv-associative-cauchy-composition-species-types :
(A : UU l1)
cauchy-composition-species-types
( S)
( cauchy-composition-species-types T U)
( A)
cauchy-composition-species-types
( cauchy-composition-species-types S T)
( U)
( A)
equiv-associative-cauchy-composition-species-types A =
( equiv-Σ
( _)
( id-equiv)
( λ D1
( ( inv-equiv right-distributive-product-Σ) ∘e
( ( equiv-Σ
( _)
( id-equiv)
( λ D2
( inv-associative-Σ
( S (indexing-type-Relaxed-Σ-Decomposition D2))
( λ _
( x : indexing-type-Relaxed-Σ-Decomposition D2)
T ( cotype-Relaxed-Σ-Decomposition D2 x))
_))) ∘e
( ( equiv-Σ
( _)
( id-equiv)
( λ D2
( equiv-product
( id-equiv)
( ( equiv-product
( id-equiv)
( ( inv-equiv
( equiv-precomp-Π
( inv-equiv
( matching-correspondence-Relaxed-Σ-Decomposition
D2))
( λ x  U ( cotype-Relaxed-Σ-Decomposition D1 x)))) ∘e
( inv-equiv equiv-ev-pair))) ∘e
( distributive-Π-Σ)))))))))) ∘e
( ( associative-Σ
( Relaxed-Σ-Decomposition l1 l1 A)
( λ D  Relaxed-Σ-Decomposition l1 l1
( indexing-type-Relaxed-Σ-Decomposition D))
( _)) ∘e
( ( inv-equiv
( equiv-Σ-equiv-base
( _)
( equiv-displayed-fibered-Relaxed-Σ-Decomposition))) ∘e
( ( inv-associative-Σ
( Relaxed-Σ-Decomposition l1 l1 A)
( λ D
( x : indexing-type-Relaxed-Σ-Decomposition D)
Relaxed-Σ-Decomposition l1 l1
( cotype-Relaxed-Σ-Decomposition D x))
( _)) ∘e
( ( equiv-Σ
( _)
( id-equiv)
( λ D  left-distributive-product-Σ)) ∘e
( ( equiv-Σ
( _)
( id-equiv)
( λ D  equiv-product id-equiv distributive-Π-Σ)))))))

htpy-associative-cauchy-composition-species-types :
cauchy-composition-species-types
( S)
( cauchy-composition-species-types T U) ~
cauchy-composition-species-types (cauchy-composition-species-types S T) U
htpy-associative-cauchy-composition-species-types A =
eq-equiv (equiv-associative-cauchy-composition-species-types A)

associative-cauchy-composition-species-types :
( cauchy-composition-species-types
( S)
( cauchy-composition-species-types T U))
( cauchy-composition-species-types (cauchy-composition-species-types S T) U)
associative-cauchy-composition-species-types =
eq-htpy htpy-associative-cauchy-composition-species-types