re-arrange NaturalDeduction

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2b65a18..61993a1 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -34,12 +34,13 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 

+Require Import ProgrammingLanguage.
+

 Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
 Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.

-Require Import ReificationsEquivalentToGeneralizedArrows.
-Require Import ProgrammingLanguage.

 *)
 *)

+Require Import ReificationsEquivalentToGeneralizedArrows.

 
 Open Scope string_scope.
 Extraction Language Haskell.
 
 Open Scope string_scope.
 Extraction Language Haskell.

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index f246567..bf7743b 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -22,14 +22,14 @@ Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 

-Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) :=
+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
 }.
 Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
 
 { 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
 }.
 Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
 

-Implicit Arguments GeneralizedArrow    [ ].
-Implicit Arguments ga_functor_obj      [ K C ].
-Implicit Arguments ga_functor          [ K C ].
-Implicit Arguments ga_functor_monoidal [ K C ].
+Implicit Arguments GeneralizedArrow    [ [ce] ].
+Implicit Arguments ga_functor_obj      [ K ce C ].
+Implicit Arguments ga_functor          [ K ce C ].
+Implicit Arguments ga_functor_monoidal [ K ce C ].

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index cd43282..d98f85a 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -9,6 +9,21 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.

-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+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.
+
+Instance CategoryOfGeneralizedArrows : Category SMME GeneralizedArrow.
+  admit.
+  Qed.

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 6aeaace..e6d3cbd 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -26,7 +26,7 @@ Require Import GeneralizedArrow.
 
 Section GArrowFromReification.
 
 
 Section GArrowFromReification.
 

