nLab finitely complete type

Idea

The concept of finitely complete in simplicial type theory. Note that in the context of simplicial type theory, finitely complete makes sense for any type, not just the Segal types.

Definition

In simplicial type theory, a type $A$ is finitely complete if

• $A$ has a terminal object $1:A$

• There is a pullback $x \times_z^{f, g} y:A$ for all elements $x:A$, $y:A$, $z:A$ and morphisms $f:\mathrm{hom}_A(x, z)$ and $g:\mathrm{hom}_A(y, z)$.

Equivalenty, a type $A$ is finitely complete if

• $A$ has a terminal object $1:A$

• All elements $x:A$ and $y:A$ have a product $x \times y:A$

• All elements $x:A$ and $y:A$ and morphisms $f:\mathrm{hom}_A(x, y)$ and $g:\mathrm{hom}_A(x, y)$ have an equalizer $\mathrm{eq}(f, g):A$

If A is a Rezk type then this notion coincides with the usual notion of finitely complete (infinity,1)-category.

Related concepts

• simplicial type theory

• finitely complete

• finitely complete (infinity,1)-category

• finitely cocomplete type