# Separated types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.

module foundation.separated-types where

Imports
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)