update to new coq-categories, base ND_Relation on inert sequences

diff --git a/src/Enrichments.v b/src/Enrichments.v
index f78415d..a98b047 100644 (file)
--- a/src/Enrichments.v
+++ b/src/Enrichments.v
@@ -20,78 +20,117 @@ Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import BinoidalCategories.
 Require Import PreMonoidalCategories.
 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.
 
 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 :=
 (* 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_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_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.

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index bf7743b..9149734 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -20,14 +20,22 @@ Require Import NaturalIsomorphisms_ch7_5.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 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 RepresentableStructure_ch7_2.

+Require Import PreMonoidalCenter.
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.

 
 Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
 
 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 ].
 
 Implicit Arguments GeneralizedArrow    [ [ce] ].
 Implicit Arguments ga_functor_obj      [ K ce C ].

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index 28b7555..3a6a74a 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -23,10 +23,10 @@ Require Import PreMonoidalCategories.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 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 RepresentableStructure_ch7_2.
 Require Import GeneralizedArrow.
 Require Import WeakFunctorCategory.

-Require Import SmallSMMEs.

 
 (*
  * Technically reifications form merely a *semicategory* (no identity
 
 (*
  * Technically reifications form merely a *semicategory* (no identity

@@ -49,28 +49,19 @@ Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
 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
 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 _
   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.
 
   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.
 
 Definition generalizedArrowOrIdentityComp
   : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.

@@ -97,7 +88,6 @@ Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
     apply if_right_identity.
   unfold mf_F.
   idtac.
     apply if_right_identity.
   unfold mf_F.
   idtac.

-  unfold mf_f.

   apply if_associativity.
   Defined.
 
   apply if_associativity.
   Defined.
 

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 15d1b09..810e862 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -19,146 +19,536 @@ Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import BinoidalCategories.
 Require Import PreMonoidalCategories.
 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 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.
 
 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
     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
     | 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.
 
     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 *)
    * 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 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;
       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;
       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.
 
       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.
 
     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.
     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.
 
     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.
 
 End GArrowFromReification.

-Opaque homset_tensor_iso.
+

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
index d0d8b84..82bc678 100644 (file)
--- a/src/HaskProofFlattener.v
+++ b/src/HaskProofFlattener.v
@@ -136,7 +136,7 @@ Section HaskProofFlattener.
   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
       (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
   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.
 
 
     set (@nil (HaskTyVar Γ ★)) as lev.
 

@@ -162,7 +162,7 @@ Section HaskProofFlattener.
     (* 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 ].
     (* 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.
         (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
       eapply nd_comp.
       eapply nd_prod.

@@ -184,42 +184,45 @@ Section HaskProofFlattener.
     eapply nd_comp.
       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
       clear IHX1 IHX2 X1 X2.
     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 _))) ].
 
     (* 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 _))) ].
       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 _))) ].
       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 _))) ].
       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 _ _ _))) ].
       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 _ _ _))) ].
       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].
       auto.
 
       destruct r as [r rp].

@@ -342,7 +345,7 @@ Section HaskProofFlattener.
 
       Defined.
 
 
       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.
     { fmor := FlatteningFunctor_fmor }.
     admit.
     admit.

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
index d6058e5..1f7d85d 100644 (file)
--- a/src/HaskProofStratified.v
+++ b/src/HaskProofStratified.v
@@ -198,8 +198,6 @@ Section HaskProofStratified.
       admit.
       admit.
       admit.
       admit.
       admit.
       admit.

-      admit.
-      admit.

       Defined.
 
   (*
       Defined.
 
   (*

@@ -347,31 +345,10 @@ Section HaskProofStratified.
       admit.
       admit.
       admit.
       admit.
       admit.
       admit.

-      admit.
-      admit.

       Defined.
 
   Hint Constructors Rule_Flat.
 
       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.
   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
     admit.
     Defined.

@@ -407,16 +384,30 @@ Section HaskProofStratified.
     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 ] ].
 
   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 _ _ _).
     apply nd_rule.
     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
     refine (existT _ _ _).

@@ -425,29 +416,38 @@ Section HaskProofStratified.
 
   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 ] ].
 
   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.
 
     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.
     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) :=
     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.
     apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 
     apply nd_rule. unfold PCFRule. simpl.

@@ -474,26 +474,7 @@ Section HaskProofStratified.
       exists (RArrange _ _ _ _ _ (RuCanR _)).
       apply (PCF_RArrange lev _ (a,,[]) _).
       Defined.
       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.
 
   Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
     intros.

@@ -524,16 +505,31 @@ Section HaskProofStratified.
     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
     Defined.
 
     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 ] ].
 
   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.
     apply nd_rule.
     apply org_fc with (r:=RJoin Γ Δ a b a c).
     auto.

