This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Cartesian exponents of species

module species.cartesian-exponents-species-of-types where
Imports 
open import foundation.universe-levels

open import species.species-of-types

Idea

The Cartesian exponent of two species F and G is the pointwise exponent of F and G.

Note that we call such exponents cartesian to disambiguate from other notions of exponents, such as Cauchy exponentials.

Definitions

Cartesian exponents of species of types

function-species-types :
  {l1 l2 l3 : Level} →
  species-types l1 l2 → species-types l1 l3 → species-types l1 (l2 ⊔ l3)
function-species-types F G X = F X → G X