Let be simplicial maps. We say that
is homotopic to
(denoted by
) if there exists a simplicial map
such that
and
for all
. If
is a simplicial subset of
and
are simplicial maps such that
, we say that
if there is a homotopy
such that
,
and
for all
,
,
.
Let be a simplicial set. The elements
are said to be matching faces with respect to
if
for
and
.
A simplicial set is said to be fibrant (or Kan complex) if it satisfies the following homotopy extension condition for each
:
Let be any elements that are matching faces with respect to
. Then there exists an element
such that
for
.
We define as the simplicial subset of
generated by all
for
, where
is the nondegenerate element.
Proposition: Let be a simplicial set. Then
is fibrant if and only if every simplicial map
has an extension for each
.