This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Separated types

module orthogonal-factorization-systems.separated-types where

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-map-separated-family : (X → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
  is-map-separated-family A = (x : X) (y z : A x) → is-local f (y ＝ z)

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

References

[Rij19]

Egbert Rijke. Classifying Types. PhD thesis, Carnegie Mellon University, 06 2019. arXiv:1906.09435.