⊥ : Type;
⊥ = {};

-- Curry's paradox (usually ruled out by positivity check).

A : Type;
A = [A] → ⊥;

¬A : A → ⊥;
¬A = λ x → x x;

contradiction : ⊥;
contradiction = ¬A (λ x → ¬A x);