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
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

Recent changes