# Exponential of Cauchy series of species of types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2023-04-27.

module species.exponentials-cauchy-series-of-types where
Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.unit-type
open import foundation.universe-levels

open import species.cauchy-composition-species-of-types
open import species.cauchy-exponentials-species-of-types
open import species.cauchy-series-species-of-types
open import species.composition-cauchy-series-species-of-types
open import species.species-of-types

## Definition

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

exponential-cauchy-series-species-types :
UU (lsuc l1  l2  l3)
exponential-cauchy-series-species-types =
Σ ( UU l1)
( λ F  F  (Σ ( UU l1)  U  S U × (U  X))))

## Properties

### The exponential of a Cauchy series as a composition

equiv-exponential-cauchy-series-composition-unit-species-types :
composition-cauchy-series-species-types  _  unit) S X
exponential-cauchy-series-species-types
equiv-exponential-cauchy-series-composition-unit-species-types =
equiv-tot λ F  left-unit-law-product-is-contr is-contr-unit

### The Cauchy series associated to the Cauchy exponential of S is equal to the exponential of its Cauchy series

equiv-cauchy-series-cauchy-exponential-species-types :
cauchy-series-species-types (cauchy-exponential-species-types S) X
exponential-cauchy-series-species-types
equiv-cauchy-series-cauchy-exponential-species-types =
( equiv-exponential-cauchy-series-composition-unit-species-types) ∘e
( ( equiv-cauchy-series-composition-species-types  _  unit) S X) ∘e
( equiv-cauchy-series-equiv-species-types
( cauchy-exponential-species-types S)
( cauchy-composition-species-types  _  unit) S)
( λ F
inv-equiv
( equiv-cauchy-exponential-composition-unit-species-types S F))
( X)))