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     admit.
 269     Defined.
 270
 271 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 272 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 273 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 274
 275   Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
 276     iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
 277     #((mf_first F b) _) >>>  F \ #(pmon_cancell b).
 278     set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
 279     setoid_rewrite associativity in q.
 280     set (@comp_respects) as qq.
 281     unfold Proper in qq.
 282     unfold respectful in qq.
 283     set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
 284     setoid_rewrite <- associativity in q'.
 285     clear q qq.
 286     setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
 287     eapply transitivity; [ apply q' | idtac ].
 288     clear q'.
 289     setoid_rewrite <- associativity.
 290     apply comp_respects; try reflexivity.
 291     symmetry.
 292     apply iso_shift_left.
 293     setoid_rewrite iso_comp1.
 294     symmetry.
 295     eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
 296     apply (fmor_respects (-⋉ F b)).
 297     apply iso_comp2.
 298     Qed.
 299
 300   Lemma cancell_coherent (b:enr_v K) :
 301    #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
 302    (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
 303     #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
 304     Opaque Underlying.
 305     Opaque fmor.
 306     intros; simpl.
 307       setoid_rewrite right_identity.
 308       symmetry.
 309       eapply transitivity; [ idtac | apply left_identity ].
 310       apply comp_respects.
 311       apply (fmor_preserves_id (ebc_first (garrow_functor b))).
 312       unfold garrow_functor.
 313       unfold step2_functor.
 314       Transparent fmor.
 315       unfold functor_fobj.
 316       unfold functor_comp.
 317       simpl.
 318
 319       apply (me_faithful(MonicEnrichment:=CMon)).
 320       eapply transitivity; [ eapply full_roundtrip | idtac ].
 321
 322       eapply transitivity.
 323       apply comp_respects; [ idtac | reflexivity ].
 324       apply comp_respects; [ idtac | reflexivity ].
 325       apply comp_respects; [ reflexivity | idtac ].
 326       apply comp_respects; [ idtac | reflexivity ].
 327       apply comp_respects; [ reflexivity | idtac ].
 328       eapply symmetry.
 329       apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
 330
 331       apply symmetry.
 332       apply iso_shift_left.
 333
 334       symmetry.
 335       eapply transitivity.
 336       eapply transitivity.
 337       apply associativity.
 338       apply comp_respects; [ reflexivity | idtac ].
 339       eapply transitivity.
 340       apply associativity.
 341       eapply transitivity.
 342       apply associativity.
 343       apply comp_respects; [ reflexivity | idtac ].
 344       eapply transitivity.
 345       apply associativity.
 346       apply comp_respects; [ reflexivity | idtac ].
 347       eapply symmetry.
 348       set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
 349       eapply transitivity; [ idtac | apply associativity ].
 350       apply q.
 351
 352       apply iso_shift_left'.
 353       eapply transitivity.
 354       apply associativity.
 355       symmetry.
 356       set (@iso_shift_right') as qq.
 357       simpl in qq.
 358       apply qq.
 359       clear qq.
 360       unfold me_homfunctor.
 361       eapply transitivity.
 362       symmetry.
 363       apply (cancell_lemma CM (garrow_fobj b)).
 364
 365       apply symmetry.
 366       eapply transitivity.
 367       apply comp_respects; [ idtac | reflexivity ].
 368       eapply transitivity.
 369       eapply symmetry.
 370       eapply associativity.
 371       apply comp_respects; [ idtac | reflexivity ].
 372       eapply symmetry.
 373       eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 374
 375       eapply transitivity.
 376       apply associativity.
 377       eapply transitivity.
 378       apply associativity.
 379       apply comp_respects; try reflexivity.
 380
 381       unfold functor_fobj.
 382       unfold pmon_I.
 383
 384       set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
 385       eapply transitivity.
 386       eapply symmetry.
 387       apply associativity.
 388       eapply transitivity.
 389       apply comp_respects; [ idtac | reflexivity ].
 390       eapply symmetry.
 391       apply q.
 392       clear q.
 393       unfold fmor; simpl.
 394
 395       eapply transitivity.
 396       apply associativity.
 397       eapply transitivity; [ idtac | apply right_identity ].
 398       apply comp_respects; try reflexivity.
 399       apply iso_comp2.
 400       Qed.
 401
 402   Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
 403     (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
 404     #((mf_first F _) _) >>>  F \ #(pmon_cancelr b).
 405     set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
 406     setoid_rewrite associativity in q.
 407     set (@comp_respects) as qq.
 408     unfold Proper in qq.
 409     unfold respectful in qq.
 410     set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
 411     setoid_rewrite <- associativity in q'.
 412     clear q qq.
 413     setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
 414     eapply transitivity; [ apply q' | idtac ].
 415     clear q'.
 416     setoid_rewrite <- associativity.
 417     apply comp_respects; try reflexivity.
 418     symmetry.
 419     apply iso_shift_left.
 420     setoid_rewrite iso_comp1.
 421     symmetry.
 422     eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
 423     apply (fmor_respects (-⋉ F b)).
 424     apply iso_comp2.
 425     Qed.
 426
 427   Lemma cancelr_coherent (b:enr_v K) :
 428    #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
 429    (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
 430     #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
 431
 432     Opaque Underlying.
 433     Opaque fmor.
 434     intros; simpl.
 435       setoid_rewrite right_identity.
 436       symmetry.
 437       eapply transitivity; [ idtac | apply left_identity ].
 438       apply comp_respects.
 439       apply (fmor_preserves_id (ebc_second (garrow_functor b))).
 440       unfold garrow_functor.
 441       unfold step2_functor.
 442       Transparent fmor.
 443       unfold functor_fobj.
 444       unfold functor_comp.
 445       simpl.
 446
 447       apply (me_faithful(MonicEnrichment:=CMon)).
 448       eapply transitivity; [ eapply full_roundtrip | idtac ].
 449
 450       eapply transitivity.
 451       apply comp_respects; [ idtac | reflexivity ].
 452       apply comp_respects; [ idtac | reflexivity ].
 453       apply comp_respects; [ reflexivity | idtac ].
 454       apply comp_respects; [ idtac | reflexivity ].
 455       apply comp_respects; [ idtac | reflexivity ].
 456       eapply symmetry.
 457       apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
 458
 459       apply symmetry.
 460       apply iso_shift_left.
 461
 462       symmetry.
 463       eapply transitivity.
 464       eapply transitivity.
 465       apply associativity.
 466       apply comp_respects; [ reflexivity | idtac ].
 467       eapply transitivity.
 468       apply associativity.
 469
 470       set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
 471       setoid_rewrite associativity in q.
 472
 473       eapply transitivity.
 474       apply associativity.
 475       eapply transitivity.
 476       apply associativity.
 477       apply comp_respects; [ reflexivity | idtac ].
 478       eapply transitivity.
 479       eapply symmetry.
 480       apply associativity.
 481       eapply transitivity.
 482       apply comp_respects; [ idtac | reflexivity ].
 483       symmetry.
 484       eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 485       eapply transitivity.
 486       apply associativity.
 487       apply comp_respects; [ reflexivity | idtac ].
 488       eapply transitivity.
 489       apply comp_respects; [ reflexivity | idtac ].
 490       apply comp_respects; [ idtac | reflexivity ].
 491       apply mf_consistent.
 492       eapply symmetry.
 493       apply q.
 494
 495       apply iso_shift_left'.
 496       eapply transitivity.
 497       apply associativity.
 498       symmetry.
 499       set (@iso_shift_right') as qq.
 500       simpl in qq.
 501       apply qq.
 502       clear qq.
 503       unfold me_homfunctor.
 504       eapply transitivity.
 505       symmetry.
 506       apply (cancelr_lemma CM (garrow_fobj b)).
 507
 508       unfold functor_fobj.
 509       unfold pmon_I.
 510
 511       set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
 512       apply symmetry.
 513       eapply transitivity.
 514       apply comp_respects; [ idtac | reflexivity ].
 515       apply comp_respects; [ reflexivity | idtac ].
 516       eapply symmetry.
 517       apply q.
 518       clear q.
 519
 520       eapply transitivity.
 521       apply associativity.
 522       apply comp_respects; try reflexivity.
 523       simpl.
 524
 525       eapply transitivity.
 526       apply associativity.
 527       eapply transitivity; [ idtac | apply right_identity ].
 528       apply comp_respects; try reflexivity.
 529       apply iso_comp2.
 530       Qed.
 531
 532   Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
 533   { mf_first      := garrow_first
 534   ; mf_second     := garrow_second
 535   ; mf_i          := iso_id _ }.
 536     intros; reflexivity.
 537     intros.
 538       unfold garrow_functor.
 539       unfold fmor.
 540       Opaque fmor. simpl.
 541       unfold step2_functor.
 542       admit.
 543       Transparent fmor.
 544
 545     apply cancell_coherent.
 546     apply cancelr_coherent.
 547     admit.
 548     Defined.
 549
 550   Definition garrow_from_reification : GeneralizedArrow K CM :=
 551     {| ga_functor_monoidal := garrow_monoidal |}.
 552
 553 End GArrowFromReification.
 554