UniAgda.Core.Types.Empty

Table of Contents

1 Prelude

2 Empty Type

The empty type is an inductive type with no elements defined.

data Empty : Type lzero where

3 Induction

The induction principle is defined as follows:

Empty-ind :  {i} {A : Type i}
             Empty  A
Empty-ind ()

4 Negation

The empty type allows us to define logical negation.

¬ :  {i}
    (A : Type i)
     Type i
¬ A = A  Empty
infix 50 ¬

Author: James Leslie

Created: 2021-03-27 Sat 10:47