-  Context  (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)).
+  Context  `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)).

 
   Fixpoint garrow_fobj_ vk : C :=
     match vk with
 
   Fixpoint garrow_fobj_ vk : C :=
     match vk with

@@ -35,13 +35,13 @@ Section GArrowFromReification.
     | t1,,t2          => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2))
     end.
 
     | t1,,t2          => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2))
     end.
 

-  Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp K vk)).
+  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.
 
   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.
+    set (se_decomp _ K  vk) as sevk.

     destruct sevk.
     simpl in *.
     rewrite e.
     destruct sevk.
     simpl in *.
     rewrite e.

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 855b66a..06b6efe 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -333,11 +333,56 @@ Section Natural_Deduction.
   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
   end.
 
   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
   end.
 

+  Section Sequents.
+    Context {S:Type}.   (* type of sequent components *)
+    Context (sequent:S->S->Judgment).
+    Context (ndr:ND_Relation).
+    Notation "a |= b" := (sequent a b).
+    Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
+
+    Class SequentCalculus :=
+    { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
+    }.
+    
+    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_cut a b c ** nd_id1 (c|=d)) ;; (nd_cut a c d) === nd_assoc ;; (nd_id1 (a|=b) ** nd_cut b c d) ;; nd_cut a b d
+    }.
+
+  End Sequents.
+
+  Section SequentsOfTrees.
+    Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}(sc:SequentCalculus sequent).
+    Context (ndr:ND_Relation).
+    Notation "a |= b" := (sequent a b).
+    Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
+
+    Class TreeStructuralRules :=
+    { tsr_ant_assoc     : forall {x a b c}, Rule [((a,,b),,c) |= x]     [(a,,(b,,c)) |= x]
+    ; tsr_ant_cossa     : forall {x a b c}, Rule [(a,,(b,,c)) |= x]     [((a,,b),,c) |= x]
+    ; tsr_ant_cancell   : forall {x a    }, Rule [  [],,a     |= x]     [        a   |= x]
+    ; tsr_ant_cancelr   : forall {x a    }, Rule [a,,[]       |= x]     [        a   |= x]
+    ; tsr_ant_llecnac   : forall {x a    }, Rule [      a     |= x]     [    [],,a   |= x]
+    ; tsr_ant_rlecnac   : forall {x a    }, Rule [      a     |= x]     [    a,,[]   |= x]
+    }.
+
+    Class SequentExpansion :=
+    { se_expand_left            : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
+    ; se_expand_right           : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
+    }.
+  End SequentsOfTrees.
+

   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.
+

 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.

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 5e3432b..b64ac4b 100644 (file)
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -201,41 +201,6 @@ Section Judgments_Category.
     apply nd_structural_cancelr; auto.
     Defined.
 
     apply nd_structural_cancelr; auto.
     Defined.
 

-  (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment,
-   * this asserts that we have sensible structural rules with respect
-   * to that mapping.  Doing all of this "with respect to a mapping"
-   * lets us avoid duplicating code for both the antecedent and
-   * succedent of sequent deductions. *)
-  Class TreeStructuralRules  {T:Type}(rep:Tree ??T -> Judgment) :=
-  { tsr_eqv           : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2)
-  ; tsr_ant_assoc     : forall {a b c}, Rule [rep ((a,,b),,c)]     [rep ((a,,(b,,c)))]
-  ; tsr_ant_cossa     : forall {a b c}, Rule [rep (a,,(b,,c))]     [rep (((a,,b),,c))]
-  ; tsr_ant_cancell   : forall {a    }, Rule [rep (  [],,a  )]     [rep (        a  )]
-  ; tsr_ant_cancelr   : forall {a    }, Rule [rep (a,,[]    )]     [rep (        a  )]
-  ; tsr_ant_llecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  [],,a    )]
-  ; tsr_ant_rlecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  a,,[]    )]
-  }.
-
-  Section Sequents.
-    Context {S:Type}.   (* type of sequent components *)
-    Context (sequent:S->S->Judgment).
-    Notation "a |= b" := (sequent a b).
-
-    Class SequentCalculus :=
-    { nd_seq_reflexive : forall a, ND Rule [ ] [ a |= a ]
-    }.
-    
-    Class CutRule :=
-    { nd_cutrule_seq       :> SequentCalculus
-    ; nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
-    ; nd_cut_associativity :  forall {a b c d},
-      ((nd_cut a b c) ** (nd_id1 (c|=d))) ;; (nd_cut a c d)
-        ===
-        nd_assoc ;; ((nd_id1 (a|=b)) ** (nd_cut b c d) ;; (nd_cut a b d))
-    ; 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
-    }.
-  End Sequents.

 
   (* Structure ExpressionAlgebra (sig:Signature) := *)
 
 
   (* Structure ExpressionAlgebra (sig:Signature) := *)
 

diff --git a/src/Preamble.v b/src/Preamble.v
index f83d9a1..453027a 100644 (file)
--- a/src/Preamble.v
+++ b/src/Preamble.v
@@ -16,8 +16,11 @@ Export Coq.Setoids.Setoid.
 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
 Generalizable All Variables.
 
 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
 Generalizable All Variables.
 

+Reserved Notation "a ** b"                      (at level 40).
+Reserved Notation "a ;; b"                      (at level 45).
+

 Reserved Notation "a -~- b"                     (at level 10).
 Reserved Notation "a -~- b"                     (at level 10).

-Reserved Notation "a ** b"                      (at level 10).
+Reserved Notation "pf1 === pf2"                 (at level 80).

 Reserved Notation "?? x"                        (at level 1).
 Reserved Notation "a ,, b"                      (at level 50).
 Reserved Notation "!! f"                        (at level 3).
 Reserved Notation "?? x"                        (at level 1).
 Reserved Notation "a ,, b"                      (at level 50).
 Reserved Notation "!! f"                        (at level 3).

@@ -52,7 +55,6 @@ Reserved Notation "A ⋊ f"                       (at level 40).
 Reserved Notation "- ⋉ A"                       (at level 40).
 Reserved Notation "A ⋊ -"                       (at level 40).
 Reserved Notation "a *** b"                     (at level 40).
 Reserved Notation "- ⋉ A"                       (at level 40).
 Reserved Notation "A ⋊ -"                       (at level 40).
 Reserved Notation "a *** b"                     (at level 40).

-Reserved Notation "a ;; b"                      (at level 45).

 Reserved Notation "[# f #]"                     (at level 2).
 Reserved Notation "a ---> b"                    (at level 11, right associativity).
 Reserved Notation "a <- b"                      (at level 100, only parsing).
 Reserved Notation "[# f #]"                     (at level 2).
 Reserved Notation "a ---> b"                    (at level 11, right associativity).
 Reserved Notation "a <- b"                      (at level 100, only parsing).

@@ -69,7 +71,6 @@ Reserved Notation "f ○ g"                       (at level 100).
 Reserved Notation "a ==[ n ]==> b"              (at level 20).
 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
 Reserved Notation "H /⋯⋯/ C"                    (at level 70).
 Reserved Notation "a ==[ n ]==> b"              (at level 20).
 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
 Reserved Notation "H /⋯⋯/ C"                    (at level 70).

-Reserved Notation "pf1 === pf2"                 (at level 80).

 Reserved Notation "a |== b @@ c"                (at level 100).
 Reserved Notation "f >>>> g"                    (at level 45).
 Reserved Notation "a >>[ n ]<< b"               (at level 100).
 Reserved Notation "a |== b @@ c"                (at level 100).
 Reserved Notation "f >>>> g"                    (at level 45).
 Reserved Notation "a >>[ n ]<< b"               (at level 100).

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index b00d1ad..7630440 100644 (file)
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -9,6 +9,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Categories_ch1_3.
 Require Import Preamble.
 Require Import General.
 Require Import Categories_ch1_3.

+Require Import InitialTerminal_ch2_2.

 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import ProductCategories_ch1_6_1.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import ProductCategories_ch1_6_1.

@@ -21,15 +22,17 @@ Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.

+Require Import FunctorCategories_ch7_7.
+

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

-Require Import Reification.
+

 Require Import FreydCategories.
 Require Import FreydCategories.

-Require Import InitialTerminal_ch2_2.
-Require Import FunctorCategories_ch7_7.
-Require Import GeneralizedArrowFromReification.
-Require Import GeneralizedArrow.

 
 

+Require Import Reification.
+Require Import GeneralizedArrow.
+Require Import GeneralizedArrowFromReification.
+Require Import ReificationFromGeneralizedArrow.

 
 (*
  *  Everything in the rest of this section is just groundwork meant to
 
 (*
  *  Everything in the rest of this section is just groundwork meant to

@@ -42,7 +45,6 @@ Require Import GeneralizedArrow.
  *)   
 Section Programming_Language.
 
  *)   
 Section Programming_Language.
 

-  (* Formalized Definition 4.1.1, production $\tau$ *)

   Context {T    : Type}.               (* types of the language *)
 
   Context (Judg : Type).
   Context {T    : Type}.               (* types of the language *)
 
   Context (Judg : Type).

@@ -63,7 +65,7 @@ Section Programming_Language.
   Open Scope nd_scope.
   Open Scope al_scope.
 
   Open Scope nd_scope.
   Open Scope al_scope.
 

-  (* Formalized Definition 4.1
+  (*

    *
    * Note that from this abstract interface, the terms (expressions)
    * in the proof are not accessible at all; they don't need to be --
    *
    * Note that from this abstract interface, the terms (expressions)
    * in the proof are not accessible at all; they don't need to be --

@@ -82,145 +84,21 @@ Section Programming_Language.
    * This also means that we don't need an explicit proof obligation for 4.1.2.
    *)
   Class ProgrammingLanguage :=
    * This also means that we don't need an explicit proof obligation for 4.1.2.
    *)
   Class ProgrammingLanguage :=

-
-  (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
-  { al_eqv                   : @ND_Relation Judg Rule
-                                     where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
-
-  (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
-   * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
-   * to generate the rest *)
-  ; al_reflexive_seq         : forall t, Rule [] [t|=t]
-
-  (* these can all be absorbed into a separate "sequent calculus" presentation *)
-  ; al_ant_assoc     : forall {a b c d}, Rule [(a,,b),,c|=d]     [(a,,(b,,c))|=d]
-  ; al_ant_cossa     : forall {a b c d}, Rule [a,,(b,,c)|=d]     [((a,,b),,c)|=d]
-  ; al_ant_cancell   : forall {a b    }, Rule [  [],,a  |=b]     [        a  |=b]
-  ; al_ant_cancelr   : forall {a b    }, Rule [a,,[]    |=b]     [        a  |=b]
-  ; al_ant_llecnac   : forall {a b    }, Rule [      a  |=b]     [  [],,a    |=b]
-  ; al_ant_rlecnac   : forall {a b    }, Rule [      a  |=b]     [  a,,[]    |=b]
-  ; al_suc_assoc     : forall {a b c d}, Rule [d|=(a,,b),,c]     [d|=(a,,(b,,c))]
-  ; al_suc_cossa     : forall {a b c d}, Rule [d|=a,,(b,,c)]     [d|=((a,,b),,c)]
-  ; al_suc_cancell   : forall {a b    }, Rule [a|=[],,b    ]     [a|=      b    ]
-  ; al_suc_cancelr   : forall {a b    }, Rule [a|=b,,[]    ]     [a|=      b    ]
-  ; al_suc_llecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=[],,b      ]
-  ; al_suc_rlecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=b,,[]      ]
-
-  ; al_horiz_expand_left            : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
-  ; al_horiz_expand_right           : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
-
-  (* these are essentially one way of formalizing
-   * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
-  ; al_horiz_expand_left_reflexive  : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left  a#]===[#al_reflexive_seq (a,,b)#]
-  ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
-  ; al_horiz_expand_right_then_cancel : forall a,
-    ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
-
-  ; al_vert_expand_ant_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [x,,a   |=   b   ]/⋯⋯/[x,,c   |=   d   ]
-  ; al_vert_expand_ant_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a,,x|=   b   ]/⋯⋯/[   c,,x|=   d   ]
-  ; al_vert_expand_suc_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=x,,b   ]/⋯⋯/[   c   |=x,,d   ]
-  ; al_vert_expand_suc_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=   b,,x]/⋯⋯/[   c   |=   d,,x]
-  ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-      f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left  x g
-  ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-    f===g -> al_vert_expand_ant_right  x f === al_vert_expand_ant_right x g
-  ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-    f===g -> al_vert_expand_suc_left   x f === al_vert_expand_suc_left  x g
-  ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-    f===g -> al_vert_expand_suc_right  x f === al_vert_expand_suc_right x g
-  ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left   x (nd_id [a|=b]) === nd_id [x,,a|=b]
-  ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right  x (nd_id [a|=b]) === nd_id [a,,x|=b]
-  ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left   x (nd_id [a|=b]) === nd_id [a|=x,,b]
-  ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right  x (nd_id [a|=b]) === nd_id [a|=b,,x]
-  ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
-  ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
-  ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
-  ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
-
-  ; al_subst                 : forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
-  ; al_subst_associativity : forall {a b c d},
-      ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
-      (al_subst a c d)
-      ===
-      nd_assoc ;;
-      ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
-      (al_subst a b d))
-  ; al_subst_associativity' : forall {a b c d},
-      nd_cossa ;;
-      ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
-      (al_subst a c d)
-      ===
-      ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
-      (al_subst a b d))
-
-  ; al_subst_left_identity  : forall a b, ((    [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell
-  ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#]    );; al_subst b _ _) === nd_cancelr
-  ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
-    [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
-    === al_subst a b c;; [#al_horiz_expand_left d#]
-  ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
-    [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
-    === al_subst a b c;; [#al_horiz_expand_right d#]
-  ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
-   (((nd_rlecnac;;
-      ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
-        (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
-     (nd_id [t1 |= t0]) **
-     ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
-       (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));; 
-    al_subst t1 t0 t2)
-   ===
-    ((([#al_reflexive_seq (t1,, [])#];;
-          (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
-           al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));; 
-         (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
+  { al_eqv                : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
+  ; al_tsr                : TreeStructuralRules
+  ; al_subst              : CutRule
+  ; al_sequent_join       : SequentJoin

   }.
   }.

-

   Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
   Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.

-  Open Scope temporary_scope3.
-
-  Lemma al_subst_respects {PL:ProgrammingLanguage} :
-    forall {a b c},
-      forall
-      (f  : [] /⋯⋯/ [a |= b])
-      (f' : [] /⋯⋯/ [a |= b])
-      (g  : [] /⋯⋯/ [b |= c])
-      (g' : [] /⋯⋯/ [b |= c]),
-      (f === f') ->
-      (g === g') ->
-      (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
-    intros.
-    setoid_rewrite H.
-    setoid_rewrite H0.
-    reflexivity.
-    Defined.
-
-  (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
-  Class ProgrammingLanguageWithUnrestrictedSubstructuralRules :=
-  { alwusr_al :> ProgrammingLanguage
-  ; al_contr  : forall a b,     Rule [a,,a |= b ]  [    a |= b]
-  ; al_exch   : forall a b c,   Rule [a,,b |= c ]  [(b,,a)|= c]
-  ; al_weak   : forall a b,     Rule [[] |= b ]  [    a |= b]
-  }.
-  Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage.
-
-  (* languages with a fixpoint operator *)
-  Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) :=
-  { alwfpo_al := al
-  ; al_fix    : forall a b x,   Rule [a,,x |= b,,x]  [a |= b]
-  }.
-  Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage.

 
   Section LanguageCategory.
 
     Context (PL:ProgrammingLanguage).
 
     (* category of judgments in a fixed type/coercion context *)
 
   Section LanguageCategory.
 
     Context (PL:ProgrammingLanguage).
 
     (* category of judgments in a fixed type/coercion context *)

-    Definition JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv.
+    Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule al_eqv.
+
+    Definition JudgmentsL          := Judgments_cartesian.

 
     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
       unfold hom; simpl.
 
     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
       unfold hom; simpl.

@@ -233,7 +111,7 @@ Section Programming_Language.
       apply al_subst.
       Defined.
 
       apply al_subst.
       Defined.
 

-    Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
+    Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).

       refine
       {| eid   := identityProof
        ; ecomp := cutProof
       refine
       {| eid   := identityProof
        ; ecomp := cutProof

@@ -248,98 +126,107 @@ Section Programming_Language.
       apply al_subst_associativity'.
       Defined.
 
       apply al_subst_associativity'.
       Defined.
 

-    Definition TypesEnrichedInJudgments : Enrichment.
-      refine {| enr_c := TypesLFC |}.
-      Defined.
-
-    Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
-(*
+    Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
+      (*

       eapply Build_EFunctor; intros.
       eapply MonoidalCat_all_central.
       unfold eqv.
       simpl.
       eapply Build_EFunctor; intros.
       eapply MonoidalCat_all_central.
       unfold eqv.
       simpl.

-*)
+      *)

       admit.
       Defined.
 
       admit.
       Defined.
 

-    Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
+    Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x ).

       admit.
       Defined.
 
       admit.
       Defined.
 

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

       refine
       refine

-        {| bin_first  := TypesL_first
-         ; bin_second := TypesL_second
+        {| bin_first  := Types_first
+         ; bin_second := Types_second

          |}.
       Defined.
 
          |}.
       Defined.
 

-    Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal.
-      admit.
-      Defined.
-    Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing.
-      admit.
-      Defined.
-    Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor [].
-      admit.
-      Defined.
+    Definition TypesL_binoidal : BinoidalCat TypesL (@T_Branch _).
+    admit.
+    Defined.

 
 

-    Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment.
-      refine {| se_enr := TypesLEnrichedInJudgments0 |}.
-      simpl.
-      admit.
-      Defined.
+    Definition Types_PreMonoidal : PreMonoidalCat TypesL_binoidal [].
+    admit.
+    Defined.

 
 

-    Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment.
-      refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}.
-      simpl.
-      admit.
+    Definition TypesEnrichedInJudgments : Enrichment.
+      refine {| enr_c := TypesL |}.

       Defined.
 
       Defined.
 

-    Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment.
-      refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl.
-      admit.
-      admit.
+    Structure HasProductTypes :=
+    {
+    }.
+
+    (* need to prove that if we have cartesian tuples we have cartesian contexts *)
+    Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.

       admit.
       Defined.
 
   End LanguageCategory.
       admit.
       Defined.
 
   End LanguageCategory.

-   
-  (*
-  Definition ArrowInProgrammingLanguage (L:ProgrammingLanguage)(tc:Terminal (TypesL L)) :=
-    FreydCategory (TypesL L) (TypesL L).
+
+  Structure ProgrammingLanguageSMME :=
+  { plsmme_pl   : ProgrammingLanguage
+  ; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments plsmme_pl)
+  }.
+  Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
+  Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
+
+  Section ArrowInLanguage.
+    Context  (Host:ProgrammingLanguageSMME).
+    Context `(CC:CartesianCat (me_mon Host)).
+    Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
+    Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
+      (* FIXME *)
+      (*
+      Definition ArrowInProgrammingLanguage := 
+        @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
+        *)
+  End ArrowInLanguage.
+
+  Section GArrowInLanguage.
+    Context (Guest:ProgrammingLanguageSMME).
+    Context (Host :ProgrammingLanguageSMME).
+    Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
+
+    (* FIXME
+    Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.

     *)
     *)

