Unset Strict Universe Declaration. (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *) 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 (A : Type@{i}) : Type@{j} := A. End lift.
Goalforall (A : Type@{i}) (x y : A), @paths@{i j} A x y -> @paths@{j k} A x y. intros A x y p. compute in *. destruct p. exact idpath. Defined.
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
