module Issue117 where

Set′ = Set

record ⊤ : Set′ where
data   ⊥ : Set′ where