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

Pointing of species of types

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

open import species.species-of-types

Idea

A pointing of a species of types F is the species of types F* given by F* X := X × (F X). In other words, it is the species of pointed F-structures

Definition

pointing-species-types :
  {l1 l2 : Level} → species-types l1 l2 → species-types l1 (l1 ⊔ l2)
pointing-species-types F X = X × F X