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

[Bruno Barras]

On 09/01/2014 11:40, Matthieu Sozeau wrote:
> Hi,
>
>    I can’t speak for Andrej, but my point was not to disqualify sized-types,
> they are a fine, evidence-based foundation, just like wellfounded relations,
> to define recursive definitions. The nice thing about wellfounded relations
> is that they are readily available, supposing we have at least eliminators.
> I’m curious about the respective expressive power of both, my gut feeling is
> that w.f. relations are most general but this is not backed up by anything
> formal. My question about sized types is how do you justify definitions
> on big ordinals defined *in* the type theory using the metatheoretical ordinals.
> It might reduce to Bruno’s [… and the fact that those ordinals are not used in the
> process you iterate…] and be a solved question. Then Andrej might be worried that
> the metatheory has to be classical if you use ordinals (?) (but for wfs it wouldn’t
> be??).

The metatheory does not need to be classical. When I talked about 
ordinals, I meant "something you can use to iterate long enough". No 
need for the well-ordering property to justify inductive definitions, 
for both the sized-types or the recursor-based approaches (the former 
implies the latter).

I use Paul Taylor's directed plump ordinals, and you can go a long way 
with them. The strictly positive inductive types of Coq (those in Type) 
can be modeled (to prove consistency and SN) in IZF with replacement. If 
you include those in Prop, then I did manage to go through using the 
collection axiom, but still without excluded-middle. (BTW, I'm talking 
of machine checked proofs.)

Bruno.