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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
Unset Strict Universe Declaration.
Module Version1.
Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.
Record SpecializedCategory (obj : Type) :=
{
Object :> _ := obj
}.
Record > Category :=
{
CObject : Type;
UnderlyingCategory :> @SpecializedCategory CObject
}.
Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
{
ObjectOf :> objC -> objD
}.
Definition Functor (C D : Category) := SpecializedFunctor C D.
Parameter TerminalCategory : SpecializedCategory unit.
Definition focus A (_ : A) := True.
Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
assert (Hf : focus ((S tt) = (S tt))) by constructor.
let C1 := constr:(CObject) in
let C2 := constr:(fun C => @Object (CObject C) C) in
unify C1 C2; idtac C1 C2. Show Universes.
progress change @CObject with (fun C => @Object (CObject C) C) in *.
simpl in *.
match type of Hf with
| focus ?V => exact V
end.
Defined.
Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
Parameter SetCat : @SpecializedCategory Set.
Set Printing Universes.
Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
(* (fun (A : Category (* Top.68 *))
(F : Functor (* Set Top.68 *) TerminalCategory A) =>
{| |}) SetCat (* Top.68 *)
: forall
F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
SpecializedCategory (* Top.69 *)
(CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
< Top.51). *)
End Version1.
Module Version2.
Set Implicit Arguments.
Set Universe Polymorphism.
Record SpecializedCategory (obj : Type) :=
{
Object : _ := obj
}.
Record > Category :=
{
CObject : Type;
UnderlyingCategory :> @SpecializedCategory CObject
}.
Parameter TerminalCategory : SpecializedCategory unit.
Definition focus A (_ : A) := True.
Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
(objD : Type) (D : SpecializedCategory objD), Prop.
Definition CommaCategory_Object (A : Category) : Type.
assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
progress change CObject with (fun C => @Object (CObject C) C) in *;
simpl in *.
match type of Hf with
| focus ?V => exact V
end.
Defined.
Definition Build_SliceCategory := @CommaCategory_Object.
Parameter SetCat : @SpecializedCategory Set.
Set Printing Universes.
Check @Build_SliceCategory SetCat.
End Version2.
Module OtherBug.
Set Implicit Arguments.
Set Universe Polymorphism.
Record SpecializedCategory (obj : Type) : Set :=
{
Object : _ := obj
}.
Record > Category :=
{
CObject : Type;
UnderlyingCategory :> @SpecializedCategory CObject
}.
Parameter TerminalCategory : SpecializedCategory unit.
Definition focus A (_ : A) := True.
Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
(objD : Type) (D : SpecializedCategory objD), Prop.
Definition CommaCategory_Object (A : Category@{i}) : Type.
assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
progress change CObject with (fun C => @Object (CObject C) C) in *;
simpl in *.
match type of Hf with
| focus ?V => exact V
end.
Defined.
Parameter SetCat : @SpecializedCategory Set.
Set Printing Universes.
Definition Build_SliceCategory := @CommaCategory_Object.
Check @CommaCategory_Object SetCat.
(* CommaCategory_Object (* Top.43 Top.44 Top.43 *) SetCat (* Top.43 *)
: Type (* Top.44 *) *)
Check @Build_SliceCategory SetCat.
(* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.36 <= Set because Set
< Top.36). *)
End OtherBug.
|
