here's a point:

data P : Set where
  ∙ : P

congrats now you know (-2)-category theory