Cauchy exponentials of species of types in a subuniverse

module species.cauchy-exponentials-species-of-types-in-subuniverses where
Imports
open import foundation.cartesian-product-types
open import foundation.coproduct-decompositions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.relaxed-sigma-decompositions
open import foundation.sigma-decomposition-subuniverse
open import foundation.subuniverses
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.unit-type
open import foundation.univalence
open import foundation.universe-levels

open import species.cauchy-composition-species-of-types-in-subuniverses
open import species.cauchy-exponentials-species-of-types
open import species.cauchy-products-species-of-types-in-subuniverses
open import species.coproducts-species-of-types
open import species.coproducts-species-of-types-in-subuniverses
open import species.species-of-types-in-subuniverses

Idea

The Cauchy exponential of a species S : P → Q of types in subuniverse is defined by

  X ↦ Σ ((U , V , e) : Σ-Decomposition-subuniverse P X),  Π (u : U) → S (V u).

If Q is a global subuniverse, and if the previous definition is in Q, then the Cauchy exponential is also a species of types in subuniverse from P to Q.

Definition

module _
  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
  where

  cauchy-exponential-species-subuniverse' :
    (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
    (X : type-subuniverse P)  UU (lsuc l1  l2  l3)
  cauchy-exponential-species-subuniverse' S X =
    Σ ( Σ-Decomposition-Subuniverse P X)
      ( λ D 
        ( b : indexing-type-Σ-Decomposition-Subuniverse P X D) 
        ( inclusion-subuniverse
            ( subuniverse-global-subuniverse Q l3)
            ( S (subuniverse-cotype-Σ-Decomposition-Subuniverse P X D b))))

module _
  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
  ( C1 :
    ( {l4 : Level}
    (S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
    (X : type-subuniverse P) 
      is-in-subuniverse
        ( subuniverse-global-subuniverse Q (lsuc l1  l2  l4))
        ( cauchy-exponential-species-subuniverse' P Q S X)))
  where

  cauchy-exponential-species-subuniverse :
    species-subuniverse P (subuniverse-global-subuniverse Q l3) 
    species-subuniverse P (subuniverse-global-subuniverse Q (lsuc l1  l2  l3))
  pr1 (cauchy-exponential-species-subuniverse S X) =
    cauchy-exponential-species-subuniverse' P Q S X
  pr2 (cauchy-exponential-species-subuniverse S X) = C1 S X

Propositions

The Cauchy exponential in term of composition

module _
  {l1 l2 l3 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse id)
  (C1 :
    ( {l4 : Level}
    (S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
    (X : type-subuniverse P) 
      is-in-subuniverse
        ( subuniverse-global-subuniverse Q (lsuc l1  l2  l4))
        ( cauchy-exponential-species-subuniverse' P Q S X)))
  (C2 : is-in-subuniverse (subuniverse-global-subuniverse Q lzero) unit)
  (C3 : is-closed-under-cauchy-composition-species-subuniverse P Q)
  (C4 : is-closed-under-Σ-subuniverse P)
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (X : type-subuniverse P)
  where

  equiv-cauchy-exponential-composition-unit-species-subuniverse :
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1  l2  lzero  l3))
      ( cauchy-composition-species-subuniverse
        P Q C3 C4  _  unit , C2) S X) 
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3))
      ( cauchy-exponential-species-subuniverse P Q C1 S X)
  equiv-cauchy-exponential-composition-unit-species-subuniverse =
    equiv-tot λ _  left-unit-law-prod-is-contr is-contr-unit

Equivalence form with species of types

module _
  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
  ( C1 :
    {l4 : Level}
    (S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
    (X : type-subuniverse P) 
      is-in-subuniverse
        ( subuniverse-global-subuniverse Q (lsuc l1  l2  l4))
        ( cauchy-exponential-species-subuniverse' P Q S X))
  ( C2 :
    ( U : UU l1) 
    ( V : U  UU l1) 
    ( (u : U)  is-in-subuniverse P (V u)) 
    is-in-subuniverse P (Σ U V)  is-in-subuniverse P U)
  ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  ( X : type-subuniverse P)
  where

  private
    reassociate :
      Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3))
        ( cauchy-exponential-species-subuniverse P Q C1 S)
        ( inclusion-subuniverse P X) 
      Σ ( Relaxed-Σ-Decomposition l1 l1 (inclusion-subuniverse P X))
        ( λ (U , V , e) 
          Σ ( ( is-in-subuniverse P U × ((u : U)  is-in-subuniverse P (V u))) ×
              is-in-subuniverse P (inclusion-subuniverse P X))
            ( λ p  (u : U)  pr1 (S (V u , (pr2 (pr1 p)) u))))
    pr1 reassociate (pX , ((U , pU) , V , e) , s) =
      ((U , ((λ u  pr1 (V u)) , e)) , ((pU ,  u  pr2 (V u))) , pX) , s)
    pr2 reassociate =
      is-equiv-has-inverse
        ( λ ((U , V , e) , ( ((pU , pV), pX) , s)) 
          ( pX , ((U , pU) ,  u  V u , pV u) , e) , s))
        ( refl-htpy)
        ( refl-htpy)

    reassociate' :
      Σ ( Relaxed-Σ-Decomposition l1 l1 (inclusion-subuniverse P X))
        ( λ d 
           Σ ( ( u : (indexing-type-Relaxed-Σ-Decomposition d)) 
               is-in-subuniverse P (cotype-Relaxed-Σ-Decomposition d u))
             ( λ p 
               ( ( u : indexing-type-Relaxed-Σ-Decomposition d) 
                 inclusion-subuniverse
                   ( subuniverse-global-subuniverse Q l3)
                   ( S (cotype-Relaxed-Σ-Decomposition d u , p u)))))
        
        cauchy-exponential-species-types
          ( Σ-extension-species-subuniverse
              ( P)
              ( subuniverse-global-subuniverse Q l3)
              ( S))
        ( inclusion-subuniverse P X)
    pr1 reassociate' (d , pV , s) = d , ( λ u  (pV u) , (s u))
    pr2 reassociate' =
      is-equiv-has-inverse
        ( λ (d , f)  (d , pr1  f , pr2  f))
        ( refl-htpy)
        ( refl-htpy)

  equiv-cauchy-exponential-Σ-extension-species-subuniverse :
    Σ-extension-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3))
      ( cauchy-exponential-species-subuniverse P Q C1 S)
      ( inclusion-subuniverse P X) 
    cauchy-exponential-species-types
      ( Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l3)
        ( S))
      ( inclusion-subuniverse P X)
  equiv-cauchy-exponential-Σ-extension-species-subuniverse =
    ( reassociate') ∘e
    ( ( equiv-tot
        ( λ d 
          equiv-Σ-equiv-base
            ( λ p 
              ( u : indexing-type-Relaxed-Σ-Decomposition d) 
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l3)
                ( S (cotype-Relaxed-Σ-Decomposition d u , p u)))
            ( ( inv-equiv
                ( equiv-add-redundant-prop
                  ( is-prop-type-Prop
                    ( P (indexing-type-Relaxed-Σ-Decomposition d)))
                  ( λ pV 
                    C2
                      ( indexing-type-Relaxed-Σ-Decomposition d)
                      ( cotype-Relaxed-Σ-Decomposition d)
                      ( pV)
                      ( tr
                        ( is-in-subuniverse P)
                        ( eq-equiv
                          ( pr1 X)
                          ( Σ ( indexing-type-Relaxed-Σ-Decomposition d)
                              ( cotype-Relaxed-Σ-Decomposition d))
                          ( matching-correspondence-Relaxed-Σ-Decomposition d))
                        ( pr2 X))))) ∘e
              ( ( commutative-prod) ∘e
                ( inv-equiv
                  ( equiv-add-redundant-prop
                    ( is-prop-type-Prop (P (inclusion-subuniverse P X)))
                    ( λ _  pr2 X))))))) ∘e
      ( reassociate))

