Definition
A finite presentable type is a type whose presentation uses a finite signature: finitely many sorts, finitely many constructors, and a finite telescope for each constructor. What may still be infinitary is the shape of an argument type. For example, is infinitary because it takes a -indexed family of elements of as input. By contrast, an expression such as is not itself a valid finite presentation of a constructor.
Motivation
In type theory, one typically requires types and terms to be finitely presentable. This matters especially in the presence of polymorphism and dependent terms, where terms are meant to encode programs. If terms are allowed to depend on non-finitely-presentable data, then one can model objects such as lawless functions or choice sequences, which go beyond the usual computational reading of type theory.
From an intuitionistic perspective, non-finitely-presentable types can therefore have more strength than is usually accepted as constructive. They can encode completed infinite data in a way that is no longer computationally feasible; for example, such presentations can be used in arguments that amount to encoding solutions to the halting problem. For this reason, followers of Brouwer often regard such completed infinities as undesirable in foundational type theory.