Large identity types

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-23.
Last modified on 2023-06-10.

module foundation.large-identity-types where
Imports 
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

Recent changes