--- /dev/null
+(*********************************************************************************************************************************)
+(* Enrichments *)
+(* *)
+(* *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import Enrichment_ch2_8.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+
+(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
+(*
+Definition SurjectiveEnrichment `(ec:ECategory(Hom:=Vhom)(V:=V)(bin_obj':=Vbobj)(EI:=EI)) :=
+ @treeDecomposition _ _
+ (fun t => match t with
+ | None => EI
+ | Some x => match x with pair y z => Vhom y z end
+ end)
+ bin_obj.
+*)
+
+(* in the paper this is called simply an "enrichment" *)
+Structure PreMonoidalEnrichment :=
+{ enr_v_ob : Type
+; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
+; enr_v : Category enr_v_ob enr_v_hom
+; enr_v_i : enr_v_ob
+; enr_v_bobj : enr_v -> enr_v -> enr_v
+; enr_v_bin : BinoidalCat enr_v enr_v_bobj
+; enr_v_pmon : PreMonoidalCat enr_v_bin enr_v_i
+; enr_v_mon : MonoidalCat enr_v_pmon
+; enr_c_obj : Type
+; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v
+; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom
+; enr_c_bin : EBinoidalCat enr_c
+; enr_c_i : enr_c
+; enr_c_pm : PreMonoidalCat enr_c_bin enr_c_i
+}.
+Coercion enr_c : PreMonoidalEnrichment >-> ECategory.
+
+(*
+Structure MonoidalEnrichment {e:Enrichment} :=
+{ me_enr :=e
+; me_fobj : prod_obj e e -> e
+; me_f : Functor (e ×× e) e me_fobj
+; me_i : e
+; me_mon : MonoidalCat e me_fobj me_f me_i
+; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i)
+}.
+Implicit Arguments MonoidalEnrichment [ ].
+Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
+Coercion me_enr : MonoidalEnrichment >-> Enrichment.
+
+(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
+Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
+{ ffme_enr := me
+; ffme_mf_full : FullFunctor (HomFunctor e (me_i me))
+; ffme_mf_faithful : FaithfulFunctor (HomFunctor e (me_i me))
+; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me))
+}.
+Implicit Arguments MonicMonoidalEnrichment [ ].
+Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
+Transparent HomFunctor.
+
+Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
+{ smme_se : SurjectiveEnrichment e
+; smme_monoidal : MonoidalEnrichment e
+; smme_me : MonicMonoidalEnrichment _ smme_monoidal
+}.
+Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
+Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
+
+(* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
+Structure SMME :=
+{ smme_e : Enrichment
+; smme_see : SurjectiveEnrichment smme_e
+; smme_mon : MonoidalEnrichment smme_e
+; smme_mee : MonicMonoidalEnrichment _ smme_mon
+}.
+Coercion smme_e : SMME >-> Enrichment.
+Coercion smme_see : SMME >-> SurjectiveEnrichment.
+Coercion smme_mon : SMME >-> MonoidalEnrichment.
+Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.
+*)
\ No newline at end of file
(* products and duplication must distribute over each other *)
; ndr_prod_preserves_copy : forall `(f:a/⋯⋯/b), nd_copy a;; f**f === f ;; nd_copy b
+ ; ndr_comp_preserves_cancell : forall `(f:a/⋯⋯/b), nd_cancell;; f === nd_id _ ** f ;; nd_cancell
+ ; ndr_comp_preserves_cancelr : forall `(f:a/⋯⋯/b), nd_cancelr;; f === f ** nd_id _ ;; nd_cancelr
+ ; ndr_comp_preserves_assoc : forall `(f:a/⋯⋯/b)`(g:a1/⋯⋯/b1)`(h:a2/⋯⋯/b2),
+ nd_assoc;; (f ** (g ** h)) === ((f ** g) ** h) ;; nd_assoc
+
(* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
(* Sequent systems in which we can re-arrange the tree to the left of the turnstile - note that these rules
* mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
Class TreeStructuralRules :=
- { tsr_ant_assoc : forall {x a b c}, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
- ; tsr_ant_cossa : forall {x a b c}, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
- ; tsr_ant_cancell : forall {x a }, ND [ [],,a |= x] [ a |= x]
- ; tsr_ant_cancelr : forall {x a }, ND [a,,[] |= x] [ a |= x]
- ; tsr_ant_llecnac : forall {x a }, ND [ a |= x] [ [],,a |= x]
- ; tsr_ant_rlecnac : forall {x a }, ND [ a |= x] [ a,,[] |= x]
+ { tsr_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
+ ; tsr_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
+ ; tsr_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x]
+ ; tsr_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x]
+ ; tsr_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x]
+ ; tsr_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x]
}.
Notation "[# a #]" := (nd_rule a) : nd_scope.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
Require Import OppositeCategories_ch1_6_2.
Require Import Enrichment_ch2_8.
Require Import Subcategories_ch7_1.
intros; apply ndr_comp_associativity.
Defined.
- (* it is monoidal, with the judgment-tree-formation operator as its tensor *)
- Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
- fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
- Definition Judgments_Category_monoidal_endofunctor_fmor :
- forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) ->
- ((Judgments_Category_monoidal_endofunctor_fobj a)
- ~~{Judgments_Category}~~>
- (Judgments_Category_monoidal_endofunctor_fobj b)).
- intros.
- destruct a.
- destruct b.
- destruct X.
- simpl in *.
- exact (h**h0).
- Defined.
- Definition Judgments_Category_monoidal_endofunctor
- : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj.
- refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl.
- abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto).
- abstract (destruct a; simpl in *; reflexivity).
- abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp).
- Defined.
+ Hint Extern 1 => apply nd_structural_id0.
+ Hint Extern 1 => apply nd_structural_id1.
+ Hint Extern 1 => apply nd_structural_weak.
+ Hint Extern 1 => apply nd_structural_copy.
+ Hint Extern 1 => apply nd_structural_prod.
+ Hint Extern 1 => apply nd_structural_comp.
+ Hint Extern 1 => apply nd_structural_cancell.
+ Hint Extern 1 => apply nd_structural_cancelr.
+ Hint Extern 1 => apply nd_structural_llecnac.
+ Hint Extern 1 => apply nd_structural_rlecnac.
+ Hint Extern 1 => apply nd_structural_assoc.
+ Hint Extern 1 => apply nd_structural_cossa.
+ Hint Extern 1 => apply weak'_structural.
+ Instance jud_first (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => x,,a) :=
+ { fmor := fun b c (f:b /⋯⋯/ c) => f ** (nd_id a) }.
+ intros; unfold eqv; simpl.
+ apply ndr_prod_respects; auto.
+ intros; unfold eqv in *; simpl in *.
+ reflexivity.
+ intros; unfold eqv in *; simpl in *.
+ setoid_rewrite <- ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ reflexivity.
+ Defined.
+ Instance jud_second (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => a,,x) :=
+ { fmor := fun b c (f:b /⋯⋯/ c) => (nd_id a) ** f }.
+ intros; unfold eqv; simpl.
+ apply ndr_prod_respects; auto.
+ intros; unfold eqv in *; simpl in *.
+ reflexivity.
+ intros; unfold eqv in *; simpl in *.
+ setoid_rewrite <- ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ reflexivity.
+ Defined.
+ Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) :=
+ { bin_first := jud_first
+ ; bin_second := jud_second }.
Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
refine
{| iso_forward := nd_assoc
; iso_backward := nd_llecnac |};
abstract (simpl; auto).
Defined.
-
- Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
- refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl.
- abstract (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).
+ Instance jud_mon_cancelr : jud_first [] <~~~> functor_id Judgments_Category :=
+ { ni_iso := jud_cancelr_iso }.
+ intros; unfold eqv in *; simpl in *.
+ apply ndr_comp_preserves_cancelr.
Defined.
- Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
- eapply Build_NaturalIsomorphism.
- instantiate (1:=fun x => jud_cancell_iso x).
- abstract (intros; simpl;
- 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).
+ Instance jud_mon_cancell : jud_second [] <~~~> functor_id Judgments_Category :=
+ { ni_iso := jud_cancell_iso }.
+ intros; unfold eqv in *; simpl in *.
+ apply ndr_comp_preserves_cancell.
Defined.
- Definition jud_mon_assoc_iso : forall X,
- (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>>
- Judgments_Category_monoidal_endofunctor) X) ≅
- (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>>
- Judgments_Category_monoidal_endofunctor))) X.
- intros.
- destruct X as [a c].
- destruct a as [a b].
- exact (jud_assoc_iso a b c).
+ Instance jud_mon_assoc : forall a b, a ⋊- >>>> - ⋉b <~~~> - ⋉b >>>> a ⋊- :=
+ { ni_iso := fun c => jud_assoc_iso a c b }.
+ intros; unfold eqv in *; simpl in *.
+ apply ndr_comp_preserves_assoc.
Defined.
- Definition jud_mon_assoc :
- ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
- <~~~>
- func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
- refine {| ni_iso := jud_mon_assoc_iso |}.
+ Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b.
intros.
- unfold hom in *.
- destruct A as [a1 a3]. destruct a1 as [a1 a2]. simpl in *.
- destruct B as [b1 b3]. destruct b1 as [b1 b2]. simpl in *.
- destruct f as [f1 f3]. destruct f1 as [f1 f2]. simpl in *.
- unfold hom in *.
- unfold ob in *.
- unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
- setoid_rewrite ndr_prod_associativity.
- setoid_rewrite ndr_comp_associativity.
- setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- etransitivity.
- symmetry.
- apply ndr_comp_right_identity.
- apply ndr_comp_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
+ apply ni_inv.
+ refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}.
+ intros; unfold eqv in *; simpl in *.
+ apply ndr_comp_preserves_assoc.
Defined.
-
- Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] :=
- { mon_cancelr := jud_mon_cancelr
- ; mon_cancell := jud_mon_cancell
- ; mon_assoc := jud_mon_assoc }.
- abstract
- (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
- apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto).
- abstract
- (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
- apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto).
+ Instance jud_mon_assoc_ll : forall a b, (a ⊗ b) ⋊- <~~~> b ⋊- >>>> a ⋊- :=
+ { ni_iso := fun c => jud_assoc_iso _ _ _ }.
+ intros; unfold eqv in *; simpl in *.
+ apply ndr_comp_preserves_assoc.
Defined.
- Instance Judgments_Category_Terminal : Terminal Judgments_Category.
- refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}.
+ Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
+ { pmon_cancelr := jud_mon_cancelr
+ ; pmon_cancell := jud_mon_cancell
+ ; pmon_assoc := jud_mon_assoc
+ ; pmon_assoc_rr := jud_mon_assoc_rr
+ ; pmon_assoc_ll := jud_mon_assoc_ll
+ }.
+ unfold functor_fobj; unfold fmor; simpl;
+ apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
+
+ unfold functor_fobj; unfold fmor; simpl;
+ apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
+
+ intros; unfold eqv; simpl; auto.
+
+ intros; unfold eqv; simpl; auto.
+
+ intros; unfold eqv; simpl.
+ apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+
+ intros; unfold eqv; simpl.
+ apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+
+ intros; unfold eqv; simpl.
+ apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+
+ Defined.
+
+ Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal.
+ apply Build_MonoidalCat.
+ apply Build_CommutativeCat.
+ intros; apply Build_CentralMorphism; intros; unfold eqv; simpl in *.
+
+ setoid_rewrite <- (ndr_prod_preserves_comp (nd_id a) g f (nd_id d)).
+ setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+
+ setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
+ setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+ Defined.
+
+ Instance Judgments_Category_Terminal : TerminalObject Judgments_Category [].
+ refine {| drop := nd_weak' ; drop_unique := _ |}.
abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
Defined.
Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
- refine {| copy_nt := _ |}.
intros.
- refine {| nt_component := nd_copy |}.
- intros.
- unfold hom in *; unfold ob in *; unfold eqv.
- simpl.
- rewrite ndr_prod_preserves_copy; auto.
- reflexivity.
- Defined.
+ refine {| copy := nd_copy |}; intros; simpl.
+ setoid_rewrite ndr_comp_associativity.
+ setoid_rewrite <- (ndr_prod_preserves_copy f).
+ apply ndr_comp_respects; try reflexivity.
+ etransitivity.
+ symmetry.
+ apply ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+ setoid_rewrite ndr_comp_associativity.
+ setoid_rewrite <- (ndr_prod_preserves_copy f).
+ apply ndr_comp_respects; try reflexivity.
+ etransitivity.
+ symmetry.
+ apply ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+ Defined.
+
+ Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal :=
+ { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }.
- Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
- refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
- ; car_one := iso_id [] |}
- ; intros; unfold hom; simpl
- ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
-
- apply ndr_structural_indistinguishable; auto.
- apply nd_structural_comp; auto.
- apply nd_structural_comp; auto.
- unfold copy; simpl; apply nd_structural_copy; auto.
- apply nd_structural_prod; auto.
- apply nd_structural_comp; auto.
- apply weak'_structural.
- apply nd_structural_id0; auto.
- apply nd_structural_cancell; auto.
-
- apply ndr_structural_indistinguishable; auto.
- apply nd_structural_comp; auto.
- apply nd_structural_comp; auto.
- unfold copy; simpl; apply nd_structural_copy; auto.
- apply nd_structural_prod; auto.
- apply nd_structural_comp; auto.
- apply weak'_structural.
- apply nd_structural_id0; auto.
- apply nd_structural_cancelr; auto.
+ intros; unfold hom; simpl; unfold functor_fobj; unfold fmor; simpl.
+ apply ndr_structural_indistinguishable; auto.
+ intros; unfold hom; simpl; unfold functor_fobj; unfold fmor; simpl.
+ apply ndr_structural_indistinguishable; auto.
Defined.
End Judgments_Category.
apply pl_subst.
Defined.
+ Existing Instance pl_eqv.
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.
+ apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+ apply (mon_commutative(MonoidalCat:=JudgmentsL)).
unfold identityProof; unfold cutProof; simpl.
apply nd_cut_left_identity.
unfold identityProof; unfold cutProof; simpl.
Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
refine {| efunc := fun x y => (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y) |}.
- intros; apply MonoidalCat_all_central.
+ intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
apply se_reflexive_right.
intros. unfold ehom. unfold comp. simpl. unfold cutProof.
Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
eapply Build_EFunctor.
instantiate (1:=(fun x y => ((@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
- intros; apply MonoidalCat_all_central.
+ intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
apply se_reflexive_left.
intros. unfold ehom. unfold comp. simpl. unfold cutProof.
|}.
Defined.
- Definition Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a.
+ Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
+ { iso_forward := nd_seq_reflexive _ ;; tsr_ant_cossa _ a b c
+ ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_assoc _ a b c
+ }.
+ admit.
+ admit.
+ Defined.
+
+ 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 }.
+ admit.
+ Defined.
+
+ Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
+ { iso_forward := nd_seq_reflexive _ ;; tsr_ant_rlecnac _ a
+ ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_cancelr _ a
+ }.
+ admit.
admit.
Defined.
- Definition Types_cancelr : Types_first [] <~~~> functor_id _.
+ Instance Types_cancelr : Types_first [] <~~~> functor_id _ :=
+ { ni_iso := Types_cancelr_iso }.
admit.
Defined.
- Definition Types_cancell : Types_second [] <~~~> functor_id _.
+ Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
+ { iso_forward := nd_seq_reflexive _ ;; tsr_ant_llecnac _ a
+ ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_cancell _ a
+ }.
+ admit.
admit.
Defined.
- Definition Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a.
+ Instance Types_cancell : Types_second [] <~~~> functor_id _ :=
+ { ni_iso := Types_cancell_iso }.
admit.
Defined.
- Definition Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b.
+ 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 }.
+ admit.
+ 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) }.
admit.
Defined.
}.
admit. (* pentagon law *)
admit. (* triangle law *)
- admit. (* assoc_rr/assoc coherence *)
- admit. (* assoc_ll/assoc coherence *)
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
+ admit. (* assoc central *)
+ admit. (* cancelr central *)
+ admit. (* cancell central *)
Defined.
+ (*
Definition TypesEnrichedInJudgments : Enrichment.
refine {| enr_c := TypesL |}.
Defined.
Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
admit.
Defined.
-
+ *)
End LanguageCategory.
End Programming_Language.
-
+(*
Structure ProgrammingLanguageSMME :=
{ plsmme_t : Type
; plsmme_judg : Type
}.
Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
-
+*)
Implicit Arguments ND [ Judgment ].
projects / coq-hetmet.git / commitdiff