# Small Cauchy composition of species types in subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-27.

module species.small-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.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
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.small-types
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


## Idea

A species S : Inhabited-Type → UU l can be thought of as the analytic endofunctor

  X ↦ Σ (A : Inhabited-Type) (S A) × (A → X)


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

## Definition

### Cauchy composition of species

module _
{l1 l2 l3 l4 : Level}
(P : subuniverse l1 l2)
(Q : subuniverse l3 l4)
(S : species-subuniverse P Q)
(T : species-subuniverse P Q)
where

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

module _
{l1 l2 l3 l4 : Level}
(P : subuniverse l1 l2)
(Q : subuniverse l3 l4)
(C1 :
( S T : species-subuniverse P Q) → (X : type-subuniverse P) →
is-small l3 (small-cauchy-composition-species-subuniverse' P Q S T X))
(C2 :
( S T : species-subuniverse P Q) → (X : type-subuniverse P) →
( is-in-subuniverse Q (type-is-small (C1 S T X))))
(C3 : is-closed-under-Σ-subuniverse P)
where

small-cauchy-composition-species-subuniverse :
species-subuniverse P Q →
species-subuniverse P Q →
species-subuniverse P Q
small-cauchy-composition-species-subuniverse S T X =
type-is-small (C1 S T X) , C2 S T X


## Properties

### Equivalent form with species of types

  equiv-small-cauchy-composition-Σ-extension-species-subuniverse :
( S : species-subuniverse P Q)
( T : species-subuniverse P Q)
( X : UU l1) →
Σ-extension-species-subuniverse P Q
( small-cauchy-composition-species-subuniverse S T)
( X) ≃
( cauchy-composition-species-types
( Σ-extension-species-subuniverse P Q S)
( Σ-extension-species-subuniverse P Q T)
( X))
equiv-small-cauchy-composition-Σ-extension-species-subuniverse S T 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
( is-prop-type-Prop (P X))
( λ D →
( tr
( is-in-subuniverse P)
( eq-equiv
( inv-equiv
( matching-correspondence-Relaxed-Σ-Decomposition
(pr1 D))))
( C3
( 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))
( _)) ∘e
( ( equiv-tot
( λ p → inv-equiv (equiv-is-small (C1 S T (X , p))))))))))


### Unit laws for Cauchy composition of species-subuniverse

  module _
(C4 : is-in-subuniverse P (raise-unit l1))
(C5 :
(X : UU l1) →
is-small l3 (is-contr (X)))
(C6 :
( X : type-subuniverse P) →
( is-in-subuniverse
( Q)
( type-is-small (C5 (inclusion-subuniverse P X)))))
where

small-cauchy-composition-unit-species-subuniverse :
species-subuniverse P Q
small-cauchy-composition-unit-species-subuniverse X =
type-is-small (C5 (inclusion-subuniverse P X)) , C6 X

equiv-Σ-extension-small-cauchy-composition-unit-subuniverse :
(X : UU l1) →
Σ-extension-species-subuniverse
( P)
( Q)
( small-cauchy-composition-unit-species-subuniverse)
( X) ≃
unit-species-types X
pr1 (equiv-Σ-extension-small-cauchy-composition-unit-subuniverse X) S =
map-inv-equiv-is-small
( C5 X)
( pr2 S)
pr2 (equiv-Σ-extension-small-cauchy-composition-unit-subuniverse X) =
is-equiv-is-invertible
( λ S →
( tr
( is-in-subuniverse P)
( eq-equiv
( ( inv-equiv
( terminal-map X , is-equiv-terminal-map-is-contr S)) ∘e
( inv-equiv (compute-raise-unit l1))))
( C4) ,
map-equiv-is-small (C5 X) S))
( λ x → eq-is-prop is-property-is-contr)
( λ x →
eq-pair
( eq-is-prop (is-prop-type-Prop (P X)))
( eq-is-prop
( is-prop-equiv
( inv-equiv (equiv-is-small (C5 X))) is-property-is-contr)))

htpy-left-unit-law-small-cauchy-composition-species-subuniverse :
( S : species-subuniverse P Q)
( X : type-subuniverse P) →
inclusion-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( small-cauchy-composition-unit-species-subuniverse)
( S) X) ≃
inclusion-subuniverse Q (S X)
htpy-left-unit-law-small-cauchy-composition-species-subuniverse S X =
( ( inv-equiv
( equiv-Σ-extension-species-subuniverse P Q S X)) ∘e
( ( left-unit-law-cauchy-composition-species-types
( Σ-extension-species-subuniverse P Q S)
( inclusion-subuniverse P X)) ∘e
( ( equiv-tot
( λ D →
equiv-product
( equiv-Σ-extension-small-cauchy-composition-unit-subuniverse
( indexing-type-Relaxed-Σ-Decomposition D))
( id-equiv))) ∘e
( ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse
( small-cauchy-composition-unit-species-subuniverse)
( S)
( inclusion-subuniverse P X)) ∘e
( ( equiv-Σ-extension-species-subuniverse P Q
( small-cauchy-composition-species-subuniverse
( small-cauchy-composition-unit-species-subuniverse)
( S))
( X)))))))

