src/ProgrammingLanguageCategory.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguageCategory                                                                                                   *)
   3 (*                                                                                                                               *)
   4 (*   The category Types(L)                                                                                                       *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import InitialTerminal_ch2_2.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import BinoidalCategories.
  22 Require Import PreMonoidalCategories.
  23 Require Import MonoidalCategories_ch7_8.
  24 Require Import Coherence_ch7_8.
  25 Require Import Enrichment_ch2_8.
  26 Require Import RepresentableStructure_ch7_2.
  27 Require Import FunctorCategories_ch7_7.
  28
  29 Require Import NaturalDeduction.
  30 Require Import ProgrammingLanguage.
  31         Export ProgrammingLanguage.
  32
  33 Require Import NaturalDeductionCategory.
  34
  35 Open Scope nd_scope.
  36 (* I am at a loss to explain why "auto" can't handle this *)
  37 Ltac ndpc_tac :=
  38   match goal with
  39     | [ |- NDPredicateClosure ?P (?A ;; ?B) ] => apply ndpc_comp; ndpc_tac
  40     | [ |- NDPredicateClosure ?P (?A ** ?B) ] => apply ndpc_prod; ndpc_tac
  41     | _                                       => auto
  42   end.
  43
  44 (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
  45 Ltac nd_swap_ltac P EQV :=
  46   match goal with
  47     [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] =>
  48       set (@nd_swap _ _ EQV _ _ _ _ F G) as P
  49   end.
  50
  51 (* I still wish I knew why "Hint Constructors" doesn't work *)
  52 Hint Extern 5 => apply snd_inert_initial.
  53 Hint Extern 5 => apply snd_inert_cut.
  54 Hint Extern 5 => apply snd_inert_structural.
  55 Hint Extern 5 => apply cnd_inert_initial.
  56 Hint Extern 5 => apply cnd_inert_cut.
  57 Hint Extern 5 => apply cnd_inert_structural.
  58 Hint Extern 5 => apply cnd_inert_cnd_ant_assoc.
  59 Hint Extern 5 => apply cnd_inert_cnd_ant_cossa.
  60 Hint Extern 5 => apply cnd_inert_cnd_ant_cancell.
  61 Hint Extern 5 => apply cnd_inert_cnd_ant_cancelr.
  62 Hint Extern 5 => apply cnd_inert_cnd_ant_llecnac.
  63 Hint Extern 5 => apply cnd_inert_cnd_ant_rlecnac.
  64 Hint Extern 5 => apply cnd_inert_se_expand_left.
  65 Hint Extern 5 => apply cnd_inert_se_expand_right.
  66
  67 Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ []   )) => simpl; auto.
  68 Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ [ _ ])) => simpl; auto.
  69
  70 Section ProgrammingLanguageCategory.
  71
  72   Context {T    : Type}.               (* types of the language *)
  73
  74   Context {Rule : Tree ??(@PLJudg T) -> Tree ??(@PLJudg T) -> Type}.
  75      Notation "cs |= ss" := (@sequent T cs ss) : pl_scope.
  76
  77   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
  78
  79   Open Scope pf_scope.
  80   Open Scope nd_scope.
  81   Open Scope pl_scope.
  82
  83   Context (PL:@ProgrammingLanguage T Rule).
  84
  85   (* category of judgments in a fixed type/coercion context *)
  86   Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
  87
  88   Definition JudgmentsL          := Judgments_cartesian.
  89
  90   Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
  91     unfold hom; simpl.
  92     apply snd_initial.
  93     Defined.
  94
  95   Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
  96     unfold hom; simpl.
  97     apply snd_cut.
  98     Defined.
  99
 100   Instance TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]) :=
 101   { eid   := identityProof
 102   ; ecomp := cutProof
 103   }.
 104     intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
 105     intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
 106     abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL).
 107     abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL).
 108     abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert;
 109                 [ apply PL | idtac | idtac ]; apply ndpc_comp; auto).
 110     Defined.
 111
 112   Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) :=
 113     { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }.
 114     intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
 115     abstract (intros; simpl; apply (cndr_inert pl_cnd); auto).
 116     abstract (intros; unfold ehom; unfold comp; simpl; unfold cutProof;
 117               rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0))
 118                           _ (nd_id1 (a,,c |= b,,c))  _ (cnd_expand_right _ _ c));
 119               setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [a,, c |= b,, c]);
 120               setoid_rewrite (@ndr_comp_left_identity  _ _ PL [b |= c0]);
 121               simpl; eapply cndr_inert; [ apply PL | auto | auto ]).
 122     Defined.
 123
 124   Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) :=
 125     { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }.
 126     intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
 127     abstract (intros; simpl; apply (cndr_inert pl_cnd); auto).
 128     intros; unfold ehom; unfold comp; simpl; unfold cutProof;
 129     abstract (rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0))
 130                           _ (nd_id1 (c,,a |= c,,b))  _ (cnd_expand_left _ _ c));
 131               setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [c,,a |= c,,b]);
 132               setoid_rewrite (@ndr_comp_left_identity  _ _ PL [b |= c0]);
 133               simpl; eapply cndr_inert; [ apply PL | auto | auto ]).
 134     Defined.
 135
 136   Instance Types_binoidal : EBinoidalCat TypesL (@T_Branch _) :=
 137   { ebc_first  := Types_first
 138   ; ebc_second := Types_second
 139   }.
 140
 141   Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
 142   { iso_forward  := snd_initial _ ;; cnd_ant_cossa _ a b c
 143   ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
 144   }.
 145     abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
 146     abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
 147     Defined.
 148
 149   Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
 150   { iso_forward  := snd_initial _ ;; cnd_ant_rlecnac _ a
 151   ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
 152   }.
 153     abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
 154     abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
 155     Defined.
 156
 157   Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
 158     { iso_forward  := snd_initial _ ;; cnd_ant_llecnac _ a
 159     ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
 160     }.
 161     abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
 162     abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
 163     Defined.
 164
 165   Lemma coincide' : nd_llecnac === nd_rlecnac.
 166     set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 167     set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 168     apply qq.
 169     Qed.
 170
 171   Lemma Types_assoc_lemma : ∀a b X Y : TypesL,
 172       ∀f : X ~~{ TypesL }~~> Y,
 173       #(Types_assoc_iso a X b) >>> (Types_first b >>>> Types_second a) \ f ~~
 174       (Types_second a >>>> Types_first b) \ f >>> #(Types_assoc_iso a Y b).
 175     intros.
 176     Opaque nd_id.
 177       simpl.
 178       Transparent nd_id.
 179     unfold ehom.
 180
 181     nd_swap_ltac p PL.
 182       setoid_rewrite p.
 183       clear p.
 184
 185     repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 186
 187     setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 188     setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 189     setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 190     setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 191
 192     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 193     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 194     setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 195
 196     set (ni_commutes' (jud_mon_cancelr PL) f) as q.
 197       simpl in q.
 198       setoid_rewrite <- q.
 199       clear q.
 200
 201     set (ni_commutes' (jud_mon_cancell PL) f) as q.
 202       simpl in q.
 203       setoid_rewrite coincide' in q.
 204       setoid_rewrite <- q.
 205       clear q.
 206
 207     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 208       apply ndr_comp_respects; try reflexivity.
 209
 210     apply (cndr_inert pl_cnd); auto; ndpc_tac; auto.
 211     Qed.
 212
 213   Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a :=
 214     { ni_iso := fun c => Types_assoc_iso a c b }.
 215     apply Types_assoc_lemma.
 216     Defined.
 217
 218   Lemma Types_assoc_ll_lemma :
 219     ∀a b X Y : TypesL,
 220     ∀f : X ~~{ TypesL }~~> Y,
 221     #(Types_assoc_iso a b X) >>> (Types_second b >>>> Types_second a) \ f ~~
 222     Types_second (a,, b) \ f >>> #(Types_assoc_iso a b Y).
 223
 224     intros.
 225     Opaque nd_id.
 226     simpl.
 227     Transparent nd_id.
 228     unfold ehom.
 229     nd_swap_ltac p PL.
 230     setoid_rewrite p.
 231     clear p.
 232
 233     setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 234     setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 235     setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 236
 237     repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 238     setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 239
 240     set (ni_commutes' (jud_mon_cancelr PL) f) as q.
 241     Opaque nd_id.
 242     simpl in q.
 243     setoid_rewrite <- q.
 244
 245     clear q.
 246     set (ni_commutes' (jud_mon_cancell PL) f) as q.
 247     simpl in q.
 248     set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 249     set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 250     simpl in qq.
 251     setoid_rewrite qq in q.
 252     clear q' qq.
 253     setoid_rewrite <- q.
 254
 255     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 256     apply ndr_comp_respects; try reflexivity.
 257
 258     Transparent nd_id.
 259     apply (cndr_inert pl_cnd); auto; ndpc_tac.
 260     Qed.
 261
 262   Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a :=
 263     { ni_iso := fun c => Types_assoc_iso a b c }.
 264     apply Types_assoc_ll_lemma.
 265     Defined.
 266
 267   Lemma Types_assoc_rr_lemma :
 268     ∀a b A B : TypesL,
 269     ∀f : A ~~{ TypesL }~~> B,
 270     #(Types_assoc_iso A a b) ⁻¹ >>> (Types_first a >>>> Types_first b) \ f ~~
 271     Types_first (a,, b) \ f >>> #(Types_assoc_iso B a b) ⁻¹.
 272     intros.
 273     Opaque nd_id.
 274     simpl.
 275     Transparent nd_id.
 276
 277     rename A into X.
 278     rename B into Y.
 279     unfold ehom.
 280     nd_swap_ltac p PL.
 281     setoid_rewrite p.
 282     clear p.
 283
 284     setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 285     setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 286     setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 287
 288     repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 289     setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 290
 291     set (ni_commutes' (jud_mon_cancelr PL) f) as q.
 292     Opaque nd_id.
 293     simpl in q.
 294     setoid_rewrite <- q.
 295
 296     clear q.
 297     set (ni_commutes' (jud_mon_cancell PL) f) as q.
 298     simpl in q.
 299     set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 300     set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 301     simpl in qq.
 302     setoid_rewrite qq in q.
 303     clear q' qq.
 304     setoid_rewrite <- q.
 305
 306     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 307     apply ndr_comp_respects; try reflexivity.
 308
 309     Transparent nd_id.
 310     apply (cndr_inert pl_cnd); auto; ndpc_tac.
 311     Qed.
 312
 313   Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b :=
 314     { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }.
 315     apply Types_assoc_rr_lemma.
 316     Defined.
 317
 318   Lemma Types_cancelr_lemma :
 319     ∀A B : TypesL,
 320     ∀f : A ~~{ TypesL }~~> B,
 321     #(Types_cancelr_iso A) >>> functor_id TypesL \ f ~~
 322     Types_first [] \ f >>> #(Types_cancelr_iso B).
 323     intros.
 324     Opaque nd_id.
 325     simpl.
 326     unfold ehom.
 327     nd_swap_ltac p PL.
 328     setoid_rewrite p.
 329     setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 330     repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 331     setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 332
 333     set (ni_commutes' (jud_mon_cancelr PL) f) as q.
 334     Opaque nd_id.
 335     simpl in q.
 336     setoid_rewrite <- q.
 337     clear q.
 338
 339     set (ni_commutes' (jud_mon_cancell PL) f) as q.
 340     simpl in q.
 341     set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 342     set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 343     simpl in qq.
 344     setoid_rewrite qq in q.
 345     clear q' qq.
 346     setoid_rewrite <- q.
 347
 348     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 349     apply ndr_comp_respects; try reflexivity.
 350     Transparent nd_id.
 351     simpl.
 352     apply (cndr_inert pl_cnd); auto; ndpc_tac.
 353     Qed.
 354
 355   Instance Types_cancelr   : Types_first [] <~~~> functor_id _ :=
 356     { ni_iso := Types_cancelr_iso }.
 357     apply Types_cancelr_lemma.
 358     Defined.
 359
 360   Lemma Types_cancell_lemma :
 361     ∀A B : TypesL,
 362     ∀f : A ~~{ TypesL }~~> B,
 363     #(Types_cancell_iso A) >>> functor_id TypesL \ f ~~
 364     Types_second [] \ f >>> #(Types_cancell_iso B).
 365     intros.
 366     Opaque nd_id.
 367     simpl.
 368     unfold ehom.
 369     nd_swap_ltac p PL.
 370     setoid_rewrite p.
 371     setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 372     repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 373     setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 374
 375     set (ni_commutes' (jud_mon_cancelr PL) f) as q.
 376     Opaque nd_id.
 377     simpl in q.
 378     setoid_rewrite <- q.
 379     clear q.
 380
 381     set (ni_commutes' (jud_mon_cancell PL) f) as q.
 382     simpl in q.
 383     set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 384     set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 385     simpl in qq.
 386     setoid_rewrite qq in q.
 387     clear q' qq.
 388     setoid_rewrite <- q.
 389     setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 390
 391     apply ndr_comp_respects; try reflexivity.
 392     Transparent nd_id.
 393     simpl.
 394     apply (cndr_inert pl_cnd); auto; ndpc_tac.
 395     Qed.
 396
 397   Instance Types_cancell   : Types_second [] <~~~> functor_id _ :=
 398     { ni_iso := Types_cancell_iso }.
 399     apply Types_cancell_lemma.
 400     Defined.
 401
 402   Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c).
 403     intros.
 404       apply Build_CentralMorphism.
 405       intros.
 406       unfold bin_obj.
 407       unfold ebc_bobj.
 408       Opaque nd_id.
 409       simpl.
 410       unfold ehom.
 411       nd_swap_ltac p PL.
 412       setoid_rewrite p.
 413       clear p.
 414       setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 415       setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 416       repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 417       setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 418
 419       set (ni_commutes' (jud_mon_cancelr PL) g) as q.
 420       Opaque nd_id.
 421       simpl in q.
 422       setoid_rewrite <- q.
 423       clear q.
 424
 425       set (ni_commutes' (jud_mon_cancell PL) g) as q.
 426       simpl in q.
 427       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 428       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 429       simpl in qq.
 430       setoid_rewrite qq in q.
 431       clear q' qq.
 432       setoid_rewrite <- q.
 433
 434       setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 435       apply ndr_comp_respects.
 436       reflexivity.
 437
 438       Transparent nd_id.
 439       apply (cndr_inert pl_cnd); auto; ndpc_tac.
 440
 441       Opaque nd_id.
 442       intros.
 443       unfold bin_obj.
 444       unfold ebc_bobj.
 445       simpl.
 446       unfold ehom.
 447       symmetry.
 448       nd_swap_ltac p PL.
 449       setoid_rewrite p.
 450       clear p.
 451       setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 452       setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 453       repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 454       setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 455
 456       set (ni_commutes' (jud_mon_cancelr PL) g) as q.
 457       Opaque nd_id.
 458       simpl in q.
 459       setoid_rewrite <- q.
 460       clear q.
 461
 462       set (ni_commutes' (jud_mon_cancell PL) g) as q.
 463       simpl in q.
 464       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 465       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 466       simpl in qq.
 467       setoid_rewrite qq in q.
 468       clear q' qq.
 469       setoid_rewrite <- q.
 470
 471       setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 472       apply ndr_comp_respects.
 473       reflexivity.
 474
 475       Transparent nd_id.
 476       apply (cndr_inert pl_cnd); auto; ndpc_tac.
 477       Qed.
 478
 479   Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a).
 480     intros.
 481       apply Build_CentralMorphism.
 482       Opaque nd_id.
 483       intros.
 484       unfold bin_obj.
 485       unfold ebc_bobj.
 486       simpl.
 487       unfold ehom.
 488       nd_swap_ltac p PL.
 489       setoid_rewrite p.
 490       clear p.
 491       setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 492       setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 493       repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 494       setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 495
 496       set (ni_commutes' (jud_mon_cancelr PL) g) as q.
 497       Opaque nd_id.
 498       simpl in q.
 499       setoid_rewrite <- q.
 500       clear q.
 501
 502       set (ni_commutes' (jud_mon_cancell PL) g) as q.
 503       simpl in q.
 504       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 505       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 506       simpl in qq.
 507       setoid_rewrite qq in q.
 508       clear q' qq.
 509       setoid_rewrite <- q.
 510
 511       setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 512       apply ndr_comp_respects.
 513       reflexivity.
 514
 515       Transparent nd_id.
 516       apply (cndr_inert pl_cnd); auto; ndpc_tac.
 517
 518       Opaque nd_id.
 519       intros.
 520       unfold bin_obj.
 521       unfold ebc_bobj.
 522       simpl.
 523       unfold ehom.
 524       symmetry.
 525       nd_swap_ltac p PL.
 526       setoid_rewrite p.
 527       clear p.
 528       setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 529       setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 530       repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 531       setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 532
 533       set (ni_commutes' (jud_mon_cancelr PL) g) as q.
 534       Opaque nd_id.
 535       simpl in q.
 536       setoid_rewrite <- q.
 537       clear q.
 538
 539       set (ni_commutes' (jud_mon_cancell PL) g) as q.
 540       simpl in q.
 541       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 542       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 543       simpl in qq.
 544       setoid_rewrite qq in q.
 545       clear q' qq.
 546       setoid_rewrite <- q.
 547
 548       setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 549       apply ndr_comp_respects.
 550       reflexivity.
 551
 552       Transparent nd_id.
 553       apply (cndr_inert pl_cnd); auto; ndpc_tac.
 554       Qed.
 555
 556   Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a).
 557     intros.
 558       apply Build_CentralMorphism.
 559       Opaque nd_id.
 560       intros.
 561       unfold bin_obj.
 562       unfold ebc_bobj.
 563       simpl.
 564       unfold ehom.
 565       nd_swap_ltac p PL.
 566       setoid_rewrite p.
 567       clear p.
 568       setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 569       setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 570       repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 571       setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 572
 573       set (ni_commutes' (jud_mon_cancelr PL) g) as q.
 574       Opaque nd_id.
 575       simpl in q.
 576       setoid_rewrite <- q.
 577       clear q.
 578
 579       set (ni_commutes' (jud_mon_cancell PL) g) as q.
 580       simpl in q.
 581       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 582       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 583       simpl in qq.
 584       setoid_rewrite qq in q.
 585       clear q' qq.
 586       setoid_rewrite <- q.
 587
 588       setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 589       apply ndr_comp_respects.
 590       reflexivity.
 591
 592       Transparent nd_id.
 593       apply (cndr_inert pl_cnd); auto; ndpc_tac.
 594
 595       Opaque nd_id.
 596       intros.
 597       unfold bin_obj.
 598       unfold ebc_bobj.
 599       simpl.
 600       unfold ehom.
 601       symmetry.
 602       nd_swap_ltac p PL.
 603       setoid_rewrite p.
 604       clear p.
 605       setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
 606       setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
 607       repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 608       setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
 609
 610       set (ni_commutes' (jud_mon_cancelr PL) g) as q.
 611       Opaque nd_id.
 612       simpl in q.
 613       setoid_rewrite <- q.
 614       clear q.
 615
 616       set (ni_commutes' (jud_mon_cancell PL) g) as q.
 617       simpl in q.
 618       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
 619       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 620       simpl in qq.
 621       setoid_rewrite qq in q.
 622       clear q' qq.
 623       setoid_rewrite <- q.
 624
 625       setoid_rewrite (@ndr_comp_associativity _ Rule PL).
 626       apply ndr_comp_respects.
 627       reflexivity.
 628
 629       Transparent nd_id.
 630       apply (cndr_inert pl_cnd); auto; ndpc_tac.
 631       Qed.
 632
 633   Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
 634     { pmon_assoc    := Types_assoc
 635     ; pmon_cancell  := Types_cancell
 636     ; pmon_cancelr  := Types_cancelr
 637     ; pmon_assoc_rr := Types_assoc_rr
 638     ; pmon_assoc_ll := Types_assoc_ll
 639     }.
 640     abstract (apply Build_Pentagon; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac).
 641     abstract (apply Build_Triangle; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac).
 642     intros; simpl; reflexivity.
 643     intros; simpl; reflexivity.
 644     apply TypesL_assoc_central.
 645     apply TypesL_cancelr_central.
 646     apply TypesL_cancell_central.
 647     Defined.
 648
 649 End ProgrammingLanguageCategory.
 650