⊥ : Type;
⊥ = {};

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

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

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

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