Derivatives of species

Content created by Fredrik Bakke and Victor Blanchi.

Created on 2023-03-21.
Last modified on 2023-03-21.

module species.derivatives-species-of-types where
Imports 
open import foundation.coproduct-types
open import foundation.unit-type
open import foundation.universe-levels

open import species.species-of-types

Idea

When we think of a species of types as the coefficients of a formal power series, the derivative of a species of types is the species of types representing the derivative of that formal power series.

Definition

derivative-species-types :
  {l1 l2 : Level} → species-types l1 l2 → species-types l1 l2
derivative-species-types F X = F (X + unit)

Recent changes