blob: 3c2b7a7d66b8623af56fe20b1d8b7795884009c3 (
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
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
|
Module Short.
Set Universe Polymorphism.
Inductive relevant (A : Type) (B : Type) : Prop := .
Section foo.
Variables A B : Type.
Definition foo := prod (relevant A B) A.
End foo.
Section bar.
Variable A : Type.
Variable B : Type.
Definition bar := prod (relevant A B) A.
End bar.
Set Printing Universes.
Check bar nat Set : Set. (* success *)
Fail Check foo nat Set : Set. (* Toplevel input, characters 6-17:
Error:
The term "foo (* Top.303 Top.304 *) nat Set" has type
"Type (* Top.304 *)" while it is expected to have type
"Set" (Universe inconsistency: Cannot enforce Top.304 = Set because Set
< Top.304)). *)
End Short.
Section Long.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Record SpecializedCategory (obj : Type) :=
{
Object :> _ := obj;
Morphism : obj -> obj -> Type
}.
Record > Category :=
{
CObject : Type;
UnderlyingCategory :> @SpecializedCategory CObject
}.
Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
{
ObjectOf :> objC -> objD;
MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
}.
(* Replacing this with [Definition Functor (C D : Category) :=
SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
Section Functor.
Variable C D : Category.
Definition Functor := SpecializedFunctor C D.
End Functor.
Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) :=
{
ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
}.
Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D.
admit.
Defined.
Definition TypeCat : @SpecializedCategory Type.
admit.
Defined.
Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat.
refine (Build_SpecializedFunctor C TypeCat
(fun X : C => C.(Morphism) X X)
_
); admit.
Defined.
Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D).
refine (@Build_SpecializedCategory _
(SpecializedNaturalTransformation (C := C) (D := D))).
Defined.
Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat).
match goal with
| [ |- SpecializedFunctor ?C0 ?D0 ] =>
refine (Build_SpecializedFunctor C0 D0
(fun c => CovariantHomFunctor C)
_
)
end;
admit.
Defined.
Section FullyFaithful.
Context `(C : @SpecializedCategory objC).
Let TypeCatC := FunctorCategory C TypeCat.
Let YC := (Yoneda C).
Set Printing Universes.
Fail Check @FunctorProduct' C TypeCatC (Yoneda C).
(* Toplevel input, characters 35-43:
Error:
In environment
objC : Type (* Top.186 *)
C : SpecializedCategory (* Top.185 Top.186 *) objC
TypeCatC := FunctorCategory (* Top.187 Top.185 Top.189 Top.186 Top.191
Top.192 *) C TypeCat (* Top.193 Top.192 Top.195 Top.191 *)
: SpecializedCategory (* Top.189 Top.187 *)
(SpecializedFunctor (* Top.192 Top.186 Top.191 Top.185 *) C
TypeCat (* Top.193 Top.192 Top.195 Top.191 *))
YC := Yoneda (* Top.197 Top.198 Top.185 Top.186 Top.201 Top.202 Top.203
Top.204 Top.185 Top.206 *) C
: SpecializedFunctor (* Top.202 Top.186 Top.203 Top.185 *) C
(FunctorCategory (* Top.203 Top.185 Top.202 Top.186 Top.197 Top.198 *)
C TypeCat (* Top.185 Top.198 Top.204 Top.197 *))
The term
"Yoneda (* Top.225 Top.226 Top.227 Top.186 Top.229 Top.230 Top.231 Top.232
Top.185 Top.234 *) C" has type
"SpecializedFunctor (* Top.230 Top.228 Top.231 Top.233 *) C
(FunctorCategory (* Top.231 Top.233 Top.230 Top.228 Top.225 Top.226 *) C
TypeCat (* Top.227 Top.226 Top.232 Top.225 *))"
while it is expected to have type
"Functor (* Top.216 Top.219 Top.217 Top.220 *) C TypeCatC"
(Universe inconsistency: Cannot enforce Top.230 = Top.217 because Top.217
<= Top.227 < Top.225 <= Top.231 <= Top.230)).
*)
End FullyFaithful.
End Long.
|