left-unit-law-small-cauchy-composition-species-subuniverse :
( S : species-subuniverse P Q) →
small-cauchy-composition-species-subuniverse
small-cauchy-composition-unit-species-subuniverse
S ＝ S
left-unit-law-small-cauchy-composition-species-subuniverse S =
eq-equiv-fam-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( small-cauchy-composition-unit-species-subuniverse)
( S))
( S)
( htpy-left-unit-law-small-cauchy-composition-species-subuniverse S)

htpy-right-unit-law-small-cauchy-composition-species-subuniverse :
( S : species-subuniverse P Q)
( X : type-subuniverse P) →
inclusion-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( S)
( small-cauchy-composition-unit-species-subuniverse) X) ≃
inclusion-subuniverse Q (S X)
htpy-right-unit-law-small-cauchy-composition-species-subuniverse S X =
( ( inv-equiv (equiv-Σ-extension-species-subuniverse P Q S X)) ∘e
( ( right-unit-law-cauchy-composition-species-types
( Σ-extension-species-subuniverse P Q S)
( inclusion-subuniverse P X)) ∘e
( ( equiv-tot
( λ D →
equiv-product
( id-equiv)
( equiv-Π
( _)
( id-equiv)
( λ x →
equiv-Σ-extension-small-cauchy-composition-unit-subuniverse
( cotype-Relaxed-Σ-Decomposition D x))))) ∘e
( ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse
( S)
( small-cauchy-composition-unit-species-subuniverse)
( inclusion-subuniverse P X)) ∘e
( ( equiv-Σ-extension-species-subuniverse P Q
( small-cauchy-composition-species-subuniverse
S
small-cauchy-composition-unit-species-subuniverse)
( X)))))))

right-unit-law-small-cauchy-composition-species-subuniverse :
( S : species-subuniverse P Q) →
small-cauchy-composition-species-subuniverse
S
small-cauchy-composition-unit-species-subuniverse ＝ S
right-unit-law-small-cauchy-composition-species-subuniverse S =
eq-equiv-fam-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( S)
( small-cauchy-composition-unit-species-subuniverse))
( S)
( htpy-right-unit-law-small-cauchy-composition-species-subuniverse S)


### Associativity of composition of species of types in subuniverse

  htpy-associative-small-cauchy-composition-species-subuniverse :
(S : species-subuniverse P Q)
(T : species-subuniverse P Q)
(U : species-subuniverse P Q)
(X : type-subuniverse P) →
inclusion-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( S)
( small-cauchy-composition-species-subuniverse T U)
( X)) ≃
inclusion-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( small-cauchy-composition-species-subuniverse S T)
( U)
( X))
htpy-associative-small-cauchy-composition-species-subuniverse S T U X =
( ( inv-equiv
( equiv-Σ-extension-species-subuniverse P Q
( small-cauchy-composition-species-subuniverse
( small-cauchy-composition-species-subuniverse S T) U)
( X))) ∘e
( ( inv-equiv
( equiv-small-cauchy-composition-Σ-extension-species-subuniverse
( small-cauchy-composition-species-subuniverse S T)
( U)
( inclusion-subuniverse P X))) ∘e
( ( equiv-tot
( λ D →
equiv-product
( inv-equiv
( equiv-small-cauchy-composition-Σ-extension-species-subuniverse
( S)
( T)
( indexing-type-Relaxed-Σ-Decomposition D)))
( id-equiv))) ∘e
( ( equiv-associative-cauchy-composition-species-types
( Σ-extension-species-subuniverse P Q S)
( Σ-extension-species-subuniverse P Q T)
( Σ-extension-species-subuniverse P Q U)
( inclusion-subuniverse P X)) ∘e
( ( equiv-tot
( λ D →
equiv-product
( id-equiv)
( equiv-Π
( λ y →
( cauchy-composition-species-types
( Σ-extension-species-subuniverse P Q T)
( Σ-extension-species-subuniverse P Q U)
( cotype-Relaxed-Σ-Decomposition D y)))
( id-equiv)
( λ y →
( equiv-small-cauchy-composition-Σ-extension-species-subuniverse
( T)
( U)
( cotype-Relaxed-Σ-Decomposition D y)))))) ∘e
( ( equiv-small-cauchy-composition-Σ-extension-species-subuniverse
( S)
( small-cauchy-composition-species-subuniverse T U)
( inclusion-subuniverse P X)) ∘e
( ( equiv-Σ-extension-species-subuniverse P Q
( small-cauchy-composition-species-subuniverse
( S)
( small-cauchy-composition-species-subuniverse T U))
( X)))))))))

associative-small-cauchy-composition-species-subuniverse :
(S : species-subuniverse P Q)
(T : species-subuniverse P Q)
(U : species-subuniverse P Q) →
small-cauchy-composition-species-subuniverse
( S)
( small-cauchy-composition-species-subuniverse T U) ＝
small-cauchy-composition-species-subuniverse
( small-cauchy-composition-species-subuniverse S T)
( U)
associative-small-cauchy-composition-species-subuniverse S T U =
eq-equiv-fam-subuniverse
( Q)
( small-cauchy-composition-species-subuniverse
( S)
( small-cauchy-composition-species-subuniverse T U))
( small-cauchy-composition-species-subuniverse
( small-cauchy-composition-species-subuniverse S T)
( U))
( htpy-associative-small-cauchy-composition-species-subuniverse S T U)