blob: 6b206a2f581f4ca027cc061fac0fc4f875d30b07 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.
Record Category (obj : Type) := { Morphism : obj -> obj -> Type }.
Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d).
Record Foo := { foo : forall A (f : Morphism SetCat A A), True }.
Local Notation PartialBuild_Foo pf := (@Build_Foo (fun A f => pf A f)).
Set Printing Universes.
Let SetCatFoo' : Foo.
let pf := fresh in
let pfT := fresh in
evar (pfT : Prop);
cut pfT;
[ subst pfT; intro pf;
let t := constr:(PartialBuild_Foo pf) in
let t' := (eval simpl in t) in
exact t'
| ].
admit.
(* Toplevel input, characters 15-20:
Error: Universe inconsistency (cannot enforce Set <= Prop).
*)
|
