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

[Vladimir Voevodsky]

On Jan 8, 2014, at 5:19 PM, Andrej Bauer <andrej.bauer at andrej.com> wrote:

> It would
> seem sensible to me to go the same route with inductive definitions,
> namely, rely on semantic justifications rather than syntactic ones. 

This would certainly be cool. What I do not quite understand however is what ordinals or well-founded relations have with such inductive definition as, for example, the definition of "less or equal" on nat in the Coq standard library?

(It's something like:

Inductive le : forall ( n m : nat ) , Type := le_refl : forall ( n : nat ) , le n n | le_succ : forall ( n m : nat ) , le n m -> le (S n ) ( S m ) .

)

V.