src/GeneralizedArrowFromReification.v

   1 (*********************************************************************************************************************************)
   2 (* GeneralizedArrowFromReification:                                                                                              *)
   3 (*                                                                                                                               *)
   4 (*   Turn a reification into a generalized arrow                                                                                 *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import Functors_ch1_4.
  13 Require Import Isomorphisms_ch1_5.
  14 Require Import ProductCategories_ch1_6_1.
  15 Require Import OppositeCategories_ch1_6_2.
  16 Require Import Enrichment_ch2_8.
  17 Require Import Subcategories_ch7_1.
  18 Require Import NaturalTransformations_ch7_4.
  19 Require Import NaturalIsomorphisms_ch7_5.
  20 Require Import BinoidalCategories.
  21 Require Import PreMonoidalCategories.
  22 Require Import PreMonoidalCenter.
  23 Require Import MonoidalCategories_ch7_8.
  24 Require Import Coherence_ch7_8.
  25 Require Import Enrichment_ch2_8.
  26 Require Import Enrichments.
  27 Require Import RepresentableStructure_ch7_2.
  28 Require Import Reification.
  29 Require Import GeneralizedArrow.
  30
  31 Section GArrowFromReification.
  32
  33   Definition binoidalcat_iso `{bc:BinoidalCat}{a1 b1 a2 b2:bc} (i1:a1≅a2)(i2:b1≅b2) : (a1⊗b1)≅(a2⊗b2) :=
  34     iso_comp
  35       (functors_preserve_isos (- ⋉ b1) i1 )
  36       (functors_preserve_isos (a2 ⋊ -) i2).
  37
  38   Context  `(K           : SurjectiveEnrichment)
  39            `(CMon        : MonicEnrichment C)
  40             (CM          : MonoidalEnrichment C)
  41             (reification : Reification K C (pmon_I (enr_c_pm C))).
  42
  43   Fixpoint garrow_fobj (vk:senr_v K) : C :=
  44     match vk with
  45     | T_Leaf None     => enr_c_i C
  46     | T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end
  47     | t1,,t2          => bin_obj(BinoidalCat:=enr_c_bin C) (garrow_fobj t1) (garrow_fobj t2)
  48     end.
  49
  50   Fixpoint homset_tensor_iso (vk:enr_v_mon K) : reification vk ≅ enr_c_i C ~~> garrow_fobj vk :=
  51     match vk as VK return reification VK ≅ enr_c_i C ~~> garrow_fobj VK with
  52     | T_Leaf None     => (mf_i(PreMonoidalFunctor:=reification))⁻¹ >>≅>> (mf_i(PreMonoidalFunctor:=CM))
  53     | T_Leaf (Some a) => match a as A
  54                            return reification (T_Leaf (Some A)) ≅ enr_c_i C ~~> garrow_fobj (T_Leaf (Some A)) with
  55                            (s,s0) => iso_inv _ _ (ni_iso (reification_commutes reification s) s0)
  56                          end
  57     | t1,,t2          => (ni_iso (@mf_first _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ reification _) _)⁻¹ >>≅>>
  58                          (binoidalcat_iso (homset_tensor_iso t1) (homset_tensor_iso t2)) >>≅>>
  59                          (ni_iso (mf_first(PreMonoidalFunctor:=CM) (garrow_fobj t2)) _)
  60     end.
  61
  62   Definition HomFunctor_fullimage := FullImage CM.
  63
  64   (* R' is a functor from the domain of the reification functor
  65    * to the full subcategory in the range of the [host language's] Hom(I,-) functor *)
  66   Instance R' : Functor (FullImage (reification_rstar reification)) HomFunctor_fullimage garrow_fobj :=
  67     { fmor := fun a b (f:a~~{FullImage (reification_rstar reification)}~~>b) =>
  68       (#(homset_tensor_iso a)⁻¹ >>> f >>> #(homset_tensor_iso b))
  69     }.
  70     abstract (intros; simpl;
  71               apply comp_respects; try reflexivity;
  72               apply comp_respects; try reflexivity;
  73               auto).
  74     abstract (intros; simpl;
  75       setoid_rewrite right_identity;
  76       apply iso_comp2).
  77     abstract (intros;
  78       simpl;
  79       repeat setoid_rewrite <- associativity;
  80       apply comp_respects; try reflexivity;
  81       repeat setoid_rewrite associativity;
  82       apply comp_respects; try apply reflexivity;
  83       apply comp_respects; try apply reflexivity;
  84       eapply transitivity; [ symmetry; apply associativity | idtac ];
  85       eapply transitivity; [ idtac | apply left_identity ];
  86       apply comp_respects; try apply reflexivity;
  87       apply iso_comp1).
  88       Defined.
  89
  90   (* the "step2_functor" is the section of the Hom(I,-) functor *)
  91   Definition step2_functor :=
  92     ff_functor_section_functor _ (me_full(MonicEnrichment:=CMon)) (me_faithful(MonicEnrichment:=CMon)).
  93
  94   Definition garrow_functor :=
  95     RestrictToImage (reification_rstar reification) >>>> (R' >>>> step2_functor).
  96
  97   Lemma iso_id_lemma1 `{C':Category}(a b:C')(f:a~~{C'}~~>b) : #(iso_id a) >>> f ~~ f.
  98     simpl.
  99     apply left_identity.
 100     Qed.
 101
 102   Lemma iso_id_lemma2 `{C':Category}(a b:C')(f:b~~{C'}~~>a) : f >>> #(iso_id a) ~~ f.
 103     simpl.
 104     apply right_identity.
 105     Qed.
 106
 107   Lemma full_roundtrip : forall a b (f:a~>b), me_homfunctor \ (ff_functor_section_fmor me_homfunctor me_full f) ~~ f.
 108     intros.
 109     unfold ff_functor_section_fmor.
 110     set (me_full a b f) as full.
 111     destruct full.
 112     apply e.
 113     Qed.
 114
 115   Opaque UnderlyingFunctor.
 116   Instance garrow_first a :
 117     (garrow_functor >>>> bin_first(BinoidalCat:=enr_c_bin C) (R' a)) <~~~>
 118     (bin_first(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
 119     { ni_iso := fun a => iso_id _ }.
 120     intros.
 121       etransitivity.  apply iso_id_lemma1.  symmetry.
 122       etransitivity.  apply iso_id_lemma2.  symmetry.
 123
 124     Opaque Underlying.
 125     unfold garrow_functor.
 126       unfold functor_comp at 1.
 127       unfold functor_comp at 1.
 128       Opaque functor_comp. simpl. Transparent functor_comp.
 129
 130     symmetry.
 131       eapply transitivity.
 132       apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_first (R' a)) f).
 133       unfold functor_comp at 1.
 134       unfold functor_comp at 1.
 135       Opaque functor_comp. simpl. Transparent functor_comp.
 136
 137     symmetry.
 138       eapply transitivity.
 139       set (ni_commutes (mf_first(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
 140       unfold functor_comp in qq.
 141       simpl in qq.
 142       apply iso_shift_right' in qq.
 143       apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
 144
 145     apply (me_faithful(MonicEnrichment:=CMon)).
 146       symmetry.
 147       unfold fmor at 1.
 148       eapply transitivity.
 149       set (ni_commutes (mf_first(PreMonoidalFunctor:=CM) (R' a))) as zz.
 150       unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
 151       set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
 152       apply iso_shift_right' in zz'.
 153       apply zz'.
 154
 155     unfold functor_comp; simpl.
 156
 157     symmetry.
 158       eapply transitivity.
 159       set full_roundtrip as full_roundtrip'.
 160       unfold fmor in full_roundtrip'.
 161       simpl in full_roundtrip'.
 162       apply full_roundtrip'.
 163
 164     set (@iso_shift_right') as q. simpl in q. apply q. clear q.
 165
 166     set (@iso_shift_left) as q.   simpl in q. apply q. clear q.
 167
 168     symmetry.
 169       eapply transitivity.
 170       set full_roundtrip as full_roundtrip'.
 171       unfold fmor in full_roundtrip'.
 172       simpl in full_roundtrip'.
 173       apply (fun a' b' f z => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
 174       symmetry.
 175
 176     intros.
 177       unfold bin_obj.
 178       unfold senr_v_bobj.
 179
 180     setoid_rewrite <- associativity.
 181       setoid_rewrite <- associativity.
 182       setoid_rewrite <- associativity.
 183       setoid_rewrite <- associativity.
 184       simpl.
 185       setoid_rewrite <- associativity.
 186       etransitivity.
 187       apply iso_comp1_left.
 188
 189     eapply transitivity.
 190       eapply comp_respects; [ idtac | reflexivity ].
 191       eapply comp_respects; [ idtac | reflexivity ].
 192       eapply comp_respects; [ idtac | reflexivity ].
 193       eapply comp_respects; [ idtac | reflexivity ].
 194       apply iso_comp1_right.
 195
 196     eapply symmetry.
 197       eapply transitivity.
 198       setoid_rewrite <- fmor_preserves_comp.
 199       setoid_rewrite <- fmor_preserves_comp.
 200       eapply reflexivity.
 201       eapply symmetry.
 202
 203     eapply transitivity.
 204       apply associativity.
 205       eapply transitivity.
 206       eapply comp_respects; [ reflexivity | idtac ].
 207       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 208       eapply transitivity.
 209       eapply symmetry.
 210       apply associativity.
 211       apply comp_respects; try apply reflexivity.
 212
 213     eapply transitivity.
 214       eapply comp_respects; [ idtac | reflexivity ].
 215       eapply comp_respects; [ idtac | reflexivity ].
 216       eapply symmetry.
 217       eapply associativity.
 218       eapply transitivity.
 219       eapply comp_respects; [ idtac | reflexivity ].
 220       eapply comp_respects; [ idtac | reflexivity ].
 221       eapply comp_respects; [ idtac | reflexivity ].
 222       apply iso_comp1_left.
 223
 224     eapply transitivity.
 225       eapply comp_respects; [ idtac | reflexivity ].
 226       eapply transitivity.
 227       eapply comp_respects.
 228       eapply symmetry.
 229       eapply associativity.
 230       eapply reflexivity.
 231       apply iso_comp1_left.
 232
 233     eapply transitivity.
 234       eapply comp_respects; [ idtac | reflexivity ].
 235       eapply comp_respects; [ idtac | reflexivity ].
 236       eapply symmetry.
 237       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 238       eapply transitivity.
 239       eapply comp_respects; [ idtac | reflexivity ].
 240       eapply transitivity.
 241       apply associativity.
 242       eapply comp_respects; [ reflexivity | idtac ].
 243       eapply symmetry.
 244       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 245       eapply transitivity.
 246       eapply transitivity.
 247       apply associativity.
 248       eapply comp_respects; [ reflexivity | idtac ].
 249       eapply transitivity.
 250       apply associativity.
 251       eapply transitivity; [ idtac | apply right_identity ].
 252       eapply comp_respects; [ reflexivity | idtac ].
 253       eapply transitivity.
 254       unfold functor_fobj.
 255       apply fmor_preserves_comp.
 256       setoid_rewrite iso_comp2.
 257       apply fmor_preserves_id.
 258
 259     apply comp_respects.
 260       reflexivity.
 261       reflexivity.
 262       Defined.
 263
 264   Instance garrow_second a :
 265        (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a))
 266     <~~~>  (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
 267     { ni_iso := fun a => iso_id _ }.
 268     intros.
 269       etransitivity.  apply iso_id_lemma1.  symmetry.
 270       etransitivity.  apply iso_id_lemma2.  symmetry.
 271
 272     Opaque Underlying.
 273     unfold garrow_functor.
 274       unfold functor_comp at 1.
 275       unfold functor_comp at 1.
 276       Opaque functor_comp. simpl. Transparent functor_comp.
 277
 278     symmetry.
 279       eapply transitivity.
 280       apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f).
 281       unfold functor_comp at 1.
 282       unfold functor_comp at 1.
 283       Opaque functor_comp. simpl. Transparent functor_comp.
 284
 285     symmetry.
 286       eapply transitivity.
 287       set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
 288       unfold functor_comp in qq.
 289       simpl in qq.
 290       apply iso_shift_right' in qq.
 291       apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
 292
 293     apply (me_faithful(MonicEnrichment:=CMon)).
 294       symmetry.
 295       unfold fmor at 1.
 296       eapply transitivity.
 297       set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz.
 298       unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
 299       set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
 300       apply iso_shift_right' in zz'.
 301       apply zz'.
 302
 303     unfold functor_comp; simpl.
 304
 305     symmetry.
 306       eapply transitivity.
 307       set full_roundtrip as full_roundtrip'.
 308       unfold fmor in full_roundtrip'.
 309       simpl in full_roundtrip'.
 310       apply full_roundtrip'.
 311
 312     set (@iso_shift_right') as q. simpl in q. apply q. clear q.
 313
 314     set (@iso_shift_left) as q.   simpl in q. apply q. clear q.
 315
 316     symmetry.
 317       eapply transitivity.
 318       set full_roundtrip as full_roundtrip'.
 319       unfold fmor in full_roundtrip'.
 320       simpl in full_roundtrip'.
 321       apply (fun a' b' f z => fmor_respects (bin_second(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
 322       symmetry.
 323
 324     intros.
 325       unfold bin_obj.
 326       unfold senr_v_bobj.
 327
 328     setoid_rewrite <- associativity.
 329       setoid_rewrite <- associativity.
 330       setoid_rewrite <- associativity.
 331       setoid_rewrite <- associativity.
 332       simpl.
 333       setoid_rewrite <- associativity.
 334       etransitivity.
 335       eapply transitivity.
 336         apply associativity.
 337         eapply transitivity; [ idtac | apply right_identity ].
 338         apply comp_respects; [ reflexivity | idtac ].
 339         etransitivity.
 340         apply comp_respects; [ idtac | reflexivity ].
 341         apply (mf_consistent(PreMonoidalFunctor:=CM)).
 342         apply iso_comp1.
 343
 344     eapply transitivity.
 345       eapply comp_respects; [ idtac | reflexivity ].
 346       eapply comp_respects; [ idtac | reflexivity ].
 347       eapply comp_respects; [ idtac | reflexivity ].
 348       eapply comp_respects; [ idtac | reflexivity ].
 349       eapply transitivity.
 350         eapply symmetry.
 351         eapply associativity.
 352       eapply transitivity; [ idtac | apply left_identity ].
 353       eapply comp_respects; [ idtac | reflexivity ].
 354       eapply transitivity.
 355         eapply comp_respects; [ idtac | reflexivity ].
 356         eapply symmetry.
 357         apply (mf_consistent(PreMonoidalFunctor:=CM)).
 358         apply iso_comp1.
 359
 360     eapply symmetry.
 361       eapply transitivity.
 362       setoid_rewrite <- fmor_preserves_comp.
 363       setoid_rewrite <- fmor_preserves_comp.
 364       eapply reflexivity.
 365       eapply symmetry.
 366
 367     apply comp_respects; try reflexivity.
 368
 369     eapply transitivity.
 370       apply associativity.
 371       eapply transitivity.
 372       apply associativity.
 373       eapply transitivity.
 374       apply associativity.
 375       eapply transitivity.
 376       apply associativity.
 377       apply comp_respects; try reflexivity.
 378
 379     eapply transitivity.
 380       eapply comp_respects; [ reflexivity | idtac ].
 381       eapply transitivity.
 382       eapply comp_respects; [ idtac | reflexivity ].
 383       apply mf_consistent.
 384       eapply transitivity.
 385       eapply comp_respects; [ reflexivity | idtac ].
 386         apply associativity.
 387       apply iso_comp1_right.
 388
 389     eapply transitivity.
 390       eapply comp_respects; [ reflexivity | idtac ].
 391       eapply transitivity.
 392         apply associativity.
 393       eapply comp_respects; [ reflexivity | idtac ].
 394       eapply transitivity.
 395         eapply symmetry.
 396         apply associativity.
 397       eapply transitivity; [ idtac | apply left_identity ].
 398       eapply comp_respects; [ idtac | reflexivity ].
 399       eapply transitivity.
 400         eapply comp_respects; [ idtac | reflexivity ].
 401         eapply symmetry.
 402         eapply (mf_consistent(PreMonoidalFunctor:=reification)).
 403       apply iso_comp1.
 404
 405     eapply transitivity.
 406       eapply comp_respects; [ reflexivity | idtac ].
 407       eapply symmetry.
 408       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 409       eapply transitivity; [ idtac | apply right_identity ].
 410
 411     eapply transitivity.
 412       eapply symmetry.
 413       apply associativity.
 414     eapply transitivity.
 415       eapply comp_respects; [ idtac | reflexivity ].
 416       unfold functor_fobj.
 417       apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
 418
 419     apply symmetry.
 420       eapply transitivity.
 421       apply right_identity.
 422       apply symmetry.
 423       eapply transitivity; [ idtac | apply left_identity ].
 424       apply comp_respects; [ idtac | reflexivity ].
 425
 426     eapply transitivity.
 427       Focus 2.
 428       eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
 429       idtac.
 430       apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
 431       apply iso_comp2.
 432     Defined.
 433
 434 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 435 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 436 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 437
 438   Lemma assoc_coherent (a b c : enr_v K) :
 439    (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C)
 440      (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>>
 441    #((garrow_second a) (b ⊗ c)) ~~
 442    (#((garrow_second a) b) ⋉ garrow_functor c >>>
 443      #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
 444     Opaque Underlying.
 445     eapply transitivity.
 446       eapply transitivity; [ idtac | apply right_identity ].
 447       eapply comp_respects; [ eapply reflexivity | idtac ].
 448       reflexivity.
 449
 450     apply symmetry.
 451       eapply transitivity.
 452       eapply transitivity; [ idtac | apply left_identity ].
 453       eapply comp_respects; [ idtac | eapply reflexivity ].
 454       eapply transitivity; [ idtac | apply right_identity ].
 455       apply comp_respects.
 456       simpl.
 457       apply (fmor_preserves_id (ebc_first (garrow_functor c))).
 458       reflexivity.
 459
 460     symmetry.
 461       eapply transitivity.
 462       eapply transitivity; [ idtac | apply right_identity ].
 463       apply comp_respects.
 464       reflexivity.
 465       simpl.
 466       apply (fmor_preserves_id (ebc_second (garrow_functor a))).
 467       symmetry.
 468
 469     unfold functor_fobj.
 470       unfold garrow_functor.
 471       unfold step2_functor.
 472       Opaque R'.
 473       Opaque ff_functor_section_functor.
 474       unfold functor_comp.
 475       simpl.
 476       Transparent R'.
 477       Transparent ff_functor_section_functor.
 478       idtac.
 479       apply (me_faithful(MonicEnrichment:=CMon)).
 480       eapply transitivity; [ eapply full_roundtrip | idtac ].
 481
 482     unfold fmor at 1.
 483       unfold R'.
 484       unfold me_homfunctor.
 485       set (mf_assoc(PreMonoidalFunctor:=reification) a b c) as q.
 486       set (mf_assoc(PreMonoidalFunctor:=CM) (garrow_fobj a) (garrow_fobj b) (garrow_fobj c)) as q'.
 487       unfold mf_F in q'.
 488       unfold pmon_I in q'.
 489       admit.
 490       Qed.
 491
 492   Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
 493     iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
 494     #((mf_first F b) _) >>>  F \ #(pmon_cancell b).
 495     set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
 496     setoid_rewrite associativity in q.
 497     set (@comp_respects) as qq.
 498     unfold Proper in qq.
 499     unfold respectful in qq.
 500     set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
 501     setoid_rewrite <- associativity in q'.
 502     clear q qq.
 503     setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
 504     eapply transitivity; [ apply q' | idtac ].
 505     clear q'.
 506     setoid_rewrite <- associativity.
 507     apply comp_respects; try reflexivity.
 508     symmetry.
 509     apply iso_shift_left.
 510     setoid_rewrite iso_comp1.
 511     symmetry.
 512     eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
 513     apply (fmor_respects (-⋉ F b)).
 514     apply iso_comp2.
 515     Qed.
 516
 517   Lemma cancell_coherent (b:enr_v K) :
 518    #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
 519    (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
 520     #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
 521     Opaque Underlying.
 522     Opaque fmor.
 523     intros; simpl.
 524       setoid_rewrite right_identity.
 525       symmetry.
 526       eapply transitivity; [ idtac | apply left_identity ].
 527       apply comp_respects.
 528       apply (fmor_preserves_id (ebc_first (garrow_functor b))).
 529       unfold garrow_functor.
 530       unfold step2_functor.
 531       Transparent fmor.
 532       unfold functor_fobj.
 533       unfold functor_comp.
 534       simpl.
 535
 536       apply (me_faithful(MonicEnrichment:=CMon)).
 537       eapply transitivity; [ eapply full_roundtrip | idtac ].
 538
 539       eapply transitivity.
 540       apply comp_respects; [ idtac | reflexivity ].
 541       apply comp_respects; [ idtac | reflexivity ].
 542       apply comp_respects; [ reflexivity | idtac ].
 543       apply comp_respects; [ idtac | reflexivity ].
 544       apply comp_respects; [ reflexivity | idtac ].
 545       eapply symmetry.
 546       apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
 547
 548       apply symmetry.
 549       apply iso_shift_left.
 550
 551       symmetry.
 552       eapply transitivity.
 553       eapply transitivity.
 554       apply associativity.
 555       apply comp_respects; [ reflexivity | idtac ].
 556       eapply transitivity.
 557       apply associativity.
 558       eapply transitivity.
 559       apply associativity.
 560       apply comp_respects; [ reflexivity | idtac ].
 561       eapply transitivity.
 562       apply associativity.
 563       apply comp_respects; [ reflexivity | idtac ].
 564       eapply symmetry.
 565       set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
 566       eapply transitivity; [ idtac | apply associativity ].
 567       apply q.
 568
 569       apply iso_shift_left'.
 570       eapply transitivity.
 571       apply associativity.
 572       symmetry.
 573       set (@iso_shift_right') as qq.
 574       simpl in qq.
 575       apply qq.
 576       clear qq.
 577       unfold me_homfunctor.
 578       eapply transitivity.
 579       symmetry.
 580       apply (cancell_lemma CM (garrow_fobj b)).
 581
 582       apply symmetry.
 583       eapply transitivity.
 584       apply comp_respects; [ idtac | reflexivity ].
 585       eapply transitivity.
 586       eapply symmetry.
 587       eapply associativity.
 588       apply comp_respects; [ idtac | reflexivity ].
 589       eapply symmetry.
 590       eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 591
 592       eapply transitivity.
 593       apply associativity.
 594       eapply transitivity.
 595       apply associativity.
 596       apply comp_respects; try reflexivity.
 597
 598       unfold functor_fobj.
 599       unfold pmon_I.
 600
 601       set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
 602       eapply transitivity.
 603       eapply symmetry.
 604       apply associativity.
 605       eapply transitivity.
 606       apply comp_respects; [ idtac | reflexivity ].
 607       eapply symmetry.
 608       apply q.
 609       clear q.
 610       unfold fmor; simpl.
 611
 612       eapply transitivity.
 613       apply associativity.
 614       eapply transitivity; [ idtac | apply right_identity ].
 615       apply comp_respects; try reflexivity.
 616       apply iso_comp2.
 617       Qed.
 618
 619   Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
 620     (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
 621     #((mf_first F _) _) >>>  F \ #(pmon_cancelr b).
 622     set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
 623     setoid_rewrite associativity in q.
 624     set (@comp_respects) as qq.
 625     unfold Proper in qq.
 626     unfold respectful in qq.
 627     set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
 628     setoid_rewrite <- associativity in q'.
 629     clear q qq.
 630     setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
 631     eapply transitivity; [ apply q' | idtac ].
 632     clear q'.
 633     setoid_rewrite <- associativity.
 634     apply comp_respects; try reflexivity.
 635     symmetry.
 636     apply iso_shift_left.
 637     setoid_rewrite iso_comp1.
 638     symmetry.
 639     eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
 640     apply (fmor_respects (-⋉ F b)).
 641     apply iso_comp2.
 642     Qed.
 643
 644   Lemma cancelr_coherent (b:enr_v K) :
 645    #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
 646    (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
 647     #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
 648     Opaque Underlying.
 649     Opaque fmor.
 650     intros; simpl.
 651       setoid_rewrite right_identity.
 652       symmetry.
 653       eapply transitivity; [ idtac | apply left_identity ].
 654       apply comp_respects.
 655       apply (fmor_preserves_id (ebc_second (garrow_functor b))).
 656       unfold garrow_functor.
 657       unfold step2_functor.
 658       Transparent fmor.
 659       unfold functor_fobj.
 660       unfold functor_comp.
 661       simpl.
 662
 663       apply (me_faithful(MonicEnrichment:=CMon)).
 664       eapply transitivity; [ eapply full_roundtrip | idtac ].
 665
 666       eapply transitivity.
 667       apply comp_respects; [ idtac | reflexivity ].
 668       apply comp_respects; [ idtac | reflexivity ].
 669       apply comp_respects; [ reflexivity | idtac ].
 670       apply comp_respects; [ idtac | reflexivity ].
 671       apply comp_respects; [ idtac | reflexivity ].
 672       eapply symmetry.
 673       apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
 674
 675       apply symmetry.
 676       apply iso_shift_left.
 677
 678       symmetry.
 679       eapply transitivity.
 680       eapply transitivity.
 681       apply associativity.
 682       apply comp_respects; [ reflexivity | idtac ].
 683       eapply transitivity.
 684       apply associativity.
 685
 686       set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
 687       setoid_rewrite associativity in q.
 688
 689       eapply transitivity.
 690       apply associativity.
 691       eapply transitivity.
 692       apply associativity.
 693       apply comp_respects; [ reflexivity | idtac ].
 694       eapply transitivity.
 695       eapply symmetry.
 696       apply associativity.
 697       eapply transitivity.
 698       apply comp_respects; [ idtac | reflexivity ].
 699       symmetry.
 700       eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 701       eapply transitivity.
 702       apply associativity.
 703       apply comp_respects; [ reflexivity | idtac ].
 704       eapply transitivity.
 705       apply comp_respects; [ reflexivity | idtac ].
 706       apply comp_respects; [ idtac | reflexivity ].
 707       apply mf_consistent.
 708       eapply symmetry.
 709       apply q.
 710
 711       apply iso_shift_left'.
 712       eapply transitivity.
 713       apply associativity.
 714       symmetry.
 715       set (@iso_shift_right') as qq.
 716       simpl in qq.
 717       apply qq.
 718       clear qq.
 719       unfold me_homfunctor.
 720       eapply transitivity.
 721       symmetry.
 722       apply (cancelr_lemma CM (garrow_fobj b)).
 723
 724       unfold functor_fobj.
 725       unfold pmon_I.
 726
 727       set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
 728       apply symmetry.
 729       eapply transitivity.
 730       apply comp_respects; [ idtac | reflexivity ].
 731       apply comp_respects; [ reflexivity | idtac ].
 732       eapply symmetry.
 733       apply q.
 734       clear q.
 735
 736       eapply transitivity.
 737       apply associativity.
 738       apply comp_respects; try reflexivity.
 739       simpl.
 740
 741       eapply transitivity.
 742       apply associativity.
 743       eapply transitivity; [ idtac | apply right_identity ].
 744       apply comp_respects; try reflexivity.
 745       apply iso_comp2.
 746       Qed.
 747
 748   Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
 749   { mf_first      := garrow_first
 750   ; mf_second     := garrow_second
 751   ; mf_i          := iso_id _ }.
 752     intros; reflexivity.
 753     intros; apply (reification_host_lang_pure _ _ _ reification).
 754     apply cancell_coherent.
 755     apply cancelr_coherent.
 756     apply assoc_coherent.
 757     Defined.
 758
 759   Definition garrow_from_reification : GeneralizedArrow K CM :=
 760     {| ga_functor_monoidal := garrow_monoidal
 761      ; ga_host_lang_pure   := reification_host_lang_pure _ _ _ reification
 762     |}.
 763
 764 End GArrowFromReification.
 765