Types separated at subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-11-19.
Last modified on 2026-05-02.

module foundation.separated-types-subuniverses where
Imports 
open import foundation.dependent-products-propositions
open import foundation.subuniverses
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.propositions

Idea

Consider a subuniverse P. A type A is said to be P-separated if its identity types are in P. Similarly, a type A is said to be essentially P-separated if its identity types are equivalent to types in P.

Definitions

The predicate of being separated

module _
  {l1 l2 : Level} (P : subuniverse l1 l2)
  where

  is-separated-Prop : (X : UU l1) → Prop (l1 ⊔ l2)
  is-separated-Prop X = Π-Prop X (λ x → Π-Prop X (λ y → P (x ＝ y)))

  is-separated : (X : UU l1) → UU (l1 ⊔ l2)
  is-separated X = type-Prop (is-separated-Prop X)

  is-prop-is-separated : (X : UU l1) → is-prop (is-separated X)
  is-prop-is-separated X = is-prop-type-Prop (is-separated-Prop X)

The predicate of being essentially separated

module _
  {l1 l2 : Level} (P : subuniverse l1 l2)
  where

  is-essentially-separated : {l3 : Level} (X : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3)
  is-essentially-separated X =
    (x y : X) → is-essentially-in-subuniverse P (x ＝ y)

Recent changes