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
|
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from 335 lines to 115 lines. *)
Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.
Record Category (obj : Type) :=
Build_Category {
Object :> _ := obj;
Morphism : obj -> obj -> Type;
Identity : forall x, Morphism x x;
Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
}.
Arguments Identity {obj%type} [!C] x : rename.
Arguments Compose {obj%type} [!C s d d'] m1 m2 : rename.
Record > Category' :=
{
LSObject : Type;
LSUnderlyingCategory :> @Category LSObject
}.
Section Functor.
Context `(C : @Category objC).
Context `(D : @Category objD).
Record Functor :=
{
ObjectOf :> objC -> objD;
MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
}.
End Functor.
Section FunctorComposition.
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).
Definition ComposeFunctors (G : Functor D E) (F : Functor C D) : Functor C E.
Admitted.
End FunctorComposition.
Section IdentityFunctor.
Context `(C : @Category objC).
Definition IdentityFunctor : Functor C C.
admit.
Defined.
End IdentityFunctor.
Section ProductCategory.
Context `(C : @Category objC).
Context `(D : @Category objD).
Definition ProductCategory : @Category (objC * objD)%type.
refine (@Build_Category _
(fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
(fun o => (Identity (fst o), Identity (snd o)))
(fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).
Defined.
End ProductCategory.
Parameter TerminalCategory : Category unit.
Section ComputableCategory.
Variable I : Type.
Variable Index2Object : I -> Type.
Variable Index2Cat : forall i : I, @Category (@Index2Object i).
Local Coercion Index2Cat : I >-> Category.
Definition ComputableCategory : @Category I.
refine (@Build_Category _
(fun C D : I => Functor C D)
(fun o : I => IdentityFunctor o)
(fun C D E : I => ComposeFunctors (C := C) (D := D) (E := E))).
Defined.
End ComputableCategory.
Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory.
Section CommaCategory.
Context `(A : @Category objA).
Context `(B : @Category objB).
Context `(C : @Category objC).
Variable S : Functor A C.
Variable T : Functor B C.
Record CommaCategory_Object := { CommaCategory_Object_Member :> { ab : objA * objB & C.(Morphism) (S (fst ab)) (T (snd ab)) } }.
End CommaCategory.
Definition SliceCategory_Functor `(C : @Category objC) (a : C) : Functor TerminalCategory C
:= {| ObjectOf := (fun _ => a);
MorphismOf := (fun _ _ _ => Identity a)
|}.
Definition SliceCategoryOver
: forall (objC : Type) (C : Category objC) (a : C),
Category
(CommaCategory_Object (IdentityFunctor C)
(SliceCategory_Functor C a)).
admit.
Defined.
Section CommaCategoryProjectionFunctor.
Context `(A : Category objA).
Context `(B : Category objB).
Let X : LocallySmallCat.
Proof.
hnf.
pose (@SliceCategoryOver _ LocallySmallCat).
exact (ProductCategory A B).
Set Printing Universes.
Defined.
(* Error: Illegal application:
The term
"CommaCategory_Object (* Top.306 Top.307 Top.305 Top.300 Top.305 Top.306 *)"
of type
"forall (objA : Type (* Top.305 *))
(A : Category (* Top.306 Top.305 *) objA) (objB : Type (* Top.307 *))
(B : Category (* Top.300 Top.307 *) objB) (objC : Type (* Top.305 *))
(C : Category (* Top.306 Top.305 *) objC),
Functor (* Top.306 Top.305 Top.305 Top.306 *) A C ->
Functor (* Top.300 Top.307 Top.305 Top.306 *) B C ->
Type (* max(Top.307, Top.305, Top.306) *)"
cannot be applied to the terms
"Category' (* Top.312 Top.311 *)" : "Type (* max(Top.311+1, Top.312+1) *)"
"LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316 Top.305 *)"
: "Category (* Top.306 Top.305 *) Category' (* Top.312 Top.311 *)"
"unit" : "Set"
"TerminalCategory (* Top.300 *)" : "Category (* Top.300 Set *) unit"
"Category' (* Top.312 Top.311 *)" : "Type (* max(Top.311+1, Top.312+1) *)"
"LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316 Top.305 *)"
: "Category (* Top.306 Top.305 *) Category' (* Top.312 Top.311 *)"
"IdentityFunctor (* Top.299 Top.302 Top.301 Top.305 Top.306 *)
LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314
Top.306 Top.316 Top.305 *)"
: "Functor (* Top.306 Top.305 Top.305 Top.306 *) LocallySmallCat
(* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316
Top.305 *) LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313
Top.314 Top.306 Top.316 Top.305 *)"
"SliceCategory_Functor (* Top.305 Top.306 Top.307 Top.300 *) LocallySmallCat
(* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316
Top.305 *) a"
: "Functor (* Top.300 Top.307 Top.305 Top.306 *) TerminalCategory
(* Top.300 *) LocallySmallCat (* Top.309 Top.310 Top.311 Top.312
Top.313 Top.314 Top.306 Top.316 Top.305 *)"
The 4th term has type "Category (* Top.300 Set *) unit"
which should be coercible to "Category (* Top.300 Top.307 *) unit". *)
|
