trivial cofibration-fibration factorisation of a map) in constructive set theory.

Since one has to define inductively at the same time a family of sets and

suitable maps between these sets, this is an example of an indexed

inductive-recursive definition, and one can follow Stuart Allen’s idea

(LICS 1987) of defining by induction instead relations which should represent

the -graphs- of these functions, and prove then by induction that these are functional graphs.

(This replaces the transfinite induction of the small object argument.)