+    Definition TwoLevelLanguage := Reification Guest Host (me_i Host).

 
 

-  Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) :=
-    Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)).
+    Context (GuestHost:TwoLevelLanguage).

 
 

-  Inductive NLevelLanguage : nat -> ProgrammingLanguage -> Type :=
-  | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
-  | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
+    Definition FlatObject (x:TypesL Host) :=
+      forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).

 
 

-  Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type :=
-    forall n:nat, NLevelLanguage n PL.
+    Definition FlatSubCategory := FullSubcategory (TypesL Host) FlatObject.

 
 

-  Section TwoLevelLanguage.
-    Context `(L12:TwoLevelLanguage L1 L2).
+    Section Flattening.

 
 

-    Definition FlatObject (x:TypesL L2) :=
-      forall y1 y2, not ((reification_r_obj L12 y1 y2)=x).
+      Context  (F:Retraction (TypesL Host) FlatSubCategory).
+      Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
+      Lemma FlatteningIsNotDestructive : 
+        FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
+        admit.
+        Qed.

 
 

-    Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject.
+    End Flattening.

 
 

-    Context `(retraction      :@Functor _ _ (TypesL L2) _ _ FlatSubCategory retract_obj).
-    Context `(retraction_inv  :@Functor _ _ FlatSubCategory _ _ (TypesL L2) retract_inv_obj).
-    Context  (retraction_works:retraction >>>> retraction_inv ~~~~ functor_id _).
+  End GArrowInLanguage.

 
 

-    Definition FlatteningOfReification :=
-      (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction.
-
-    Lemma FlatteningIsNotDestructive : 
-      FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12.
-      admit.
-      Qed.
+  Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
+  | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
+  | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
+    TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.

 
 

-  End TwoLevelLanguage.      
+  Definition OmegaLevelLanguage : Type :=
+    { f : nat -> ProgrammingLanguageSMME
+    & forall n, TwoLevelLanguage (f n) (f (S n)) }.

     
   Close Scope temporary_scope3.
   Close Scope al_scope.
     
   Close Scope temporary_scope3.
   Close Scope al_scope.

@@ -349,146 +236,3 @@ Section Programming_Language.
 End Programming_Language.
 
 Implicit Arguments ND [ Judgment ].
 End Programming_Language.
 
 Implicit Arguments ND [ Judgment ].

-
-(*
-Open Scope nd_scope.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_suc_right.
-    intros; apply al_vert_expand_suc_r_respects; auto.
-    Defined.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_suc_left.
-    intros; apply al_vert_expand_suc_l_respects; auto.
-    Defined.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_ant_right.
-    intros; apply al_vert_expand_ant_r_respects; auto.
-    Defined.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_ant_left.
-    intros; apply al_vert_expand_ant_l_respects; auto.
-    Defined.
-Close Scope nd_scope.
-
-Notation "cs |= ss" := (@sequent _ cs ss) : al_scope.
-(*
-Definition mapJudg {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Judg T) : @Judg R :=
-  match seq with sequentpair a b => pair (f a) (f b) end.
-Implicit Arguments Judg [ ].
-*)
-
-
-(* proofs which are generic and apply to any acceptable langauge (most of section 4) *)
-Section Programming_Language_Facts.
-
-  (* the ambient language about which we are proving facts *)
-  Context `(Lang : @ProgrammingLanguage T Rule).
-
-  (* just for this section *)
-  Open Scope nd_scope.
-  Open Scope al_scope.
-  Open Scope pf_scope.
-  Notation "H /⋯⋯/ C" := (@ND Judg Rule H C)     : temporary_scope4.
-  Notation "a === b"  := (@ndr_eqv _ _ al_eqv _ _ a b)                   : temporary_scope4.
-  Open Scope temporary_scope4.
-
-  Definition lang_al_eqv := al_eqv(ProgrammingLanguage:=Lang).
-  Existing Instance lang_al_eqv.
-
-  Ltac distribute :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(?A ** ?B) ;; (?C ** ?D)] => 
-           setoid_rewrite <- (ndr_prod_preserves_comp A B C D)
-      end
-      end.
-
-  Ltac sequentialize_product A B :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-      | context ct [(A ** B)] =>
-          setoid_replace (A ** B)
-        with ((A ** (nd_id _)) ;; ((nd_id _) ** B))
-        (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
-    end end.
-  Ltac sequentialize_product' A B :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-      | context ct [(A ** B)] =>
-          setoid_replace (A ** B)
-        with (((nd_id _) ** B) ;; (A ** (nd_id _)))
-        (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
-    end end.
-  Ltac distribute' :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(?A ;; ?B) ** (?C ;; ?D)] => 
-           setoid_rewrite (ndr_prod_preserves_comp A B C D)
-      end
-      end.
-  Ltac distribute_left_product_with_id :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(nd_id ?A) ** (?C ;; ?D)] => 
-           setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D));
-        [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ]
-      end
-      end.
-  Ltac distribute_right_product_with_id :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(?C ;; ?D) ** (nd_id ?A)] => 
-           setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A));
-        [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ]
-      end
-      end.
-
-  (* another phrasing of al_subst_associativity; obligations tend to show up in this form *)
-  Lemma al_subst_associativity'' : 
-    forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]]) 
-    (d : T) (h : [] /⋯⋯/ [[c] |= [d]]),
-    nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) ===
-    nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]).
-    intros.
-      sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h.
-      repeat setoid_rewrite <- ndr_comp_associativity.
-      distribute_right_product_with_id.
-      repeat setoid_rewrite ndr_comp_associativity.
-      set (@al_subst_associativity) as q. setoid_rewrite q. clear q.
-      apply ndr_comp_respects; try reflexivity.
-      repeat setoid_rewrite <- ndr_comp_associativity.
-      apply ndr_comp_respects; try reflexivity.
-      sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]).
-      distribute_left_product_with_id.
-      repeat setoid_rewrite <- ndr_comp_associativity.
-      apply ndr_comp_respects; try reflexivity.
-      setoid_rewrite <- ndr_prod_preserves_comp.
-      repeat setoid_rewrite ndr_comp_left_identity.
-      repeat setoid_rewrite ndr_comp_right_identity.
-    admit.
-    admit.
-    admit.
-    admit.
-    admit.
-    Qed.
-
-  Close Scope temporary_scope4.
-  Close Scope al_scope.
-  Close Scope nd_scope.
-  Close Scope pf_scope.
-  Close Scope isomorphism_scope.
-End Programming_Language_Facts.
-
-(*Coercion AL_SurjectiveEnrichment    : ProgrammingLanguage >-> SurjectiveEnrichment.*)
-(*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*)
-*)
\ No newline at end of file

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index 4d83b78..eb6b5fd 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -9,6 +9,21 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.

-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+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 Reification.
+
+Instance CategoryOfReifications : Category SMME Reification.
+  admit.
+  Qed.
\ No newline at end of file

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index 678de5c..8d94dca 100644 (file)
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -24,7 +24,7 @@ Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
 
 Require Import Reification.
 Require Import GeneralizedArrow.
 

-Definition reification_from_garrow (K:Enrichment) (C:MonoidalEnrichment) (garrow : GeneralizedArrow K C)
+Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)

  : Reification K C (mon_i C).
   refine
   {| reification_r         := fun k:K => RepresentableFunctor K k >>>> garrow
  : Reification K C (mon_i C).
   refine
   {| reification_r         := fun k:K => RepresentableFunctor K k >>>> garrow

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index a81c895..1b626a2 100644 (file)
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -83,4 +83,8 @@ Section ReificationsEquivalentToGeneralizedArrows.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 

+  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
+    admit.
+    Qed.
+

 End ReificationsEquivalentToGeneralizedArrows.
 End ReificationsEquivalentToGeneralizedArrows.