Cartesian exponents of species

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-27.
Last modified on 2023-04-28.

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

Recent changes