src/Arrows.v

   1 (*******************************************************************************)
   2 (* Hughes Arrows                                                               *)
   3 (*******************************************************************************)
   4
   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.
  21
  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 ⟩ ⟩).
  25
  26 Class Arrow
  27 ( arr_hom'            :  Type->Type->Type      ) :=
  28 { arr_hom             := arr_hom' (* hack to make Coq notations work *)     where "a ~> b" := (arr_hom a b)
  29
  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)
  33
  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)
  36
  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)
  40
  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⋊_
  50 }.
  51
  52 (*
  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⁻¹)
  60 *)
  61
  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.
  71   Defined.
  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.
  75   Defined.
  76
  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.
  81
  82 Open Scope arrow_scope.
  83
  84 (* Formalized Definition 2.3 *)
  85 Class BiArrow
  86 ( biarr_hom   :  Type -> Type -> Type            ) :=
  87 { biarr_super :> Arrow biarr_hom
  88
  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)
  91
  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 ⋊ _)
 103
 104 (* for complete example, we'd also need biarr_biarr_respects and biarr_inv_respects, but this paper isn't about BiArrows *)
 105 }.
 106
 107 Notation "f <--> g" := (biarr_biarr g f) :biarrow_scope.
 108 Notation "! f"      := (biarr_inv     f) :biarrow_scope.
 109
 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.
 114
 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.
 120
 121 (* Formalized Lemma 3.2 *)
 122 Definition arrows_are_categories : forall `(ba:Arrow), Category Type arr_hom.
 123   intros.
 124   refine
 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.
 131   Defined.
 132 Coercion arrows_are_categories : Arrow >-> Category.
 133
 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 *)
 135 Ltac magic :=
 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 *)
 145
 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
 159     ]; intros; auto.
 160     idtac.
 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.
 176     Defined.
 177
 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.
 184     Defined.
 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).
 189     intros;
 190       transitivity (
 191         arr_comp(Arrow:=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))
 194       ).
 195     symmetry.
 196     apply (arr_unit(Arrow:=ba)(c:=(Datatypes.unit)) f).
 197     apply Equivalence_Reflexive.
 198     Defined.
 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.
 206     Defined.
 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).
 211     intros. simpl.
 212     repeat setoid_rewrite arr_associativity.
 213       setoid_rewrite <- arr_comp_preserves.
 214       simpl;
 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.
 219       magic.
 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.
 225       destruct x; auto.
 226       apply Equivalence_Reflexive.
 227       apply arr_arr_respects.
 228       intros; destruct X; auto.
 229       intros; destruct X; auto.
 230       unfold extensionality; intros; simpl.
 231       destruct x.
 232       auto.
 233    Defined.
 234
 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.
 241     Defined.
 242   Definition arrow_assoc_ni_iso `(ba:Arrow) :
 243   (∀A : ba, ∀B : ba,
 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).
 248   intros.
 249   eapply Build_NaturalIsomorphism.
 250   instantiate (1:=(fun X:ba => (arrow_assoc_iso ba A X B))).
 251   simpl; intros.
 252   setoid_rewrite arr_first_preserves.
 253   setoid_rewrite arr_first_preserves.
 254   setoid_rewrite arr_associativity.
 255   setoid_replace
 256     ( (arr_first(Arrow:=ba) A (arr_first(Arrow:=ba) B f)) >>> @arr_arr arr_hom' ba (B0 * B * A) (A * (B0 * B)) _swap)
 257     with
 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.
 263   setoid_replace
 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)))
 267     with
 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.
 281   repeat magic.
 282   repeat setoid_rewrite <- arr_associativity.
 283   repeat magic.
 284   repeat setoid_rewrite arr_associativity.
 285   repeat magic.
 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.
 293   reflexivity.
 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.
 300   magic.
 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.
 304   reflexivity.
 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.
 312   repeat magic.
 313   reflexivity.
 314   repeat magic.
 315   repeat setoid_rewrite arr_associativity.
 316   repeat magic.
 317   apply arr_comp_respects.
 318   reflexivity.
 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.
 325   repeat magic.
 326   apply arr_comp_respects.
 327   reflexivity.
 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.
 333   Defined.
 334
 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)
 340       >>>>
 341       (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) b)).
 342     intros; eapply Build_NaturalIsomorphism.
 343     instantiate(1:=arrow_assoc_rr_iso ba a b).
 344     intros.
 345     simpl.
 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.
 352     magic.
 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.
 358     intros; auto.
 359     transitivity (arr_first(Arrow:=ba) b (arr_first(Arrow:=ba) a f) >>> arr_arr (fun x=>x)).
 360     setoid_rewrite arr_right_identity.
 361     reflexivity.
 362     apply arr_comp_respects.
 363     reflexivity.
 364     apply arr_arr_respects.
 365     intros. destruct X. destruct p. auto.
 366     intros. destruct X. destruct p. auto.
 367     unfold extensionality.
 368     intros; auto.
 369     destruct x.
 370     destruct p.
 371     auto.
 372     setoid_rewrite <- arr_associativity.
 373     magic.
 374     transitivity (arr_arr (fun x=>x) >>> (arr_first(Arrow:=ba) (a*b) f)).
 375     setoid_rewrite arr_left_identity.
 376     reflexivity.
 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.
 382     intros; auto.
 383     destruct x.
 384     destruct p.
 385     auto.
 386     reflexivity.
 387     Defined.
 388
 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)
 394       >>>>
 395       (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) a)).
 396   intros.
 397   eapply Build_NaturalIsomorphism.
 398   simpl; intros.
 399   instantiate(1:=(arrow_assoc_ll_iso ba a b)).
 400   simpl.
 401   magic.
 402   repeat setoid_rewrite arr_associativity.
 403   setoid_replace
 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))
 406     with
 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) >>>
 413        arr_arr(Arrow:=ba)
 414          (fun xy : B * (b * a) =>
 415           let (a0, b0) := xy in ⟨a0, let (y, z) := b0 in ⟨z, y ⟩ ⟩))
 416   with
 417     (arr_arr(a:=((A*b)*a)) _assoc >>> ((arr_first(Arrow:=ba) (b*a) f) >>>
 418       arr_arr(Arrow:=ba)
 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.
 422   repeat magic.
 423   repeat setoid_rewrite <- arr_associativity.
 424   repeat magic.
 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.
 431   destruct x.
 432   destruct b0.
 433   auto.
 434   reflexivity.
 435   apply arr_arr_respects.
 436   intros. destruct X. destruct b1. auto.
 437   intros. destruct X. destruct b1. auto.
 438   unfold extensionality; intros; simpl.
 439   destruct x.
 440   destruct b1.
 441   auto.
 442   repeat setoid_rewrite <- arr_associativity.
 443   apply arr_comp_respects.
 444   reflexivity.
 445   apply arr_arr_respects.
 446   intros. destruct X. destruct p. auto.
 447   intros. destruct X. destruct p. auto.
 448   unfold extensionality; intros; simpl.
 449   destruct x.
 450   destruct p.
 451   auto.
 452   setoid_rewrite arr_extension.
 453   repeat setoid_rewrite arr_associativity.
 454   magic.
 455   apply arr_comp_respects.
 456   reflexivity.
 457   apply arr_arr_respects.
 458   intros. destruct X. destruct p. auto.
 459   intros. destruct X. destruct p. auto.
 460   unfold extensionality; intros; simpl.
 461   destruct x.
 462   destruct p.
 463   auto.
 464   Defined.
 465
 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
 472   }.
 473   apply Build_Pentagon; intros.
 474   intros; simpl.
 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)
 490   | idtac
 491   ]; unfold extensionality; intros; simpl; destruct x; destruct u; destruct u0; auto.
 492   intros; reflexivity.
 493   intros; reflexivity.
 494   Defined.
 495
 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
 500     | reflexivity
 501     | symmetry; apply arr_comp_preserves ].
 502   Defined.
 503
 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
 507 }.
 508   simpl; apply iso_id.
 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.
 516   intros.
 517   intros; apply Build_CentralMorphism; intros. simpl.
 518
 519   simpl.
 520   setoid_rewrite arr_extension.
 521   setoid_rewrite <- arr_associativity.
 522   setoid_rewrite <- arr_associativity.
 523   repeat setoid_rewrite <- arr_comp_preserves.
 524   transitivity (
 525     arr_arr (fun x:a*c => let (a0,c0) := x in (c0,a0))
 526     >>>
 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.
 547
 548   simpl.
 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.
 561   Defined.
 562
 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.
 571   Defined.
 572
 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));
 575     intros; simpl;
 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.
 581   Defined.
 582
 583 Instance arrows_are_symmetric `(ba:Arrow) : SymmetricCat (arrows_are_braided ba).
 584   intros; apply Build_SymmetricCat; intros. simpl. reflexivity.
 585   Defined.
 586
 587 Instance Freyd_from_Arrow `(ba:Arrow)
 588 : FreydCategory coqPreMonoidalCat :=
 589 { freyd_C_cartesian   := coqCartesianCat
 590 ; freyd_K             := ba
 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
 596 }.
 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.
 601   setoid_replace
 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))
 603       with
 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.
 613
 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.
 619
 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.
 627
 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.
 633   Defined.
 634
 635 Theorem converter (fc:FreydCategory coqPreMonoidalCat) : forall q:Type, freyd_K(FreydCategory:=fc).
 636    intros. exact q. Defined.
 637
 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.
 642
 643 Close Scope arrow_scope.
 644 Open Scope arrow_scope.
 645 Open Scope category_scope.
 646
 647 Lemma inverse_of_identity_is_identity : forall `{C:Category}{a:C}(i:Isomorphic a a), #i ~~ (id a) -> #i⁻¹ ~~ (id a).
 648   intros.
 649   transitivity (#i >>> #i⁻¹).
 650   setoid_rewrite H.
 651   symmetry; apply left_identity.
 652   apply iso_comp1.
 653   Qed.
 654
 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
 658   ->
 659   #i2 >>> f ~~ g >>> #i1.
 660   symmetry.
 661   apply iso_shift_right.
 662   setoid_rewrite <- associativity.
 663   symmetry.
 664   apply iso_shift_left.
 665   auto.
 666   Qed.
 667
 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)).
 672     apply iso_monic.
 673   symmetry.
 674   set (ni_commutes (mf_preserves_first(PreMonoidalFunctor:=fc) d) f) as help.
 675     simpl in help.
 676     symmetry in help.
 677     apply (transitivity(R:=eqv _ _) help).
 678     clear 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.
 683   symmetry.
 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.
 691   Qed.
 692
 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.
 697   symmetry.
 698   apply (monic #((mf_preserves_second(PreMonoidalFunctor:=fc) b d))).
 699     apply iso_monic.
 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))).
 702     apply associativity.
 703   transitivity (f ⋉ `c >>> (#(mf_preserves_second(PreMonoidalFunctor:=fc) `b c) >>> (fc >>>> bin_second (fc b)) \ g)).
 704     apply comp_respects; try reflexivity.
 705     symmetry.
 706     apply (ni_commutes ( (mf_preserves_second(PreMonoidalFunctor:=fc) b)) g).
 707   symmetry.
 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.
 713   symmetry.
 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) |
 718       reflexivity ].
 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.
 724     apply 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.
 728     apply q.
 729   symmetry.
 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.
 738   symmetry.
 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).
 743   apply left_identity.
 744   Qed.
 745
 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.
 756    symmetry.
 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)).
 767    symmetry.
 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).
 777    symmetry.
 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 ].
 786      symmetry.
 787      transitivity (iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) a c) >>>
 788        fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩)).
 789      symmetry.
 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.
 794      simpl in foo.
 795      apply foo.
 796      apply (freyd_F_strict_second(FreydCategory:=fc) a c).
 797      apply left_identity.
 798    symmetry.
 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)).
 806      symmetry.
 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.
 811      symmetry.
 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 ].
 825      apply left_identity.
 826      symmetry.
 827      transitivity (((`a ⋊ fc \ (fun _ : c => tt) >>>
 828        id _) >>>
 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.
 834      simpl in foo.
 835      apply 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.
 841    symmetry.
 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))).
 850      apply associativity.
 851    symmetry.
 852    transitivity (`a ⋊ fc \ (fun _ : c => tt) >>> (#(pmon_cancelr fc a) >>> f)).
 853      apply associativity.
 854      apply comp_respects; [ reflexivity | idtac ].
 855    set (ni_commutes (pmon_cancelr fc)) as help.
 856      simpl in help. apply help.
 857    Qed.
 858
 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.
 863    simpl in f.
 864    symmetry.
 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).
 868    symmetry.
 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).
 872    symmetry.
 873    apply (iso_both_sides' _ _ (pmon_assoc fc `b d c) (pmon_assoc fc `a d c)).
 874    symmetry.
 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.
 878    symmetry.
 879    apply ((pmon_coherent_r(PreMonoidalCat:=freyd_K_monoidal(FreydCategory:=fc))) a c d).
 880    symmetry.
 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.
 884    symmetry.
 885    apply ((pmon_coherent_r(PreMonoidalCat:=freyd_K_monoidal(FreydCategory:=fc))) b c d).
 886    symmetry.
 887    simpl.
 888    apply (@ni_commutes _ _ _ _ _ _ _ _ _ _ (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) c d) a `b f).
 889    Qed.
 890
 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)).
 894     intros.
 895     set (freyd_K(FreydCategory:=fc)) as kc.
 896     apply (@Build_Arrow
 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;
 903     intros ; simpl.
 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)).
 914       apply left_identity.
 915     transitivity (f >>> (id _)).
 916       apply comp_respects; try reflexivity.
 917       apply (fmor_preserves_id(Functor:=fc)).
 918       apply right_identity.
 919     apply associativity.
 920     symmetry. apply (fmor_preserves_comp(Functor:=fc) f g).
 921     apply (l1 fc f d).
 922     symmetry; apply (fmor_preserves_comp(Functor:=(bin_first `d)) f g).
 923     apply (l2 fc f g).
 924     apply (l3 fc f c).
 925     apply (l4 fc f c d).
 926   Defined.
 927
 928 (* one half: every Arrow is isomorphic to its implied Freyd category *)
 929 (*
 930
 931 (* FIXME: isomorphism of categories must be via a premonoidal functor *)
 932
 933
 934 (* FIXME: the isomorphism needs to be a premonoidal functor *)
 935 Theorem arrow_both_defs : forall `(ba:Arrow), IsomorphicCategories (Freyd_from_Arrow ba) (ba).
 936   intros.
 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.
 942   Defined.
 943
 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)).
 950       Defined.
 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)).
 955         Defined.
 956   intros; apply (@Build_IsomorphicCategories _ _ (ToFunc (iforward fc)) (ToFunc (ibackward fc))); simpl; intros; auto.
 957     unfold EqualFunctors; simpl; auto.
 958     unfold EqualFunctors; simpl; auto.
 959   Defined.
 960 *)
 961
 962 Close Scope arrow_scope.
 963 Close Scope temporary_scope1.
 964 Open Scope tree_scope.
 965