UniAgda.Core.Types.FiniteSets

Table of Contents

1 Prelude

2 Finite sets

We give the definition of the \(n\)th ordinal.

Fin :   Type lzero
Fin zero = Empty
Fin (suc n) = Fin n + Unit

We will prove that these are sets in a different file.

Author: James Leslie

Created: 2021-03-27 Sat 10:47