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
open import foundation.universe-levels

open import species.species-of-types


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.


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