This article is about locally finite types in dependent type theory. For the notion of homomorphisms between schemes which are locally of finite type, see morphism of finite type.

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

In dependent type theory, a **locally finite type** is a type $A$ such that for all elements $x:A$ and $y:A$, there is a natural number $n:\mathbb{N}$ and an equivalence of types between the identity type $x =_A y$ and the standard finite type $\mathrm{Fin}(n)$.

The type of all finite types is a univalent universe $Fin$; thus one could also refer to a locally finite type as a **locally $Fin$-small type**, since locally finite types are precisely the types that are locally small relative to the univalent universe $Fin$ of finite types.

Every locally finite univalent category is a locally finite type.

The locally finite h-sets are precisely the h-sets with decidable equality

Since finite types are h-sets, every locally finite type is an h-groupoid, because its identity types are all h-sets. In particular, locally finite types are precisely the locally finite univalent categories which are groupoids.

Last revised on August 15, 2023 at 14:35:31. See the history of this page for a list of all contributions to it.