The Cauchy exponential of the sum of a species is equivalent to the Cauchy product of the exponential of the two species

module _
  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
  ( C1 :
    {l4 : Level}
    ( S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
    ( X : type-subuniverse P) 
      is-in-subuniverse
        ( subuniverse-global-subuniverse Q (lsuc l1  l2  l4))
        ( cauchy-exponential-species-subuniverse' P Q S X))
  ( C2 :
    {l4 l5 : Level}
    (S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
    (T : species-subuniverse P (subuniverse-global-subuniverse Q l5))
    (X : type-subuniverse P) 
      is-in-subuniverse
        ( subuniverse-global-subuniverse Q (l4  l5))
        ( coproduct-species-subuniverse' P Q S T X))
  ( C3 : is-closed-under-cauchy-product-species-subuniverse P Q)
  ( C4 :
    ( U : UU l1) 
    ( V : U  UU l1) 
    ( (u : U)  is-in-subuniverse P (V u)) 
      ( is-in-subuniverse P (Σ U V)) 
      ( is-in-subuniverse P U))
  ( C5 : is-closed-under-coproducts-subuniverse P)
  ( C6 :
    ( A B : UU l1) 
    is-in-subuniverse P (A + B) 
    is-in-subuniverse P A × is-in-subuniverse P B)
  ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  ( T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  ( X : type-subuniverse P)
  where

  equiv-cauchy-exponential-sum-species-subuniverse :
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3  l4))
      ( cauchy-exponential-species-subuniverse P Q C1
        ( coproduct-species-subuniverse P Q C2 S T) X) 
    inclusion-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3  l4))
      ( cauchy-product-species-subuniverse P Q C3
        ( cauchy-exponential-species-subuniverse P Q C1 S)
        ( cauchy-exponential-species-subuniverse P Q C1 T)
        ( X))
  equiv-cauchy-exponential-sum-species-subuniverse =
    ( ( inv-equiv
        ( equiv-Σ-extension-species-subuniverse
          ( P)
          ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3  l4))
          ( cauchy-product-species-subuniverse P Q C3
            ( cauchy-exponential-species-subuniverse P Q C1 S)
            ( cauchy-exponential-species-subuniverse P Q C1 T))
          ( X))) ∘e
      ( ( inv-equiv
          ( equiv-cauchy-product-Σ-extension-species-subuniverse
            ( P)
            ( Q)
            ( C3)
            ( C5)
            ( cauchy-exponential-species-subuniverse P Q C1 S)
            ( cauchy-exponential-species-subuniverse P Q C1 T)
            ( inclusion-subuniverse P X))) ∘e
        ( ( equiv-tot
            ( λ d 
              equiv-prod
                ( inv-equiv
                  ( equiv-cauchy-exponential-Σ-extension-species-subuniverse
                    ( P)
                    ( Q)
                    ( C1)
                    ( C4)
                    ( S)
                    ( left-summand-binary-coproduct-Decomposition d ,
                      pr1 (lemma-C6 d))))
                ( inv-equiv
                  ( equiv-cauchy-exponential-Σ-extension-species-subuniverse
                    ( P)
                    ( Q)
                    ( C1)
                    ( C4)
                    ( T)
                    ( right-summand-binary-coproduct-Decomposition d ,
                      pr2 (lemma-C6 d)))))) ∘e
          ( ( equiv-cauchy-exponential-sum-species-types
              ( Σ-extension-species-subuniverse
                ( P)
                ( subuniverse-global-subuniverse Q l3)
                ( S))
              ( Σ-extension-species-subuniverse
                ( P)
                ( subuniverse-global-subuniverse Q l4)
                ( T))
              ( pr1 X)) ∘e
            ( ( equiv-tot
                ( λ d 
                  equiv-Π
                    ( λ x 
                      coproduct-species-types
                        ( Σ-extension-species-subuniverse
                          ( P)
                          ( subuniverse-global-subuniverse Q l3)
                          ( S))
                        ( Σ-extension-species-subuniverse
                          ( P)
                          ( subuniverse-global-subuniverse Q l4)
                          ( T))
                        ( cotype-Relaxed-Σ-Decomposition d x))
                    ( id-equiv)
                    ( λ x 
                      equiv-coproduct-Σ-extension-species-subuniverse
                        ( P)
                        ( Q)
                        ( C2)
                        ( S)
                        ( T)
                        ( cotype-Relaxed-Σ-Decomposition d x)))) ∘e
              ( ( equiv-cauchy-exponential-Σ-extension-species-subuniverse
                  ( P)
                  ( Q)
                  ( C1)
                  ( C4)
                  ( coproduct-species-subuniverse P Q C2 S T)
                  ( X)) ∘e
                ( equiv-Σ-extension-species-subuniverse
                  ( P)
                  ( subuniverse-global-subuniverse Q (lsuc l1  l2  l3  l4))
                  ( cauchy-exponential-species-subuniverse P Q C1
                    ( coproduct-species-subuniverse P Q C2 S T))
                  ( X))))))))
    where
    lemma-C6 =
      λ d 
      C6
        ( left-summand-binary-coproduct-Decomposition d)
        ( right-summand-binary-coproduct-Decomposition d)
        ( tr
          ( is-in-subuniverse P)
          ( eq-equiv
            ( inclusion-subuniverse P X)
            ( left-summand-binary-coproduct-Decomposition d +
              right-summand-binary-coproduct-Decomposition d)
            ( matching-correspondence-binary-coproduct-Decomposition d))
          ( pr2 X))