@@ -541,12 +537,13 @@ Section HaskProofStratified.
 
   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 ] ].
 
   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.
 
     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 Γ Δ }.
   Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
   { se_expand_left  := SystemFCa_left  Γ Δ 
   ; se_expand_right := SystemFCa_right Γ Δ }.

@@ -555,11 +552,12 @@ Section HaskProofStratified.
     admit.
     admit.
     Defined.
     admit.
     admit.
     Defined.

-
+*)

   (* 5.1.2 *)
   (* 5.1.2 *)

-  Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR :=
+  Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR.
+(*

   { pl_eqv                := OrgNDR
   { pl_eqv                := OrgNDR

-  ; pl_sc                 := SystemFCa_sequents     Γ Δ
+  ; pl_sn                 := SystemFCa_sequents     Γ Δ

   ; pl_subst              := SystemFCa_cutrule      Γ Δ
   ; pl_sequent_join       := SystemFCa_sequent_join Γ Δ
   }.
   ; pl_subst              := SystemFCa_cutrule      Γ Δ
   ; pl_sequent_join       := SystemFCa_sequent_join Γ Δ
   }.

@@ -570,6 +568,8 @@ Section HaskProofStratified.
     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.
     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.
     Defined.
 
 End HaskProofStratified.

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index d38286d..06f97a1 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -577,7 +577,7 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
     apply FreshMon.
     destruct pf as [ vnew [ pf1 pf2 ]].
     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 (X_ ξ' (vars,,[vnew]) _ >>>= _).
     apply FreshMon.
     simpl.

@@ -642,7 +642,7 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
     apply FreshMon.
     destruct pf as [ vnew [ pf1 pf2 ]].
     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.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 74ecaef..3a06d66 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -137,7 +137,7 @@ Section Natural_Deduction.
     | nd_id1    : forall  h,  [ h ] /⋯⋯/ [ h ]
   
     (* natural deduction: you may discard conclusions *)
     | 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)
   
     (* natural deduction: you may duplicate conclusions *)
     | nd_copy   : forall  h,    h   /⋯⋯/ (h,,h)

@@ -176,14 +176,13 @@ Section Natural_Deduction.
     Open Scope nd_scope.
     Open Scope pf_scope.
 
     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)
   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_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)

@@ -192,6 +191,26 @@ Section Natural_Deduction.
   | nd_structural_cossa   : forall {a b c},                                                            Structural (@nd_cossa a b c)
   .
 
   | 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
   (* 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

@@ -200,30 +219,35 @@ Section Natural_Deduction.
       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
     end.
 
       | 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
     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.
     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.
 
     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 :=
   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
    * structural variations  *)
   Class ND_Relation :=

@@ -233,31 +257,31 @@ Section Natural_Deduction.
   (* 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)
   (* 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
 
   (* 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 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 _

   }.
 
   (* 
   }.
 
   (* 

@@ -349,74 +373,161 @@ Section Natural_Deduction.
   end.
 
   (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
   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" := (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).
     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.
 
 
   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.
 
 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. *)
 
 (* 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. *)

@@ -446,6 +557,21 @@ Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
     intros; apply ndr_prod_respects; auto.
     Defined.
 
     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
 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
 Definition nd_replicate
   : forall

@@ -482,7 +608,7 @@ Definition nd_map
         with
         | nd_id0                     => let case_nd_id0     := tt in _
         | nd_id1     h               => let case_nd_id1     := 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 _
         | 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 _

@@ -530,7 +656,7 @@ Definition nd_map'
         with
         | nd_id0                     => let case_nd_id0     := tt in _
         | nd_id1     h               => let case_nd_id1     := 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 _
         | 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 _

@@ -633,7 +759,7 @@ Section ToLatex.
                                        rawLatexMath "% nd_id0 " +++ eolL
       | nd_id1  h'                  => rawLatexMath indent +++
                                        rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
                                        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+++
                                        rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
       | nd_copy h'                  => rawLatexMath indent +++
                                        rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index fd352e1..7ac59b3 100644 (file)
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -1,7 +1,7 @@
 (*********************************************************************************************************************************)
 (* NaturalDeductionCategory:                                                                                                     *)
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 (* NaturalDeductionCategory:                                                                                                     *)
 (*                                                                                                                               *)

-(*   Natural Deduction proofs form a category (under mild assumptions, see below)                                                *)
+(*   Natural Deduction proofs form a category                                                                                    *)

 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 

@@ -48,96 +48,86 @@ Section Judgments_Category.
     | unfold Symmetric; intros; symmetry; auto
     | unfold Transitive; intros; transitivity y; auto ].
   unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
     | 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.
 
   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) }.
   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.
     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 }.
     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.
     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 }.
     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)).
   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.
     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.
     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 }.
     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 }.
     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 }.
     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 _ _ _) |}.
     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 _ _ _ }.
     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.
     Defined.

