  We introduce the notion of an effective Kan fibration, a new mathematical
structure that can be used to study simplicial homotopy theory. Our main
motivation is to make simplicial homotopy theory suitable for homotopy type
theory. Effective Kan fibrations are maps of simplicial sets equipped with a
structured collection of chosen lifts that satisfy certain non-trivial
properties. This contrasts with the ordinary, unstructured notion of a Kan
fibration. We show that fundamental properties of Kan fibrations can be
extended to explicit constructions on effective Kan fibrations. In particular,
we give a constructive (explicit) proof showing that effective Kan fibrations
are stable under push forward, or fibred exponentials. This is known to be
impossible for ordinary Kan fibrations. We further show that effective Kan
fibrations are local, or completely determined by their fibres above
representables. We also give an (ineffective) proof saying that the maps which
can be equipped with the structure of an effective Kan fibration are precisely
the ordinary Kan fibrations. Hence implicitly, both notions still describe the
same homotopy theory. By showing that the effective Kan fibrations combine all
these properties, we solve an open problem in homotopy type theory. In this way
our work provides a first step in giving a constructive account of Voevodsky's
model of univalent type theory in simplicial sets.
