Equivalences 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.equivalences-species-of-types where
Imports 
open import foundation.equivalences
open import foundation.identity-types
open import foundation.univalence
open import foundation.universe-levels

open import species.species-of-types

Idea

An equivalence of species of types from F to G is a pointwise equivalence.

Definition

equiv-species-types :
  {l1 l2 l3 : Level} → species-types l1 l2 → species-types l1 l3 →
  UU (lsuc l1 ⊔ l2 ⊔ l3)
equiv-species-types {l1} F G = ((X : UU l1) → F X ≃ G X)

Properties

The identity type of two species of types is equivalent to the type of equivalences between them

extensionality-species-types :
  {l1 l2 : Level} (F G : species-types l1 l2) →
  (F ＝ G) ≃ (equiv-species-types F G)
extensionality-species-types = extensionality-fam

Recent changes