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
|
(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines. *)
Set Implicit Arguments.
Set Universe Polymorphism.
Definition admit {T} : T.
Admitted.
Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.
Delimit Scope natural_transformation_scope with natural_transformation.
Reserved Infix "o" (at level 40, left associativity).
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
:= match p with idpath => idpath end.
Record PreCategory :=
{
Object :> Type;
Morphism : Object -> Object -> Type;
Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g)
}.
Bind Scope category_scope with PreCategory.
Arguments Compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
Infix "o" := Compose : morphism_scope.
Local Open Scope morphism_scope.
Record Functor (C D : PreCategory) :=
{
ObjectOf :> C -> D;
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 _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1)
}.
Bind Scope functor_scope with Functor.
Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
Definition ComposeFunctors C D E
(G : Functor D E) (F : Functor C D) : Functor C E
:= Build_Functor C E
(fun c => G (F c))
admit
admit.
Infix "o" := ComposeFunctors : functor_scope.
Record NaturalTransformation C D (F G : Functor C D) :=
{
ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
Commutes : forall s d (m : C.(Morphism) s d),
ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s
}.
Generalizable All Variables.
Section NTComposeT.
Variable C : PreCategory.
Variable D : PreCategory.
Variables F F' F'' : Functor C D.
Variable T' : NaturalTransformation F' F''.
Variable T : NaturalTransformation F F'.
Let CO := fun c => T' c o T c.
Definition NTComposeT_Commutes s d (m : Morphism C s d)
: CO d o MorphismOf F m = MorphismOf F'' m o CO s.
admit.
Defined.
Definition NTComposeT
: NaturalTransformation F F''
:= Build_NaturalTransformation F F''
(fun c => T' c o T c)
NTComposeT_Commutes.
End NTComposeT.
Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F')
(G : Functor C D)
:= Build_NaturalTransformation (F o G) (F' o G)
(fun c => T (G c))
admit.
Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
Notation "T 'o' U"
:= (@NTC_Composable_term _ _ T%natural_transformation U%natural_transformation _ _ _)
: natural_transformation_scope.
Local Open Scope natural_transformation_scope.
Lemma NTWhiskerR_CompositionOf C D
(F G H : Functor C D)
(T : NaturalTransformation G H)
(T' : NaturalTransformation F G) B (I : Functor B C)
: NTWhiskerR (NTComposeT T T') I = NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I).
admit.
Defined.
Definition FunctorCategory C D : PreCategory
:= @Build_PreCategory (Functor C D)
(NaturalTransformation (C := C) (D := D))
admit.
Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
Variable C : PreCategory.
Variable D : PreCategory.
Variable E : PreCategory.
Fail Definition NTWhiskerR_Functorial (G : [C, D]%category)
: [[D, E], [C, E]]%category
:= Build_Functor
[C, D] [C, E]
(fun F => F o G)
(fun _ _ T => T o G)
(fun _ _ _ _ _ => inverse (NTWhiskerR_CompositionOf _ _ _)).
(* Anomaly: Uncaught exception Not_found(_). Please report. *)
|
