src/ProgrammingLanguage.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguage                                                                                                           *)
   3 (*                                                                                                                               *)
   4 (*   Basic assumptions about programming languages.                                                                              *)
   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 Enrichments.
  30 Require Import NaturalDeduction.
  31 Require Import NaturalDeductionCategory.
  32
  33 Section Programming_Language.
  34
  35   Context {T    : Type}.               (* types of the language *)
  36
  37   Definition PLJudg := (Tree ??T) * (Tree ??T).
  38   Definition sequent := @pair (Tree ??T) (Tree ??T).
  39      Notation "cs |= ss" := (sequent cs ss) : pl_scope.
  40
  41   Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}.
  42
  43   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
  44
  45   Open Scope pf_scope.
  46   Open Scope nd_scope.
  47   Open Scope pl_scope.
  48
  49   Class ProgrammingLanguage :=
  50   { pl_eqv0               :  @ND_Relation PLJudg Rule
  51   ; pl_snd                :> @SequentND PLJudg Rule _ sequent
  52   ; pl_cnd                :> @ContextND PLJudg Rule T sequent pl_snd
  53   ; pl_eqv1               :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0
  54   ; pl_eqv                :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
  55   }.
  56   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
  57
  58   Section LanguageCategory.
  59
  60     Context (PL:ProgrammingLanguage).
  61
  62     (* category of judgments in a fixed type/coercion context *)
  63     Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
  64
  65     Definition JudgmentsL          := Judgments_cartesian.
  66
  67     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
  68       unfold hom; simpl.
  69       apply snd_initial.
  70       Defined.
  71
  72     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
  73       unfold hom; simpl.
  74       apply snd_cut.
  75       Defined.
  76
  77     Existing Instance pl_eqv.
  78
  79     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
  80       refine
  81       {| eid   := identityProof
  82        ; ecomp := cutProof
  83       |}; intros.
  84       apply (mon_commutative(MonoidalCat:=JudgmentsL)).
  85       apply (mon_commutative(MonoidalCat:=JudgmentsL)).
  86       unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
  87       unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
  88       unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
  89       apply ndpc_comp; auto.
  90       apply ndpc_comp; auto.
  91       Defined.
  92
  93     Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) :=
  94       { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }.
  95       intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
  96       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
  97       apply (cndr_inert pl_cnd); auto.
  98       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
  99       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0))
 100                   _ (nd_id1 (a,,c |= b,,c))  _ (cnd_expand_right _ _ c)).
 101       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
 102       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 103       simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
 104       Defined.
 105
 106     Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) :=
 107       { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }.
 108       intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
 109       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 110       eapply cndr_inert; auto. apply pl_eqv.
 111       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 112       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0))
 113                   _ (nd_id1 (c,,a |= c,,b))  _ (cnd_expand_left _ _ c)).
 114       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
 115       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 116       simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
 117       Defined.
 118
 119     Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _).
 120       refine
 121         {| ebc_first  := Types_first
 122          ; ebc_second := Types_second
 123          |}.
 124       Defined.
 125
 126     Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
 127       { iso_forward  := snd_initial _ ;; cnd_ant_cossa _ a b c
 128       ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
 129       }.
 130       simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
 131         apply ndpc_comp; auto.
 132         apply ndpc_comp; auto.
 133         auto.
 134       simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
 135         apply ndpc_comp; auto.
 136         apply ndpc_comp; auto.
 137         auto.
 138         Defined.
 139
 140     Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
 141       { iso_forward  := snd_initial _ ;; cnd_ant_rlecnac _ a
 142       ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
 143       }.
 144       unfold eqv; unfold comp; simpl.
 145       eapply cndr_inert. apply pl_eqv. auto.
 146         apply ndpc_comp; auto.
 147         apply ndpc_comp; auto.
 148         auto.
 149       unfold eqv; unfold comp; simpl.
 150       eapply cndr_inert. apply pl_eqv. auto.
 151         apply ndpc_comp; auto.
 152         apply ndpc_comp; auto.
 153         auto.
 154       Defined.
 155
 156     Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
 157       { iso_forward  := snd_initial _ ;; cnd_ant_llecnac _ a
 158       ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
 159       }.
 160       unfold eqv; unfold comp; simpl.
 161       eapply cndr_inert. apply pl_eqv. auto.
 162         apply ndpc_comp; auto.
 163         apply ndpc_comp; auto.
 164         auto.
 165       unfold eqv; unfold comp; simpl.
 166       eapply cndr_inert. apply pl_eqv. auto.
 167         apply ndpc_comp; auto.
 168         apply ndpc_comp; auto.
 169         auto.
 170       Defined.
 171
 172     (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
 173     Ltac nd_swap_ltac P EQV :=
 174       match goal with
 175         [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] =>
 176           set (@nd_swap _ _ EQV _ _ _ _ F G) as P
 177       end.
 178
 179     Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a :=
 180       { ni_iso := fun c => Types_assoc_iso a c b }.
 181       intros.
 182       Opaque nd_id.
 183       simpl.
 184       Transparent nd_id.
 185
 186       rename A into X.
 187       rename B into Y.
 188       unfold ehom.
 189       nd_swap_ltac p pl_eqv.
 190       setoid_rewrite p.
 191       clear p.
 192
 193       setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 194       setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 195       setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 196       setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 197
 198       repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 199       setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 200
 201       set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
 202       Opaque nd_id.
 203       simpl in q.
 204       setoid_rewrite <- q.
 205
 206       clear q.
 207       set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.
 208       simpl in q.
 209       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 210       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 211       simpl in qq.
 212       setoid_rewrite qq in q.
 213       clear q' qq.
 214       setoid_rewrite <- q.
 215
 216       setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 217       apply ndr_comp_respects; try reflexivity.
 218
 219       Transparent nd_id.
 220       apply (cndr_inert pl_cnd); auto.
 221         apply ndpc_comp; auto.
 222         apply ndpc_comp; auto.
 223         apply ndpc_comp; auto.
 224         apply ndpc_comp; auto.
 225         apply ndpc_comp; auto.
 226         apply ndpc_comp; auto.
 227         Defined.
 228
 229     Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a :=
 230       { ni_iso := fun c => Types_assoc_iso a b c }.
 231       intros.
 232       Opaque nd_id.
 233       simpl.
 234       Transparent nd_id.
 235
 236       rename A into X.
 237       rename B into Y.
 238       unfold ehom.
 239       nd_swap_ltac p pl_eqv.
 240       setoid_rewrite p.
 241       clear p.
 242
 243       setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 244       setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 245       setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 246
 247       repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 248       setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 249
 250       set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
 251       Opaque nd_id.
 252       simpl in q.
 253       setoid_rewrite <- q.
 254
 255       clear q.
 256       set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.
 257       simpl in q.
 258       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 259       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 260       simpl in qq.
 261       setoid_rewrite qq in q.
 262       clear q' qq.
 263       setoid_rewrite <- q.
 264
 265       setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 266       apply ndr_comp_respects; try reflexivity.
 267
 268       Transparent nd_id.
 269       apply (cndr_inert pl_cnd); auto.
 270         apply ndpc_comp; auto.
 271         apply ndpc_comp; auto.
 272         apply ndpc_comp; auto.
 273         apply ndpc_comp; auto.
 274         apply ndpc_comp; auto.
 275         Defined.
 276
 277     Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b :=
 278       { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }.
 279       intros.
 280       Opaque nd_id.
 281       simpl.
 282       Transparent nd_id.
 283
 284       rename A into X.
 285       rename B into Y.
 286       unfold ehom.
 287       nd_swap_ltac p pl_eqv.
 288       setoid_rewrite p.
 289       clear p.
 290
 291       setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 292       setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 293       setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 294
 295       repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 296       setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 297
 298       set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
 299       Opaque nd_id.
 300       simpl in q.
 301       setoid_rewrite <- q.
 302
 303       clear q.
 304       set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.
 305       simpl in q.
 306       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 307       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 308       simpl in qq.
 309       setoid_rewrite qq in q.
 310       clear q' qq.
 311       setoid_rewrite <- q.
 312
 313       setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 314       apply ndr_comp_respects; try reflexivity.
 315
 316       Transparent nd_id.
 317       apply (cndr_inert pl_cnd); auto.
 318         apply ndpc_comp; auto.
 319         apply ndpc_comp; auto.
 320         apply ndpc_comp; auto.
 321         apply ndpc_comp; auto.
 322         apply ndpc_comp; auto.
 323         Defined.
 324
 325     Instance Types_cancelr   : Types_first [] <~~~> functor_id _ :=
 326       { ni_iso := Types_cancelr_iso }.
 327       intros.
 328       Opaque nd_id.
 329       simpl.
 330       unfold ehom.
 331       nd_swap_ltac p pl_eqv.
 332       setoid_rewrite p.
 333       setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 334       repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 335       setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 336
 337       set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
 338       Opaque nd_id.
 339       simpl in q.
 340       setoid_rewrite <- q.
 341       clear q.
 342
 343       set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.
 344       simpl in q.
 345       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 346       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 347       simpl in qq.
 348       setoid_rewrite qq in q.
 349       clear q' qq.
 350       setoid_rewrite <- q.
 351
 352       setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 353       apply ndr_comp_respects; try reflexivity.
 354       Transparent nd_id.
 355       simpl.
 356       apply (cndr_inert pl_cnd); auto.
 357         apply ndpc_comp; auto.
 358         apply ndpc_comp; auto.
 359         apply ndpc_comp; auto.
 360       Defined.
 361
 362     Instance Types_cancell   : Types_second [] <~~~> functor_id _ :=
 363       { ni_iso := Types_cancell_iso }.
 364       intros.
 365       Opaque nd_id.
 366       simpl.
 367       unfold ehom.
 368       nd_swap_ltac p pl_eqv.
 369       setoid_rewrite p.
 370       setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 371       repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 372       setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 373
 374       set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
 375       Opaque nd_id.
 376       simpl in q.
 377       setoid_rewrite <- q.
 378       clear q.
 379
 380       set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.
 381       simpl in q.
 382       set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 383       set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 384       simpl in qq.
 385       setoid_rewrite qq in q.
 386       clear q' qq.
 387       setoid_rewrite <- q.
 388       setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 389
 390       apply ndr_comp_respects; try reflexivity.
 391       Transparent nd_id.
 392       simpl.
 393       apply (cndr_inert pl_cnd); auto.
 394         apply ndpc_comp; auto.
 395         apply ndpc_comp; auto.
 396         apply ndpc_comp; auto.
 397       Defined.
 398
 399       Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c).
 400       intros.
 401         apply Build_CentralMorphism.
 402         Opaque nd_id.
 403         intros.
 404         unfold bin_obj.
 405         unfold ebc_bobj.
 406         simpl.
 407         unfold ehom.
 408         nd_swap_ltac p pl_eqv.
 409         setoid_rewrite p.
 410         clear p.
 411         setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 412         setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 413         repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 414         setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 415
 416         set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
 417         Opaque nd_id.
 418         simpl in q.
 419         setoid_rewrite <- q.
 420         clear q.
 421
 422         set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
 423         simpl in q.
 424         set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 425         set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 426         simpl in qq.
 427         setoid_rewrite qq in q.
 428         clear q' qq.
 429         setoid_rewrite <- q.
 430
 431         setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 432         apply ndr_comp_respects.
 433         reflexivity.
 434
 435         Transparent nd_id.
 436         apply (cndr_inert pl_cnd); auto.
 437           apply ndpc_comp; auto.
 438           apply ndpc_comp; auto.
 439           apply ndpc_comp; auto.
 440           apply ndpc_comp; auto.
 441           apply ndpc_comp; auto.
 442           apply ndpc_comp; auto.
 443
 444         Opaque nd_id.
 445         intros.
 446         unfold bin_obj.
 447         unfold ebc_bobj.
 448         simpl.
 449         unfold ehom.
 450         symmetry.
 451         nd_swap_ltac p pl_eqv.
 452         setoid_rewrite p.
 453         clear p.
 454         setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 455         setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 456         repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 457         setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 458
 459         set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
 460         Opaque nd_id.
 461         simpl in q.
 462         setoid_rewrite <- q.
 463         clear q.
 464
 465         set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
 466         simpl in q.
 467         set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 468         set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 469         simpl in qq.
 470         setoid_rewrite qq in q.
 471         clear q' qq.
 472         setoid_rewrite <- q.
 473
 474         setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 475         apply ndr_comp_respects.
 476         reflexivity.
 477
 478         Transparent nd_id.
 479         apply (cndr_inert pl_cnd); auto.
 480           apply ndpc_comp; auto.
 481           apply ndpc_comp; auto.
 482           apply ndpc_comp; auto.
 483           apply ndpc_comp; auto.
 484           apply ndpc_comp; auto.
 485           apply ndpc_comp; auto.
 486           Qed.
 487
 488       Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a).
 489       intros.
 490         apply Build_CentralMorphism.
 491         Opaque nd_id.
 492         intros.
 493         unfold bin_obj.
 494         unfold ebc_bobj.
 495         simpl.
 496         unfold ehom.
 497         nd_swap_ltac p pl_eqv.
 498         setoid_rewrite p.
 499         clear p.
 500         setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 501         setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 502         repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 503         setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 504
 505         set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
 506         Opaque nd_id.
 507         simpl in q.
 508         setoid_rewrite <- q.
 509         clear q.
 510
 511         set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
 512         simpl in q.
 513         set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 514         set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 515         simpl in qq.
 516         setoid_rewrite qq in q.
 517         clear q' qq.
 518         setoid_rewrite <- q.
 519
 520         setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 521         apply ndr_comp_respects.
 522         reflexivity.
 523
 524         Transparent nd_id.
 525         apply (cndr_inert pl_cnd); auto.
 526           apply ndpc_comp; auto.
 527           apply ndpc_comp; auto.
 528           apply ndpc_comp; auto.
 529           apply ndpc_comp; auto.
 530           apply ndpc_comp; auto.
 531           apply ndpc_comp; auto.
 532
 533         Opaque nd_id.
 534         intros.
 535         unfold bin_obj.
 536         unfold ebc_bobj.
 537         simpl.
 538         unfold ehom.
 539         symmetry.
 540         nd_swap_ltac p pl_eqv.
 541         setoid_rewrite p.
 542         clear p.
 543         setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 544         setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 545         repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 546         setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 547
 548         set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
 549         Opaque nd_id.
 550         simpl in q.
 551         setoid_rewrite <- q.
 552         clear q.
 553
 554         set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
 555         simpl in q.
 556         set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 557         set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 558         simpl in qq.
 559         setoid_rewrite qq in q.
 560         clear q' qq.
 561         setoid_rewrite <- q.
 562
 563         setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 564         apply ndr_comp_respects.
 565         reflexivity.
 566
 567         Transparent nd_id.
 568         apply (cndr_inert pl_cnd); auto.
 569           apply ndpc_comp; auto.
 570           apply ndpc_comp; auto.
 571           apply ndpc_comp; auto.
 572           apply ndpc_comp; auto.
 573           apply ndpc_comp; auto.
 574           apply ndpc_comp; auto.
 575           Qed.
 576
 577       Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a).
 578       intros.
 579         apply Build_CentralMorphism.
 580         Opaque nd_id.
 581         intros.
 582         unfold bin_obj.
 583         unfold ebc_bobj.
 584         simpl.
 585         unfold ehom.
 586         nd_swap_ltac p pl_eqv.
 587         setoid_rewrite p.
 588         clear p.
 589         setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 590         setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 591         repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 592         setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 593
 594         set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
 595         Opaque nd_id.
 596         simpl in q.
 597         setoid_rewrite <- q.
 598         clear q.
 599
 600         set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
 601         simpl in q.
 602         set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 603         set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 604         simpl in qq.
 605         setoid_rewrite qq in q.
 606         clear q' qq.
 607         setoid_rewrite <- q.
 608
 609         setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 610         apply ndr_comp_respects.
 611         reflexivity.
 612
 613         Transparent nd_id.
 614         apply (cndr_inert pl_cnd); auto.
 615           apply ndpc_comp; auto.
 616           apply ndpc_comp; auto.
 617           apply ndpc_comp; auto.
 618           apply ndpc_comp; auto.
 619           apply ndpc_comp; auto.
 620           apply ndpc_comp; auto.
 621
 622         Opaque nd_id.
 623         intros.
 624         unfold bin_obj.
 625         unfold ebc_bobj.
 626         simpl.
 627         unfold ehom.
 628         symmetry.
 629         nd_swap_ltac p pl_eqv.
 630         setoid_rewrite p.
 631         clear p.
 632         setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
 633         setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
 634         repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 635         setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
 636
 637         set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
 638         Opaque nd_id.
 639         simpl in q.
 640         setoid_rewrite <- q.
 641         clear q.
 642
 643         set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
 644         simpl in q.
 645         set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
 646         set (isos_forward_equal_then_backward_equal _ _ q') as qq.
 647         simpl in qq.
 648         setoid_rewrite qq in q.
 649         clear q' qq.
 650         setoid_rewrite <- q.
 651
 652         setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
 653         apply ndr_comp_respects.
 654         reflexivity.
 655
 656         Transparent nd_id.
 657         apply (cndr_inert pl_cnd); auto.
 658           apply ndpc_comp; auto.
 659           apply ndpc_comp; auto.
 660           apply ndpc_comp; auto.
 661           apply ndpc_comp; auto.
 662           apply ndpc_comp; auto.
 663           apply ndpc_comp; auto.
 664           Qed.
 665
 666     Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
 667       { pmon_assoc    := Types_assoc
 668       ; pmon_cancell  := Types_cancell
 669       ; pmon_cancelr  := Types_cancelr
 670       ; pmon_assoc_rr := Types_assoc_rr
 671       ; pmon_assoc_ll := Types_assoc_ll
 672       }.
 673       apply Build_Pentagon.
 674         intros; simpl.
 675         eapply cndr_inert. apply pl_eqv.
 676         apply ndpc_comp.
 677         apply ndpc_comp.
 678         auto.
 679         apply ndpc_comp.
 680         apply ndpc_prod.
 681         apply ndpc_comp.
 682         apply ndpc_comp.
 683         auto.
 684         apply ndpc_comp.
 685         auto.
 686         auto.
 687         auto.
 688         auto.
 689         auto.
 690         auto.
 691         apply ndpc_comp.
 692         apply ndpc_comp.
 693         auto.
 694         apply ndpc_comp.
 695         auto.
 696         auto.
 697         auto.
 698
 699       apply Build_Triangle; intros; simpl.
 700         eapply cndr_inert. apply pl_eqv.
 701         auto.
 702         apply ndpc_comp.
 703         apply ndpc_comp.
 704         auto.
 705         apply ndpc_comp.
 706         auto.
 707         auto.
 708         auto.
 709         eapply cndr_inert. apply pl_eqv. auto.
 710           auto.
 711       intros; simpl; reflexivity.
 712       intros; simpl; reflexivity.
 713       apply TypesL_assoc_central.
 714       apply TypesL_cancelr_central.
 715       apply TypesL_cancell_central.
 716       Defined.
 717
 718     Definition TypesEnrichedInJudgments : SurjectiveEnrichment.
 719       refine
 720         {| senr_c_pm     := TypesL_PreMonoidal
 721          ; senr_v        := JudgmentsL
 722          ; senr_v_bin    := Judgments_Category_binoidal _
 723          ; senr_v_pmon   := Judgments_Category_premonoidal _
 724          ; senr_v_mon    := Judgments_Category_monoidal _
 725          ; senr_c_bin    := Types_binoidal
 726          ; senr_c        := TypesL
 727         |}.
 728       Defined.
 729
 730   End LanguageCategory.
 731
 732 End Programming_Language.
 733 Implicit Arguments ND [ Judgment ].