Contents

# Contents

## Idea

The counterpart of finite sets in type theory

## Definition

In type theory, given natural numbers $n:\mathbb{N}$, the family of finite types $\mathrm{Fin}_\mathcal{U}(n)$ of a universe $\mathcal{U}$ with empty type $\emptyset_\mathcal{U}:\mathcal{U}$, unit type $\mathbb{1}_\mathcal{U}:\mathcal{U}$, and binary coproducts $(-)+_\mathcal{U}(-):\mathcal{U} \times \mathcal{U} \to \mathcal{U}$ is an inductive family inductively defined by

$\mathrm{Fin}_\mathcal{U}(0) \coloneqq \sum_{A:\mathcal{U}} A \cong_\mathcal{U} \emptyset_\mathcal{U}$
$\mathrm{Fin}_\mathcal{U}(s(n)) \coloneqq \sum_{A:\mathcal{U}} \left[\sum_{B:\mathrm{Fin}_\mathcal{U}(n)} A \cong_\mathcal{U} B +_\mathcal{U} \mathbb{1}_\mathcal{U}\right]$