For completness, I wrote here<http://www.cse.chalmers.se/~coquand/fac.pdf> the semantics of some HIT (the circle and the
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.)
 Thierry