Require Import Coherence_ch7_8.
Require Import BinoidalCategories.
Require Import PreMonoidalCategories.
+Require Import PreMonoidalCenter.
+Require Import RepresentableStructure_ch7_2.
+Require Import WeakFunctorCategory.
+
+(* in the paper this is called simply an "enrichment" *)
+Structure Enrichment :=
+{ 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
+; enr_c_center := Center enr_c_bin
+; enr_c_center_mon := Center_is_Monoidal enr_c_pm
+}.
+Coercion enr_c : Enrichment >-> ECategory.
+
+Structure SurjectiveEnrichment :=
+{ senr_c_obj : Type
+; senr_v_ob := Tree ??(senr_c_obj * senr_c_obj)
+; senr_c_hom := fun (c1 c2:senr_c_obj) => [(c1, c2)]
+; senr_v_hom : senr_v_ob -> senr_v_ob -> Type
+; senr_v : Category senr_v_ob senr_v_hom
+; senr_v_i := []
+; senr_v_bobj := @T_Branch (option (senr_c_obj * senr_c_obj))
+; senr_v_bin : BinoidalCat senr_v senr_v_bobj
+; senr_v_pmon : PreMonoidalCat senr_v_bin senr_v_i
+; senr_v_mon : MonoidalCat senr_v_pmon
+; senr_c : ECategory senr_v_mon senr_c_obj senr_c_hom
+; senr_c_bin : EBinoidalCat senr_c
+; senr_c_i : senr_c
+; senr_c_pm : PreMonoidalCat senr_c_bin senr_c_i
+}.
+
+Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment.
+refine
+{| enr_v_ob := senr_v_ob se
+; enr_v_hom := senr_v_hom se
+; enr_v := senr_v se
+; enr_v_i := senr_v_i se
+; enr_v_bobj := senr_v_bobj se
+; enr_v_bin := senr_v_bin se
+; enr_v_pmon := senr_v_pmon se
+; enr_v_mon := senr_v_mon se
+; enr_c_obj := senr_c_obj se
+; enr_c_hom := senr_c_hom se
+; enr_c := senr_c se
+; enr_c_bin := senr_c_bin se
+; enr_c_i := senr_c_i se
+; enr_c_pm := senr_c_pm se
+|}.
+Defined.
+Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment.
-(* 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.
+Definition MonoidalEnrichment (e:Enrichment) :=
+ PreMonoidalFunctor
+ (enr_c_center_mon e)
+ (enr_v_pmon e)
+ (RestrictDomain (HomFunctor e (pmon_I (enr_c_pm e))) (Center (enr_c_pm e))).
*)
+Definition MonoidalEnrichment (e:Enrichment) :=
+ PreMonoidalFunctor
+ (enr_c_pm e)
+ (enr_v_pmon e)
+ (HomFunctor e (pmon_I (enr_c_pm e))).
-(* 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.
+(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
(*
-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.
+Definition SurjectiveEnrichment (ec:Enrichment) :=
+ @treeDecomposition (enr_v ec) (option (ec*ec))
+ (fun t => match t with
+ | None => enr_v_i ec
+ | Some x => match x with pair y z => enr_c_hom ec y z end
+ end)
+ (enr_v_bobj ec).
+*)
-(* 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))
+Class MonicEnrichment {e:Enrichment} :=
+{ me_enr := e
+; me_homfunctor := HomFunctor e (enr_c_i e)
+(*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*)
+; me_full : FullFunctor me_homfunctor
+; me_faithful : FaithfulFunctor me_homfunctor
+; me_conservative : ConservativeFunctor me_homfunctor
}.
-Implicit Arguments MonicMonoidalEnrichment [ ].
-Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
+Implicit Arguments MonicEnrichment [ ].
+Coercion me_enr : MonicEnrichment >-> Enrichment.
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_e : SurjectiveEnrichment
+(*; smme_see : SurjectiveEnrichment smme_e*)
; smme_mon : MonoidalEnrichment smme_e
-; smme_mee : MonicMonoidalEnrichment _ smme_mon
+; smme_mee : MonicEnrichment smme_e
}.
-Coercion smme_e : SMME >-> Enrichment.
-Coercion smme_see : SMME >-> SurjectiveEnrichment.
+Coercion smme_e : SMME >-> SurjectiveEnrichment.
Coercion smme_mon : SMME >-> MonoidalEnrichment.
-Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.
-*)
\ No newline at end of file
+
+Definition SMMEs : SmallCategories.
+ refine {| small_cat := SMME
+ ; small_cat_cat := fun smme => enr_v smme
+ |}.
+ Defined.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
+Require Import Enrichments.
Require Import RepresentableStructure_ch7_2.
+Require Import PreMonoidalCenter.
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.
Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
-{ ga_functor_obj : enr_v_mon K -> C
-; ga_functor : Functor (enr_v_mon K) C ga_functor_obj
-; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor
+{ ga_functor_obj : enr_v K -> ce
+; ga_functor : Functor (enr_v_mon K) (enr_c_pm ce) ga_functor_obj
+; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor
+(*
+; ga_functor : Functor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj
+; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor
+*)
}.
-Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
+Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.
Implicit Arguments GeneralizedArrow [ [ce] ].
Implicit Arguments ga_functor_obj [ K ce C ].
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
+Require Import Enrichments.
Require Import RepresentableStructure_ch7_2.
Require Import GeneralizedArrow.
Require Import WeakFunctorCategory.
-Require Import SmallSMMEs.
(*
* Technically reifications form merely a *semicategory* (no identity
Definition generalizedArrowOrIdentityFobj (s1 s2:SMMEs) (f:GeneralizedArrowOrIdentity s1 s2) : s1 -> s2 :=
match f in GeneralizedArrowOrIdentity S1 S2 return S1 -> S2 with
| gaoi_id s => fun x => x
- | gaoi_ga s1 s2 f => fun a => ehom(ECategory:=s2) (mon_i (smme_mon s2)) (ga_functor_obj f a)
+ | gaoi_ga s1 s2 f => fun a => ehom(ECategory:=s2) (enr_c_i (smme_e s2)) (ga_functor_obj f a)
end.
Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 s2)
: Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) :=
match f with
| gaoi_id s => functor_id _
- | gaoi_ga s1 s2 f => ga_functor f >>>> HomFunctor s2 (mon_i s2)
+ | gaoi_ga s1 s2 f => ga_functor f >>>> HomFunctor s2 (enr_c_i s2)
end.
-Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
- GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
- intro g01.
- intro g12.
- refine
- {| ga_functor := g01 >>>> HomFunctor s1 (mon_i s1) >>>> g12 |}.
- apply MonoidalFunctorsCompose.
- apply MonoidalFunctorsCompose.
- apply (ga_functor_monoidal g01).
- apply (me_mf s1).
- apply (ga_functor_monoidal g12).
- Defined.
+Instance compose_generalizedArrows (s0 s1 s2:SMMEs)
+ (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 :=
+ { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }.
Definition generalizedArrowOrIdentityComp
: forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.
apply if_right_identity.
unfold mf_F.
idtac.
- unfold mf_f.
apply if_associativity.
Defined.
Require Import NaturalIsomorphisms_ch7_5.
Require Import BinoidalCategories.
Require Import PreMonoidalCategories.
+Require Import PreMonoidalCenter.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
+Require Import Enrichments.
Require Import RepresentableStructure_ch7_2.
Require Import Reification.
Require Import GeneralizedArrow.
Section GArrowFromReification.
- Context `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)).
+ Definition binoidalcat_iso `{bc:BinoidalCat}{a1 b1 a2 b2:bc} (i1:a1≅a2)(i2:b1≅b2) : (a1⊗b1)≅(a2⊗b2) :=
+ iso_comp
+ (functors_preserve_isos (- ⋉ b1) i1 )
+ (functors_preserve_isos (a2 ⋊ -) i2).
- Fixpoint garrow_fobj_ vk : C :=
+ Context `(K : SurjectiveEnrichment)
+ `(CMon : MonicEnrichment C)
+ (CM : MonoidalEnrichment C)
+ (reification : Reification K C (pmon_I (enr_c_pm C))).
+
+ Fixpoint garrow_fobj (vk:senr_v K) : C :=
match vk with
- | T_Leaf None => me_i C
+ | T_Leaf None => enr_c_i C
| T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end
- | t1,,t2 => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2))
+ | t1,,t2 => bin_obj(BinoidalCat:=enr_c_bin C) (garrow_fobj t1) (garrow_fobj t2)
end.
- Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp _ K vk)).
-
- Definition homset_tensor_iso
- : forall vk:enr_v_mon K, (reification_rstar reification vk) ≅ ehom(ECategory:=C) (me_i C) (garrow_fobj vk).
- intros.
- unfold garrow_fobj.
- set (se_decomp _ K vk) as sevk.
- destruct sevk.
- simpl in *.
- rewrite e.
- clear e.
- induction x; simpl.
-
- destruct a.
- destruct p.
-
- apply iso_inv.
- apply (ni_iso (reification_commutes reification e) e0).
-
- eapply id_comp.
- apply iso_inv.
- apply (mf_id (reification_rstar reification)).
- apply (mf_id (me_mf C)).
-
- eapply id_comp.
- apply iso_inv.
- apply (ni_iso (mf_coherence (reification_rstar reification)) (pair_obj _ _)).
- eapply id_comp.
- Focus 2.
- apply (ni_iso (mf_coherence (me_mf C)) (pair_obj _ _)).
- unfold bin_obj.
- apply (functors_preserve_isos (enr_v_f C) (a:=(pair_obj _ _))(b:=(pair_obj _ _))).
- apply (iso_prod IHx1 IHx2).
- Defined.
-
- Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (HomFunctor C (me_i C)).
- exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)).
- abstract (exists (garrow_fobj vk); auto).
- Defined.
+ Fixpoint homset_tensor_iso (vk:enr_v_mon K) : reification vk ≅ enr_c_i C ~~> garrow_fobj vk :=
+ match vk as VK return reification VK ≅ enr_c_i C ~~> garrow_fobj VK with
+ | T_Leaf None => (mf_i(PreMonoidalFunctor:=reification))⁻¹ >>≅>> (mf_i(PreMonoidalFunctor:=CM))
+ | T_Leaf (Some a) => match a as A
+ return reification (T_Leaf (Some A)) ≅ enr_c_i C ~~> garrow_fobj (T_Leaf (Some A)) with
+ (s,s0) => iso_inv _ _ (ni_iso (reification_commutes reification s) s0)
+ end
+ | t1,,t2 => (ni_iso (@mf_first _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ reification _) _)⁻¹ >>≅>>
+ (binoidalcat_iso (homset_tensor_iso t1) (homset_tensor_iso t2)) >>≅>>
+ (ni_iso (mf_first(PreMonoidalFunctor:=CM) (garrow_fobj t2)) _)
+ end.
- Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (HomFunctor C (me_i C))}~~>(garrow_fobj' b).
- exists (iso_backward (homset_tensor_iso a)
- >>> reification_rstar reification \ f
- >>> iso_forward (homset_tensor_iso b)).
- abstract (auto).
- Defined.
+ Definition HomFunctor_fullimage := FullImage CM.
- (* The poorly-named "step1_functor" is a functor from the full subcategory in the range of the reification functor
+ (* R' is a functor from the domain of the reification functor
* to the full subcategory in the range of the [host language's] Hom(I,-) functor *)
- Definition step1_functor : Functor (enr_v_mon K) (FullImage (HomFunctor C (me_i C))) garrow_fobj'.
- refine {| fmor := fun a b f => step1_mor f |}.
- abstract (intros; unfold step1_mor; simpl;
+ Instance R' : Functor (FullImage (reification_rstar reification)) HomFunctor_fullimage garrow_fobj :=
+ { fmor := fun a b (f:a~~{FullImage (reification_rstar reification)}~~>b) =>
+ (#(homset_tensor_iso a)⁻¹ >>> f >>> #(homset_tensor_iso b))
+ }.
+ abstract (intros; simpl;
apply comp_respects; try reflexivity;
apply comp_respects; try reflexivity;
- apply fmor_respects; auto).
- abstract (intros; unfold step1_mor; simpl;
- setoid_rewrite fmor_preserves_id;
+ auto).
+ abstract (intros; simpl;
setoid_rewrite right_identity;
apply iso_comp2).
abstract (intros;
- unfold step1_mor;
simpl;
repeat setoid_rewrite <- associativity;
apply comp_respects; try reflexivity;
repeat setoid_rewrite associativity;
- apply comp_respects; try reflexivity;
- setoid_rewrite juggle2;
- set (iso_comp1 (homset_tensor_iso b)) as qqq;
- setoid_rewrite qqq;
- clear qqq;
- setoid_rewrite right_identity;
- apply (fmor_preserves_comp reification)).
+ apply comp_respects; try apply reflexivity;
+ apply comp_respects; try apply reflexivity;
+ eapply transitivity; [ symmetry; apply associativity | idtac ];
+ eapply transitivity; [ idtac | apply left_identity ];
+ apply comp_respects; try apply reflexivity;
+ apply iso_comp1).
Defined.
- Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C))).
- exists (fun c1 => homset_tensor_iso c1).
- abstract (intros;
- simpl;
- repeat setoid_rewrite <- associativity;
- setoid_rewrite iso_comp1;
- setoid_rewrite left_identity;
- reflexivity).
+ (* the "step2_functor" is the section of the Hom(I,-) functor *)
+ Definition step2_functor :=
+ ff_functor_section_functor _ (me_full(MonicEnrichment:=CMon)) (me_faithful(MonicEnrichment:=CMon)).
+
+ Definition garrow_functor :=
+ RestrictToImage (reification_rstar reification) >>>> (R' >>>> step2_functor).
+
+ Lemma iso_id_lemma1 `{C':Category}(a b:C')(f:a~~{C'}~~>b) : #(iso_id a) >>> f ~~ f.
+ simpl.
+ apply left_identity.
Qed.
- (* the "step2_functor" is the section of the Hom(I,-) functor *)
- Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C).
+ Lemma iso_id_lemma2 `{C':Category}(a b:C')(f:b~~{C'}~~>a) : f >>> #(iso_id a) ~~ f.
+ simpl.
+ apply right_identity.
+ Qed.
- (* the generalized arrow is the composition of the two steps *)
- Definition garrow_functor := step1_functor >>>> step2_functor.
+ Lemma full_roundtrip : forall a b (f:a~>b), me_homfunctor \ (ff_functor_section_fmor me_homfunctor me_full f) ~~ f.
+ intros.
+ unfold ff_functor_section_fmor.
+ set (me_full a b f) as full.
+ destruct full.
+ apply e.
+ Qed.
- Lemma garrow_functor_monoidal_iso_i
- : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
- admit.
- Defined.
+ Opaque UnderlyingFunctor.
+ Instance garrow_first a :
+ (garrow_functor >>>> bin_first(BinoidalCat:=enr_c_bin C) (R' a)) <~~~>
+ (bin_first(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
+ { ni_iso := fun a => iso_id _ }.
+ intros.
+ etransitivity. apply iso_id_lemma1. symmetry.
+ etransitivity. apply iso_id_lemma2. symmetry.
- Lemma garrow_functor_monoidal_iso :
- forall X Y:enr_v_mon K,
- garrow_functor (bin_obj(BinoidalCat:=enr_v_mon K) X Y) ≅ bin_obj(BinoidalCat:=me_mon C) (garrow_functor X) (garrow_functor Y).
- admit.
- Defined.
+ Opaque Underlying.
+ unfold garrow_functor.
+ unfold functor_comp at 1.
+ unfold functor_comp at 1.
+ Opaque functor_comp. simpl. Transparent functor_comp.
+
+ symmetry.
+ eapply transitivity.
+ apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_first (R' a)) f).
+ unfold functor_comp at 1.
+ unfold functor_comp at 1.
+ Opaque functor_comp. simpl. Transparent functor_comp.
+
+ symmetry.
+ eapply transitivity.
+ set (ni_commutes (mf_first(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
+ unfold functor_comp in qq.
+ simpl in qq.
+ apply iso_shift_right' in qq.
+ apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ symmetry.
+ unfold fmor at 1.
+ eapply transitivity.
+ set (ni_commutes (mf_first(PreMonoidalFunctor:=CM) (R' a))) as zz.
+ unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
+ set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
+ apply iso_shift_right' in zz'.
+ apply zz'.
+
+ unfold functor_comp; simpl.
+
+ symmetry.
+ eapply transitivity.
+ set full_roundtrip as full_roundtrip'.
+ unfold fmor in full_roundtrip'.
+ simpl in full_roundtrip'.
+ apply full_roundtrip'.
+
+ set (@iso_shift_right') as q. simpl in q. apply q. clear q.
+
+ set (@iso_shift_left) as q. simpl in q. apply q. clear q.
+
+ symmetry.
+ eapply transitivity.
+ set full_roundtrip as full_roundtrip'.
+ unfold fmor in full_roundtrip'.
+ simpl in full_roundtrip'.
+ apply (fun a' b' f z => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
+ symmetry.
+
+ intros.
+ unfold bin_obj.
+ unfold senr_v_bobj.
+
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ simpl.
+ setoid_rewrite <- associativity.
+ etransitivity.
+ apply iso_comp1_left.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ apply iso_comp1_right.
+
+ eapply symmetry.
+ eapply transitivity.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ eapply reflexivity.
+ eapply symmetry.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ eapply comp_respects; [ reflexivity | idtac ].
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; try apply reflexivity.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ eapply associativity.
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ apply iso_comp1_left.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply comp_respects.
+ eapply symmetry.
+ eapply associativity.
+ eapply reflexivity.
+ apply iso_comp1_left.
- Definition garrow_functor_monoidal_niso
- : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply associativity.
+ eapply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ eapply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ eapply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ unfold functor_fobj.
+ apply fmor_preserves_comp.
+ setoid_rewrite iso_comp2.
+ apply fmor_preserves_id.
+
+ apply comp_respects.
+ reflexivity.
+ reflexivity.
+ Defined.
+
+ Instance garrow_second a :
+ (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a))
+ <~~~> (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
+ { ni_iso := fun a => iso_id _ }.
admit.
Defined.
- Opaque homset_tensor_iso.
- Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
- { mf_coherence := garrow_functor_monoidal_niso
- ; mf_id := garrow_functor_monoidal_iso_i
- }.
- admit.
- admit.
+Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
+Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
+Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
+
+ Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
+ iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
+ #((mf_first F b) _) >>> F \ #(pmon_cancell b).
+ set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
+ setoid_rewrite associativity in q.
+ set (@comp_respects) as qq.
+ unfold Proper in qq.
+ unfold respectful in qq.
+ set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
+ setoid_rewrite <- associativity in q'.
+ clear q qq.
+ setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
+ eapply transitivity; [ apply q' | idtac ].
+ clear q'.
+ setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ symmetry.
+ apply iso_shift_left.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
+ apply (fmor_respects (-⋉ F b)).
+ apply iso_comp2.
+ Qed.
+
+ Lemma cancell_coherent (b:enr_v K) :
+ #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
+ (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
+ #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
+ Opaque Underlying.
+ Opaque fmor.
+ intros; simpl.
+ setoid_rewrite right_identity.
+ symmetry.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects.
+ apply (fmor_preserves_id (ebc_first (garrow_functor b))).
+ unfold garrow_functor.
+ unfold step2_functor.
+ Transparent fmor.
+ unfold functor_fobj.
+ unfold functor_comp.
+ simpl.
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
+
+ apply symmetry.
+ apply iso_shift_left.
+
+ symmetry.
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
+ eapply transitivity; [ idtac | apply associativity ].
+ apply q.
+
+ apply iso_shift_left'.
+ eapply transitivity.
+ apply associativity.
+ symmetry.
+ set (@iso_shift_right') as qq.
+ simpl in qq.
+ apply qq.
+ clear qq.
+ unfold me_homfunctor.
+ eapply transitivity.
+ symmetry.
+ apply (cancell_lemma CM (garrow_fobj b)).
+
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply symmetry.
+ eapply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; try reflexivity.
+
+ unfold functor_fobj.
+ unfold pmon_I.
+
+ set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply q.
+ clear q.
+ unfold fmor; simpl.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects; try reflexivity.
+ apply iso_comp2.
+ Qed.
+
+ Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
+ (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
+ #((mf_first F _) _) >>> F \ #(pmon_cancelr b).
+ set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
+ setoid_rewrite associativity in q.
+ set (@comp_respects) as qq.
+ unfold Proper in qq.
+ unfold respectful in qq.
+ set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
+ setoid_rewrite <- associativity in q'.
+ clear q qq.
+ setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
+ eapply transitivity; [ apply q' | idtac ].
+ clear q'.
+ setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ symmetry.
+ apply iso_shift_left.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
+ apply (fmor_respects (-⋉ F b)).
+ apply iso_comp2.
+ Qed.
+
+ Lemma cancelr_coherent (b:enr_v K) :
+ #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
+ (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
+ #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
+
+ Opaque Underlying.
+ Opaque fmor.
+ intros; simpl.
+ setoid_rewrite right_identity.
+ symmetry.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects.
+ apply (fmor_preserves_id (ebc_second (garrow_functor b))).
+ unfold garrow_functor.
+ unfold step2_functor.
+ Transparent fmor.
+ unfold functor_fobj.
+ unfold functor_comp.
+ simpl.
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+
+ apply symmetry.
+ apply iso_shift_left.
+
+ symmetry.
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+
+ set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
+ setoid_rewrite associativity in q.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ symmetry.
+ eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply mf_consistent.
+ eapply symmetry.
+ apply q.
+
+ apply iso_shift_left'.
+ eapply transitivity.
+ apply associativity.
+ symmetry.
+ set (@iso_shift_right') as qq.
+ simpl in qq.
+ apply qq.
+ clear qq.
+ unfold me_homfunctor.
+ eapply transitivity.
+ symmetry.
+ apply (cancelr_lemma CM (garrow_fobj b)).
+
+ unfold functor_fobj.
+ unfold pmon_I.
+
+ set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply q.
+ clear q.
+
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; try reflexivity.
+ simpl.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects; try reflexivity.
+ apply iso_comp2.
+ Qed.
+
+ Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
+ { mf_first := garrow_first
+ ; mf_second := garrow_second
+ ; mf_i := iso_id _ }.
+ intros; reflexivity.
+ intros.
+ unfold garrow_functor.
+ unfold fmor.
+ Opaque fmor. simpl.
+ unfold step2_functor.
+ admit.
+ Transparent fmor.
+
+ apply cancell_coherent.
+ apply cancelr_coherent.
admit.
Defined.
- Definition garrow_from_reification : GeneralizedArrow K C.
- refine
- {| ga_functor := garrow_functor
- ; ga_functor_monoidal := garrow_functor_monoidal
- |}.
- Defined.
+ Definition garrow_from_reification : GeneralizedArrow K CM :=
+ {| ga_functor_monoidal := garrow_monoidal |}.
End GArrowFromReification.
-Opaque homset_tensor_iso.
+
Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
: forall h c,
(h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
- ((obact ec h)~~{TypesL _ _ (SystemFCa _ Γ Δ)}~~>(obact ec c)).
+ ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)).
set (@nil (HaskTyVar Γ ★)) as lev.
(* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
- set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))
+ set (snd_initial(SequentND:=@pl_snd _ _ _ _ (SystemFCa Γ Δ))
(mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
eapply nd_comp.
eapply nd_prod.
eapply nd_comp.
apply (nd_llecnac ;; nd_prod IHX1 IHX2).
clear IHX1 IHX2 X1 X2.
- apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa _ Γ Δ))).
+ (*
+ apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
+ *)
+ admit.
(* nd_cancell becomes RVar;;RuCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_cancelr becomes RVar;;RuCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_llecnac becomes RVar;;RCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_rlecnac becomes RVar;;RCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_assoc becomes RVar;;RAssoc *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_cossa becomes RVar;;RCossa *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
destruct r as [r rp].
Defined.
- Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa _ Γ Δ)) (obact ec) :=
+ Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) :=
{ fmor := FlatteningFunctor_fmor }.
admit.
admit.
admit.
admit.
admit.
- admit.
- admit.
Defined.
(*
admit.
admit.
admit.
- admit.
- admit.
Defined.
Hint Constructors Rule_Flat.
- Instance PCF_sequents Γ Δ lev : @SequentCalculus _ (PCFRule Γ Δ lev) _ pcfjudg.
- apply Build_SequentCalculus.
- intros.
- induction a.
- destruct a; simpl.
- apply nd_rule.
- exists (RVar _ _ _ _).
- apply PCF_RVar.
- apply nd_rule.
- exists (RVoid _ _ ).
- apply PCF_RVoid.
- eapply nd_comp.
- eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply (nd_prod IHa1 IHa2).
- apply nd_rule.
- exists (RJoin _ _ _ _ _ _).
- apply PCF_RJoin.
- Defined.
-
Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
admit.
Defined.
admit.
Defined.
- Instance PCF_cutrule Γ Δ lev : CutRule (PCF_sequents Γ Δ lev) :=
- { nd_cut := PCF_cut Γ Δ lev }.
- admit.
- admit.
- admit.
- Defined.
+ Instance PCF_sequents Γ Δ lev : @SequentND _ (PCFRule Γ Δ lev) _ pcfjudg :=
+ { snd_cut := PCF_cut Γ Δ lev }.
+ apply Build_SequentND.
+ intros.
+ induction a.
+ destruct a; simpl.
+ apply nd_rule.
+ exists (RVar _ _ _ _).
+ apply PCF_RVar.
+ apply nd_rule.
+ exists (RVoid _ _ ).
+ apply PCF_RVoid.
+ eapply nd_comp.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply (nd_prod IHa1 IHa2).
+ apply nd_rule.
+ exists (RJoin _ _ _ _ _ _).
+ apply PCF_RJoin.
+ admit.
+ Defined.
Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
- eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
+ eapply nd_prod; [ apply snd_initial | apply nd_id ].
apply nd_rule.
set (@PCF_RJoin Γ Δ lev a b a c) as q'.
refine (existT _ _ _).
Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
- eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
+ eapply nd_prod; [ apply nd_id | apply snd_initial ].
apply nd_rule.
set (@PCF_RJoin Γ Δ lev b a c a) as q'.
refine (existT _ _ _).
apply q'.
Defined.
- Instance PCF_sequent_join Γ Δ lev : @SequentExpansion _ _ _ _ _ (PCF_sequents Γ Δ lev) (PCF_cutrule Γ Δ lev) :=
- { se_expand_left := PCF_left Γ Δ lev
- ; se_expand_right := PCF_right Γ Δ lev }.
+ Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ pcfjudg _ :=
+ { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b
+ ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
+ admit.
admit.
admit.
admit.
admit.
+ admit.
+ Defined.
+
+ Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) OrgND.
+ admit.
+ Defined.
+
+ Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev).
+ admit.
Defined.
(* 5.1.3 *)
Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
- { pl_eqv := OrgPCF Γ Δ lev
- ; pl_sc := PCF_sequents Γ Δ lev
- ; pl_subst := PCF_cutrule Γ Δ lev
- ; pl_sequent_join := PCF_sequent_join Γ Δ lev
+ { pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev
+ ; pl_snd := PCF_sequents Γ Δ lev
}.
+ (*
apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
apply nd_rule. unfold PCFRule. simpl.
exists (RArrange _ _ _ _ _ (RuCanR _)).
apply (PCF_RArrange lev _ (a,,[]) _).
Defined.
-
- Instance SystemFCa_sequents Γ Δ : @SequentCalculus _ OrgR _ (mkJudg Γ Δ).
- apply Build_SequentCalculus.
- intros.
- induction a.
- destruct a; simpl.
- apply nd_rule.
- destruct l.
- apply org_fc with (r:=RVar _ _ _ _).
- auto.
- apply nd_rule.
- apply org_fc with (r:=RVoid _ _ ).
- auto.
- eapply nd_comp.
- eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply (nd_prod IHa1 IHa2).
- apply nd_rule.
- apply org_fc with (r:=RJoin _ _ _ _ _ _).
- auto.
- Defined.
+*)
Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
intros.
apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
Defined.
- Instance SystemFCa_cutrule Γ Δ : CutRule (SystemFCa_sequents Γ Δ) :=
- { nd_cut := SystemFCa_cut Γ Δ }.
- admit.
- admit.
- admit.
- Defined.
+ Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) :=
+ { snd_cut := SystemFCa_cut Γ Δ }.
+ apply Build_SequentND.
+ intros.
+ induction a.
+ destruct a; simpl.
+ apply nd_rule.
+ destruct l.
+ apply org_fc with (r:=RVar _ _ _ _).
+ auto.
+ apply nd_rule.
+ apply org_fc with (r:=RVoid _ _ ).
+ auto.
+ eapply nd_comp.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply (nd_prod IHa1 IHa2).
+ apply nd_rule.
+ apply org_fc with (r:=RJoin _ _ _ _ _ _).
+ auto.
+ admit.
+ Defined.
Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
- eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
+ eapply nd_prod; [ apply snd_initial | apply nd_id ].
apply nd_rule.
apply org_fc with (r:=RJoin Γ Δ a b a c).
auto.
Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
- eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
+ eapply nd_prod; [ apply nd_id | apply snd_initial ].
apply nd_rule.
apply org_fc with (r:=RJoin Γ Δ b a c a).
auto.
Defined.
+(*
Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
{ se_expand_left := SystemFCa_left Γ Δ
; se_expand_right := SystemFCa_right Γ Δ }.
admit.
admit.
Defined.
-
+*)
(* 5.1.2 *)
- Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR :=
+ Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR.
+(*
{ pl_eqv := OrgNDR
- ; pl_sc := SystemFCa_sequents Γ Δ
+ ; pl_sn := SystemFCa_sequents Γ Δ
; pl_subst := SystemFCa_cutrule Γ Δ
; pl_sequent_join := SystemFCa_sequent_join Γ Δ
}.
apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR a ))). apply Flat_RArrange.
apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a ))). apply Flat_RArrange.
apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a ))). apply Flat_RArrange.
+*)
+admit.
Defined.
End HaskProofStratified.
refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
apply FreshMon.
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *.
+ set (update_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *.
refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
apply FreshMon.
simpl.
refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
apply FreshMon.
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
+ set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
inversion X_.
apply ileaf in X.
apply ileaf in X0.
| nd_id1 : forall h, [ h ] /⋯⋯/ [ h ]
(* natural deduction: you may discard conclusions *)
- | nd_weak : forall h, [ h ] /⋯⋯/ [ ]
+ | nd_weak1 : forall h, [ h ] /⋯⋯/ [ ]
(* natural deduction: you may duplicate conclusions *)
| nd_copy : forall h, h /⋯⋯/ (h,,h)
Open Scope nd_scope.
Open Scope pf_scope.
- (* a proof is "structural" iff it does not contain any invocations of nd_rule *)
+ (* a predicate on proofs *)
+ Definition NDPredicate := forall h c, h /⋯⋯/ c -> Prop.
+
+ (* the structural inference rules are those which do not change, add, remove, or re-order the judgments *)
Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
| nd_structural_id0 : Structural nd_id0
| nd_structural_id1 : forall h, Structural (nd_id1 h)
- | nd_structural_weak : forall h, Structural (nd_weak h)
- | nd_structural_copy : forall h, Structural (nd_copy h)
- | nd_structural_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2)
- | nd_structural_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2)
| nd_structural_cancell : forall {a}, Structural (@nd_cancell a)
| nd_structural_cancelr : forall {a}, Structural (@nd_cancelr a)
| nd_structural_llecnac : forall {a}, Structural (@nd_llecnac a)
| nd_structural_cossa : forall {a b c}, Structural (@nd_cossa a b c)
.
+ (* the closure of an NDPredicate under nd_comp and nd_prod *)
+ Inductive NDPredicateClosure (P:NDPredicate) : forall {h c}, h /⋯⋯/ c -> Prop :=
+ | ndpc_p : forall h c f, P h c f -> NDPredicateClosure P f
+ | ndpc_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2),
+ NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1**pf2)
+ | ndpc_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2),
+ NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1;;pf2).
+
+ (* proofs built up from structural rules via comp and prod *)
+ Definition StructuralND {h}{c} f := @NDPredicateClosure (@Structural) h c f.
+
+ (* The Predicate (BuiltFrom f P h) asserts that "h" was built from a single occurrence of "f" and proofs which satisfy P *)
+ Inductive BuiltFrom {h'}{c'}(f:h'/⋯⋯/c')(P:NDPredicate) : forall {h c}, h/⋯⋯/c -> Prop :=
+ | builtfrom_refl : BuiltFrom f P f
+ | builtfrom_P : forall h c g, @P h c g -> BuiltFrom f P g
+ | builtfrom_prod1 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f1 ** f2)
+ | builtfrom_prod2 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f2 ** f1)
+ | builtfrom_comp1 : forall h x c f1 f2, P h x f1 -> @BuiltFrom _ _ f P x c f2 -> BuiltFrom f P (f1 ;; f2)
+ | builtfrom_comp2 : forall h x c f1 f2, P x c f1 -> @BuiltFrom _ _ f P h x f2 -> BuiltFrom f P (f2 ;; f1).
+
(* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
match sl with
| T_Branch a b => nd_prod (nd_id a) (nd_id b)
end.
- Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
+ Fixpoint nd_weak (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
match sl as SL return SL /⋯⋯/ [] with
| T_Leaf None => nd_id0
- | T_Leaf (Some x) => nd_weak x
- | T_Branch a b => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr
+ | T_Leaf (Some x) => nd_weak1 x
+ | T_Branch a b => nd_prod (nd_weak a) (nd_weak b) ;; nd_cancelr
end.
Hint Constructors Structural.
- Lemma nd_id_structural : forall sl, Structural (nd_id sl).
+ Hint Constructors BuiltFrom.
+ Hint Constructors NDPredicateClosure.
+
+ Hint Extern 1 => apply nd_structural_id0.
+ Hint Extern 1 => apply nd_structural_id1.
+ 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 ndpc_p.
+ Hint Extern 1 => apply ndpc_prod.
+ Hint Extern 1 => apply ndpc_comp.
+
+ Lemma nd_id_structural : forall sl, StructuralND (nd_id sl).
intros.
induction sl; simpl; auto.
destruct a; auto.
Defined.
- Lemma weak'_structural : forall a, Structural (nd_weak' a).
- intros.
- induction a.
- destruct a; auto.
- simpl.
- auto.
- simpl.
- auto.
- Qed.
-
(* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
* structural variations *)
Class ND_Relation :=
(* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
; ndr_comp_respects : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c), f === f' -> g === g' -> f;;g === f';;g'
; ndr_comp_associativity : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d), (f;;g);;h === f;;(g;;h)
- ; ndr_comp_left_identity : forall `(f:a/⋯⋯/c), nd_id _ ;; f === f
- ; ndr_comp_right_identity : forall `(f:a/⋯⋯/c), f ;; nd_id _ === f
(* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
; ndr_prod_respects : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d), f===f' -> g===g' -> f**g === f'**g'
; ndr_prod_associativity : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'), (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
- ; ndr_prod_left_identity : forall `(f:a/⋯⋯/b), (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac
- ; ndr_prod_right_identity : forall `(f:a/⋯⋯/b), (f ** nd_id0) === nd_cancelr ;; f ;; nd_rlecnac
(* products and composition must distribute over each other *)
; ndr_prod_preserves_comp : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g')
- (* 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
+ (* Given a proof f, any two proofs built from it using only structural rules are indistinguishable. Keep in mind that
+ * nd_weak and nd_copy aren't considered structural, so the hypotheses and conclusions of such proofs will be an identical
+ * list, differing only in the "parenthesization" and addition or removal of empty leaves. *)
+ ; ndr_builtfrom_structural : forall `(f:a/⋯⋯/b){a' b'}(g1 g2:a'/⋯⋯/b'),
+ BuiltFrom f (@StructuralND) g1 ->
+ BuiltFrom f (@StructuralND) g2 ->
+ g1 === g2
- ; 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
+ (* proofs of nothing are not distinguished from each other *)
+ ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
- (* 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
+ (* 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
- (* any two proofs of nothing are "equally good" *)
- ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
+ (* duplicating a hypothesis and discarding it is irrelevant *)
+ ; ndr_copy_then_weak_left : forall a, nd_copy a;; (nd_weak _ ** nd_id _) ;; nd_cancell === nd_id _
+ ; ndr_copy_then_weak_right : forall a, nd_copy a;; (nd_id _ ** nd_weak _) ;; nd_cancelr === nd_id _
}.
(*
end.
(* Natural Deduction systems whose judgments happen to be pairs of the same type *)
- Section Sequents.
- Context {S:Type}. (* type of sequent components *)
- Context {sequent:S->S->Judgment}.
- Context {ndr:ND_Relation}.
+ Section SequentND.
+ Context {S:Type}. (* type of sequent components *)
+ Context {sequent:S->S->Judgment}. (* pairing operation which forms a sequent from its halves *)
Notation "a |= b" := (sequent a b).
- Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope.
-
- (* Sequent systems with initial sequents *)
- Class SequentCalculus :=
- { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
- }.
- (* Sequent systems with a cut rule *)
- Class CutRule (nd_cutrule_seq:SequentCalculus) :=
- { nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
- ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
- ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr
- ; nd_cut_associativity : forall {a b c d},
- (nd_id1 (a|=b) ** nd_cut b c d) ;; (nd_cut a b d) === nd_cossa ;; (nd_cut a b c ** nd_id1 (c|=d)) ;; nd_cut a c d
+ (* a SequentND is a natural deduction whose judgments are sequents, has initial sequents, and has a cut rule *)
+ Class SequentND :=
+ { snd_initial : forall a, [ ] /⋯⋯/ [ a |= a ]
+ ; snd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
}.
- End Sequents.
-
- (* Sequent systems in which each side of the sequent is a tree of something *)
- Section SequentsOfTrees.
- Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}.
+ Context (sequentND:SequentND).
Context (ndr:ND_Relation).
- Notation "a |= b" := (sequent a b).
- Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope.
-
- (* 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]
- }.
- Notation "[# a #]" := (nd_rule a) : nd_scope.
+ (*
+ * A predicate singling out structural rules, initial sequents,
+ * and cut rules.
+ *
+ * Proofs using only structural rules cannot add or remove
+ * judgments - their hypothesis and conclusion judgment-trees will
+ * differ only in "parenthesization" and the presence/absence of
+ * empty leaves. This means that a proof involving only
+ * structural rules, cut, and initial sequents can ADD new
+ * non-empty judgment-leaves only via snd_initial, and can only
+ * REMOVE non-empty judgment-leaves only via snd_cut. Since the
+ * initial sequent is a left and right identity for cut, and cut
+ * is associative, any two proofs (with the same hypotheses and
+ * conclusions) using only structural rules, cut, and initial
+ * sequents are logically indistinguishable - their differences
+ * are logically insignificant.
+ *
+ * Note that it is important that nd_weak and nd_copy aren't
+ * considered to be "structural".
+ *)
+ Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | snd_inert_initial : forall a, SequentND_Inert _ _ (snd_initial a)
+ | snd_inert_cut : forall a b c, SequentND_Inert _ _ (snd_cut a b c)
+ | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f
+ .
+
+ (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions
+ * if those proofs use only initial sequents, cut, and structural rules (see comment above) *)
+ Class SequentND_Relation :=
+ { sndr_ndr := ndr
+ ; sndr_inert : forall a b (f g:a/⋯⋯/b),
+ NDPredicateClosure SequentND_Inert f ->
+ NDPredicateClosure SequentND_Inert g ->
+ ndr_eqv f g }.
+
+ End SequentND.
+
+ (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
+ Section ContextND.
+ Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}.
+ Context {snd:SequentND(sequent:=sequent)}.
+ Notation "a |= b" := (sequent a b).
- (* Sequent systems in which we can add any proposition to both sides of the sequent (sort of a "horizontal weakening") *)
- Context `{se_cut : @CutRule _ sequent ndr sc}.
- Class SequentExpansion :=
- { se_expand_left : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
- ; se_expand_right : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
+ (* Note that these rules mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
+ Class ContextND :=
+ { cnd_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x ]
+ ; cnd_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x ]
+ ; cnd_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x ]
+ ; cnd_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x ]
+ ; cnd_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x ]
+ ; cnd_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x ]
+ ; cnd_expand_left : forall a b c , ND [ a |= b] [ c,,a |= c,,b]
+ ; cnd_expand_right : forall a b c , ND [ a |= b] [ a,,c |= b,,c]
+ ; cnd_snd := snd
+ }.
- (* left and right expansion must commute with cut *)
- ; se_reflexive_left : ∀ a c, nd_seq_reflexive a;; se_expand_left c === nd_seq_reflexive (c,, a)
- ; se_reflexive_right : ∀ a c, nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c)
- ; se_cut_left : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c)
- ; se_cut_right : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c)
+ Context `(ContextND).
+
+ (*
+ * A predicate singling out initial sequents, cuts, context expansion,
+ * and structural rules.
+ *
+ * Any two proofs (with the same hypotheses and conclusions) whose
+ * non-structural rules do nothing other than expand contexts,
+ * re-arrange contexts, or introduce additional initial-sequent
+ * conclusions are indistinguishable. One important consequence
+ * is that asking for a small initial sequent and then expanding
+ * it using cnd_expand_{right,left} is no different from simply
+ * asking for the larger initial sequent in the first place.
+ *
+ *)
+ Inductive ContextND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | cnd_inert_initial : forall a, ContextND_Inert _ _ (snd_initial a)
+ | cnd_inert_cut : forall a b c, ContextND_Inert _ _ (snd_cut a b c)
+ | cnd_inert_structural : forall a b f, Structural f -> ContextND_Inert a b f
+ | cnd_inert_cnd_ant_assoc : forall x a b c, ContextND_Inert _ _ (cnd_ant_assoc x a b c)
+ | cnd_inert_cnd_ant_cossa : forall x a b c, ContextND_Inert _ _ (cnd_ant_cossa x a b c)
+ | cnd_inert_cnd_ant_cancell : forall x a , ContextND_Inert _ _ (cnd_ant_cancell x a)
+ | cnd_inert_cnd_ant_cancelr : forall x a , ContextND_Inert _ _ (cnd_ant_cancelr x a)
+ | cnd_inert_cnd_ant_llecnac : forall x a , ContextND_Inert _ _ (cnd_ant_llecnac x a)
+ | cnd_inert_cnd_ant_rlecnac : forall x a , ContextND_Inert _ _ (cnd_ant_rlecnac x a)
+ | cnd_inert_se_expand_left : forall t g s , ContextND_Inert _ _ (@cnd_expand_left _ t g s)
+ | cnd_inert_se_expand_right : forall t g s , ContextND_Inert _ _ (@cnd_expand_right _ t g s).
+
+ Class ContextND_Relation {ndr}{sndr:SequentND_Relation _ ndr} :=
+ { cndr_inert : forall {a}{b}(f g:a/⋯⋯/b),
+ NDPredicateClosure ContextND_Inert f ->
+ NDPredicateClosure ContextND_Inert g ->
+ ndr_eqv f g
+ ; cndr_sndr := sndr
}.
- End SequentsOfTrees.
+
+ End ContextND.
Close Scope nd_scope.
Open Scope pf_scope.
End Natural_Deduction.
-Coercion nd_cut : CutRule >-> Funclass.
+Coercion snd_cut : SequentND >-> Funclass.
+Coercion cnd_snd : ContextND >-> SequentND.
+Coercion sndr_ndr : SequentND_Relation >-> ND_Relation.
+Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation.
Implicit Arguments ND [ Judgment ].
Hint Constructors Structural.
Hint Extern 1 => apply nd_id_structural.
-Hint Extern 1 => apply ndr_structural_indistinguishable.
+Hint Extern 1 => apply ndr_builtfrom_structural.
+Hint Extern 1 => apply nd_structural_id0.
+Hint Extern 1 => apply nd_structural_id1.
+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 ndpc_p.
+Hint Extern 1 => apply ndpc_prod.
+Hint Extern 1 => apply ndpc_comp.
+Hint Extern 1 => apply builtfrom_refl.
+Hint Extern 1 => apply builtfrom_prod1.
+Hint Extern 1 => apply builtfrom_prod2.
+Hint Extern 1 => apply builtfrom_comp1.
+Hint Extern 1 => apply builtfrom_comp2.
+Hint Extern 1 => apply builtfrom_P.
+
+Hint Extern 1 => apply snd_inert_initial.
+Hint Extern 1 => apply snd_inert_cut.
+Hint Extern 1 => apply snd_inert_structural.
+
+Hint Extern 1 => apply cnd_inert_initial.
+Hint Extern 1 => apply cnd_inert_cut.
+Hint Extern 1 => apply cnd_inert_structural.
+Hint Extern 1 => apply cnd_inert_cnd_ant_assoc.
+Hint Extern 1 => apply cnd_inert_cnd_ant_cossa.
+Hint Extern 1 => apply cnd_inert_cnd_ant_cancell.
+Hint Extern 1 => apply cnd_inert_cnd_ant_cancelr.
+Hint Extern 1 => apply cnd_inert_cnd_ant_llecnac.
+Hint Extern 1 => apply cnd_inert_cnd_ant_rlecnac.
+Hint Extern 1 => apply cnd_inert_se_expand_left.
+Hint Extern 1 => apply cnd_inert_se_expand_right.
(* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
* of proofs. When only one kind of proof is in use, it's quite helpful though. *)
intros; apply ndr_prod_respects; auto.
Defined.
+Section ND_Relation_Facts.
+ Context `{ND_Relation}.
+
+ (* useful *)
+ Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f.
+ intros; apply (ndr_builtfrom_structural f); auto.
+ Defined.
+
+ (* useful *)
+ Lemma ndr_comp_left_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (nd_id h ;; f) f.
+ intros; apply (ndr_builtfrom_structural f); auto.
+ Defined.
+
+End ND_Relation_Facts.
+
(* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
Definition nd_replicate
: forall
with
| nd_id0 => let case_nd_id0 := tt in _
| nd_id1 h => let case_nd_id1 := tt in _
- | nd_weak h => let case_nd_weak := tt in _
+ | nd_weak1 h => let case_nd_weak := tt in _
| nd_copy h => let case_nd_copy := tt in _
| nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
| nd_comp _ _ _ top bot => let case_nd_comp := tt in _
with
| nd_id0 => let case_nd_id0 := tt in _
| nd_id1 h => let case_nd_id1 := tt in _
- | nd_weak h => let case_nd_weak := tt in _
+ | nd_weak1 h => let case_nd_weak := tt in _
| nd_copy h => let case_nd_copy := tt in _
| nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
| nd_comp _ _ _ top bot => let case_nd_comp := tt in _
rawLatexMath "% nd_id0 " +++ eolL
| nd_id1 h' => rawLatexMath indent +++
rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
- | nd_weak h' => rawLatexMath indent +++
+ | nd_weak1 h' => rawLatexMath indent +++
rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
| nd_copy h' => rawLatexMath indent +++
rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
(*********************************************************************************************************************************)
(* NaturalDeductionCategory: *)
(* *)
-(* Natural Deduction proofs form a category (under mild assumptions, see below) *)
+(* Natural Deduction proofs form a category *)
(* *)
(*********************************************************************************************************************************)
| 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_builtfrom_structural f); auto.
+ intros; apply (ndr_builtfrom_structural f); auto.
intros; apply ndr_comp_associativity.
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.
-
+ (* Judgments form a binoidal category *)
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; simpl; apply ndr_prod_respects; auto.
+ intros; unfold eqv in *; simpl in *; reflexivity.
+ intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto.
intros; unfold eqv in *; simpl in *.
setoid_rewrite <- ndr_prod_preserves_comp.
- setoid_rewrite ndr_comp_left_identity.
- reflexivity.
+ apply (ndr_builtfrom_structural (f;;g)); auto.
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; simpl; apply ndr_prod_respects; auto.
+ intros; unfold eqv in *; simpl in *; reflexivity.
+ intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto.
intros; unfold eqv in *; simpl in *.
setoid_rewrite <- ndr_prod_preserves_comp.
- setoid_rewrite ndr_comp_left_identity.
- reflexivity.
+ apply (ndr_builtfrom_structural (f;;g)); auto.
Defined.
Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) :=
{ bin_first := jud_first
; bin_second := jud_second }.
+
+ (* and that category is commutative (all morphisms central) *)
+ Instance Judgments_Category_Commutative : CommutativeCat Judgments_Category_binoidal.
+ 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.
+
+ (* Judgments form a premonoidal category *)
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_cossa |};
- abstract (simpl; auto).
+ refine {| iso_forward := nd_assoc ; iso_backward := nd_cossa |}.
+ unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
+ unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
Defined.
Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
- refine
- {| iso_forward := nd_cancelr
- ; iso_backward := nd_rlecnac |};
- abstract (simpl; auto).
+ refine {| iso_forward := nd_cancelr ; iso_backward := nd_rlecnac |};
+ unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
Defined.
Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
- refine
- {| iso_forward := nd_cancell
- ; iso_backward := nd_llecnac |};
- abstract (simpl; auto).
+ refine {| iso_forward := nd_cancell ; iso_backward := nd_llecnac |};
+ unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
Defined.
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.
+ intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
Defined.
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.
+ intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
Defined.
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.
+ intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
Defined.
Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b.
intros.
apply ni_inv.
refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}.
- intros; unfold eqv in *; simpl in *.
- apply ndr_comp_preserves_assoc.
+ intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
Defined.
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.
+ intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
Defined.
-
Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
{ pmon_cancelr := jud_mon_cancelr
; pmon_cancell := jud_mon_cancell
; pmon_assoc_ll := jud_mon_assoc_ll
}.
unfold functor_fobj; unfold fmor; simpl;
- apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
-
+ apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); 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.
-
+ apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+ intros; unfold eqv; simpl; auto; reflexivity.
+ intros; unfold eqv; simpl; auto; reflexivity.
+ intros; unfold eqv; simpl; apply Judgments_Category_Commutative.
+ intros; unfold eqv; simpl; apply Judgments_Category_Commutative.
+ intros; unfold eqv; simpl; apply Judgments_Category_Commutative.
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.
+ (* commutative premonoidal categories are monoidal *)
+ Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal :=
+ { mon_commutative := Judgments_Category_Commutative }.
- 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.
-
+ (* Judgments also happens to have a terminal object - the empty list of judgments *)
Instance Judgments_Category_Terminal : TerminalObject Judgments_Category [].
- refine {| drop := nd_weak' ; drop_unique := _ |}.
+ refine {| drop := nd_weak ; drop_unique := _ |}.
abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
Defined.
+ (* Judgments is also a diagonal category via nd_copy *)
Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
intros.
refine {| copy := nd_copy |}; intros; simpl.
reflexivity.
Defined.
+ (* Judgments is a cartesian category: it has a terminal object, diagonal morphisms, and the right naturalities *)
Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal :=
{ car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }.
-
- 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.
+ intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_left.
+ intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_right.
Defined.
End Judgments_Category.
Require Import RepresentableStructure_ch7_2.
Require Import FunctorCategories_ch7_7.
+Require Import Enrichments.
Require Import NaturalDeduction.
Require Import NaturalDeductionCategory.
Open Scope pl_scope.
Class ProgrammingLanguage :=
- { pl_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)
- ; pl_tsr :> @TreeStructuralRules Judg Rule T sequent
- ; pl_sc :> @SequentCalculus Judg Rule _ sequent
- ; pl_subst :> @CutRule Judg Rule _ sequent pl_eqv pl_sc
- ; pl_sequent_join :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst
+ { pl_eqv0 : @ND_Relation Judg Rule
+ ; pl_snd :> @SequentND Judg Rule _ sequent
+ ; pl_cnd :> @ContextND Judg Rule T sequent pl_snd
+ ; pl_eqv1 :> @SequentND_Relation Judg Rule _ sequent pl_snd pl_eqv0
+ ; pl_eqv :> @ContextND_Relation Judg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
}.
Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
unfold hom; simpl.
- apply nd_seq_reflexive.
+ apply snd_initial.
Defined.
Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
unfold hom; simpl.
- apply pl_subst.
+ apply snd_cut.
Defined.
Existing Instance pl_eqv.
+
Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
refine
{| eid := identityProof
|}; intros.
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.
- apply nd_cut_right_identity.
- unfold identityProof; unfold cutProof; simpl.
- symmetry.
- apply nd_cut_associativity.
+ 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.
- 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) |}.
+ 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 se_reflexive_right.
+ apply (cndr_inert pl_cnd); auto.
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)).
+ 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]).
- apply se_cut_right.
+ simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
Defined.
- 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)))).
+ 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.
- apply se_reflexive_left.
+ eapply cndr_inert; auto. apply pl_eqv.
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)).
+ 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]).
- apply se_cut_left.
+ simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
Defined.
- Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
+ Definition Types_binoidal : EBinoidalCat TypesL.
refine
- {| bin_first := Types_first
- ; bin_second := Types_second
+ {| 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 := nd_seq_reflexive _ ;; tsr_ant_cossa _ a b c
- ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_assoc _ a b c
+ { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c
+ ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
}.
- admit.
- admit.
- Defined.
+ 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_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.
+ 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_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
+ 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
}.
- admit.
- admit.
+ 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_cancelr : Types_first [] <~~~> functor_id _ :=
- { ni_iso := Types_cancelr_iso }.
+ 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; unfold eqv; simpl.
admit.
Defined.
- 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.
+ Instance Types_cancelr : Types_first [] <~~~> functor_id _ :=
+ { ni_iso := Types_cancelr_iso }.
+ intros; simpl.
admit.
Defined.
Defined.
Instance Types_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
- }.
- admit. (* pentagon law *)
- admit. (* triangle law *)
- intros; simpl; reflexivity.
- intros; simpl; reflexivity.
- admit. (* assoc central *)
- admit. (* cancelr central *)
- admit. (* cancell central *)
- Defined.
+ { 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.
+*)
+admit.
+admit.
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
+ admit. (* assoc central *)
+ admit. (* cancelr central *)
+ admit. (* cancell central *)
+ Defined.
- (*
Definition TypesEnrichedInJudgments : Enrichment.
- refine {| enr_c := TypesL |}.
+ refine
+ {| enr_v_mon := Judgments_Category_monoidal _
+ ; enr_c_pm := Types_PreMonoidal
+ ; enr_c_bin := Types_binoidal
+ |}.
Defined.
Structure HasProductTypes :=
{
}.
- Lemma CartesianEnrMonoidal (e:Enrichment) `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e.
+ (*
+ Lemma CartesianEnrMonoidal (e:PreMonoidalEnrichment)
+ `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e.
admit.
Defined.
+ *)
(* need to prove that if we have cartesian tuples we have cartesian contexts *)
+ (*
Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
admit.
Defined.
Require Import GeneralizedArrow.
-Section ExtendFunctor.
-
- Context `(F:Functor).
- Context (P:c1 -> Prop).
-
- Definition domain_subcat := FullSubcategory c1 P.
-
- Definition functor_restricts_to_full_subcat_on_domain_fobj (a:domain_subcat) : c2 :=
- F (projT1 a).
-
- Definition functor_restricts_to_full_subcat_on_domain_fmor (a b:domain_subcat)(f:a~~{domain_subcat}~~>b) :
- (functor_restricts_to_full_subcat_on_domain_fobj a)~~{c2}~~>(functor_restricts_to_full_subcat_on_domain_fobj b) :=
- F \ (projT1 f).
-
- Lemma functor_restricts_to_full_subcat_on_domain : Functor domain_subcat c2 functor_restricts_to_full_subcat_on_domain_fobj.
- refine {| fmor := functor_restricts_to_full_subcat_on_domain_fmor |};
- unfold functor_restricts_to_full_subcat_on_domain_fmor; simpl; intros.
- setoid_rewrite H; reflexivity.
- setoid_rewrite fmor_preserves_id; reflexivity.
- setoid_rewrite <- fmor_preserves_comp; reflexivity.
- Defined.
-
-End ExtendFunctor.
-
-Section MonoidalSubCat.
-
- (* a monoidal subcategory is a full subcategory, closed under tensor and containing the unit object *)
- Class MonoidalSubCat {Ob}{Hom}{C:Category Ob Hom}{MFobj}{MF}{MI}(MC:MonoidalCat C MFobj MF MI) :=
- { msc_P : MC -> Prop
- ; msc_closed_under_tensor : forall o1 o2, msc_P o1 -> msc_P o2 -> msc_P (MC (pair_obj o1 o2))
- ; msc_contains_unit : msc_P (mon_i MC)
- ; msc_subcat := FullSubcategory MC msc_P
- }.
- Local Coercion msc_subcat : MonoidalSubCat >-> SubCategory.
-
- Context `(MSC:MonoidalSubCat).
-
- (* any full subcategory of a monoidal category, , is itself monoidal *)
- Definition mf_restricts_to_full_subcat_on_domain_fobj (a:MSC ×× MSC) : MSC.
- destruct a.
- destruct o.
- destruct o0.
- set (MC (pair_obj x x0)) as m'.
- exists m'.
- apply msc_closed_under_tensor; auto.
- Defined.
-
- Definition mf_restricts_to_full_subcat_on_domain_fmor
- {a}{b}
- (f:a~~{MSC ×× MSC}~~>b)
- :
- (mf_restricts_to_full_subcat_on_domain_fobj a)~~{MSC}~~>(mf_restricts_to_full_subcat_on_domain_fobj b).
- destruct a as [[a1 a1pf] [a2 a2pf]].
- destruct b as [[b1 b1pf] [b2 b2pf]].
- destruct f as [[f1 f1pf] [f2 f2pf]].
- simpl in *.
- exists (MC \ (pair_mor (pair_obj a1 a2) (pair_obj b1 b2) f1 f2)); auto.
- Defined.
-
- Lemma mf_restricts_to_full_subcat_on_domain : Functor (MSC ×× MSC) MSC
- mf_restricts_to_full_subcat_on_domain_fobj.
- refine {| fmor := fun a b f => mf_restricts_to_full_subcat_on_domain_fmor f |};
- unfold functor_restricts_to_full_subcat_on_domain_fmor; simpl; intros.
- admit.
- admit.
- admit.
- Defined.
-
- Definition subcat_i : MSC.
- exists (mon_i MC).
- apply msc_contains_unit.
- Defined.
-
- Lemma full_subcat_is_monoidal : MonoidalCat MSC _ mf_restricts_to_full_subcat_on_domain subcat_i.
- admit.
- Defined.
-
- Lemma inclusion_functor_monoidal : MonoidalFunctor full_subcat_is_monoidal MC (InclusionFunctor _ MSC).
- admit.
- Defined.
-
-End MonoidalSubCat.
-Coercion full_subcat_is_monoidal : MonoidalSubCat >-> MonoidalCat.
-
-(*
Section ArrowInLanguage.
(* an Arrow In A Programming Language consists of... *)
(* a premonoidal category enriched in aforementioned full subcategory *)
Context (Kehom:center_of_TypesL -> center_of_TypesL -> @ob _ _ VK).
-Check (@ECategory).
- Context (KE:@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VK (mon_i (full_subcat_is_monoidal VK)) (full_subcat_is_monoidal VK) center_of_TypesL Kehom).
-Check (Underlying KE).
+ Context (KE:@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VK
+ (mon_i (full_subcat_is_monoidal VK)) (full_subcat_is_monoidal VK) center_of_TypesL Kehom).
Context {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}.
Defined.
Context (K_surjective:SurjectiveEnrichment K_enrichment).
*)
-Check (@FreydCategory).
Definition ArrowInProgrammingLanguage :=
@FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K.
Defined.
End GArrowInLanguage.
-*)
\ No newline at end of file
; reification_rstar_obj : enr_v K -> enr_v C
; reification_r : forall k:K, Functor K C (reification_r_obj k)
; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj
-; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
-; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f
+; reification_rstar : PreMonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
+; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f
}.
Transparent HomFunctor.
Transparent functor_comp.
-Coercion reification_rstar : Reification >-> MonoidalFunctor.
+Coercion reification_rstar : Reification >-> PreMonoidalFunctor.
Implicit Arguments Reification [ ].
Implicit Arguments reification_r_obj [ K C CI ].
Implicit Arguments reification_r [ K C CI ].
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
+Require Import PreMonoidalCategories.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
+Require Import Enrichments.
Require Import RepresentableStructure_ch7_2.
Require Import Reification.
Require Import WeakFunctorCategory.
-Require Import SmallSMMEs.
(*
* Technically reifications form merely a *semicategory* (no identity
* use it as a host language. But that's for the next paper...
*)
Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
- | roi_id : forall smme:SMMEs, ReificationOrIdentity smme smme
- | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1 s2.
+ | roi_id : forall smme:SMMEs, ReificationOrIdentity smme smme
+ | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (enr_c_i s2) -> ReificationOrIdentity s1 s2.
Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
match f with
Defined.
Definition compose_reifications (s0 s1 s2:SMMEs) :
- Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
+ Reification s0 s1 (enr_c_i s1) -> Reification s1 s2 (enr_c_i s2) -> Reification s0 s2 (enr_c_i s2).
intros.
refine
{| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
- ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
- ; reification_r := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
+ ; reification_rstar := PreMonoidalFunctorsCompose (reification_rstar X) (reification_rstar X0)
+ ; reification_r := fun K => (reification_r X K) >>>> (reification_r X0 (enr_c_i s1))
|}.
intro K.
- set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (HomFunctor s2 (mon_i s2))) as q.
+ set (ni_associativity (reification_r X K) (reification_r X0 (enr_c_i s1)) (HomFunctor s2 (enr_c_i s2))) as q.
eapply ni_comp.
apply q.
clear q.
set (reification_commutes X K) as comm1.
- set (reification_commutes X0 (mon_i s1)) as comm2.
+ set (reification_commutes X0 (enr_c_i s1)) as comm2.
set (HomFunctor s0 K) as a in *.
set (reification_rstar_f X) as a' in *.
set (reification_rstar_f X0) as x in *.
set (reification_r X K) as b in *.
- set (reification_r X0 (mon_i s1)) as c in *.
- set (HomFunctor s2 (mon_i s2)) as c' in *.
- set (HomFunctor s1 (mon_i s1)) as b' in *.
+ set (reification_r X0 (enr_c_i s1)) as c in *.
+ set (HomFunctor s2 (enr_c_i s2)) as c' in *.
+ set (HomFunctor s1 (enr_c_i s1)) as b' in *.
apply (ni_comp(F2:=b >>>> (b' >>>> x))).
- apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
- apply ni_id.
+ apply (ni_respects1 b (c >>>> c') (b' >>>> x)).
apply comm2.
eapply ni_comp.
eapply ni_inv.
eapply ni_comp.
eapply ni_inv.
apply (ni_associativity a a' x).
- apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
+ apply (ni_respects2 (a >>>> a') (b >>>> b') x).
apply ni_inv.
apply comm1.
- apply ni_id.
Defined.
Definition reificationOrIdentityComp
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
+Require Import PreMonoidalCategories.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
+Require Import Enrichments.
Require Import RepresentableStructure_ch7_2.
Require Import Reification.
Require Import GeneralizedArrow.
Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)
- : Reification K C (mon_i C).
+ : Reification K ce (enr_c_i ce).
refine
- {| reification_r := fun k:K => HomFunctor K k >>>> garrow
- ; reification_rstar_f := garrow >>>> me_mf C
- ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C)
+ {| reification_r := fun k:K => HomFunctor K k >>>> ga_functor garrow
+ ; reification_rstar_f := ga_functor garrow >>>> C
+ ; reification_rstar := PreMonoidalFunctorsCompose garrow C
|}.
abstract (intros; set (@ni_associativity) as q; apply q).
Defined.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import MonoidalCategories_ch7_8.
+Require Import PreMonoidalCategories.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
+Require Import Enrichments.
Require Import RepresentableStructure_ch7_2.
Require Import Reification.
Require Import GeneralizedArrow.
match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
end.
- Lemma roundtrip_lemma'
- `{C:Category}`{D:Category}`{E:Category}
- {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) :
- ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _).
+ Lemma roundtrip_lemma
+ `{D:Category}`{E:Category}
+ {Gobj}{G:Functor E D Gobj} G_full G_faithful `{C:Category}{Fobj}(F:Functor C (FullImage G) Fobj) :
+ (F >>>> (ff_functor_section_functor G G_full G_faithful >>>> G)) ≃ (F >>>> FullImage_InclusionFunctor _).
+ if_transitive.
+ eapply if_inv.
+ apply (if_associativity F (ff_functor_section_functor G _ _) G).
if_transitive.
apply (if_associativity F (ff_functor_section_functor G _ _) G).
apply if_respects.
apply if_id.
if_transitive; [ idtac | apply if_left_identity ].
- apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)).
+ apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> FullImage_InclusionFunctor _)).
apply if_inv.
- apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))).
+ apply (if_associativity (ff_functor_section_functor G G_full G_faithful)
+ (RestrictToImage G) (FullImage_InclusionFunctor G)).
apply if_respects.
apply ff_functor_section_splits_niso.
apply if_id.
Qed.
- Definition roundtrip_lemma
- `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
- := roundtrip_lemma' (HomFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
-
- Lemma roundtrip_reification_to_reification
- `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
- : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
+ Definition step1_niso
+ `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
+ : reification_rstar reification ≃ (RestrictToImage reification >>>> R' K CM reification >>>> FullImage_InclusionFunctor CM).
+ exists (fun c1 => homset_tensor_iso K CM reification c1).
+ intros.
simpl.
- unfold mon_f.
- unfold garrow_functor.
- apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
- apply (@step1_niso _ K _ _ C reification).
- apply (if_inv (roundtrip_lemma K C reification)).
+ etransitivity.
+ eapply comp_respects; [ apply reflexivity | idtac ].
+ apply associativity.
+ apply iso_comp1_right.
Qed.
Lemma roundtrip_garrow_to_garrow
- `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C)
- : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
- apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)).
+ `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K CM)
+ : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow).
+
apply if_inv.
- apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
- >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
- unfold mf_f.
+ eapply if_comp.
+ eapply if_inv.
unfold garrow_from_reification.
+ simpl.
+ unfold mf_F.
unfold garrow_functor.
- unfold step2_functor.
- set (@roundtrip_lemma _ K _ _ C) as q.
- apply (q (reification_from_garrow K C garrow)).
+ apply (if_associativity
+ (RestrictToImage (reification_from_garrow K CM garrow))
+ (R' K CM (reification_from_garrow K CM garrow))
+ (step2_functor C)).
+
+ apply (ffc_functor_weakly_monic _ me_full me_faithful me_conservative me_conservative).
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage (reification_from_garrow K CM garrow) >>>> R' K CM (reification_from_garrow K CM garrow))
+ (step2_functor C)
+ me_homfunctor).
+
+ set ((R' K CM (reification_from_garrow K CM garrow))) as f.
+ unfold HomFunctor_fullimage in f.
+ set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
+ set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
+
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (step2_functor C >>>> me_homfunctor)).
+ unfold step2_functor.
+ eapply if_comp.
+ apply (if_respects
+ (RestrictToImage (reification_from_garrow K CM garrow))
+ (RestrictToImage (reification_from_garrow K CM garrow))
+ _ _ (if_id _) q').
+
+ eapply if_comp.
+ eapply if_inv.
+ apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (FullImage_InclusionFunctor me_homfunctor)).
+
apply if_inv.
- apply (step1_niso K C (reification_from_garrow K C garrow)).
- Qed.
+ apply (step1_niso K C CM (reification_from_garrow K CM garrow)).
+ Qed.
+
+ Lemma roundtrip_reification_to_reification
+ `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
+ : reification ≃ reification_from_garrow K CM (garrow_from_reification K C CM reification).
+
+ simpl.
+ unfold garrow_functor.
+
+ eapply if_comp.
+ apply (step1_niso K C CM reification).
+
+ unfold garrow_monoidal.
+ unfold mf_F.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C)
+ (HomFunctor ce (pmon_I (enr_c_pm ce)))).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage reification) (R' K CM reification)
+ (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))).
+
+ apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (R' K CM reification) (step2_functor C) (HomFunctor ce _)).
+
+ set ((R' K CM reification)) as f.
+ unfold HomFunctor_fullimage in f.
+ set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
+ set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
+ apply q'.
+ Qed.
End ReificationsEquivalentToGeneralizedArrows.
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
+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 Reification.
Require Import GeneralizedArrow.
Require Import ReificationsAndGeneralizedArrows.
Require Import WeakFunctorCategory.
Require Import BijectionLemma.
+Require Import Enrichments.
Section ReificationsIsomorphicToGeneralizedArrows.
- Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
+ Definition M1 {c1 c2 : SMMEs} :
(c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
(c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
intro GA.
destruct GA; [ apply roi_id | idtac ].
apply roi_reif.
- apply reification_from_garrow.
- apply g.
+ apply (reification_from_garrow s1 s2 g).
Defined.
(* I tried really hard to avoid this *)
apply if_id.
destruct g; simpl.
apply if_id.
- unfold mf_f; simpl.
+ simpl.
apply (if_associativity
- ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
+ ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))).
Defined.
- Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
+ Definition M2 (c1 c2 : SMMEs) :
(c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
(c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
intro RE.
destruct RE; [ apply gaoi_id | idtac ].
apply gaoi_ga.
- apply (garrow_from_reification s1 s2 r).
+ apply (garrow_from_reification s1 (smme_mee s2) s2 r).
Defined.
Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
(H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
unfold hom in *.
- set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
+ set (@roundtrip_garrow_to_garrow a b (smme_mee b) (smme_mon b)) as q.
destruct f; simpl in *.
apply H.
apply if_inv.
apply (if_comp (if_inv H)).
clear H.
- unfold mf_f in q.
- apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
- (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
+ apply (if_respects
+ (ga_functor g)
+ (garrow_functor s1 (smme_mee s2) s2 (reification_from_garrow s1 s2 g))
+ (HomFunctor (senr_c s2) (senr_c_i s2))
+ (HomFunctor (senr_c s2) (senr_c_i s2))
+ ).
apply q.
apply if_id.
- Qed.
-
+ Qed.
Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
(f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
(H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
unfold hom in *.
- set (@roundtrip_reification_to_reification _ a _ _ b) as q.
+ set (@roundtrip_reification_to_reification a b (smme_mee b) (smme_mon b)) as q.
destruct f; simpl.
apply H.
apply if_inv.
apply (if_comp (if_inv H)).
clear H.
simpl.
- unfold mf_f; simpl.
simpl in q.
- unfold mf_f in q.
simpl in q.
apply q.
- Qed.
+ Qed.
Lemma M2_respects :
forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
unfold eqv in *.
simpl in *.
destruct f.
- set (invert_reif _ f') as q.
- destruct q; subst.
- apply if_id.
- simpl in *.
- destruct H0; subst.
- simpl in *.
- unfold garrow_functor.
- unfold step2_functor.
- apply (if_comp H).
- clear H.
- apply (if_comp (@step1_niso _ smme _ _ smme x)).
- apply if_inv.
- apply (@roundtrip_lemma _ smme _ _ smme x).
+ set (invert_reif _ f') as q.
+ destruct q; subst.
+ apply if_id.
+
+ simpl in *.
+ destruct H0; subst.
+ simpl in *.
+ unfold garrow_functor.
+ unfold step2_functor.
+ apply (if_comp H).
+ clear H.
+ eapply if_comp.
+ apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
+ apply if_inv.
+ set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+ ff_functor_section_functor me_homfunctor me_full me_faithful))
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ apply (if_respects (RestrictToImage x) (RestrictToImage x)).
+ apply (if_id (RestrictToImage x)).
+ unfold mf_F.
+ unfold me_homfunctor in q.
+ unfold pmon_I.
+ apply q.
+
simpl in *.
destruct f'; simpl in *.
- apply if_inv.
+ simpl in *.
apply if_inv in H.
- apply (if_comp H).
+ eapply if_comp; [ idtac | eapply if_inv; apply H ].
clear H.
unfold garrow_functor.
unfold step2_functor.
- apply (if_comp (@step1_niso _ smme _ _ smme r)).
apply if_inv.
- apply (@roundtrip_lemma _ smme _ _ smme r).
+ eapply if_comp.
+ apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
+
+ rename r into x.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+ ff_functor_section_functor me_homfunctor me_full me_faithful))
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
+ apply (if_respects (RestrictToImage x) (RestrictToImage x)).
+ apply (if_id (RestrictToImage x)).
+
+ unfold mf_F.
+ set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
+ apply if_inv.
+ unfold me_homfunctor in q.
+ unfold pmon_I.
+ apply q.
+
simpl in *.
unfold garrow_functor.
unfold step2_functor.
- apply if_inv in H.
- apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
+ set (step1_niso s1 (smme_mee s2) s2 r) as q.
+ apply if_inv in q.
+ eapply if_comp.
+ eapply if_comp; [ idtac | apply q ].
+
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage r)
+ (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c s2) (senr_c_i s2))).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage r)
+ (R' s1 s2 r)
+ (FullImage_InclusionFunctor _)).
+ apply (if_respects
+ (RestrictToImage r)
+ (RestrictToImage r)
+ (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
+ (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
+ HomFunctor (senr_c s2) (senr_c_i s2)))).
+ apply (if_id _).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity
+ (R' s1 s2 r)
+ (ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c s2) (senr_c_i s2))).
+ apply if_inv.
+ apply (if_respects
+ (R' s1 s2 r)
+ (R' s1 s2 r)
+ (FullImage_InclusionFunctor _)
+ ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _))
+ ).
+ apply (if_id _).
apply if_inv.
- apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
- apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
+ apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))).
Qed.
Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
+++ /dev/null
-(*********************************************************************************************************************************)
-(* SmallSMMEs: *)
-(* *)
-(* The collection of SMMEs is a collection of small categories (see SmallCategories) *)
-(* *)
-(*********************************************************************************************************************************)
-
-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 Enrichment_ch2_8.
-Require Import RepresentableStructure_ch7_2.
-Require Import GeneralizedArrow.
-Require Import WeakFunctorCategory.
-
-
-Definition SMMEs : SmallCategories.
- refine {| small_cat := SMME
- ; small_cat_cat := fun smme => enr_v smme
- |}.
- Defined.
-Subproject commit e928451c4c45cdbdd975bbfb229e8cc2616b8194
+Subproject commit 1104780d775bf36ff9f44ab287c22604ab47f0b5