Small Cauchy composition of species types in subuniverses

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-decomposition-subuniverse
open import foundation.small-types
open import foundation.subuniverses
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-prod id-equiv (inv-equiv distributive-Π-Σ)) ∘e
          ( ( inv-equiv right-distributive-prod-Σ) ∘e
          ( ( equiv-tot  _  inv-equiv (left-distributive-prod-Σ)))))) ∘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
                ( equiv-add-redundant-prop
                  ( is-prop-type-Prop (P X))
                  ( λ D 
                    ( tr
                      ( is-in-subuniverse P)
                      ( eq-equiv
                        ( Σ (indexing-type-Relaxed-Σ-Decomposition (pr1 D))
                          (cotype-Relaxed-Σ-Decomposition (pr1 D)))
                        ( X)
                        ( 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-prod ∘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-has-inverse
        ( λ S 
          ( tr
              ( is-in-subuniverse P)
              ( eq-equiv
                  ( raise-unit l1)
                  ( X)
                  ( ( inv-equiv
                        ( terminal-map , 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-prod
                  ( 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-prod
                  ( 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-prod
               ( 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-prod
                    ( 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)