1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguage *)
4 (* Basic assumptions about programming languages . *)
6 (*********************************************************************************************************************************)
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 MonoidalCategories_ch7_8.
21 Require Import Coherence_ch7_8.
22 Require Import Enrichment_ch2_8.
23 Require Import RepresentableStructure_ch7_2.
24 Require Import NaturalDeduction.
25 Require Import NaturalDeductionCategory.
26 Require Import Reification.
27 Require Import FreydCategories.
28 Require Import InitialTerminal_ch2_2.
29 Require Import FunctorCategories_ch7_7.
30 Require Import GeneralizedArrowFromReification.
31 Require Import GeneralizedArrow.
35 * Everything in the rest of this section is just groundwork meant to
36 * build up to the definition of the ProgrammingLanguage class, which
37 * appears at the end of the section. References to "the instance"
38 * mean instances of that class. Think of this section as being one
39 * big Class { ... } definition, except that we declare most of the
40 * stuff outside the curly brackets in order to take advantage of
41 * Coq's section mechanism.
43 Section Programming_Language.
45 (* Formalized Definition 4.1.1, production $\tau$ *)
46 Context {T : Type}. (* types of the language *)
48 Context (Judg : Type).
49 Context (sequent : Tree ??T -> Tree ??T -> Judg).
50 Notation "cs |= ss" := (sequent cs ss) : al_scope.
51 (* Because of term irrelevance we need only store the *erased* (def
52 * 4.4) trees; for this reason there is no Coq type directly
53 * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
54 * be used for productions $\Gamma$ and $\Sigma$ *)
56 (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
58 Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
60 Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
66 (* Formalized Definition 4.1
68 * Note that from this abstract interface, the terms (expressions)
69 * in the proof are not accessible at all; they don't need to be --
70 * so long as we have access to the equivalence relation upon
71 * proof-conclusions. Moreover, hiding the expressions actually
72 * makes the encoding in CiC work out easier for two reasons:
74 * 1. Because the denotation function is provided a proof rather
75 * than a term, it is a total function (the denotation function is
76 * often undefined for ill-typed terms).
78 * 2. We can define arr_composition of proofs without having to know how
79 * to compose expressions. The latter task is left up to the client
80 * function which extracts an expression from a completed proof.
82 * This also means that we don't need an explicit proof obligation for 4.1.2.
84 Class ProgrammingLanguage :=
86 (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
87 { al_eqv : @ND_Relation Judg Rule
88 where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
90 (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
91 * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
92 * to generate the rest *)
93 ; al_reflexive_seq : forall t, Rule [] [t|=t]
95 (* these can all be absorbed into a separate "sequent calculus" presentation *)
96 ; al_ant_assoc : forall {a b c d}, Rule [(a,,b),,c|=d] [(a,,(b,,c))|=d]
97 ; al_ant_cossa : forall {a b c d}, Rule [a,,(b,,c)|=d] [((a,,b),,c)|=d]
98 ; al_ant_cancell : forall {a b }, Rule [ [],,a |=b] [ a |=b]
99 ; al_ant_cancelr : forall {a b }, Rule [a,,[] |=b] [ a |=b]
100 ; al_ant_llecnac : forall {a b }, Rule [ a |=b] [ [],,a |=b]
101 ; al_ant_rlecnac : forall {a b }, Rule [ a |=b] [ a,,[] |=b]
102 ; al_suc_assoc : forall {a b c d}, Rule [d|=(a,,b),,c] [d|=(a,,(b,,c))]
103 ; al_suc_cossa : forall {a b c d}, Rule [d|=a,,(b,,c)] [d|=((a,,b),,c)]
104 ; al_suc_cancell : forall {a b }, Rule [a|=[],,b ] [a|= b ]
105 ; al_suc_cancelr : forall {a b }, Rule [a|=b,,[] ] [a|= b ]
106 ; al_suc_llecnac : forall {a b }, Rule [a|= b ] [a|=[],,b ]
107 ; al_suc_rlecnac : forall {a b }, Rule [a|= b ] [a|=b,,[] ]
109 ; al_horiz_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
110 ; al_horiz_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
112 (* these are essentially one way of formalizing
113 * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
114 ; al_horiz_expand_left_reflexive : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left a#]===[#al_reflexive_seq (a,,b)#]
115 ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
116 ; al_horiz_expand_right_then_cancel : forall a,
117 ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
119 ; al_vert_expand_ant_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [x,,a |= b ]/⋯⋯/[x,,c |= d ]
120 ; al_vert_expand_ant_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a,,x|= b ]/⋯⋯/[ c,,x|= d ]
121 ; al_vert_expand_suc_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |=x,,b ]/⋯⋯/[ c |=x,,d ]
122 ; al_vert_expand_suc_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |= b,,x]/⋯⋯/[ c |= d,,x]
123 ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
124 f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left x g
125 ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
126 f===g -> al_vert_expand_ant_right x f === al_vert_expand_ant_right x g
127 ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
128 f===g -> al_vert_expand_suc_left x f === al_vert_expand_suc_left x g
129 ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
130 f===g -> al_vert_expand_suc_right x f === al_vert_expand_suc_right x g
131 ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left x (nd_id [a|=b]) === nd_id [x,,a|=b]
132 ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right x (nd_id [a|=b]) === nd_id [a,,x|=b]
133 ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left x (nd_id [a|=b]) === nd_id [a|=x,,b]
134 ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right x (nd_id [a|=b]) === nd_id [a|=b,,x]
135 ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
136 (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
137 ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
138 (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
139 ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
140 (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
141 ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
142 (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
144 ; al_subst : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
145 ; al_subst_associativity : forall {a b c d},
146 ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
150 ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
152 ; al_subst_associativity' : forall {a b c d},
154 ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
157 ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
160 ; al_subst_left_identity : forall a b, (( [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell
161 ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#] );; al_subst b _ _) === nd_cancelr
162 ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
163 [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
164 === al_subst a b c;; [#al_horiz_expand_left d#]
165 ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
166 [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
167 === al_subst a b c;; [#al_horiz_expand_right d#]
168 ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
170 ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
171 (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
172 (nd_id [t1 |= t0]) **
173 ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
174 (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));;
177 ((([#al_reflexive_seq (t1,, [])#];;
178 (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
179 al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));;
180 (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
183 Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
184 Open Scope temporary_scope3.
186 Lemma al_subst_respects {PL:ProgrammingLanguage} :
189 (f : [] /⋯⋯/ [a |= b])
190 (f' : [] /⋯⋯/ [a |= b])
191 (g : [] /⋯⋯/ [b |= c])
192 (g' : [] /⋯⋯/ [b |= c]),
195 (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
202 (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
203 Class ProgrammingLanguageWithUnrestrictedSubstructuralRules :=
204 { alwusr_al :> ProgrammingLanguage
205 ; al_contr : forall a b, Rule [a,,a |= b ] [ a |= b]
206 ; al_exch : forall a b c, Rule [a,,b |= c ] [(b,,a)|= c]
207 ; al_weak : forall a b, Rule [[] |= b ] [ a |= b]
209 Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage.
211 (* languages with a fixpoint operator *)
212 Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) :=
214 ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b]
216 Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage.
218 Section LanguageCategory.
220 Context (PL:ProgrammingLanguage).
222 (* category of judgments in a fixed type/coercion context *)
223 Definition JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv.
225 Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
228 apply al_reflexive_seq.
231 Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
236 Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
238 {| eid := identityProof
241 apply MonoidalCat_all_central.
242 apply MonoidalCat_all_central.
243 unfold identityProof; unfold cutProof; simpl.
244 apply al_subst_left_identity.
245 unfold identityProof; unfold cutProof; simpl.
246 apply al_subst_right_identity.
247 unfold identityProof; unfold cutProof; simpl.
248 apply al_subst_associativity'.
251 Definition TypesLEnrichedInJudgments0 : Enrichment.
252 refine {| enr_c := TypesLFC |}.
255 Definition TypesL_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
257 eapply Build_EFunctor; intros.
258 eapply MonoidalCat_all_central.
265 Definition TypesL_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
269 Definition TypesL_binoidal : BinoidalCat TypesLFC (@T_Branch _).
271 {| bin_first := TypesL_first
272 ; bin_second := TypesL_second
276 Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal.
279 Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing.
282 Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor [].
286 Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment.
287 refine {| se_enr := TypesLEnrichedInJudgments0 |}.
292 Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment.
293 refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}.
298 Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment.
299 refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl.
305 End LanguageCategory.
308 Definition ArrowInProgrammingLanguage (L:ProgrammingLanguage)(tc:Terminal (TypesL L)) :=
309 FreydCategory (TypesL L) (TypesL L).
312 Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) :=
313 Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)).
315 Inductive NLevelLanguage : nat -> ProgrammingLanguage -> Type :=
316 | NLevelLanguage_zero : forall lang, NLevelLanguage O lang
317 | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
319 Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type :=
320 forall n:nat, NLevelLanguage n PL.
322 Section TwoLevelLanguage.
323 Context `(L12:TwoLevelLanguage L1 L2).
325 Definition FlatObject (x:TypesL L2) :=
326 forall y1 y2, not ((reification_r_obj L12 y1 y2)=x).
328 Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject.
330 Context `(retraction :@Functor _ _ (TypesL L2) _ _ FlatSubCategory retract_obj).
331 Context `(retraction_inv :@Functor _ _ FlatSubCategory _ _ (TypesL L2) retract_inv_obj).
332 Context (retraction_works:retraction >>>> retraction_inv ~~~~ functor_id _).
334 Definition FlatteningOfReification :=
335 (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction.
337 Lemma FlatteningIsNotDestructive :
338 FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12.
342 End TwoLevelLanguage.
344 Close Scope temporary_scope3.
345 Close Scope al_scope.
346 Close Scope nd_scope.
347 Close Scope pf_scope.
349 End Programming_Language.
351 Implicit Arguments ND [ Judgment ].
355 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e)
356 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
357 as parametric_morphism_al_vert_expand_suc_right.
358 intros; apply al_vert_expand_suc_r_respects; auto.
360 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e)
361 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
362 as parametric_morphism_al_vert_expand_suc_left.
363 intros; apply al_vert_expand_suc_l_respects; auto.
365 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e)
366 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
367 as parametric_morphism_al_vert_expand_ant_right.
368 intros; apply al_vert_expand_ant_r_respects; auto.
370 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e)
371 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
372 as parametric_morphism_al_vert_expand_ant_left.
373 intros; apply al_vert_expand_ant_l_respects; auto.
375 Close Scope nd_scope.
377 Notation "cs |= ss" := (@sequent _ cs ss) : al_scope.
379 Definition mapJudg {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Judg T) : @Judg R :=
380 match seq with sequentpair a b => pair (f a) (f b) end.
381 Implicit Arguments Judg [ ].
385 (* proofs which are generic and apply to any acceptable langauge (most of section 4) *)
386 Section Programming_Language_Facts.
388 (* the ambient language about which we are proving facts *)
389 Context `(Lang : @ProgrammingLanguage T Rule).
391 (* just for this section *)
395 Notation "H /⋯⋯/ C" := (@ND Judg Rule H C) : temporary_scope4.
396 Notation "a === b" := (@ndr_eqv _ _ al_eqv _ _ a b) : temporary_scope4.
397 Open Scope temporary_scope4.
399 Definition lang_al_eqv := al_eqv(ProgrammingLanguage:=Lang).
400 Existing Instance lang_al_eqv.
406 context ct [(?A ** ?B) ;; (?C ** ?D)] =>
407 setoid_rewrite <- (ndr_prod_preserves_comp A B C D)
411 Ltac sequentialize_product A B :=
415 | context ct [(A ** B)] =>
416 setoid_replace (A ** B)
417 with ((A ** (nd_id _)) ;; ((nd_id _) ** B))
418 (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
420 Ltac sequentialize_product' A B :=
424 | context ct [(A ** B)] =>
425 setoid_replace (A ** B)
426 with (((nd_id _) ** B) ;; (A ** (nd_id _)))
427 (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
433 context ct [(?A ;; ?B) ** (?C ;; ?D)] =>
434 setoid_rewrite (ndr_prod_preserves_comp A B C D)
437 Ltac distribute_left_product_with_id :=
441 context ct [(nd_id ?A) ** (?C ;; ?D)] =>
442 setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D));
443 [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ]
446 Ltac distribute_right_product_with_id :=
450 context ct [(?C ;; ?D) ** (nd_id ?A)] =>
451 setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A));
452 [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ]
456 (* another phrasing of al_subst_associativity; obligations tend to show up in this form *)
457 Lemma al_subst_associativity'' :
458 forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]])
459 (d : T) (h : [] /⋯⋯/ [[c] |= [d]]),
460 nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) ===
461 nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]).
463 sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h.
464 repeat setoid_rewrite <- ndr_comp_associativity.
465 distribute_right_product_with_id.
466 repeat setoid_rewrite ndr_comp_associativity.
467 set (@al_subst_associativity) as q. setoid_rewrite q. clear q.
468 apply ndr_comp_respects; try reflexivity.
469 repeat setoid_rewrite <- ndr_comp_associativity.
470 apply ndr_comp_respects; try reflexivity.
471 sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]).
472 distribute_left_product_with_id.
473 repeat setoid_rewrite <- ndr_comp_associativity.
474 apply ndr_comp_respects; try reflexivity.
475 setoid_rewrite <- ndr_prod_preserves_comp.
476 repeat setoid_rewrite ndr_comp_left_identity.
477 repeat setoid_rewrite ndr_comp_right_identity.
485 Close Scope temporary_scope4.
486 Close Scope al_scope.
487 Close Scope nd_scope.
488 Close Scope pf_scope.
489 Close Scope isomorphism_scope.
490 End Programming_Language_Facts.
492 (*Coercion AL_SurjectiveEnrichment : ProgrammingLanguage >-> SurjectiveEnrichment.*)
493 (*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*)