Pointing of species of types

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

Created on 2023-03-21.
Last modified on 2025-08-30.

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