In mathematics, Joyal's theorem is a theorem in homotopy theory that provides necessary and sufficient conditions for the solvability of a certain lifting problem involving simplicial sets. In particular, in higher category theory, it proves the statement "an ∞-groupoid is a Kan complex", which is a version of the homotopy hypothesis.
The theorem was introduced by André Joyal.
Joyal extension theorem.
Let formula_1 be quasicategory and let formula_2 be a morphism of formula_1. The following conditions are equivalent:
(1) The morphism formula_4 is an isomorphism.
(2) Let formula_5 and let formula_6 be a morphism of simplicial sets for which the initial edge
formula_7
is equal to formula_4. Then formula_9 can be extended to an "n"-simplex formula_10.
(3) Let formula_5 and let formula_12 be a morphism of simplicial sets for which the initial edge
formula_13
is equal to formula_4. Then formula_9 can be extended to an "n"-simplex formula_10.
Joyal lifting theorem.
Let formula_17 be an inner fibration (Joyal used mid-fibration) between quasicategories, and let formula_18 be an edge such that formula_19 is an isomorphism in formula_20. The following are equivalent:
(1) The edge formula_21 is an isomorphism in formula_1.
(2) For all formula_5, every diagram of the form
admits a lift.
(3) For all formula_5, every diagram of the form
admits a lift.