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

[Matthieu Sozeau]

On 9 janv. 2014, at 00:31, Vladimir Voevodsky <vladimir at ias.edu> wrote:

> 
> 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 ) .

Well, take the transitive closure of p <_le le_succ n m p.
— Matthieu