Issue274.agda

module Issue274 where

-- data ⊥ : Set where

record U : Set where
  constructor roll
  field ap : U → U

-- lemma : U → ⊥
-- lemma (roll u) = lemma (u (roll u))

-- bottom : ⊥
-- bottom = lemma (roll λ x → x)