Homotopy Type Theory finite type > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


Given natural numbers n:β„•n:\mathbb{N}, the type of finite types Fin 𝒰(n)\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} are inductively defined by

Fin 𝒰(0)β‰”βˆ‘ A:𝒰Aβ‰… π’°βˆ… 𝒰\mathrm{Fin}_\mathcal{U}(0) \coloneqq \sum_{A:\mathcal{U}} A \cong_\mathcal{U} \emptyset_\mathcal{U}
Fin 𝒰(s(n))β‰”βˆ‘ A:𝒰[βˆ‘ B:Fin 𝒰(n)Aβ‰… 𝒰B+ π’°πŸ™ 𝒰]\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]

See also


Revision on June 10, 2022 at 13:08:15 by Anonymous?. See the history of this page for a list of all contributions to it.