Definition. Set [005N]

A set is an object in ZFC – thus subject to the ZFC-Axioms.

Backlinks

Definition. small Category [005M]

We call a category small if it's morphisms fit in a set.

Definition. locally small category [005O]

A category is locally small if for any two objects, the morphisms between them fit in a set.

The Empty Type [005P.lagda]

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 -> 𝟘