1 (*******************************************************************************)
3 (*******************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Categories_ch1_3.
9 Require Import Functors_ch1_4.
10 Require Import Isomorphisms_ch1_5.
11 Require Import ProductCategories_ch1_6_1.
12 Require Import EpicMonic_ch2_1.
13 Require Import InitialTerminal_ch2_2.
14 Require Import Subcategories_ch7_1.
15 Require Import NaturalTransformations_ch7_4.
16 Require Import NaturalIsomorphisms_ch7_5.
17 Require Import Coherence_ch7_8.
18 Require Import MonoidalCategories_ch7_8.
19 Require Import FreydCategories.
20 Require Import CoqCategory.
22 (* these notations are more for printing back than writing input (helps coax Coq into better pretty-printing) *)
23 Notation "'_swap'" := (fun xy => let (a0, b0) := xy in ⟨b0, a0 ⟩).
24 Notation "'_assoc'" := (fun xyz => let (ab, c) := xyz in let (a0, b0) := ab in ⟨a0, ⟨b0, c ⟩ ⟩).
27 ( arr_hom' : Type->Type->Type ) :=
28 { arr_hom := arr_hom' (* hack to make Coq notations work *) where "a ~> b" := (arr_hom a b)
30 ; arr_arr : forall {a b}, (a->b) -> a~>b
31 ; arr_comp : forall {a b c}, a~>b -> b~>c -> a~>c where "f >>> g" := (arr_comp f g)
32 ; arr_first : forall {a b} c, a~>b -> (a*c)~>(b*c) where "f ⋊ d" := (arr_first d f)
34 ; arr_eqv : forall {a b}, (a~>b) -> (a~>b) -> Prop where "a ~~ b" := (arr_eqv a b)
35 ; arr_eqv_equivalence : forall {a b}, Equivalence (@arr_eqv a b)
37 ; arr_comp_respects : forall {a b c}, Proper (arr_eqv ==> arr_eqv ==> arr_eqv) (@arr_comp a b c)
38 ; arr_first_respects : forall {a b c}, Proper (arr_eqv ==> arr_eqv) (@arr_first a b c)
39 ; arr_arr_respects : forall {a b}(f g:a->b), Proper (extensionality a b ==> arr_eqv) (@arr_arr a b)
41 ; arr_left_identity : forall `(f:a~>b), (arr_arr (fun x => x)) >>> f ~~ f
42 ; arr_right_identity : forall `(f:a~>b), f >>> (arr_arr (fun x => x)) ~~ f
43 ; arr_associativity : forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h)
44 ; arr_comp_preserves : forall `(f:a->b)`(g:b->c), arr_arr (g ○ f) ~~ arr_arr f >>> arr_arr g
45 ; arr_extension : forall a b (f:a->b), forall d, (arr_arr f) ⋊ d ~~ arr_arr (Λ⟨x,y⟩ ⟨f x,y⟩)
46 ; arr_first_preserves : forall {d}`(f:a~>b)`(g:b~>c), (f >>> g) ⋊ d ~~ f ⋊ d >>> g ⋊ d
47 ; arr_exchange : forall `(f:a~>b)`(g:c->d), arr_arr (Λ⟨x,y⟩ ⟨x,g y⟩) >>> f ⋊ _ ~~ f ⋊ _ >>> arr_arr (Λ⟨x,y⟩ ⟨x,g y⟩)
48 ; arr_unit : forall {c}`(f:a~>b), f ⋊ c >>> arr_arr (Λ⟨x,y⟩x) ~~ (arr_arr (Λ⟨x,y⟩x)) >>> f
49 ; arr_association : forall {c}{d}`(f:a~>b), (f⋊c)⋊d >>> arr_arr(Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩) ~~ arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩) >>> f⋊_
53 ; loop : forall {a}{b}{c}, (a⊗c~>b⊗c) -> (a~>b)
54 (* names taken from Figure 7 of Paterson's "A New Notation for Arrows", which match the CCA paper *)
55 ; left_tightening : forall {a}{b}{c}{f:a⊗b~>c⊗b}{h}, loop (first c a b h >>> f) ~~ h >>> loop f
56 ; right_tightening : forall {a}{b}{c}{f:a⊗b~>c⊗b}{h}, loop (f >>> first c a b h) ~~ loop f >>> h
57 ; sliding : forall {a}{b}{c}{f:a⊗c~>b⊗c}{k}, central k -> loop (f >>> second _ _ b k) ~~ loop (second _ _ a k >>> f)
58 ; vanishing : forall {a}{b}{c}{d}{f:(a⊗c)⊗d~>(b⊗c)⊗d}, loop (loop f) ~~ loop (#assoc⁻¹ >>> f >>> #assoc)
59 ; superposing : forall {a}{b}{c}{d}{f:a⊗c~>b⊗c}, second _ _ d (loop f) ~~ loop (#assoc >>> second _ _ d f >>> #assoc⁻¹)
62 (* register the arrow equivalence relation as a rewritable setoid, with >>> and first as morphisms *)
63 Add Parametric Relation `(ba:Arrow)(a b:Type) : (arr_hom a b) arr_eqv
64 reflexivity proved by (@Equivalence_Reflexive _ _ (@arr_eqv_equivalence _ _ a b))
65 symmetry proved by (@Equivalence_Symmetric _ _ (@arr_eqv_equivalence _ _ a b))
66 transitivity proved by (@Equivalence_Transitive _ _ (@arr_eqv_equivalence _ _ a b))
67 as parametric_relation_arr_eqv.
68 Add Parametric Morphism `(ba:Arrow)(a b c:Type) : (@arr_comp _ _ a b c)
69 with signature (arr_eqv ==> arr_eqv ==> arr_eqv) as parametric_morphism_arr_comp.
70 intros; apply arr_comp_respects; auto.
72 Add Parametric Morphism `(ba:Arrow)(a b c:Type) : (@arr_first _ _ a b c)
73 with signature (arr_eqv ==> arr_eqv) as parametric_morphism_arr_first.
74 intros; apply arr_first_respects; auto.
77 Notation "a ~> b" := (arr_hom a b) :arrow_scope.
78 Notation "f >>> g" := (arr_comp f g) :arrow_scope.
79 Notation "f ⋊ d" := (arr_first d f) :arrow_scope.
80 Notation "a ~~ b" := (arr_eqv a b) :arrow_scope.
82 Open Scope arrow_scope.
84 (* Formalized Definition 2.3 *)
86 ( biarr_hom : Type -> Type -> Type ) :=
87 { biarr_super :> Arrow biarr_hom
89 ; biarr_biarr : forall {a b}, (a->b) -> (b->a) -> (a~>b) where "f <--> g" := (biarr_biarr g f)
90 ; biarr_inv : forall {a b}, a~>b -> b~>a where "! f" := (biarr_inv f)
92 (* BiArrow laws are numbered based on section 5 of Hunen+Jacobs paper *)
93 ; biarr_law3' : forall {a}{b}{c}{f1}{f2:b->c}{g1}{c2:a->b}, f1<-->c2 >>> g1<-->f2 ~~ (f1 ○ g1) <--> (f2 ○ c2)
94 ; biarr_law4' : forall {a}{b}{f:a~>b}, (fun x=>x)<-->(fun x=>x) >>> f ~~ f
95 ; biarr_law4'': forall {a}{b}{f:a~>b}, f >>> (fun x=>x)<-->(fun x=>x) ~~ f
96 ; biarr_law8' : forall {a}{b}{f:a->b}{g}{c}, (f<-->g) ⋊ c ~~ (Λ⟨x,y⟩ ⟨f x,y⟩)<-->(Λ⟨x,y⟩ ⟨g x,y⟩)
97 ; biarr_law22 : forall {a}{b}{f:a~>b}, !(!f) ~~ f
98 ; biarr_law23 : forall {a}{b}{c}{f:b~>c}{g:a~>b}, !(g >>> f) ~~ !f >>> !g
99 ; biarr_law24 : forall {a}{b}{f:a->b}{g}, !(f<-->g) ~~ g<-->f
100 ; biarr_law25 : forall {a}{b}{f:a~>b}{c}, !(f ⋊ _) ~~ (!f) ⋊ c
101 ; biarr_law6' : forall {a}{b}{c}{d}{f:a->b}{g}{h:c~>d}, (h ⋊ _) >>> (Λ⟨x,y⟩ ⟨x,f y⟩)<-->(Λ⟨x,y⟩ ⟨x,g y⟩) ~~
102 (Λ⟨x,y⟩ ⟨x,f y⟩)<-->(Λ⟨x,y⟩ ⟨x,g y⟩) >>> (h ⋊ _)
104 (* for complete example, we'd also need biarr_biarr_respects and biarr_inv_respects, but this paper isn't about BiArrows *)
107 Notation "f <--> g" := (biarr_biarr g f) :biarrow_scope.
108 Notation "! f" := (biarr_inv f) :biarrow_scope.
110 Open Scope biarrow_scope.
111 Inductive left_invertible `{ba:BiArrow}{a}{b}(f:a~>b) : Prop := LI : ((f >>> !f) ~~ (arr_arr (fun x=>x))) -> left_invertible f.
112 Inductive right_invertible `{ba:BiArrow}{a}{b}(f:a~>b) : Prop := RI : ((!f >>> f) ~~ (arr_arr (fun x=>x))) -> right_invertible f.
113 Close Scope biarrow_scope.
115 Hint Extern 4 (?A ~~ ?A) => reflexivity.
116 Hint Extern 6 (?X ~~ ?Y) => apply Equivalence_Symmetric.
117 Hint Extern 7 (?X ~~ ?Z) => match goal with [H : ?X ~~ ?Y, H' : ?Y ~~ ?Z |- ?X ~~ ?Z] => transitivity Y end.
118 Hint Extern 10 (?X >>> ?Y ~~ ?Z >>> ?Q) => apply arr_comp_respects; auto.
119 Hint Constructors Arrow.
121 (* Formalized Lemma 3.2 *)
122 Definition arrows_are_categories : forall `(ba:Arrow), Category Type arr_hom.
125 {| id := fun a => arr_arr (fun x => x)
126 ; comp := fun a b c f g => arr_comp f g
127 ; eqv := fun a b f g => arr_eqv f g |}; intros; auto.
128 apply arr_left_identity.
129 apply arr_right_identity.
130 apply arr_associativity.
132 Coercion arrows_are_categories : Arrow >-> Category.
134 (* a tactic to throw the kitchen sink at Arrow goals; using ATBR (http://coq.inria.fr/contribs/ATBR.html) would be a better idea *)
136 repeat apply arr_comp;
137 repeat apply arr_first;
138 repeat apply arr_arr_respects;
139 repeat setoid_rewrite arr_left_identity;
140 repeat setoid_rewrite arr_right_identity;
141 repeat setoid_rewrite <- arr_comp_preserves;
142 repeat setoid_rewrite arr_extension;
143 repeat setoid_rewrite arr_first_preserves.
144 (* need to handle associat, exchange, unit, association *)
146 Definition Arrows_are_Binoidal `(ba:Arrow) : BinoidalCat ((arrows_are_categories ba)) prod.
147 intros; apply Build_BinoidalCat; intros;
148 [ apply (Build_Functor _ _ (ba) _ _ (ba) (fun X => X*a)
149 (fun X Y f => (arr_first(Arrow:=ba)) a f))
150 | apply (Build_Functor _ _ (ba) _ _ (ba) (fun X => a*X)
151 (fun X Y f => arr_arr (Λ⟨x,y⟩ ⟨y,x⟩) >>> arr_first(Arrow:=ba) a f >>> arr_arr(Arrow:=ba) (Λ⟨x,y⟩ ⟨y,x⟩)))
152 ]; intros; simpl; intros;
153 [ apply arr_first_respects; auto
154 | setoid_rewrite arr_extension; repeat setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects
155 | symmetry; apply arr_first_preserves
156 | repeat apply arr_comp_respects; try reflexivity
157 | setoid_rewrite arr_extension; repeat setoid_rewrite <- arr_comp_preserves
158 | setoid_rewrite arr_first_preserves
161 unfold extensionality; intros; destruct x; auto.
162 simpl in H; setoid_rewrite H; auto.
163 apply arr_arr_respects; intros; auto.
164 unfold extensionality; intros; destruct x; auto.
165 repeat rewrite arr_associativity; repeat setoid_rewrite <- arr_comp_preserves.
166 apply arr_comp_respects; try reflexivity.
167 apply arr_comp_respects; try reflexivity.
168 setoid_rewrite <- arr_associativity.
169 repeat setoid_rewrite <- arr_comp_preserves.
170 setoid_rewrite <- arr_associativity.
171 apply arr_comp_respects; try reflexivity.
172 transitivity (arr_comp ((arr_arr(Arrow:=ba)) (fun x=>x)) (arr_first(Arrow:=ba) a g)).
173 apply arr_comp_respects; try reflexivity.
174 apply arr_arr_respects; intros; auto; unfold extensionality; intros; auto; try destruct x; auto.
175 apply arr_left_identity.
178 Definition arrow_cancelr_iso : forall `(ba:Arrow)(A:ba), (Isomorphic(C:=ba)) (A*Datatypes.unit) A.
179 intros; apply (Build_Isomorphic _ _ ba (A*Datatypes.unit) A (arr_arr (Λ⟨x,y⟩ x)) (arr_arr (fun x => ⟨x,tt⟩))).
180 simpl; setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects.
181 intros; destruct X. auto. auto.
182 unfold extensionality; intros; simpl. destruct x. destruct u. auto.
183 simpl; setoid_rewrite <- arr_comp_preserves; reflexivity.
185 Definition arrow_cancelr_ni_iso `(ba:Arrow)
186 : (((bin_first(BinoidalCat:=Arrows_are_Binoidal ba)) (Datatypes.unit)) <~~~> functor_id (ba)).
187 intros; eapply Build_NaturalIsomorphism.
188 instantiate (1:=arrow_cancelr_iso ba).
192 (fmor (bin_first(BinoidalCat:=Arrows_are_Binoidal ba) Datatypes.unit) f)
193 (arr_arr(Arrow:=ba) (fun xy : B * unit => let (a, b) := xy in (fun (x : B) (_ : unit) => x) a b))
196 apply (arr_unit(Arrow:=ba)(c:=(Datatypes.unit)) f).
197 apply Equivalence_Reflexive.
199 Definition arrow_cancell_iso `(ba:Arrow)
200 : forall (A:ba), (Isomorphic(C:=ba)) (Datatypes.unit*A) A.
201 intros; apply (Build_Isomorphic _ _ ba _ _ (arr_arr (Λ⟨x,y⟩ y)) (arr_arr (fun x => ⟨tt,x⟩))).
202 simpl; setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects.
203 intros; destruct X. auto. auto.
204 unfold extensionality; intros; simpl. destruct x. auto. destruct u. auto.
205 simpl; setoid_rewrite <- arr_comp_preserves; reflexivity.
207 Definition arrow_cancell_ni_iso `(ba:Arrow)
208 : (((bin_second(BinoidalCat:=(Arrows_are_Binoidal ba))) (Datatypes.unit)) <~~~> functor_id (ba)).
209 intros; eapply Build_NaturalIsomorphism.
210 instantiate (1:=arrow_cancell_iso ba).
212 repeat setoid_rewrite arr_associativity.
213 setoid_rewrite <- arr_comp_preserves.
215 setoid_replace (arr_arr (fun x : B * unit => let (_, b) := let (a, b) := x in ⟨b, a ⟩ in b))
216 with (arr_arr (fun x : B * unit => let (b, _) := x in b)).
217 setoid_rewrite arr_unit.
218 setoid_rewrite <- arr_associativity.
220 apply arr_comp_respects.
221 apply arr_arr_respects.
222 intros; destruct X; auto.
223 intros; destruct X; auto.
224 unfold extensionality; intros; simpl.
226 apply Equivalence_Reflexive.
227 apply arr_arr_respects.
228 intros; destruct X; auto.
229 intros; destruct X; auto.
230 unfold extensionality; intros; simpl.
235 Definition arrow_assoc_iso `(ba:Arrow) : forall A B C, (Isomorphic(C:=ba)) ((A*B)*C) (A*(B*C)).
236 intros; eapply (Build_Isomorphic _ _ ba _ _ (arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩)) (arr_arr (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩)));
237 [ intros; simpl; setoid_rewrite <- arr_comp_preserves
238 | intros; simpl; simpl; setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects; auto
239 ]; simpl; try apply arr_arr_respects; intros; try destruct X; try destruct x; try destruct p; auto;
240 unfold extensionality; intros; intros; destruct x; destruct p; auto.
242 Definition arrow_assoc_ni_iso `(ba:Arrow) :
244 (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba))) A >>>>
245 (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba))) B <~~~>
246 (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba))) B >>>>
247 (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba))) A).
249 eapply Build_NaturalIsomorphism.
250 instantiate (1:=(fun X:ba => (arrow_assoc_iso ba A X B))).
252 setoid_rewrite arr_first_preserves.
253 setoid_rewrite arr_first_preserves.
254 setoid_rewrite arr_associativity.
256 ( (arr_first(Arrow:=ba) A (arr_first(Arrow:=ba) B f)) >>> @arr_arr arr_hom' ba (B0 * B * A) (A * (B0 * B)) _swap)
258 ((( (arr_first(Arrow:=ba) A (arr_first(Arrow:=ba) B f)) >>>
259 (arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩))) >>> (arr_arr (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩))) >>>
260 @arr_arr arr_hom' ba (B0 * B * A) (A * (B0 * B)) _swap).
261 setoid_rewrite arr_association.
262 repeat setoid_rewrite arr_associativity.
264 ((arr_first(Arrow:=ba) B (arr_first(Arrow:=ba) A f))
265 >>> ((arr_first(Arrow:=ba) B (@arr_arr arr_hom' ba (B0 * A) (A * B0) _swap))
266 >>> (@arr_arr arr_hom' ba (A * B0 * B) (A * (B0 * B)) _assoc)))
268 ((((arr_first(Arrow:=ba) B (arr_first(Arrow:=ba) A f))
269 >>> (arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩)))
270 >>> (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩))
271 >>> (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩))
272 >>> (arr_arr (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩)))
273 >>> ((arr_first(Arrow:=ba) B (@arr_arr arr_hom' ba (B0 * A) (A * B0) _swap))
274 >>> (@arr_arr arr_hom' ba (A * B0 * B) (A * (B0 * B)) _assoc))).
275 setoid_rewrite arr_association.
276 setoid_replace (arr_first(Arrow:=ba) (A*B) f)
277 with (((arr_first(Arrow:=ba) (A*B) f)
278 >>> (arr_arr (Λ⟨x,y⟩ ⟨x,(fun q => match q with (a,b) => (b,a) end) y⟩)))
279 >>> (arr_arr (Λ⟨x,y⟩ ⟨x,(fun q => match q with (a,b) => (b,a) end) y⟩))).
280 setoid_rewrite <- arr_exchange.
282 repeat setoid_rewrite <- arr_associativity.
284 repeat setoid_rewrite arr_associativity.
286 apply arr_comp_respects.
287 apply arr_arr_respects.
288 intros; destruct X; destruct p; auto.
289 intros; destruct X; destruct p; auto.
290 unfold extensionality; intros; simpl.
291 destruct x. destruct p; auto.
292 apply arr_comp_respects.
294 apply arr_arr_respects.
295 intros; destruct X; destruct p; auto.
296 intros; destruct X; destruct p; auto.
297 unfold extensionality; intros; simpl.
298 destruct x. destruct p; auto.
299 setoid_rewrite arr_associativity.
301 setoid_replace (arr_first(Arrow:=ba) (A*B) f) with (arr_first(Arrow:=ba) (A*B) f >>> arr_arr (fun x => x)).
302 apply arr_comp_respects.
303 setoid_rewrite arr_right_identity.
305 apply arr_arr_respects.
306 intros; destruct X; destruct p; auto.
307 intros; destruct X; destruct p; auto.
308 unfold extensionality; intros; simpl.
309 destruct x. destruct p; auto.
310 setoid_rewrite <- arr_right_identity.
311 setoid_rewrite arr_associativity.
315 repeat setoid_rewrite arr_associativity.
317 apply arr_comp_respects.
319 apply arr_arr_respects.
320 intros; destruct X; destruct p; auto.
321 intros; destruct X; destruct p; auto.
322 unfold extensionality; intros; simpl.
323 destruct x. destruct p; auto.
324 repeat setoid_rewrite arr_associativity.
326 apply arr_comp_respects.
328 apply arr_arr_respects.
329 intros; destruct X; destruct p; auto.
330 intros; destruct X; destruct p; auto.
331 unfold extensionality; intros; simpl.
332 destruct x. destruct p; auto.
335 Definition arrow_assoc_rr_iso `(ba:Arrow) := fun a b X:ba => iso_inv _ _ (arrow_assoc_iso ba X a b).
336 Definition arrow_assoc_rr_ni_iso `(ba:Arrow) :
337 ∀a b:ba, NaturalIsomorphism
338 (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) ((bin_obj(BinoidalCat:=(Arrows_are_Binoidal ba))) a b))
339 ((bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) a)
341 (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) b)).
342 intros; eapply Build_NaturalIsomorphism.
343 instantiate(1:=arrow_assoc_rr_iso ba a b).
346 setoid_replace ((arr_first(Arrow:=ba) (a*b) f))
347 with (arr_arr (fun q:A*(a*b) => (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩) q)
348 >>> ((arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩))
349 >>> (arr_first(Arrow:=ba) (a*b) f))).
350 setoid_rewrite <- arr_association.
351 repeat setoid_rewrite arr_associativity.
353 apply arr_comp_respects.
354 apply arr_arr_respects.
355 intros. destruct X. destruct p. auto.
356 intros. destruct X. destruct p. auto.
357 unfold extensionality.
359 transitivity (arr_first(Arrow:=ba) b (arr_first(Arrow:=ba) a f) >>> arr_arr (fun x=>x)).
360 setoid_rewrite arr_right_identity.
362 apply arr_comp_respects.
364 apply arr_arr_respects.
365 intros. destruct X. destruct p. auto.
366 intros. destruct X. destruct p. auto.
367 unfold extensionality.
372 setoid_rewrite <- arr_associativity.
374 transitivity (arr_arr (fun x=>x) >>> (arr_first(Arrow:=ba) (a*b) f)).
375 setoid_rewrite arr_left_identity.
377 apply arr_comp_respects.
378 apply arr_arr_respects.
379 intros. destruct X. destruct p. auto.
380 intros. destruct X. destruct p. auto.
381 unfold extensionality.
389 Definition arrow_assoc_ll_iso `(ba:Arrow) := fun a b X:ba => arrow_assoc_iso ba a b X.
390 Definition arrow_assoc_ll_ni_iso `(ba:Arrow) :
391 forall a b:ba, NaturalIsomorphism
392 (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) ((bin_obj(BinoidalCat:=(Arrows_are_Binoidal ba))) a b))
393 ((bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) b)
395 (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) a)).
397 eapply Build_NaturalIsomorphism.
399 instantiate(1:=(arrow_assoc_ll_iso ba a b)).
402 repeat setoid_rewrite arr_associativity.
404 ((arr_first a (arr_first(Arrow:=ba) b f)) >>> ((arr_first _ ((@arr_arr arr_hom' ba (B * b) (b * B) _swap))) >>>
405 @arr_arr arr_hom' ba (b * B * a) (a * (b * B)) _swap))
407 ((((arr_first a (arr_first(Arrow:=ba) b f)
408 >>> ((arr_arr(a:=((B*b)*a)) (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩)))))
409 >>> (arr_arr(Arrow:=ba) (Λ⟨x,yz⟩ ⟨x,(match yz with (y,z) => (z,y) end)⟩)))
410 >>> (arr_arr(Arrow:=ba) (Λ⟨x,⟨y,z⟩⟩ ⟨y,⟨z,x⟩⟩))).
411 setoid_rewrite arr_association.
412 setoid_replace (arr_arr(a:=((A*b)*a)) _assoc >>> (arr_first(Arrow:=ba) (b*a) f) >>>
414 (fun xy : B * (b * a) =>
415 let (a0, b0) := xy in ⟨a0, let (y, z) := b0 in ⟨z, y ⟩ ⟩))
417 (arr_arr(a:=((A*b)*a)) _assoc >>> ((arr_first(Arrow:=ba) (b*a) f) >>>
419 (fun xy : B * (b * a) =>
420 let (a0, b0) := xy in ⟨a0, ((fun xy:b*a => let (a0, b0) := xy in ⟨b0, a0 ⟩)) b0 ⟩))).
421 setoid_rewrite <- arr_exchange.
423 repeat setoid_rewrite <- arr_associativity.
425 apply arr_comp_respects.
426 apply arr_comp_respects.
427 apply arr_arr_respects.
428 exact (fun xyz => match xyz with (xy,z) => match xy with (x,y) => (z,(x,y)) end end).
429 exact (fun xyz => match xyz with (xy,z) => match xy with (x,y) => (z,(x,y)) end end).
430 unfold extensionality; intros; simpl.
435 apply arr_arr_respects.
436 intros. destruct X. destruct b1. auto.
437 intros. destruct X. destruct b1. auto.
438 unfold extensionality; intros; simpl.
442 repeat setoid_rewrite <- arr_associativity.
443 apply arr_comp_respects.
445 apply arr_arr_respects.
446 intros. destruct X. destruct p. auto.
447 intros. destruct X. destruct p. auto.
448 unfold extensionality; intros; simpl.
452 setoid_rewrite arr_extension.
453 repeat setoid_rewrite arr_associativity.
455 apply arr_comp_respects.
457 apply arr_arr_respects.
458 intros. destruct X. destruct p. auto.
459 intros. destruct X. destruct p. auto.
460 unfold extensionality; intros; simpl.
466 Instance arrows_monoidal `(ba:Arrow) : PreMonoidalCat (Arrows_are_Binoidal ba) (Datatypes.unit) :=
467 { pmon_assoc := arrow_assoc_ni_iso ba
468 ; pmon_cancelr := arrow_cancelr_ni_iso ba
469 ; pmon_cancell := arrow_cancell_ni_iso ba
470 ; pmon_assoc_ll := arrow_assoc_ll_ni_iso ba
471 ; pmon_assoc_rr := arrow_assoc_rr_ni_iso ba
473 apply Build_Pentagon; intros.
475 repeat setoid_rewrite arr_extension.
476 repeat setoid_rewrite <- arr_comp_preserves.
477 apply arr_arr_respects; unfold extensionality; intros; simpl;
478 try destruct x; try destruct X; try destruct b0; try destruct p; auto.
479 destruct b0. unfold bin_obj. auto.
480 destruct b0. unfold bin_obj. auto.
481 destruct b0. unfold bin_obj. auto.
482 apply Build_Triangle; intros; simpl.
483 repeat setoid_rewrite arr_extension.
484 repeat setoid_rewrite <- arr_comp_preserves.
485 apply arr_arr_respects; unfold extensionality; intros; simpl;
486 try destruct x; try destruct X; try destruct p; try destruct b0; try destruct p; unfold bin_obj; auto.
487 simpl. apply arr_arr_respects;
488 [ exact (fun (xy:unit*unit) => tt)
489 | exact (fun (xy:unit*unit) => tt)
491 ]; unfold extensionality; intros; simpl; destruct x; destruct u; destruct u0; auto.
496 Definition arrow_inclusion_functor `(ba:Arrow) : Functor coqCategory (ba) (fun x=>x).
497 intros; apply (Build_Functor _ _ coqCategory _ _ (ba) _ (fun A B => fun f:A->B => arr_arr f));
498 intros; unfold eqv; simpl;
499 [ apply arr_arr_respects; auto
501 | symmetry; apply arr_comp_preserves ].
504 Instance Arrow_inclusion_is_a_monoidal_functor `(ba:Arrow)
505 : PreMonoidalFunctor coqPreMonoidalCat (arrows_monoidal ba) (fun x=>x) :=
506 { mf_F := arrow_inclusion_functor ba
509 intros; apply (Build_NaturalIsomorphism _ _ coqCategory _ _ (ba) (fun a0 : Type => a0 * a) (fun a0 : Type => a0 * a) _ _
510 (fun A:coqCategory => (iso_id(C:=ba)) ((fun a0 : Type => a0 * a) A))).
511 intros; simpl; setoid_rewrite ((arr_extension(Arrow:=ba)) A B f a); setoid_rewrite <- arr_comp_preserves; reflexivity.
512 intros; apply (@Build_NaturalIsomorphism _ _ coqCategory _ _ (ba) (fun a0 : Type => a * a0) (fun a0 : Type => a * a0) _ _
513 (fun A:coqCategory => (iso_id(C:=ba)) ((fun a0 : Type => a * a0) A))).
514 intros; simpl; setoid_rewrite arr_extension; repeat setoid_rewrite <- arr_comp_preserves.
515 apply arr_arr_respects; intros; unfold extensionality; intros; try destruct X; try destruct x; try destruct p; auto.
517 intros; apply Build_CentralMorphism; intros. simpl.
520 setoid_rewrite arr_extension.
521 setoid_rewrite <- arr_associativity.
522 setoid_rewrite <- arr_associativity.
523 repeat setoid_rewrite <- arr_comp_preserves.
525 arr_arr (fun x:a*c => let (a0,c0) := x in (c0,a0))
527 arr_arr (fun x:c*a => let (c0,a0) := x in (c0, f a0)) >>> ((arr_first(Arrow:=ba)) b g) >>>
528 (arr_arr (fun x:d*b => let (d0,b0):=x in (b0,d0)))).
529 repeat setoid_rewrite <- arr_associativity.
530 apply arr_comp_respects; try reflexivity.
531 apply arr_comp_respects; try reflexivity.
532 repeat setoid_rewrite <- arr_comp_preserves.
533 apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto.
534 repeat setoid_rewrite arr_associativity.
535 apply arr_comp_respects; try reflexivity.
536 repeat setoid_rewrite <- arr_associativity.
537 setoid_rewrite <- arr_extension.
538 setoid_rewrite arr_extension.
539 repeat setoid_rewrite arr_associativity.
540 repeat setoid_rewrite <- arr_comp_preserves.
541 repeat setoid_rewrite <- arr_associativity.
542 setoid_rewrite arr_exchange.
543 repeat setoid_rewrite arr_associativity.
544 apply arr_comp_respects; try reflexivity.
545 repeat setoid_rewrite <- arr_comp_preserves.
546 apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto.
549 setoid_rewrite arr_extension.
550 setoid_rewrite <- arr_associativity.
551 setoid_rewrite <- arr_associativity.
552 repeat setoid_rewrite <- arr_comp_preserves.
553 transitivity (arr_arr (fun x:c*a => let (c0,a0) := x in (c0, f a0)) >>> ((arr_first(Arrow:=ba)) b g)).
554 setoid_rewrite arr_exchange.
555 repeat setoid_rewrite arr_associativity.
556 apply arr_comp_respects. reflexivity.
557 repeat setoid_rewrite <- arr_comp_preserves.
558 apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto.
559 apply arr_comp_respects; try reflexivity.
560 apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto.
563 Definition arrow_swap_iso `(ba:Arrow) : forall A B, (Isomorphic(C:=ba)) (A*B) (B*A).
564 intros; apply (Build_Isomorphic _ _ ba _ _ (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩)) (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩)));
565 simpl; setoid_rewrite <- arr_comp_preserves;
566 apply arr_arr_respects;
567 intros; auto; intros; auto;
568 unfold extensionality; intros; simpl.
569 try destruct X; try destruct x; auto; destruct x; auto.
570 destruct x. simpl. reflexivity.
573 Instance arrows_are_braided `(ba:Arrow) : BraidedCat (arrows_monoidal ba).
574 intros; apply (Build_BraidedCat _ _ (ba) _ _ _ _ (fun A B => arrow_swap_iso ba A B));
576 repeat setoid_rewrite arr_extension;
577 repeat setoid_rewrite <- arr_associativity;
578 repeat setoid_rewrite <- arr_comp_preserves;
579 apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj;
580 intros; auto; try destruct x; try destruct p; try destruct b0; auto.
583 Instance arrows_are_symmetric `(ba:Arrow) : SymmetricCat (arrows_are_braided ba).
584 intros; apply Build_SymmetricCat; intros. simpl. reflexivity.
587 Instance Freyd_from_Arrow `(ba:Arrow)
588 : FreydCategory coqPreMonoidalCat :=
589 { freyd_C_cartesian := coqCartesianCat
591 ; freyd_K_binoidal := Arrows_are_Binoidal ba
592 ; freyd_K_monoidal := arrows_monoidal ba
593 ; freyd_F := Arrow_inclusion_is_a_monoidal_functor ba
594 ; freyd_K_braided := arrows_are_braided ba
595 ; freyd_K_symmetric := arrows_are_symmetric ba
597 intros; apply Build_CentralMorphism; intros; simpl.
598 repeat setoid_rewrite arr_extension.
599 repeat setoid_rewrite <- arr_associativity.
600 repeat setoid_rewrite <- arr_comp_preserves.
602 (arr_arr (fun x : a * c => let (a0, b0) := let (a0, b0) := x in ⟨f a0, b0 ⟩ in ⟨b0, a0 ⟩) >>> (arr_first(Arrow:=ba) b g))
604 (arr_arr (fun x : a * c => let (a0, b0) := x in ⟨b0,a0 ⟩) >>> (arr_arr (fun x : c * a => let (a0, b0) := x in ⟨a0,f b0 ⟩)
605 >>> (arr_first(Arrow:=ba) b g))).
606 setoid_rewrite arr_exchange.
607 repeat setoid_rewrite arr_associativity.
608 apply arr_comp_respects; try reflexivity.
609 apply arr_comp_respects; try reflexivity.
610 setoid_rewrite <- arr_comp_preserves.
611 apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj;
612 intros; auto; try destruct x; try destruct p; try destruct b0; auto.
614 setoid_rewrite <- arr_associativity.
615 apply arr_comp_respects; try reflexivity.
616 setoid_rewrite <- arr_comp_preserves.
617 apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj;
618 intros; auto; try destruct x; try destruct p; try destruct b0; auto.
620 repeat setoid_rewrite arr_extension.
621 repeat setoid_rewrite <- arr_comp_preserves.
622 transitivity ((arr_arr(Arrow:=ba) (fun x:c*a => let (a0,b0):=x in ⟨a0,f b0 ⟩)) >>> (arr_first(Arrow:=ba) b g));
623 [ setoid_rewrite arr_exchange | idtac ];
624 apply arr_comp_respects; try reflexivity;
625 apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj;
626 intros; auto; try destruct x; try destruct p; try destruct b0; auto.
628 intros; simpl; unfold bin_obj; reflexivity.
629 intros; simpl; unfold bin_obj; reflexivity.
630 intros; simpl; unfold bin_obj; reflexivity.
631 intros; simpl; unfold bin_obj; reflexivity.
632 intros; simpl; unfold bin_obj; reflexivity.
635 Theorem converter (fc:FreydCategory coqPreMonoidalCat) : forall q:Type, freyd_K(FreydCategory:=fc).
636 intros. exact q. Defined.
638 Notation "` x" := (converter _ x) (at level 1) : temporary_scope1.
639 Notation "`( x )" := (converter _ x) : temporary_scope1.
640 Open Scope temporary_scope1.
641 Notation "a ~~> b" := (freyd_K_hom a b) : category_scope.
643 Close Scope arrow_scope.
644 Open Scope arrow_scope.
645 Open Scope category_scope.
647 Lemma inverse_of_identity_is_identity : forall `{C:Category}{a:C}(i:Isomorphic a a), #i ~~ (id a) -> #i⁻¹ ~~ (id a).
649 transitivity (#i >>> #i⁻¹).
651 symmetry; apply left_identity.
655 Lemma iso_both_sides' :
656 forall `{C:Category}{a b c d:C}(f:a~>b)(g:c~>d)(i1:Isomorphic d b)(i2:Isomorphic c a),
657 f >>> #i1 ⁻¹ ~~ #i2 ⁻¹ >>> g
659 #i2 >>> f ~~ g >>> #i1.
661 apply iso_shift_right.
662 setoid_rewrite <- associativity.
664 apply iso_shift_left.
668 Lemma l1 (fc:FreydCategory coqPreMonoidalCat)`(f:a->b)(d:Type) :
669 fc \ f ⋉ `d ~~ fc \ (fun xy : a * d => let (a0, b0) := xy in ⟨f a0, b0 ⟩).
670 intros; set (freyd_K(FreydCategory:=fc)) as kc.
671 apply (monic #(mf_preserves_first(PreMonoidalFunctor:=fc) d b)).
674 set (ni_commutes (mf_preserves_first(PreMonoidalFunctor:=fc) d) f) as help.
677 apply (transitivity(R:=eqv _ _) help).
679 transitivity (id _ >>> fc \ f ⋉ `d).
680 apply comp_respects; try reflexivity.
681 set (freyd_F_strict_first d a) as help.
682 simpl in help. apply help.
684 transitivity (fc \ f ⋉ `d >>> id _).
685 apply comp_respects; try reflexivity.
686 set (freyd_F_strict_first d b) as help.
687 simpl in help. apply help.
688 transitivity (fc \ f ⋉ `d).
689 apply right_identity.
690 symmetry; apply left_identity.
693 Lemma l2 (fc : FreydCategory coqPreMonoidalCat) : forall `(f:`a~~>`b)`(g:c->d),
694 fc \ (fun xy : a * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩) >>> f ⋉ `d ~~
695 f ⋉ `c >>> fc \ (fun xy : b * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩).
696 intros; set (freyd_K(FreydCategory:=fc)) as kc.
698 apply (monic #((mf_preserves_second(PreMonoidalFunctor:=fc) b d))).
700 transitivity (f ⋉ `c >>> ((fc \ (fun xy : b * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩)) >>>
701 #(mf_preserves_second(PreMonoidalFunctor:=fc) `b d))).
703 transitivity (f ⋉ `c >>> (#(mf_preserves_second(PreMonoidalFunctor:=fc) `b c) >>> (fc >>>> bin_second (fc b)) \ g)).
704 apply comp_respects; try reflexivity.
706 apply (ni_commutes ( (mf_preserves_second(PreMonoidalFunctor:=fc) b)) g).
708 transitivity (((fc \ (fun xy : a * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩) >>> f ⋉ `d)) >>> id _).
709 apply comp_respects; try reflexivity.
710 apply (freyd_F_strict_second(FreydCategory:=fc) b d).
711 transitivity (((fc \ (fun xy : a * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩) >>> f ⋉ `d))).
712 apply right_identity.
714 transitivity (f ⋉ `c >>> (id (`(b*c)) >>> (fc >>>> bin_second (fc b)) \ g)).
715 apply comp_respects; [ reflexivity | idtac ].
716 apply comp_respects; [
717 apply (freyd_F_strict_second(FreydCategory:=fc) b c) |
719 transitivity (f ⋉ `c >>> (fc >>>> bin_second (fc b)) \ g).
720 apply comp_respects; [ reflexivity | apply left_identity ].
721 transitivity (`a ⋊ fc \ g >>> f ⋉ `d).
722 assert (CentralMorphism (fc \ g)). apply freyd_F_central.
723 set (centralmor_second(f:=(fc \ g)) f) as help.
725 apply comp_respects; [ idtac | reflexivity ].
726 apply (epic #(iso_inv _ _ (mf_preserves_second(PreMonoidalFunctor:=fc) a c))).
727 set (iso_epic (((mf_preserves_second a) c) ⁻¹)) as q.
730 transitivity (`a ⋊ fc \ g >>> iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) `a `d)).
731 apply (ni_commutes (ni_inv (mf_preserves_second(PreMonoidalFunctor:=fc) a)) g).
732 transitivity (`a ⋊ fc \ g >>> id _).
733 apply comp_respects; try reflexivity.
734 apply (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a `d)).
735 apply (freyd_F_strict_second(FreydCategory:=fc) a d).
736 transitivity (`a ⋊ fc \ g).
737 apply right_identity.
739 transitivity (id _ >>> `a ⋊ fc \ g).
740 apply comp_respects; try reflexivity.
741 apply (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a `c)).
742 apply (freyd_F_strict_second(FreydCategory:=fc) a c).
746 Lemma l3 (fc : FreydCategory coqPreMonoidalCat) : forall `(f:`a~~>`b)(c:Type),
747 f ⋉ `c >>> fc \ (fun xy : b * c => let (a0, _) := xy in a0) ~~
748 fc \ (fun xy : a * c => let (a0, _) := xy in a0) >>> f.
749 intros; set (freyd_K(FreydCategory:=fc)) as kc.
750 transitivity (f ⋉ `c >>> (fc \ (comp(Category:=coqCategory) _ _ _
751 (fun xy : b * c => let (a0, _) := xy in (a0,tt))
752 (fun xy : b * unit => let (a0, _) := xy in a0)))).
753 apply comp_respects; [ reflexivity | idtac ].
754 simpl; apply (fmor_respects(Functor:=fc)).
755 simpl. intros. destruct x; auto.
757 transitivity (fc \ (comp(Category:=coqCategory) _ _ _
758 (fun xy : a * c => let (a0, _) := xy in (a0,tt))
759 (fun xy : a * unit => let (a0, _) := xy in a0)) >>> f).
760 apply comp_respects; [ idtac | reflexivity ].
761 simpl; apply (fmor_respects(Functor:=fc)).
762 simpl. intros. destruct x; auto.
763 transitivity ((fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>>
764 fc \ (fun xy : a * unit => let (a0, _) := xy in a0)) >>> f).
765 apply comp_respects; [ idtac | reflexivity ].
766 symmetry; apply (fmor_preserves_comp(Functor:=fc)).
768 transitivity (f ⋉ `c >>>
769 (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>>
770 fc \ (fun xy : b * unit => let (a0, _) := xy in a0))).
771 apply comp_respects; [ reflexivity | idtac ].
772 symmetry; apply (fmor_preserves_comp(Functor:=fc)).
773 transitivity (f ⋉ `c >>> (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> #(pmon_cancelr fc b))).
774 apply comp_respects; [ reflexivity | idtac ].
775 apply comp_respects; [ reflexivity | idtac ].
776 apply (freyd_F_strict_cr(FreydCategory:=fc) b).
778 transitivity ((fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> #(pmon_cancelr fc a)) >>> f).
779 apply comp_respects; [ idtac | reflexivity ].
780 apply comp_respects; [ reflexivity | idtac ].
781 apply (freyd_F_strict_cr(FreydCategory:=fc) a).
782 transitivity (((`a ⋊ fc \ (fun _ : c => tt)
783 >>> iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) `a unit)) >>> #(pmon_cancelr fc a)) >>> f).
784 apply comp_respects; [ idtac | reflexivity ].
785 apply comp_respects; [ idtac | reflexivity ].
787 transitivity (iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) a c) >>>
788 fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩)).
790 apply (ni_commutes (ni_inv (mf_preserves_second(PreMonoidalFunctor:=fc) a)) (fun x:c=>tt)).
791 transitivity (id _ >>> fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩)).
792 apply comp_respects; [ idtac | reflexivity ].
793 set (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a `c)) as foo.
796 apply (freyd_F_strict_second(FreydCategory:=fc) a c).
799 transitivity (f ⋉ `c >>>
800 ((#(mf_preserves_second(PreMonoidalFunctor:=fc) b c) >>> `b ⋊ fc \ (fun _ : c => tt)) >>>
801 #(pmon_cancelr fc b))).
802 apply comp_respects; [ reflexivity | idtac ].
803 apply comp_respects; [ idtac | reflexivity ].
804 transitivity (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩)
805 >>> #(mf_preserves_second(PreMonoidalFunctor:=fc) b unit)).
807 transitivity (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> id _).
808 apply comp_respects; [ reflexivity | idtac ].
809 apply (freyd_F_strict_second(FreydCategory:=fc) b unit).
810 apply right_identity.
812 apply (ni_commutes ( (mf_preserves_second(PreMonoidalFunctor:=fc) b)) (fun x:c=>tt)).
813 transitivity (f ⋉ `c >>>
814 ((id _ >>> `b ⋊ fc \ (fun _ : c => tt)) >>>
815 #(pmon_cancelr fc b))).
816 apply comp_respects; [ reflexivity | idtac ].
817 apply comp_respects; [ idtac | reflexivity ].
818 apply comp_respects; [ idtac | reflexivity ].
819 apply (freyd_F_strict_second(FreydCategory:=fc) b c).
820 transitivity (f ⋉ `c >>>
821 ((`b ⋊ fc \ (fun _ : c => tt)) >>>
822 #(pmon_cancelr fc b))).
823 apply comp_respects; [ reflexivity | idtac ].
824 apply comp_respects; [ idtac | reflexivity ].
827 transitivity (((`a ⋊ fc \ (fun _ : c => tt) >>>
829 #(pmon_cancelr fc a)) >>> f).
830 apply comp_respects; [ idtac | reflexivity ].
831 apply comp_respects; [ idtac | reflexivity ].
832 apply comp_respects; [ reflexivity | idtac ].
833 set (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a unit)) as foo.
836 apply (freyd_F_strict_second(FreydCategory:=fc) `a unit).
837 transitivity (((`a ⋊ fc \ (fun _ : c => tt)) >>> #(pmon_cancelr fc a)) >>> f).
838 apply comp_respects; [ idtac | reflexivity ].
839 apply comp_respects; [ idtac | reflexivity ].
840 apply right_identity.
842 transitivity ((f ⋉ `c >>> `b ⋊ fc \ (fun _ : c => tt)) >>> #(pmon_cancelr fc b)).
843 symmetry; apply associativity.
844 transitivity ((`a ⋊ fc \ (fun _ : c => tt) >>> f ⋉ `unit) >>> #(pmon_cancelr fc b)).
845 apply comp_respects; [ idtac | reflexivity ].
846 assert (CentralMorphism (fc \ (fun _ : c => tt))).
847 apply (freyd_F_central(FreydCategory:=fc)).
848 apply (centralmor_second(CentralMorphism:=H)).
849 transitivity (`a ⋊ fc \ (fun _ : c => tt) >>> (f ⋉ `unit >>> #(pmon_cancelr fc b))).
852 transitivity (`a ⋊ fc \ (fun _ : c => tt) >>> (#(pmon_cancelr fc a) >>> f)).
854 apply comp_respects; [ reflexivity | idtac ].
855 set (ni_commutes (pmon_cancelr fc)) as help.
856 simpl in help. apply help.
859 Lemma l4 (fc : FreydCategory coqPreMonoidalCat) : forall `(f:`a~>b)(c d:Type),
860 (f ⋉ `c) ⋉ `d >>> fc \ ((fun xyz:(b*c)*d => let (ab, c) := xyz in let (a0, b0) := ab in ⟨a0, ⟨b0, c ⟩ ⟩))
861 ~~ fc \ ((fun xyz:(a*c)*d => let (ab, c) := xyz in let (a0, b0) := ab in ⟨a0, ⟨b0, c ⟩ ⟩)) >>> f ⋉ _.
862 intros; set (freyd_K(FreydCategory:=fc)) as kc.
865 transitivity (#(pmon_assoc freyd_K_monoidal _ _ _) >>> f ⋉ (c*d:(freyd_K))).
866 apply comp_respects; try reflexivity.
867 apply (freyd_F_strict_a(FreydCategory:=fc) `a d c).
869 transitivity (((f ⋉ (c: (freyd_K))) ⋉ (d:(freyd_K)) >>> #(pmon_assoc freyd_K_monoidal _ _ _))).
870 apply comp_respects; try reflexivity.
871 apply (freyd_F_strict_a(FreydCategory:=fc) `b `d `c).
873 apply (iso_both_sides' _ _ (pmon_assoc fc `b d c) (pmon_assoc fc `a d c)).
875 transitivity ( #(ni_iso (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) `c `d) a) >>>
876 (f ⋉ (c:(freyd_K))) ⋉ (d:(freyd_K))).
877 apply comp_respects; try reflexivity.
879 apply ((pmon_coherent_r(PreMonoidalCat:=freyd_K_monoidal(FreydCategory:=fc))) a c d).
881 transitivity (f ⋉ (c*d:(freyd_K)) >>>
882 #(ni_iso (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) _ _ ) _)).
883 apply comp_respects; try reflexivity.
885 apply ((pmon_coherent_r(PreMonoidalCat:=freyd_K_monoidal(FreydCategory:=fc))) b c d).
888 apply (@ni_commutes _ _ _ _ _ _ _ _ _ _ (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) c d) a `b f).
891 (* Formalized Theorem 3.17 *)
892 Definition Arrow_from_Freyd (fc:FreydCategory coqPreMonoidalCat)
893 : Arrow (fun A B => freyd_K_hom(FreydCategory:=fc) (converter fc A) (converter fc B)).
895 set (freyd_K(FreydCategory:=fc)) as kc.
897 (fun A B => (`A) ~~> (`B))
898 (fun A B => fun f:A->B => fc \ f)
899 (fun (A B C : Type) (X : `A ~~> `B) (X0 : `B ~~> `C) => X >>> X0)
900 (fun (A B C : coqCategory) (X : `A ~~> `B) => X ⋉ `C)
901 (fun (A B : Type) (X X0 : `A ~~> `B) => X ~~ X0));
902 unfold Proper; unfold Reflexive; unfold Symmetric; unfold Transitive; unfold respectful;
904 apply Build_Equivalence.
905 unfold Reflexive; intros. apply Equivalence_Reflexive.
906 unfold Symmetric; intros. apply Equivalence_Symmetric. auto.
907 unfold Transitive; intros. transitivity y; auto.
908 apply comp_respects; auto.
909 apply (fmor_respects(Functor:=(bin_first(BinoidalCat:=fc) `c))); auto.
910 apply (fmor_respects(Functor:=fc)); auto.
911 transitivity ((id _) >>> f).
912 apply comp_respects; try reflexivity.
913 apply (fmor_preserves_id(Functor:=fc)).
915 transitivity (f >>> (id _)).
916 apply comp_respects; try reflexivity.
917 apply (fmor_preserves_id(Functor:=fc)).
918 apply right_identity.
920 symmetry. apply (fmor_preserves_comp(Functor:=fc) f g).
922 symmetry; apply (fmor_preserves_comp(Functor:=(bin_first `d)) f g).
928 (* one half: every Arrow is isomorphic to its implied Freyd category *)
931 (* FIXME: isomorphism of categories must be via a premonoidal functor *)
934 (* FIXME: the isomorphism needs to be a premonoidal functor *)
935 Theorem arrow_both_defs : forall `(ba:Arrow), IsomorphicCategories (Freyd_from_Arrow ba) (ba).
937 apply Build_IsomorphicCategories with (isoc_forward:=ToFunc (functor_id _))(isoc_backward:=ToFunc (functor_id _)).
938 simpl. unfold EqualFunctors. intros.
939 simpl; intros; apply (@heq_morphisms_intro (ba) a b _ _); auto.
940 simpl. unfold EqualFunctors. intros.
941 simpl; intros; apply (@heq_morphisms_intro (ba) a b _ _); auto.
944 (* the other half: [the codomain of] every Freyd category is isomorphic to its implied Arrow *)
945 Theorem arrow_both_defs' : forall (fc:FreydCategory coqPreMonoidalCat), IsomorphicCategories fc ((Arrow_from_Freyd fc)).
946 Lemma iforward (fc:FreydCategory coqPreMonoidalCat) : Functor fc ((Arrow_from_Freyd fc)) (fun x=> x).
947 intros; apply (Build_Functor fc ((Arrow_from_Freyd fc)) _ (fun a b f => f));
948 intros; auto; simpl; [ idtac | reflexivity ];
949 symmetry; apply (fmor_preserves_id(Functor:=fc)).
951 Lemma ibackward (fc:FreydCategory coqPreMonoidalCat) : Functor ((Arrow_from_Freyd fc)) fc (fun x=> x).
952 intros; apply (Build_Functor ((Arrow_from_Freyd fc)) fc _ (fun a b f => f));
953 intros; auto; simpl; [ idtac | reflexivity ];
954 apply (fmor_preserves_id(Functor:=fc)).
956 intros; apply (@Build_IsomorphicCategories _ _ (ToFunc (iforward fc)) (ToFunc (ibackward fc))); simpl; intros; auto.
957 unfold EqualFunctors; simpl; auto.
958 unfold EqualFunctors; simpl; auto.
962 Close Scope arrow_scope.
963 Close Scope temporary_scope1.
964 Open Scope tree_scope.