-

   Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
   { pmon_cancelr  := jud_mon_cancelr
   ; pmon_cancell  := jud_mon_cancell
   Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
   { pmon_cancelr  := jud_mon_cancelr
   ; pmon_cancell  := jud_mon_cancell

@@ -146,97 +136,27 @@ Section Judgments_Category.
   ; pmon_assoc_ll := jud_mon_assoc_ll
   }.
     unfold functor_fobj; unfold fmor; simpl;
   ; 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;
     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.
 
       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 [].
   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.
 
       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.
   Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
     intros.
     refine {| copy := nd_copy |}; intros; simpl.

@@ -260,13 +180,11 @@ Section Judgments_Category.
       reflexivity.
       Defined.
 
       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 }.
   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.
     Defined.
 
 End Judgments_Category.

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index 7831fad..933785a 100644 (file)
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -26,6 +26,7 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import FunctorCategories_ch7_7.
 
 Require Import RepresentableStructure_ch7_2.
 Require Import FunctorCategories_ch7_7.
 

+Require Import Enrichments.

 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 

@@ -46,11 +47,11 @@ Section Programming_Language.
   Open Scope pl_scope.
 
   Class ProgrammingLanguage :=
   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.
 
   }.
   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
 

@@ -65,15 +66,16 @@ Section Programming_Language.
 
     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
       unfold hom; simpl.
 
     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.
       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.
       Defined.
 
     Existing Instance pl_eqv.

+

     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
       refine
       {| eid   := identityProof
     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
       refine
       {| eid   := identityProof

@@ -81,80 +83,101 @@ Section Programming_Language.
       |}; intros.
       apply (mon_commutative(MonoidalCat:=JudgmentsL)).
       apply (mon_commutative(MonoidalCat:=JudgmentsL)).
       |}; 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.
 
       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.
       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.
       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]).
       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.
 
       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.
       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.
       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]).
       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.
 
       Defined.
 

-    Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
+    Definition Types_binoidal : EBinoidalCat TypesL.

       refine
       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)) :=
          |}.
       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.
 
       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.
 
       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.
 
       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.
 
       admit.
       Defined.
 

@@ -174,35 +197,81 @@ Section Programming_Language.
       Defined.
 
     Instance Types_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
       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.
     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 :=
     {
     }.
 
       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.
       admit.
       Defined.

+      *)

 
     (* need to prove that if we have cartesian tuples we have cartesian contexts *)
 
     (* need to prove that if we have cartesian tuples we have cartesian contexts *)

+    (*

     Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
       admit.
       Defined.
     Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
       admit.
       Defined.

diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v
index a4f40e3..b613455 100644 (file)
--- a/src/ProgrammingLanguageArrow.v
+++ b/src/ProgrammingLanguageArrow.v
@@ -33,91 +33,6 @@ Require Import FreydCategories.
 
 Require Import GeneralizedArrow.
 
 
 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... *)
 Section ArrowInLanguage.
 
   (* an Arrow In A Programming Language consists of... *)

@@ -133,10 +48,9 @@ Section ArrowInLanguage.
 
   (* a premonoidal category enriched in aforementioned full subcategory *)
   Context (Kehom:center_of_TypesL -> center_of_TypesL -> @ob _ _ VK).
 
   (* 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}.
 
 
   Context {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}.
 

@@ -153,7 +67,6 @@ Check (Underlying KE).
     Defined.
   Context (K_surjective:SurjectiveEnrichment K_enrichment).
     *)
     Defined.
   Context (K_surjective:SurjectiveEnrichment K_enrichment).
     *)

-Check (@FreydCategory).

 
   Definition ArrowInProgrammingLanguage :=
     @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K.
 
   Definition ArrowInProgrammingLanguage :=
     @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K.

@@ -163,4 +76,3 @@ Check (@FreydCategory).
     Defined.
 
 End GArrowInLanguage.
     Defined.
 
 End GArrowInLanguage.

-*)
\ No newline at end of file

diff --git a/src/Reification.v b/src/Reification.v
index 2b9aac9..932d78e 100644 (file)
--- a/src/Reification.v
+++ b/src/Reification.v
@@ -33,13 +33,13 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
 ; 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_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.
 
 }.
 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 ].
 Implicit Arguments Reification                [ ].
 Implicit Arguments reification_r_obj          [ K C CI ].
 Implicit Arguments reification_r              [ K C CI ].

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index e57df4d..9a7c3fd 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -18,13 +18,14 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 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 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 RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import WeakFunctorCategory.

