Separated types

Content created by Fredrik Bakke.

Created on 2023-06-08.
Last modified on 2023-06-28.

module orthogonal-factorization-systems.separated-types where
Imports 
open import foundation.identity-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-types

Idea

A type A is said to be separated with respect to a map f, or f-separated, if its identity types are f-local.

Definition

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (f : X → Y)
  where

  is-separated-family : (X → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
  is-separated-family A = (x : X) (y z : A x) → is-local f (y ＝ z)

  is-separated : UU l3 → UU (l1 ⊔ l2 ⊔ l3)
  is-separated A = is-separated-family (λ _ → A)

References

  1. Egbert Rijke, Classifying Types (arXiv:1906.09435, doi:10.48550)

Recent changes