The zero cardinal

Content created by Fredrik Bakke.

Created on 2026-02-16.
Last modified on 2026-02-16.

module set-theory.zero-cardinal where
Imports 
open import foundation.empty-types
open import foundation.universe-levels

open import set-theory.cardinals

Idea

The zero cardinal, or empty cardinal, is the isomorphism class of empty sets.

Definitions

zero-Cardinal : Cardinal lzero
zero-Cardinal = cardinality empty-Set

Recent changes