3 ms·

Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).

• caotic123 5y ago
  As far i know, pompom has a decidable type check though.