# nLab locally finite type

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.

# Contents

## Definition

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.

## Examples

###### Example

Every locally finite univalent category is a locally finite type.

###### Example

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

## Properties

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.