Yeah, I just wanted to show that (GHC) haskell has a way of getting a type with "zero" inhabitants that actually gets caught by the type checker. (I say "zero"

Yeah, I just wanted to show that (GHC) haskell has a way of getting a type with "zero" inhabitants that actually gets caught by the type checker. (I say "zero" since of course my Empty-type above does contain non-terminating programs and (undefined :: a).) With "forall a. a" I was coming from the persepctive of intuisionistic type theory where the usual parametric polymorphism just get subsumed by Π-types and universal quantification is usually represented with Π-types, so you would have: forall a.a (Universal Quantification) <==> Π(a : Type) a (Π-type) <==> (a : Type) -> a (Agda-notation) ==> a -> a (Π-type as regular function type) where Type represents any type. That's what I meant by "type-level identity function".