universe-hierarchy-not-inconsistent.idr

%default total

codata Level : Type where
  S : Level -> Level

sInjective' : (x : Level) -> (y : Level) -> S (Delay x) = S (Delay (Force (Delay (S (Delay y))))) -> x = S (Delay (Force (Delay y)))
sInjective' _ y Refl = replace {P = \level => S (Delay y) = S (Delay level)} Refl Refl

levelNotSLevel' : (level : Lazy' LazyCodata Level) -> Not ((Force level) = S level)
levelNotSLevel' (S (Delay level)) p = levelNotSLevel' level (sInjective' level level p)

sInjective : (x : Level) -> (y : Level) -> S (Delay x) = S (Delay (S (Delay y))) -> x = S (Delay (Force (Delay y)))
sInjective _ y Refl = replace {P = \level => S (Delay y) = S (Delay level)} Refl Refl

levelNotSLevel : (level : Level) -> Not (level = S (Delay level))
levelNotSLevel (S (Delay level)) p = levelNotSLevel' level (sInjective level level p)