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

[Frédéric Blanqui]

In fact, for this definition, you need no big ordinals. Iteration up to 
the first infinite ordinal \omega (i.e. on natural numbers) is enough to 
construct the semantics of [le]. But for types having constructors 
taking functions as arguments, it is necessary to use transfinite 
ordinals. For instance, with:

Inductive ord : Type :=
   | Z : ord
   | S : ord -> ord
   | L : (nat -> ord) -> ord.

The term (L f) where f is the injection of nat into ord has size (in the 
models used in size-base termination) \omega+1.

Frédéric.


Le 09/01/2014 00:31, Vladimir Voevodsky a écrit :
> 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.
>
>