Universe inconsistencies depend oddly on the stdlib (polyproj) #93
Comments
|
Here is code that used to be accepted, but is no longer, which hopefully explicates the problem. I think it is valid (and useful); do I think incorrectly? (It seems that now you require universes in inductive types to match exactly, whereas before, you required only inequality.) Set Printing All.
Set Printing Implicit.
Set Printing Universes.
Set Universe Polymorphism.
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y" := (@paths _ x y) : type_scope.
Section lift.
Let lift_type : Type.
Proof.
let U0 := constr:(Type) in
let U1 := constr:(Type) in
let unif := constr:(U0 : U1) in
exact (U0 -> U1).
Defined.
Definition Lift : lift_type := fun A => A.
End lift.
Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y.
intros A x y p.
compute in *.
exact p. |
|
I suspect the dependence on the stdlib was actually a dependence on |
|
Indeed, equality of the levels is required for consistency in general, On 1 avr. 2014, at 22:33, Jason Gross [email protected] wrote:
|
|
Here is one way to implement this rule: add half-eta-expansion for all inductive types which refreshes universes in the return type to the conversion machinery, and trigger this on universe inconsistency in the appropriate places. That is, if we have match p in (@paths _ _ y') return (@paths (* U_k *) A x y') with
| eq_refl => eq_refl
endwhere |
|
I'm thinking this could maybe be handled simply at pretyping time using the
|
|
If you can make this go through at pretyping time, then I think you're good: Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
: forall x, f x = g x
:= fun x => match h with idpath => idpath end.
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
Section local.
Let type_cast_up_type : Type.
Proof.
let U0 := constr:(Type) in
let U1 := constr:(Type) in
let unif := constr:(U0 : U1) in
exact (U0 -> U1).
Defined.
Definition Lift : type_cast_up_type
:= fun T => T.
End local.
Set Printing All.
Set Printing Universes.
Lemma Funext_downward_closed `{H : Funext} : Funext.
Proof.
constructor.
intros A P.
exact (@isequiv_apD10 H (Lift A) (fun a => Lift (P a))).
Defined.But I think you need this in unification, because the paths live inside the equiv type, and under lambdas, and then you need to talk about equalities of such paths given equalities of the original ones. But maybe you don't? Do you have an example of how you'd use the coercion mechanism? |
Here is some code that works on HoTT/coq trunk, fails on
pose (@isequiv_apD10 H (Lift A)).with polyproj, and fails onexact t'with polyproj when we replace the standard library with the one from HoTT/HoTT.The text was updated successfully, but these errors were encountered: