We need to disable the K-Axiom, which is incompatible with Homotopy type theory

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

In agda Set denotes the universe of small types. somelink

The emtpy type is the type with no elements. It can be interpreted as a proposition that has no proofs.

data 𝟘 : Set where

The elimination rule for elements of the empty type yields an element of any depended type indexed by x : 𝟘. This is analogous to the idea, that you can prove anything from falsehood.

𝟘-elim : {A : 𝟘 → Set} (x : 𝟘) → A x
𝟘-elim ()

Note that () refers to the impossible match. Since there is no x : A, there is nothing to define for that branch.

We can define negation as a map that sends any type A : Set to A -> 𝟘 : Set.

neg : Set -> Set
neg A = A -> 𝟘