-Require Import SmallSMMEs.

 
 (*
  * Technically reifications form merely a *semicategory* (no identity
 
 (*
  * Technically reifications form merely a *semicategory* (no identity

@@ -43,8 +44,8 @@ Require Import SmallSMMEs.
  * use it as a host language.  But that's for the next paper...
  *)
 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
  * 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
 
 Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
   match f with

@@ -62,30 +63,29 @@ Definition reificationOrIdentityFunc
   Defined.
 
 Definition compose_reifications (s0 s1 s2:SMMEs) :
   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
   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.
     |}.
   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.
   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 (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_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.
   apply comm2.
   eapply ni_comp.
   eapply ni_inv.

@@ -94,10 +94,9 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   eapply ni_comp.
   eapply ni_inv.
   apply (ni_associativity a a' x).
   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_inv.
   apply comm1.

-  apply ni_id.

   Defined.
 
 Definition reificationOrIdentityComp
   Defined.
 
 Definition reificationOrIdentityComp

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index a53b2e2..2a9937f 100644 (file)
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -17,19 +17,21 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 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 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)
 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
   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.
    |}.
    abstract (intros; set (@ni_associativity) as q; apply q).
    Defined.

diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v
index 6a615ac..4056c77 100644 (file)
--- a/src/ReificationsAndGeneralizedArrows.v
+++ b/src/ReificationsAndGeneralizedArrows.v
@@ -19,8 +19,10 @@ Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import MonoidalCategories_ch7_8.
 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 Coherence_ch7_8.
 Require Import Enrichment_ch2_8.

+Require Import Enrichments.

 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.

@@ -35,53 +37,115 @@ Section ReificationsEquivalentToGeneralizedArrows.
     match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
     end.
 
     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 ].
     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_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.
 
     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.
     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
     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_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.
     unfold garrow_from_reification.

+    simpl.
+    unfold mf_F.

     unfold garrow_functor.
     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 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.
 
 End ReificationsEquivalentToGeneralizedArrows.

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 8edd1e0..1230454 100644 (file)
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -17,9 +17,9 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 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 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 RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.

@@ -31,17 +31,17 @@ Require Import ReificationCategory.
 Require Import ReificationsAndGeneralizedArrows.
 Require Import WeakFunctorCategory.
 Require Import BijectionLemma.
 Require Import ReificationsAndGeneralizedArrows.
 Require Import WeakFunctorCategory.
 Require Import BijectionLemma.

+Require Import Enrichments.

 
 Section ReificationsIsomorphicToGeneralizedArrows.
 
 
 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.
       (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 *)
       Defined.
 
     (* I tried really hard to avoid this *)

@@ -137,18 +137,18 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         apply if_id.
         destruct g; simpl.
         apply if_id.
         apply if_id.
         destruct g; simpl.
         apply if_id.

-        unfold mf_f; simpl.
+        simpl.

         apply (if_associativity 
         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.
 
         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.
       (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)
       Defined.
 
     Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)

@@ -156,38 +156,38 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
       generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
         unfold hom in *.
       (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.
         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.
         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 *.
 
     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.
         destruct f; simpl.
         apply H.
         apply if_inv.
         apply (if_comp (if_inv H)).
         clear H.
         simpl.

-        unfold mf_f; simpl.

         simpl in q.
         simpl in q.

-        unfold mf_f in q.

         simpl in q.
         apply q.
         simpl in q.
         apply q.

-      Qed.
+        Qed.

 
     Lemma M2_respects :
       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
 
     Lemma M2_respects :
       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),

@@ -198,38 +198,109 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         unfold eqv in *.
         simpl in *.
         destruct f.
         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 *.
       simpl in *.
         destruct f'; simpl in *.

-        apply if_inv.
+        simpl in *.

         apply if_inv in H.
         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.
         clear H.
         unfold garrow_functor.
         unfold step2_functor.

-        apply (if_comp (@step1_niso _ smme _ _ smme r)).

         apply if_inv.
         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.
       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_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).
         Qed.
 
     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).

diff --git a/src/SmallSMMEs.v b/src/SmallSMMEs.v
deleted file mode 100644 (file)
index 828612f..0000000
--- a/src/SmallSMMEs.v
+++ /dev/null
@@ -1,32 +0,0 @@
-(*********************************************************************************************************************************)
-(* 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.

diff --git a/src/categories b/src/categories
index e928451..1104780 160000 (submodule)
--- a/src/categories
+++ b/src/categories
@@ -1 +1 @@
-Subproject commit e928451c4c45cdbdd975bbfb229e8cc2616b8194
+Subproject commit 1104780d775bf36ff9f44ab287c22604ab47f0b5