The unit of Cauchy composition of species of types in subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2026-05-02.

module species.unit-cauchy-composition-species-of-types-in-subuniverses where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.dependent-products-contractible-types
open import foundation.global-subuniverses
open import foundation.subuniverses
open import foundation.subuniverses-containing-contractible-types
open import foundation.universe-levels

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

Idea

Given a global subuniverse closed under is-contr, we define the unit of the Cauchy composition of species of types in a subuniverse by

  X ↦ is-contr X.

Definition

module _
  {α : Level → Level} {l1 l2 : Level}
  (P : subuniverse l1 l2) (Q : global-subuniverse α)
  (C4 :
    is-closed-under-is-contr-subuniverses P
      ( subuniverse-global-subuniverse Q l1))
  where

  cauchy-composition-unit-species-subuniverse :
    species-subuniverse P (subuniverse-global-subuniverse Q l1)
  cauchy-composition-unit-species-subuniverse X =
    (is-contr (inclusion-subuniverse P X) , C4 X)

Recent changes