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

Large identity types

module foundation.large-identity-types where

open import foundation.universe-levels

Definition

module _
  {A : UUω}
  where

  data Idω (x : A) : A → UUω where
    reflω : Idω x x

  _＝ω_ : A → A → UUω
  (a ＝ω b) = Idω a b