{-# OPTIONS --without-K  #-}

module sets.unit where

record  : Set where
  constructor tt

⊤-elim : (P :   Set)  P tt  (x : )  P x
⊤-elim P ptt tt = ptt