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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
Require Import TestSuite.admit.
Set Implicit Arguments.
Generalizable All Variables.
Set Universe Polymorphism.
Polymorphic Record SpecializedCategory@{l k} (obj : Type@{l}) := Build_SpecializedCategory' {
Object :> Type@{l} := obj;
Morphism' : obj -> obj -> Type@{k};
Identity' : forall o, Morphism' o o;
Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
}.
Polymorphic Definition Morphism obj (C : @SpecializedCategory obj) : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').
(* eh, I'm not terribly happy. meh. *)
Polymorphic Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory@{Set Set} obj.
Polymorphic Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.
Polymorphic Record Category := {
CObject : Type;
UnderlyingCategory :> @SpecializedCategory CObject
}.
Polymorphic Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
refine {| CObject := C.(Object) |}; auto.
Defined.
Coercion GeneralizeCategory : SpecializedCategory >-> Category.
Section SpecializedFunctor.
Set Universe Polymorphism.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Unset Universe Polymorphism.
Polymorphic Record SpecializedFunctor := {
ObjectOf' : objC -> objD;
MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d);
FCompositionOf' : forall s d d' (m1 : C.(Morphism') s d) (m2: C.(Morphism') d d'),
MorphismOf' _ _ (C.(Compose') _ _ _ m2 m1) = D.(Compose') _ _ _ (MorphismOf' _ _ m2) (MorphismOf' _ _ m1);
FIdentityOf' : forall o, MorphismOf' _ _ (C.(Identity') o) = D.(Identity') (ObjectOf' o)
}.
End SpecializedFunctor.
Global Coercion ObjectOf' : SpecializedFunctor >-> Funclass.
Set Universe Polymorphism.
Section Functor.
Variable C D : Category.
Polymorphic Definition Functor := SpecializedFunctor C D.
End Functor.
Unset Universe Polymorphism.
Polymorphic Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
Polymorphic Definition GeneralizeFunctor objC C objD D (F : @SpecializedFunctor objC C objD D) : Functor C D := F.
Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.
Arguments SpecializedFunctor {objC} C {objD} D.
Polymorphic Record SmallCategory := {
SObject : Set;
SUnderlyingCategory :> @SmallSpecializedCategory SObject
}.
Polymorphic Definition GeneralizeSmallCategory `(C : @SmallSpecializedCategory obj) : SmallCategory.
refine {| SObject := obj |}; destruct C; econstructor; eassumption.
Defined.
Coercion GeneralizeSmallCategory : SmallSpecializedCategory >-> SmallCategory.
Bind Scope category_scope with SmallCategory.
Polymorphic Definition TypeCat : @SpecializedCategory Type := (@Build_SpecializedCategory' Type
(fun s d => s -> d)
(fun _ => (fun x => x))
(fun _ _ _ f g => (fun x => f (g x)))).
(*Unset Universe Polymorphism.*)
Polymorphic Definition FunctorCategory objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD) :
@SpecializedCategory (SpecializedFunctor C D).
Admitted.
Polymorphic Definition DiscreteCategory (O : Type) : @SpecializedCategory O.
Admitted.
Polymorphic Definition ComputableCategory (I : Type) (Index2Object : I -> Type) (Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)) :
@SpecializedCategory I.
Admitted.
Polymorphic Definition is_unique (A : Type) (x : A) := forall x' : A, x' = x.
Polymorphic Definition InitialObject obj {C : SpecializedCategory obj} (o : C) :=
forall o', { m : Morphism C o o' | is_unique m }.
Polymorphic Definition SmallCat := ComputableCategory _ SUnderlyingCategory.
Lemma InitialCategory_Initial : InitialObject (C := SmallCat) (DiscreteCategory Empty_set : SmallSpecializedCategory _).
admit.
Qed.
Set Universe Polymorphism.
Section GraphObj.
Context `(C : @SpecializedCategory objC).
Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.
Definition GraphIndex_Morphism (a b : GraphIndex) : Set :=
match (a, b) with
| (GraphIndexSource, GraphIndexSource) => unit
| (GraphIndexTarget, GraphIndexTarget) => unit
| (GraphIndexTarget, GraphIndexSource) => Empty_set
| (GraphIndexSource, GraphIndexTarget) => GraphIndex
end.
Global Arguments GraphIndex_Morphism a b /.
Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
GraphIndex_Morphism s d'.
Proof using. (* This makes no sense, but it makes this test behave as before the no admit commit *)
Admitted.
Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
refine {|
Morphism' := GraphIndex_Morphism;
Identity' := (fun x => match x with GraphIndexSource => tt | GraphIndexTarget => tt end);
Compose' := GraphIndex_Compose
|};
admit.
Defined.
Definition UnderlyingGraph_ObjectOf x :=
match x with
| GraphIndexSource => { sd : objC * objC & Morphism C (fst sd) (snd sd) }
| GraphIndexTarget => objC
end.
Global Arguments UnderlyingGraph_ObjectOf x /.
Definition UnderlyingGraph_MorphismOf s d (m : Morphism GraphIndexingCategory s d) :
UnderlyingGraph_ObjectOf s -> UnderlyingGraph_ObjectOf d.
Admitted.
Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
Proof.
match goal with
| [ |- SpecializedFunctor ?C ?D ] =>
refine (Build_SpecializedFunctor C D
UnderlyingGraph_ObjectOf
UnderlyingGraph_MorphismOf
_
_
)
end;
admit.
Defined.
End GraphObj.
Set Printing Universes.
Set Printing All.
Print Coercions.
Section test.
Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf' (C D : SmallCategory) (F : SpecializedFunctor C D) :
Morphism (FunctorCategory TypeCat GraphIndexingCategory)
(@UnderlyingGraph (SObject C)
(SmallSpecializedCategory_LocallySmallSpecializedCategory_Id (SUnderlyingCategory C)))
(UnderlyingGraph D).
(* Toplevel input, characters 216-249:
Error:
In environment
C : SmallCategory (* Top.594 *)
D : SmallCategory (* Top.595 *)
F :
@SpecializedFunctor (* Top.25 Set Top.25 Set *) (SObject (* Top.25 *) C)
(SUnderlyingCategory (* Top.25 *) C) (SObject (* Top.25 *) D)
(SUnderlyingCategory (* Top.25 *) D)
The term
"SUnderlyingCategory (* Top.25 *) C
:SpecializedCategory (* Top.25 Set *) (SObject (* Top.25 *) C)" has type
"SpecializedCategory (* Top.618 Top.619 *) (SObject (* Top.25 *) C)"
while it is expected to have type
"SpecializedCategory (* Top.224 Top.225 *) (SObject (* Top.617 *) C)"
(Universe inconsistency: Cannot enforce Set = Top.225)).
*)
Fail Admitted.
Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
Morphism (FunctorCategory TypeCat GraphIndexingCategory) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
Fail Admitted.
Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
Morphism (FunctorCategory GraphIndexingCategory TypeCat) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
Proof.
Admitted.
End test.
|
