Pointing of species of types

Content created by Egbert Rijke, Fredrik Bakke and Victor Blanchi.

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

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

open import species.species-of-types


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


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

Recent changes