- Section LanguageCategory.
-
- Context (PL:ProgrammingLanguage).
-
- (* category of judgments in a fixed type/coercion context *)
- Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
-
- Definition JudgmentsL := Judgments_cartesian.
-
- Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
- unfold hom; simpl.
- apply nd_seq_reflexive.
- Defined.
-
- Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
- unfold hom; simpl.
- apply pl_subst.
- Defined.
-
- Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
- refine
- {| eid := identityProof
- ; ecomp := cutProof
- |}; intros.
- apply MonoidalCat_all_central.
- apply MonoidalCat_all_central.
- unfold identityProof; unfold cutProof; simpl.
- apply nd_cut_left_identity.
- unfold identityProof; unfold cutProof; simpl.
- apply nd_cut_right_identity.
- unfold identityProof; unfold cutProof; simpl.
- symmetry.
- apply nd_cut_associativity.
- Defined.
-
- Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
- refine {| efunc := fun x y => (nd_rule (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)) |}.
- intros; apply MonoidalCat_all_central.
- intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
- apply se_reflexive_right.
- intros. unfold ehom. unfold comp. simpl. unfold cutProof.
- rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_right _ c#] _ _ (nd_id1 (b|=c0))
- _ (nd_id1 (a,,c |= b,,c)) _ [#se_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]).
- apply se_cut_right.
- Defined.
-
- Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
- eapply Build_EFunctor.
- instantiate (1:=(fun x y => (nd_rule (@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
- intros; apply MonoidalCat_all_central.
- intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
- apply se_reflexive_left.
- intros. unfold ehom. unfold comp. simpl. unfold cutProof.
- rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_left _ c#] _ _ (nd_id1 (b|=c0))
- _ (nd_id1 (c,,a |= c,,b)) _ [#se_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]).
- apply se_cut_left.
- Defined.
-
- Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
- refine
- {| bin_first := Types_first
- ; bin_second := Types_second
- |}.
- Defined.
-
- Definition Types_PreMonoidal : PreMonoidalCat Types_binoidal [].
- admit.
- Defined.
-
- Definition TypesEnrichedInJudgments : Enrichment.
- refine {| enr_c := TypesL |}.
- Defined.
-
- Structure HasProductTypes :=
- {
- }.
-
- (* need to prove that if we have cartesian tuples we have cartesian contexts *)
- Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
- admit.
- Defined.
-
- End LanguageCategory.