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

[Vladimir Voevodsky]

On Jan 8, 2014, at 12:40 PM, Cody Roux <cody.roux at andrew.cmu.edu> wrote:
>>=20

> That's fair, but I don't see why eliminators have a more powerful
> ontological status than sized-types. They require work to be derived =
as
> well, and the correctness proofs for them are quite similar to that =
for
> sized types. This seems like a matter of preference. Obviously I'm not
> neutral in this matter though.
>=20
> Best,
>=20
> Cody
>=20

In the case of the univalent model eliminators are better because I have =
invested a lot of effort into checking that they are compatible with the =
model (some details of it are at the end of my "Notes on Type Systems").

No other work of this kind has been done as far as I know.=20

Vladimir.