# Equivalences of species of types in subuniverses

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-27.

module species.equivalences-species-of-types-in-subuniverses where

Imports
open import foundation.equivalences
open import foundation.identity-types
open import foundation.subuniverses
open import foundation.universe-levels

open import species.species-of-types-in-subuniverses


## Idea

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

## Definition

equiv-species-subuniverse :
{l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : subuniverse l1 l3) →
species-subuniverse P Q → species-subuniverse P Q →
UU (lsuc l1 ⊔ l2)
equiv-species-subuniverse {l1} P Q S T =
(X : type-subuniverse P) →
inclusion-subuniverse Q (S X) ≃ inclusion-subuniverse Q (T X)


## Properties

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

extensionality-species-subuniverse :
{l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : subuniverse l1 l3) →
(S : species-subuniverse P Q) → (T : species-subuniverse P Q) →
(Id S T) ≃ (equiv-species-subuniverse P Q S T)
extensionality-species-subuniverse P Q S T =
extensionality-fam-subuniverse Q S T