X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguage.v;h=dc2256c6d7ebb403520f595036e9914f456cc63c;hp=073dfef0d36e64c0769d6311bd60958a6511faa8;hb=bef99d21b3f5697d6fb1871493290c8dcf9dea93;hpb=85e4f0fd6b0673c1cc763eeb2585b7dc3d388455 diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 073dfef..dc2256c 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) -(* NaturalDeduction: *) +(* ProgrammingLanguage *) (* *) -(* Structurally explicit natural deduction proofs. *) +(* Basic assumptions about programming languages. *) (* *) (*********************************************************************************************************************************) @@ -9,6 +9,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Categories_ch1_3. +Require Import InitialTerminal_ch2_2. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. Require Import ProductCategories_ch1_6_1. @@ -17,750 +18,716 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. -Require Import NaturalDeduction. +Require Import FunctorCategories_ch7_7. +Require Import Enrichments. +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. -(* - * Everything in the rest of this section is just groundwork meant to - * build up to the definition of the AcceptableLanguage class, which - * appears at the end of the section. References to "the instance" - * mean instances of that class. Think of this section as being one - * big Class { ... } definition, except that we declare most of the - * stuff outside the curly brackets in order to take advantage of - * Coq's section mechanism. - *) -Section Acceptable_Language. +Section Programming_Language. - (* Formalized Definition 4.1.1, production $\tau$ *) Context {T : Type}. (* types of the language *) - Inductive Sequent := sequent : Tree ??T -> Tree ??T -> Sequent. - Notation "cs |= ss" := (sequent cs ss) : al_scope. - (* Because of term irrelevance we need only store the *erased* (def - * 4.4) trees; for this reason there is no Coq type directly - * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can - * be used for productions $\Gamma$ and $\Sigma$ *) - - (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *) + Definition PLJudg := (Tree ??T) * (Tree ??T). + Definition sequent := @pair (Tree ??T) (Tree ??T). + Notation "cs |= ss" := (sequent cs ss) : pl_scope. - Context {Rule : Tree ??Sequent -> Tree ??Sequent -> Type}. + Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}. - Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope. + Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope. Open Scope pf_scope. Open Scope nd_scope. - Open Scope al_scope. - - (* Formalized Definition 4.1 - * - * Note that from this abstract interface, the terms (expressions) - * in the proof are not accessible at all; they don't need to be -- - * so long as we have access to the equivalence relation upon - * proof-conclusions. Moreover, hiding the expressions actually - * makes the encoding in CiC work out easier for two reasons: - * - * 1. Because the denotation function is provided a proof rather - * than a term, it is a total function (the denotation function is - * often undefined for ill-typed terms). - * - * 2. We can define arr_composition of proofs without having to know how - * to compose expressions. The latter task is left up to the client - * function which extracts an expression from a completed proof. - * - * This also means that we don't need an explicit proof obligation for 4.1.2. - *) - Class AcceptableLanguage := - - (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *) - { al_eqv : @ND_Relation Sequent Rule - where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) - - (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types; - * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) - * to generate the rest *) - ; al_reflexive_seq : forall t, Rule [] [t|=t] - - (* these can all be absorbed into a separate "sequent calculus" presentation *) - ; al_ant_assoc : forall {a b c d}, Rule [(a,,b),,c|=d] [(a,,(b,,c))|=d] - ; al_ant_cossa : forall {a b c d}, Rule [a,,(b,,c)|=d] [((a,,b),,c)|=d] - ; al_ant_cancell : forall {a b }, Rule [ [],,a |=b] [ a |=b] - ; al_ant_cancelr : forall {a b }, Rule [a,,[] |=b] [ a |=b] - ; al_ant_llecnac : forall {a b }, Rule [ a |=b] [ [],,a |=b] - ; al_ant_rlecnac : forall {a b }, Rule [ a |=b] [ a,,[] |=b] - ; al_suc_assoc : forall {a b c d}, Rule [d|=(a,,b),,c] [d|=(a,,(b,,c))] - ; al_suc_cossa : forall {a b c d}, Rule [d|=a,,(b,,c)] [d|=((a,,b),,c)] - ; al_suc_cancell : forall {a b }, Rule [a|=[],,b ] [a|= b ] - ; al_suc_cancelr : forall {a b }, Rule [a|=b,,[] ] [a|= b ] - ; al_suc_llecnac : forall {a b }, Rule [a|= b ] [a|=[],,b ] - ; al_suc_rlecnac : forall {a b }, Rule [a|= b ] [a|=b,,[] ] - - ; al_horiz_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] - ; al_horiz_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau] - - (* these are essentially one way of formalizing - * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *) - ; al_horiz_expand_left_reflexive : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left a#]===[#al_reflexive_seq (a,,b)#] - ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#] - ; al_horiz_expand_right_then_cancel : forall a, - ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#]) - - ; al_vert_expand_ant_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [x,,a |= b ]/⋯⋯/[x,,c |= d ] - ; al_vert_expand_ant_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a,,x|= b ]/⋯⋯/[ c,,x|= d ] - ; al_vert_expand_suc_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |=x,,b ]/⋯⋯/[ c |=x,,d ] - ; al_vert_expand_suc_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |= b,,x]/⋯⋯/[ c |= d,,x] - ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left x g - ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_ant_right x f === al_vert_expand_ant_right x g - ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_suc_left x f === al_vert_expand_suc_left x g - ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_suc_right x f === al_vert_expand_suc_right x g - ; 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] - ; 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] - ; 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] - ; 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] - ; 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]), - (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g) - ; 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]), - (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g) - ; 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]), - (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g) - ; 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]), - (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g) - - ; al_subst : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] - ; al_subst_associativity : forall {a b c d}, - ((al_subst a b c) ** (nd_id1 (c|=d))) ;; - (al_subst a c d) - === - nd_assoc ;; - ((nd_id1 (a|=b)) ** (al_subst b c d) ;; - (al_subst a b d)) - ; al_subst_associativity' : forall {a b c d}, - nd_cossa ;; - ((al_subst a b c) ** (nd_id1 (c|=d))) ;; - (al_subst a c d) - === - ((nd_id1 (a|=b)) ** (al_subst b c d) ;; - (al_subst a b d)) - - ; al_subst_left_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_llecnac;;(( [#al_reflexive_seq t1#]**pf);; al_subst _ _ _) === pf - ; al_subst_right_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_rlecnac;;((pf**[#al_reflexive_seq t2#] );; al_subst _ _ _) === pf - ; al_subst_commutes_with_horiz_expand_left : forall a b c d, - [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c) - === al_subst a b c;; [#al_horiz_expand_left d#] - ; al_subst_commutes_with_horiz_expand_right : forall a b c d, - [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d) - === al_subst a b c;; [#al_horiz_expand_right d#] - ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]), - (((nd_rlecnac;; - ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);; - (nd_id [t1 |= t0]) ** - ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));; - al_subst t1 t0 t2) - === - ((([#al_reflexive_seq (t1,, [])#];; - (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);; - al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) + Open Scope pl_scope. + + Class ProgrammingLanguage := + { pl_eqv0 : @ND_Relation PLJudg Rule + ; pl_snd :> @SequentND PLJudg Rule _ sequent + ; pl_cnd :> @ContextND PLJudg Rule T sequent pl_snd + ; pl_eqv1 :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0 + ; pl_eqv :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1 }. + Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3. - Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3. - Open Scope temporary_scope3. - - Lemma al_subst_respects : - forall {AL:AcceptableLanguage}{a b c}, - forall - (f : [] /⋯⋯/ [a |= b]) - (f' : [] /⋯⋯/ [a |= b]) - (g : [] /⋯⋯/ [b |= c]) - (g' : [] /⋯⋯/ [b |= c]), - (f === f') -> - (g === g') -> - (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _). - intros. - setoid_rewrite H. - setoid_rewrite H0. - reflexivity. - Defined. - - (* a contextually closed language *) - (* - Class ContextuallyClosedAcceptableLanguage := - { ccal_al : AcceptableLanguage - ; ccal_contextual_closure_operator : Tree ??T -> Tree ??T -> Tree ??T - where "a -~- b" := (ccal_contextual_closure_operator a b) - ; ccal_contextual_closure : forall {a b c d}(f:[a|=b]/⋯⋯/[c|=d]), [[]|=a-~-b]/⋯⋯/[[]|=c-~-d] - ; ccal_contextual_closure_respects : forall {a b c d}(f f':[a|=b]/⋯⋯/[c|=d]), - f===f' -> (ccal_contextual_closure f)===(ccal_contextual_closure f') - ; ccal_contextual_closure_preserves_comp : forall {a b c d e f}(f':[a|=b]/⋯⋯/[c|=d])(g':[c|=d]/⋯⋯/[e|=f]), - (ccal_contextual_closure f');;(ccal_contextual_closure g') === (ccal_contextual_closure (f';;g')) - ; ccal_contextual_closure_preserves_id : forall {a b}, ccal_contextual_closure (nd_id [a|=b]) === nd_id [[]|=a-~-b] - }. - Coercion ccal_al : ContextuallyClosedAcceptableLanguage >-> AcceptableLanguage. - *) - - (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *) - Class AcceptableLanguageWithUnrestrictedSubstructuralRules := - { alwusr_al :> AcceptableLanguage - ; al_contr : forall a b, Rule [a,,a |= b ] [ a |= b] - ; al_exch : forall a b c, Rule [a,,b |= c ] [(b,,a)|= c] - ; al_weak : forall a b, Rule [[] |= b ] [ a |= b] - }. - Coercion alwusr_al : AcceptableLanguageWithUnrestrictedSubstructuralRules >-> AcceptableLanguage. + Section LanguageCategory. - (* languages with a fixpoint operator *) - Class AcceptableLanguageWithFixpointOperator `(al:AcceptableLanguage) := - { alwfpo_al := al - ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b] - }. - Coercion alwfpo_al : AcceptableLanguageWithFixpointOperator >-> AcceptableLanguage. + Context (PL:ProgrammingLanguage). - Close Scope temporary_scope3. - Close Scope al_scope. - Close Scope nd_scope. - Close Scope pf_scope. + (* category of judgments in a fixed type/coercion context *) + Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv. -End Acceptable_Language. + Definition JudgmentsL := Judgments_cartesian. -Implicit Arguments ND [ Judgment ]. + Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. + unfold hom; simpl. + apply snd_initial. + Defined. -Open Scope nd_scope. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_suc_right. - intros; apply al_vert_expand_suc_r_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_suc_left. - intros; apply al_vert_expand_suc_l_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_ant_right. - intros; apply al_vert_expand_ant_r_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_ant_left. - intros; apply al_vert_expand_ant_l_respects; auto. - Defined. -Close Scope nd_scope. - -Notation "cs |= ss" := (@sequent _ cs ss) : al_scope. -(* -Definition mapSequent {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Sequent T) : @Sequent R := - match seq with sequentpair a b => pair (f a) (f b) end. -Implicit Arguments Sequent [ ]. -*) - - -(* proofs which are generic and apply to any acceptable langauge (most of section 4) *) -Section Acceptable_Language_Facts. - - (* the ambient language about which we are proving facts *) - Context `(Lang : @AcceptableLanguage T Rule). - - (* just for this section *) - Open Scope nd_scope. - Open Scope al_scope. - Open Scope pf_scope. - Notation "H /⋯⋯/ C" := (@ND Sequent Rule H C) : temporary_scope4. - Notation "a === b" := (@ndr_eqv _ _ al_eqv _ _ a b) : temporary_scope4. - Open Scope temporary_scope4. - - Definition lang_al_eqv := al_eqv(AcceptableLanguage:=Lang). - Existing Instance lang_al_eqv. - - Ltac distribute := - match goal with - [ |- ?G ] => - match G with - context ct [(?A ** ?B) ;; (?C ** ?D)] => - setoid_rewrite <- (ndr_prod_preserves_comp A B C D) - end - end. + Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c]. + unfold hom; simpl. + apply snd_cut. + Defined. - Ltac sequentialize_product A B := - match goal with - [ |- ?G ] => - match G with - | context ct [(A ** B)] => - setoid_replace (A ** B) - with ((A ** (nd_id _)) ;; ((nd_id _) ** B)) - (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*) - end end. - Ltac sequentialize_product' A B := - match goal with - [ |- ?G ] => - match G with - | context ct [(A ** B)] => - setoid_replace (A ** B) - with (((nd_id _) ** B) ;; (A ** (nd_id _))) - (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*) - end end. - Ltac distribute' := - match goal with - [ |- ?G ] => - match G with - context ct [(?A ;; ?B) ** (?C ;; ?D)] => - setoid_rewrite (ndr_prod_preserves_comp A B C D) - end - end. - Ltac distribute_left_product_with_id := - match goal with - [ |- ?G ] => - match G with - context ct [(nd_id ?A) ** (?C ;; ?D)] => - setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D)); - [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ] - end - end. - Ltac distribute_right_product_with_id := - match goal with - [ |- ?G ] => - match G with - context ct [(?C ;; ?D) ** (nd_id ?A)] => - setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A)); - [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ] - end + Existing Instance pl_eqv. + + Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). + refine + {| eid := identityProof + ; ecomp := cutProof + |}; intros. + apply (mon_commutative(MonoidalCat:=JudgmentsL)). + apply (mon_commutative(MonoidalCat:=JudgmentsL)). + unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Defined. + + Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) := + { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). + intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. + apply (cndr_inert pl_cnd); auto. + intros. unfold ehom. unfold comp. simpl. unfold cutProof. + rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0)) + _ (nd_id1 (a,,c |= b,,c)) _ (cnd_expand_right _ _ c)). + setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]). + setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]). + simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + Defined. + + Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) := + { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). + intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. + eapply cndr_inert; auto. apply pl_eqv. + intros. unfold ehom. unfold comp. simpl. unfold cutProof. + rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0)) + _ (nd_id1 (c,,a |= c,,b)) _ (cnd_expand_left _ _ c)). + setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]). + setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]). + simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + Defined. + + Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _). + refine + {| ebc_first := Types_first + ; ebc_second := Types_second + |}. + Defined. + + Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) := + { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c + ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c + }. + simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + Defined. + + Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a := + { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a + ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a + }. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + Defined. + + Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a := + { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a + ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a + }. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + Defined. + + (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *) + Ltac nd_swap_ltac P EQV := + match goal with + [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => + set (@nd_swap _ _ EQV _ _ _ _ F G) as P end. - (* another phrasing of al_subst_associativity; obligations tend to show up in this form *) - Lemma al_subst_associativity'' : - forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]]) - (d : T) (h : [] /⋯⋯/ [[c] |= [d]]), - nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) === - nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]). - intros. - sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h. - repeat setoid_rewrite <- ndr_comp_associativity. - distribute_right_product_with_id. - repeat setoid_rewrite ndr_comp_associativity. - set (@al_subst_associativity) as q. setoid_rewrite q. clear q. + Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a := + { ni_iso := fun c => Types_assoc_iso a c b }. + intros. + Opaque nd_id. + simpl. + Transparent nd_id. + + rename A into X. + rename B into Y. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + + clear q. + set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). apply ndr_comp_respects; try reflexivity. - repeat setoid_rewrite <- ndr_comp_associativity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Defined. + + Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a := + { ni_iso := fun c => Types_assoc_iso a b c }. + intros. + Opaque nd_id. + simpl. + Transparent nd_id. + + rename A into X. + rename B into Y. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + + clear q. + set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). apply ndr_comp_respects; try reflexivity. - sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]). - distribute_left_product_with_id. - repeat setoid_rewrite <- ndr_comp_associativity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Defined. + + Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b := + { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }. + intros. + Opaque nd_id. + simpl. + Transparent nd_id. + + rename A into X. + rename B into Y. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + + clear q. + set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). apply ndr_comp_respects; try reflexivity. - setoid_rewrite <- ndr_prod_preserves_comp. - repeat setoid_rewrite ndr_comp_left_identity. - repeat setoid_rewrite ndr_comp_right_identity. - admit. - admit. - admit. - admit. - admit. - Qed. - - (* Formalized Definition 4.6 *) - Section Types1. - Instance Types1 : Category T (fun t1 t2 => [ ] /⋯⋯/ [ [t1] |= [t2] ]) := - { eqv := fun ta tb pf1 pf2 => pf1 === pf2 - ; id := fun t => [#al_reflexive_seq [t]#] - ; comp := fun {ta tb tc:T}(pf1:[]/⋯⋯/[[ta]|=[tb]])(pf2:[]/⋯⋯/[[tb]|=[tc]]) => nd_llecnac ;; ((pf1 ** pf2) ;; (al_subst _ _ _)) - }. - intros; apply Build_Equivalence; - [ unfold Reflexive; intros; reflexivity - | unfold Symmetric; intros; symmetry; auto - | unfold Transitive; intros; transitivity y; auto ]. - unfold Proper; unfold respectful; intros; simpl. - apply ndr_comp_respects. reflexivity. - apply al_subst_respects; auto. - intros; simpl. apply al_subst_left_identity. - intros; simpl. - assert (@nd_llecnac _ Rule [] === @nd_rlecnac _ _ []). - apply ndr_structural_indistinguishable; auto. - setoid_rewrite H. - apply al_subst_right_identity. - intros; apply al_subst_associativity''. - Defined. - End Types1. - - (* Formalized Definition 4.10 *) - Instance Judgments : Category (Tree ??Sequent) (fun h c => h /⋯⋯/ c) := - { id := fun h => nd_id _ - ; comp := fun a b c f g => f ;; g - ; eqv := fun a b f g => f===g - }. - intros; apply Build_Equivalence; - [ unfold Reflexive; intros; reflexivity - | unfold Symmetric; intros; symmetry; auto - | unfold Transitive; intros; transitivity y; auto ]. - unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto. - intros; apply ndr_comp_left_identity. - intros; apply ndr_comp_right_identity. - intros; apply ndr_comp_associativity. - Defined. - - (* a "primitive" proof has exactly one hypothesis and one conclusion *) - Inductive IsPrimitive : forall (h_:Tree ??(@Sequent T)), Type := - isPrimitive : forall h, IsPrimitive [h]. - Hint Constructors IsPrimitive. - Instance IsPrimitiveSubCategory : SubCategory Judgments IsPrimitive (fun _ _ _ _ _ => True). - apply Build_SubCategory; intros; auto. - Defined. - - (* The primitive judgments form a subcategory; nearly all of the - * functors we build that go into Judgments will factor through the - * inclusion functor for this subcategory. Explicitly constructing - * it makes the formalization easier, but distracts from what's - * actually going on (from an expository perspective) *) - Definition PrimitiveJudgments := SubCategoriesAreCategories Judgments IsPrimitiveSubCategory. - Definition PrimitiveInclusion := InclusionFunctor Judgments IsPrimitiveSubCategory. - - Section Types0. - Inductive IsNil : Tree ??(@Sequent T) -> Prop := isnil : IsNil []. - Inductive IsClosed : Tree ??(@Sequent T) -> Prop := isclosed:forall t, IsClosed [[]|=[t]]. - Inductive IsIdentity : forall h c, (h /⋯⋯/ c) -> Prop := - | isidentity0 : forall t, IsIdentity t t (nd_id t) - | isidentity1 : forall t pf1 pf2, IsIdentity t t pf1 -> IsIdentity t t pf2 -> IsIdentity t t (pf1 ;; pf2). - Inductive IsInTypes0 (h c:Tree ??Sequent)(pf:h /⋯⋯/ c) : Prop := - | iit0_id0 : IsNil h -> IsNil c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf - | iit0_id1 : @IsClosed h -> @IsClosed c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf - | iit0_term : IsNil h -> @IsClosed c -> IsInTypes0 _ _ pf. - Instance Types0P : SubCategory Judgments - (fun x:Judgments => IsInTypes0 _ _ (id(Category:=Judgments) x)) - (fun h c _ _ f => IsInTypes0 h c f). - intros. - apply Build_SubCategory; intros; simpl. - auto. - inversion H0. - inversion H1; subst. - inversion H2; subst. - inversion H; subst. inversion H4; subst. - apply iit0_id0; auto. apply isidentity1; auto. - inversion H5. - inversion H5. - inversion H1; subst. - inversion H2; subst. - inversion H3; subst. clear H8. clear H7. - inversion H; subst. inversion H5. - inversion H4; subst. - inversion H6; subst. - apply iit0_id1; auto. apply isidentity1; auto. - clear H10. clear H8. - apply iit0_id1; auto. apply isidentity1; auto. - inversion H4; subst. inversion H; subst. - inversion H8. - inversion H6. - apply iit0_term; auto. - clear H7; subst. - inversion H; subst. - inversion H4; subst. - apply iit0_term; auto. - inversion H4; subst. - inversion H7; subst. clear H14. - apply iit0_id1; auto. apply isidentity1; auto. - clear H13. - apply iit0_id1; auto. apply isidentity1; auto. - inversion H4; subst. - inversion H; subst. - inversion H10. - inversion H7. - apply iit0_term; auto. - inversion H1; subst. - inversion H; subst. - inversion H3; subst. apply iit0_term; auto. - inversion H4. - inversion H4. - Qed. - - (* Formalized Definition 4.8 *) - Definition Types0 := SubCategoriesAreCategories Judgments Types0P. - End Types0. - - (* Formalized Definition 4.11 *) - Instance Judgments_binoidal : BinoidalCat Judgments (fun a b:Tree ??Sequent => a,,b) := - { bin_first := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => a,,x) (fun a b (f:a/⋯⋯/b) => f**(nd_id x)) _ _ _ - ; bin_second := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => x,,a) (fun a b (f:a/⋯⋯/b) => (nd_id x)**f) _ _ _ - }. - intros. simpl. simpl in H. setoid_rewrite H. reflexivity. - intros. simpl. reflexivity. - intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity. - intros. simpl. simpl in H. setoid_rewrite H. reflexivity. - intros. simpl. reflexivity. - intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity. - Defined. - - Definition jud_assoc_iso (a b c:Judgments) : @Isomorphic _ _ Judgments ((a,,b),,c) (a,,(b,,c)). - apply (@Build_Isomorphic _ _ Judgments _ _ nd_assoc nd_cossa); simpl; auto. - Defined. - Definition jud_cancelr_iso (a:Judgments) : @Isomorphic _ _ Judgments (a,,[]) a. - apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancelr nd_rlecnac); simpl; auto. - Defined. - Definition jud_cancell_iso (a:Judgments) : @Isomorphic _ _ Judgments ([],,a) a. - apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancell nd_llecnac); simpl; auto. - Defined. - - (* just for this section *) - Notation "a ⊗ b" := (@bin_obj _ _ Judgments _ Judgments_binoidal a b). - Notation "c ⋊ -" := (@bin_second _ _ Judgments _ Judgments_binoidal c). - Notation "- ⋉ c" := (@bin_first _ _ Judgments _ Judgments_binoidal c). - Notation "c ⋊ f" := ((c ⋊ -) \ f). - Notation "g ⋉ c" := ((- ⋉ c) \ g). - - Hint Extern 1 => apply (@nd_structural_id0 _ Rule). - Hint Extern 1 => apply (@nd_structural_id1 _ Rule). - Hint Extern 1 => apply (@nd_structural_weak _ Rule). - Hint Extern 1 => apply (@nd_structural_copy _ Rule). - Hint Extern 1 => apply (@nd_structural_prod _ Rule). - Hint Extern 1 => apply (@nd_structural_comp _ Rule). - Hint Extern 1 => apply (@nd_structural_cancell _ Rule). - Hint Extern 1 => apply (@nd_structural_cancelr _ Rule). - Hint Extern 1 => apply (@nd_structural_llecnac _ Rule). - Hint Extern 1 => apply (@nd_structural_rlecnac _ Rule). - Hint Extern 1 => apply (@nd_structural_assoc _ Rule). - Hint Extern 1 => apply (@nd_structural_cossa _ Rule). - Hint Extern 2 => apply (@ndr_structural_indistinguishable _ Rule). - - Program Instance Judgments_premonoidal : PreMonoidalCat Judgments_binoidal [ ] := - { pmon_assoc := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso a x b)) _ - ; pmon_cancell := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancell_iso x)) _ - ; pmon_cancelr := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancelr_iso x)) _ - ; pmon_assoc_rr := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso x a b)⁻¹) _ - ; pmon_assoc_ll := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => jud_assoc_iso a b x) _ - }. - Next Obligation. - setoid_rewrite (ndr_prod_associativity (nd_id a) f (nd_id b)). - repeat setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. - Defined. - Next Obligation. - setoid_rewrite (ndr_prod_right_identity f). - repeat setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. - Defined. - Next Obligation. - setoid_rewrite (ndr_prod_left_identity f). - repeat setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. - Defined. - Next Obligation. - apply Build_Pentagon; intros. - simpl; apply ndr_structural_indistinguishable; auto. - Defined. - Next Obligation. - apply Build_Triangle; intros; - simpl; apply ndr_structural_indistinguishable; auto. - Defined. - Next Obligation. - setoid_rewrite (ndr_prod_associativity f (nd_id a) (nd_id b)). - repeat setoid_rewrite <- ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - eapply transitivity; [ idtac | apply ndr_comp_left_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. - Defined. - Next Obligation. - setoid_rewrite (ndr_prod_associativity (nd_id a) (nd_id b) f). - repeat setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. - Defined. - Check (@Judgments_premonoidal). (* to force Coq to verify that we've finished all the obligations *) - - Definition Judgments_monoidal_endofunctor_fobj : Judgments ×× Judgments -> Judgments := - (fun xy => - match xy with - | pair_obj x y => T_Branch x y - end). - Definition Judgments_monoidal_endofunctor_fmor : - forall a b, (a~~{Judgments ×× Judgments}~~>b) -> - ((Judgments_monoidal_endofunctor_fobj a)~~{Judgments}~~>(Judgments_monoidal_endofunctor_fobj b)). - intros. - destruct a. - destruct b. - destruct X. - exact (h**h0). - Defined. - Definition Judgments_monoidal_endofunctor : Functor (Judgments ×× Judgments) Judgments Judgments_monoidal_endofunctor_fobj. - refine {| fmor := Judgments_monoidal_endofunctor_fmor |}; intros; simpl. - abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; apply ndr_prod_respects; auto). - abstract (destruct a; simpl; reflexivity). - abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; apply ndr_prod_preserves_comp). - Defined. - - Instance Judgments_monoidal : MonoidalCat _ _ Judgments_monoidal_endofunctor [ ]. - admit. - Defined. - - (* all morphisms in the category of Judgments are central; there's probably a very short route from here to CartesianCat *) - Lemma all_central : forall a b:Judgments, forall (f:a~>b), CentralMorphism f. - intros; apply Build_CentralMorphism; intros. - simpl. - setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g). - setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) g f (nd_id _)). - setoid_rewrite ndr_comp_left_identity. - setoid_rewrite ndr_comp_right_identity. - reflexivity. - simpl. - setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f). - setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)). - setoid_rewrite ndr_comp_left_identity. - setoid_rewrite ndr_comp_right_identity. - reflexivity. - Defined. - - (* - Instance NoHigherOrderFunctionTypes : SubCategory Judgments - Instance NoFunctionTypes : SubCategory Judgments - Lemma first_order_functions_eliminable : IsomorphicCategories NoHigherOrderFunctionTypes NoFunctionTypes - *) - - (* Formalized Theorem 4.19 *) - Instance Types_omega_e : ECategory Judgments_monoidal (Tree ??T) (fun tt1 tt2 => [ tt1 |= tt2 ]) := - { eid := fun tt => [#al_reflexive_seq tt#] - ; ecomp := fun a b c => al_subst a b c - }. - admit. - admit. - admit. - admit. - admit. - Defined. - - Definition Types_omega_monoidal_functor - : Functor (Types_omega_e ×× Types_omega_e) Types_omega_e (fun a => match a with pair_obj a1 a2 => a1,,a2 end). - admit. - Defined. - - Instance Types_omega_monoidal : MonoidalCat Types_omega_e _ Types_omega_monoidal_functor []. - admit. - Defined. - - Definition AL_Enrichment : Enrichment. - refine {| enr_c := Types_omega_e |}. - Defined. - - Definition AL_SurjectiveEnrichment : SurjectiveEnrichment. - refine {| se_enr := AL_Enrichment |}. - unfold treeDecomposition. - intros; induction d; simpl. - destruct a. - destruct s. - exists [pair t t0]; auto. - exists []; auto. - destruct IHd1. - destruct IHd2. - exists (x,,x0); subst; auto. - Defined. - - Definition AL_MonoidalEnrichment : MonoidalEnrichment. - refine {| me_enr := AL_SurjectiveEnrichment ; me_mon := Types_omega_monoidal |}. - admit. - Defined. - - Definition AL_MonicMonoidalEnrichment : MonicMonoidalEnrichment. - refine {| ffme_enr := AL_MonoidalEnrichment |}. - admit. - admit. - admit. - Defined. - - (* - Instance Types_omega_be : BinoidalECategory Types_omega_e := - { bec_obj := fun tt1 tt2 => tt1,,tt2 - ; bec_efirst := fun a b c => nd_rule (@al_horiz_expand_right _ _ Lang _ _ _) - ; bec_esecond := fun a b c => nd_rule (@al_horiz_expand_left _ _ Lang _ _ _) - }. - intros; apply all_central. - intros; apply all_central. - intros. unfold eid. simpl. - setoid_rewrite <- al_horiz_expand_right_reflexive. - reflexivity. - intros. unfold eid. simpl. - setoid_rewrite <- al_horiz_expand_left_reflexive. - reflexivity. - intros. simpl. - set (@al_subst_commutes_with_horiz_expand_right _ _ _ a b c d) as q. - setoid_rewrite <- q. clear q. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Defined. + + Instance Types_cancelr : Types_first [] <~~~> functor_id _ := + { ni_iso := Types_cancelr_iso }. + intros. + Opaque nd_id. + simpl. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). apply ndr_comp_respects; try reflexivity. - distribute. - apply ndr_prod_respects. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; reflexivity. - eapply transitivity; [ idtac | apply ndr_comp_left_identity ]. - apply ndr_comp_respects; reflexivity. - intros. simpl. - set (@al_subst_commutes_with_horiz_expand_left _ _ _ a b c d) as q. - setoid_rewrite <- q. clear q. + Transparent nd_id. + simpl. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Defined. + + Instance Types_cancell : Types_second [] <~~~> functor_id _ := + { ni_iso := Types_cancell_iso }. + intros. + Opaque nd_id. + simpl. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects; try reflexivity. - distribute. - apply ndr_prod_respects. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; reflexivity. - eapply transitivity; [ idtac | apply ndr_comp_left_identity ]. - apply ndr_comp_respects; reflexivity. + Transparent nd_id. + simpl. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Defined. + + Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c). + intros. + apply Build_CentralMorphism. + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + symmetry. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Qed. + + Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a). + intros. + apply Build_CentralMorphism. + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + symmetry. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Qed. + + Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a). + intros. + apply Build_CentralMorphism. + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + symmetry. + nd_swap_ltac p pl_eqv. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). + + set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + Qed. + + Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] := + { pmon_assoc := Types_assoc + ; pmon_cancell := Types_cancell + ; pmon_cancelr := Types_cancelr + ; pmon_assoc_rr := Types_assoc_rr + ; pmon_assoc_ll := Types_assoc_ll + }. + apply Build_Pentagon. + intros; simpl. + eapply cndr_inert. apply pl_eqv. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + apply ndpc_prod. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + auto. + auto. + auto. + auto. + auto. + auto. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + auto. + auto. + auto. + + apply Build_Triangle; intros; simpl. + eapply cndr_inert. apply pl_eqv. + auto. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + auto. + auto. + auto. + eapply cndr_inert. apply pl_eqv. auto. + auto. + intros; simpl; reflexivity. + intros; simpl; reflexivity. + apply TypesL_assoc_central. + apply TypesL_cancelr_central. + apply TypesL_cancell_central. + Defined. + + Definition TypesEnrichedInJudgments : SurjectiveEnrichment. + refine + {| senr_c_pm := TypesL_PreMonoidal + ; senr_v := JudgmentsL + ; senr_v_bin := Judgments_Category_binoidal _ + ; senr_v_pmon := Judgments_Category_premonoidal _ + ; senr_v_mon := Judgments_Category_monoidal _ + ; senr_c_bin := Types_binoidal + ; senr_c := TypesL + |}. Defined. - *) - - Definition Types_omega : Category _ (fun tt1 tt2 => [ ]/⋯⋯/[ tt1 |= tt2 ]) := Underlying Types_omega_e. - Existing Instance Types_omega. - - (* - Definition Types_omega_binoidal : BinoidalCat Types_omega (fun tt1 tt2 => tt1,,tt2) := Underlying_binoidal Types_omega_be. - Existing Instance Types_omega_binoidal. - *) - - (* takes an "operation in the context" (proof from [b|=Top]/⋯⋯/[a|=Top]) and turns it into a function a-->b; note the variance *) - Definition context_operation_as_function - : forall {a}{b} (f:[b|=[]]~~{Judgments}~~>[a|=[]]), []~~{Judgments}~~>[a|=b]. - intros. - apply (@al_vert_expand_suc_right _ _ _ b _ _) in f. - simpl in f. - apply (@al_vert_expand_ant_left _ _ _ [] _ _) in f. - simpl in f. - set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'. - exact f'. - Defined. - - (* takes an "operation in the context" (proof from [Top|=a]/⋯⋯/[Top|=b]) and turns it into a function a-->b; note the variance *) - Definition cocontext_operation_as_function - : forall {a}{b} (f:[[]|=a]~~{Judgments}~~>[[]|=b]), []~~{Judgments}~~>[a|=b]. - intros. unfold hom. unfold hom in f. - apply al_vert_expand_ant_right with (x:=a) in f. - simpl in f. - apply al_vert_expand_suc_left with (x:=[]) in f. - simpl in f. - set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'. - exact f'. - Defined. - - - Definition function_as_context_operation - : forall {a}{b}{c} (f:[]~~{Judgments}~~>[a|=b]), [b|=c]~~{Judgments}~~>[a|=c] - := fun a b c f => RepresentableFunctorºᑭ Types_omega_e c \ f. - Definition function_as_cocontext_operation - : forall {a}{b}{c} (f:[]/⋯⋯/[a|=b]), [c|=a]~~{Judgments}~~>[c|=b] - := fun a b c f => RepresentableFunctor Types_omega_e c \ f. - - Close Scope temporary_scope4. - Close Scope al_scope. - Close Scope nd_scope. - Close Scope pf_scope. - Close Scope isomorphism_scope. -End Acceptable_Language_Facts. - -Coercion AL_SurjectiveEnrichment : AcceptableLanguage >-> SurjectiveEnrichment. -Coercion AL_MonicMonoidalEnrichment : AcceptableLanguage >-> MonicMonoidalEnrichment. + + End LanguageCategory. + +End Programming_Language. +Implicit Arguments ND [ Judgment ].