Large identity types

{-# OPTIONS --safe #-}
module foundation.large-identity-types where

open import foundation-core.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