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
|
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require Coq.Program.Program.
Export Coq.Program.Program.
Set Primitive Projections.
Set Universe Polymorphism.
Close Scope nat_scope.
Require Setoid.
Require Export Coq.Classes.CMorphisms.
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity).
Class Setoid A := {
equiv : crelation A;
setoid_equiv :: Equivalence equiv
}.
Notation "f ≈ g" := (equiv f g) (at level 79).
Ltac cat :=
intros;
autorewrite with categories;
auto with category_laws;
try reflexivity.
#[export] Hint Extern 4 (equiv ?A ?A) => reflexivity : category_laws.
Ltac proper := repeat intro; simpl; try cat; intuition.
Ltac cat_simpl :=
program_simpl; autounfold;
try solve [
program_simpl; autounfold in *;
simpl in *; intros;
simpl in *; cat];
simpl in *.
Global Obligation Tactic := cat_simpl.
Reserved Infix "~>" (at level 90, right associativity).
Class Category := {
obj : Type;
uhom := Type : Type;
hom : obj -> obj -> uhom where "a ~> b" := (hom a b);
homset :: ∀ X Y, Setoid (X ~> Y);
id {x} : x ~> x;
}.
Delimit Scope category_scope with category.
Delimit Scope object_scope with object.
Notation "x ~> y" := (@hom _%category x%object y%object)
(at level 90, right associativity) : homset_scope.
Notation "x ~{ C }~> y" := (@hom C%category x%object y%object)
(at level 90) : homset_scope.
Notation "id[ x ]" := (@id _%category x%object)
(at level 9, format "id[ x ]") : morphism_scope.
Coercion obj : Category >-> Sortclass.
Open Scope homset_scope.
Open Scope morphism_scope.
Class Functor (C D : Category) := {
fobj : C -> D;
fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;
fmap_respects :: ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
fmap_id {x : C} : fmap (@id C x) ≈ id;
}.
Delimit Scope functor_scope with functor.
Coercion fobj : Functor >-> Funclass.
Notation "fmap[ F ]" := (@fmap _ _ F%functor _ _)
(at level 9, format "fmap[ F ]") : morphism_scope.
#[export] Hint Rewrite @fmap_id : categories.
Definition Product (C D : Category) : Category := {|
obj := C * D;
hom := fun x y => (fst x ~> fst y) * (snd x ~> snd y);
homset := fun x y =>
let setoid_C := @homset C (fst x) (fst y) in
let setoid_D := @homset D (snd x) (snd y) in
{| equiv := fun f g =>
(@equiv _ setoid_C (fst f) (fst g) *
@equiv _ setoid_D (snd f) (snd g))
; setoid_equiv := _
{| Equivalence_Reflexive := fun x =>
(@Equivalence_Reflexive _ _ (@setoid_equiv _ setoid_C) (fst x),
@Equivalence_Reflexive _ _ (@setoid_equiv _ setoid_D) (snd x))
; Equivalence_Symmetric := fun x y f =>
(@Equivalence_Symmetric
_ _ (@setoid_equiv _ setoid_C) (fst x) (fst y) (fst f),
@Equivalence_Symmetric
_ _ (@setoid_equiv _ setoid_D) (snd x) (snd y) (snd f))
; Equivalence_Transitive := fun x y z f g =>
(@Equivalence_Transitive
_ _ (@setoid_equiv _ setoid_C) (fst x) (fst y) (fst z)
(fst f) (fst g),
@Equivalence_Transitive
_ _ (@setoid_equiv _ setoid_D) (snd x) (snd y) (snd z)
(snd f) (snd g)) |} |};
id := fun _ => (id, id);
|}.
Section Bifunctor.
Context {C : Category}.
Context {D : Category}.
Context {E : Category}.
Definition bimap {F : Functor (Product C D) E} {x w : C} {y z : D}
(f : x ~{C}~> w) (g : y ~{D}~> z) :
F (x, y) ~{E}~> F (w, z) := @fmap (Product C D) E F (x, y) (w, z) (f, g).
Global Program Instance bimap_respects {F : Functor (Product C D) E} {x w : C} {y z : D} :
Proper (equiv ==> equiv ==> equiv) (@bimap F x w y z).
Next Obligation.
admit.
Defined.
Lemma bimap_id_id {F : Functor (Product C D) E} {x y} :
bimap (id[x]) (id[y]) ≈ id.
admit.
Defined.
End Bifunctor.
Notation "bimap[ F ]" := (@bimap _ _ _ F%functor _ _ _ _)
(at level 9, format "bimap[ F ]") : morphism_scope.
#[export] Hint Rewrite @bimap_id_id : categories.
Reserved Infix "⨂" (at level 30, right associativity).
Class Monoidal {C : Category} := {
tensor : Functor (Product C C) C where "x ⨂ y" := (tensor (x, y));
}.
Notation "x ⨂ y" := (@tensor _ _ (x%object, y%object))
(at level 30, right associativity) : object_scope.
Notation "f ⨂ g" := (bimap[@tensor _ _] f g)
(at level 30, right associativity) : morphism_scope.
#[export] Program Instance PP
{C : Category} {D : Category} `{@Monoidal D}
{F : Functor C D} {G : Functor C D} : Functor C D := {
fobj := fun x => (F x ⨂ G x)%object;
fmap := fun _ _ f => fmap[F] f ⨂ fmap[G] f
}.
Next Obligation.
proper.
rewrite X. (* was anomaly undefined universe *)
reflexivity.
Qed.
|
