The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

But I explicitly require that Q map to Type... I see now that Coq is
lying to me, because "Print Q" leads me to believe that Q maps into
Type (it says "Inductive Q (x : A) : A -> Type :=  horn : Q x x"),
whereas

Parameter a : A.
Check (Q a).

tells me that Q a is in Prop. Can I force Q to map into Type somehow,
perhaps by using another layer of indirection?

Now that's an unexpected (and undesirable) behaviour. Probably not too serious.
 

> As far as homotopy type theory goes, as long as you don't mention Prop explicitely (which coerces inductive into > doing some kind of squashing, hence going beyond the power of MLTT+univalence), you can ignore Prop safely.

I find this hat do believe, not to mention it is very non-Coq-like.

I don't understand why. This is what singleton elimitation does.

Think of it that way: Prop is a sort of singletons, everything that Coq recognizes as a singleton can be cast from Type to Prop with no loss of information, for the rest, you need brackets (which are implicit in Coq, but that's irrelevant). So Prop is an approximation of hprop, if you will. Obviously, this view is not consistent with univalence, as identity is recognized as a singleton. But Coq was never built with univalence in mind. But it doesn't matter much, as the key phrase, here is "with no loss of information", that is, as long as you don't explicitly cast something to Prop (hence risking some bracketting) you don't care that Coq assigns type Prop to anything, you can pretty much ignore it (if you want, I can provide you with a plugin that will pretty print Prop as Type so that you don't even have to actively ignore it).
 

(b) "trust" Coq and Prop.

This sounds faire
 

(c) buy someone a beer to change Coq so it does not do this (the best
would be to make it configurable, I suppose).

Well, that may require a mightier bribe than that, and a more secure position for yours truly. But it's not impossible either. Bear in mind that it would require a serious incompatibility with existing libraries as propositional equality would not support rewriting (at least not always).
 

I am in favor of (c) because the HoTT people might be the only ones
who really care about the issue. Vladimir Voevodsky's Foundations
patches don't seem to address this issue, or am I wrong?

You mean the configurable version? This is certainly the lightest but not necessarily the more foreseeing solution. It's up to the Coq team to decide. As per V.V.'s patches, I have no idea, I haven't checked them out.

However, I suspect I fixed the level of Q to some particular Type(i)
by doing so. Hmm. This is a second reason why we would want to work
with a fixed universe in HoTT. It's how Vladimir did things to avoid
various unviverse inconsistencies. The trouble is that there is no way
to parametrize a piece of Coq code with a universe, so we're screwed
when we want to have two levels of universes.

Well, you've fixed the level to some 'i' but it is still unknown, so you can combine it with any other fixed universe, as long as the constraints on them are consistent.

So no problem with

Definition Type1 := Type.
Definition Type2 := Type.

This gives you two different universes.



Best,

Arnaud