[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Andrej Bauer]

I would just like to point out that ordinals are an inherently
classical notion. The correct constructive and computationally
meaningful replacement is that of a well-founded relation, i.e., a
relation < on a set X satisfying, for all properties P,

 (forall y, ((forall x < y, P x) -> P y)) -> forall z, P z.

This is all well known, and of course you can recognize the
recursor/eliminator in the above formula. So if we are to take
computation seriously, we ought to think about inductive definitions
which are justified by a more general notion of well foundedness, not
just ordinals. The ordinals are bound to go wrong when we push them a
little bit.

Also, the HoTT experience has thought us (at least me) the value of
semantic notions over syntactic ones. I am referring to HoTT hProp vs.
CiC Prop. The former delineates the concept of "proposition" with a
semantic condition, while the latter does it formalistically. It would
seem sensible to me to go the same route with inductive definitions,
namely, rely on semantic justifications rather than syntactic ones. [I
may be misusing the words "semantic" and "syntactic" here, but I
cannot think of better ones.]

With kind regards,

Andrej