Subuniverses containing contractible types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2026-05-02.
Last modified on 2026-05-02.

module foundation.subuniverses-containing-contractible-types where
Imports 
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.subuniverses

Idea

We define the predicate on subuniverses that they contain a contractible type.

Definitions

The predicate that a subuniverse contains any contractible types

contains-contractible-types-subuniverse :
  {l1 l2 : Level} → subuniverse l1 l2 → UU (lsuc l1 ⊔ l2)
contains-contractible-types-subuniverse {l1} P =
  (X : UU l1) → is-contr X → is-in-subuniverse P X

The predicate that a subuniverse is closed under the is-contr predicate

We state a general form involving two universes, and a more traditional form using a single universe

is-closed-under-is-contr-subuniverses :
  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : subuniverse l1 l3) →
  UU (lsuc l1 ⊔ l2 ⊔ l3)
is-closed-under-is-contr-subuniverses P Q =
  (X : type-subuniverse P) →
  is-in-subuniverse Q (is-contr (inclusion-subuniverse P X))

is-closed-under-is-contr-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2)
is-closed-under-is-contr-subuniverse P =
  is-closed-under-is-contr-subuniverses P P

Recent changes