Dirichlet exponentials of a species of types

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

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

module species.dirichlet-exponentials-species-of-types where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.arithmetic-law-product-and-pi-decompositions
open import foundation.cartesian-product-types
open import foundation.coproduct-decompositions
open import foundation.dependent-binomial-theorem
open import foundation.dependent-pair-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.homotopies
open import foundation.identity-types
open import foundation.pi-decompositions
open import foundation.product-decompositions
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universe-levels

open import species.coproducts-species-of-types
open import species.dirichlet-products-species-of-types
open import species.equivalences-species-of-types
open import species.species-of-types

Idea

The Dirichlet exponential of a species of types S is defined as follows:

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

Definition

dirichlet-exponential-species-types :
  {l1 l2 : Level} → species-types l1 l2 → species-types l1 (lsuc l1 ⊔ l2)
dirichlet-exponential-species-types {l1} {l2} S X =
  Σ ( Π-Decomposition l1 l1 X)
    ( λ D →
      ( b : indexing-type-Π-Decomposition D) →
      ( S (cotype-Π-Decomposition D b)))

Properties

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

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

  private
    reassociate :
      ( X : UU l1) →
      Σ ( Σ ( binary-product-Decomposition l1 l1 X)
            ( λ d →
              ( Π-Decomposition l1 l1
                ( left-summand-binary-product-Decomposition d)) ×
              ( Π-Decomposition l1 l1
                ( right-summand-binary-product-Decomposition d))))
        ( λ D →
          ( ( b : indexing-type-Π-Decomposition (pr1 (pr2 D))) →
            S ( cotype-Π-Decomposition (pr1 (pr2 D)) b)) ×
          ( ( b : indexing-type-Π-Decomposition (pr2 (pr2 D))) →
            T ( cotype-Π-Decomposition (pr2 (pr2 D)) b))) ≃
      dirichlet-product-species-types
        ( dirichlet-exponential-species-types S)
        ( dirichlet-exponential-species-types T)
        ( X)
    pr1 (reassociate X) ((d , dl , dr) , s , t) =
      ( d , (dl , s) , dr , t)
    pr2 (reassociate X) =
      is-equiv-is-invertible
        ( λ ( d , (dl , s) , dr , t) → ((d , dl , dr) , s , t))
        ( refl-htpy)
        ( refl-htpy)

  equiv-dirichlet-exponential-sum-species-types :
    equiv-species-types
      ( dirichlet-exponential-species-types (coproduct-species-types S T))
      ( dirichlet-product-species-types
        ( dirichlet-exponential-species-types S)
        ( dirichlet-exponential-species-types T))
  equiv-dirichlet-exponential-sum-species-types X =
    ( reassociate X) ∘e
    ( ( equiv-Σ
        ( λ D →
          ( ( b : indexing-type-Π-Decomposition (pr1 (pr2 D))) →
            S (cotype-Π-Decomposition (pr1 (pr2 D)) b)) ×
          ( ( b : indexing-type-Π-Decomposition (pr2 (pr2 D))) →
            T (cotype-Π-Decomposition (pr2 (pr2 D)) b)))
        ( equiv-binary-product-Decomposition-Π-Decomposition)
        ( λ D →
          equiv-product
            ( equiv-Π-equiv-family
              ( λ a' →
                equiv-eq
                  ( ap S
                    ( inv
                      ( compute-left-equiv-binary-product-Decomposition-Π-Decomposition
                        ( D)
                        ( a'))))))
            ( equiv-Π-equiv-family
              ( λ b' →
                equiv-eq
                  ( ap T
                    ( inv
                      ( compute-right-equiv-binary-product-Decomposition-Π-Decomposition
                        ( D)
                        ( b')))))))) ∘e
      ( ( inv-associative-Σ
          ( Π-Decomposition l1 l1 X)
          ( λ d →
            binary-coproduct-Decomposition l1 l1
              ( indexing-type-Π-Decomposition d))
              ( _)) ∘e
        ( equiv-tot
          ( λ d → distributive-Π-coproduct-binary-coproduct-Decomposition))))

Recent changes