add HaskXXXXCategory, generalized arrows, and reifications

diff --git a/src/Extraction.v b/src/Extraction.v
index c23d1c5..82b0543 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -1,3 +1,10 @@
+(*********************************************************************************************************************************)
+(* Extraction:                                                                                                                   *)
+(*                                                                                                                               *)
+(*    This module is the "top level" for extraction                                                                              *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
 (* need this or the Haskell extraction fails *)
 Set Printing Width 1300000.
 
@@ -30,6 +37,10 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
+Require Import HaskProofCategory.
+Require Import HaskStrongCategory.
+Require Import ReificationsEquivalentToGeneralizedArrows.
+
 Open Scope string_scope.
 Extraction Language Haskell.
 

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
new file mode 100644 (file)
index 0000000..f246567
--- /dev/null
+++ b/src/GeneralizedArrow.v
@@ -0,0 +1,35 @@
+(*********************************************************************************************************************************)
+(* Generalized Arrow:                                                                                                            *)
+(*                                                                                                                               *)
+(*   A generalized arrow is a monoidal functor from an enriching category to an enriched category.                               *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+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.
+
+Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) :=
+{ 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 ].

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
new file mode 100644 (file)
index 0000000..cd43282
--- /dev/null
+++ b/src/GeneralizedArrowCategory.v
@@ -0,0 +1,14 @@
+(*********************************************************************************************************************************)
+(* CategoryOfGeneralizedArrows:                                                                                                  *)
+(*                                                                                                                               *)
+(*   There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms                    *)
+(*   are generalized  Arrows                                                                                                     *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
new file mode 100644 (file)
index 0000000..6aeaace
--- /dev/null
+++ b/src/GeneralizedArrowFromReification.v
@@ -0,0 +1,131 @@
+(*********************************************************************************************************************************)
+(* GeneralizedArrowFromReification:                                                                                              *)
+(*                                                                                                                               *)
+(*   Turn a generalized arrow into a reification                                                                                 *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+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 Reification.
+Require Import GeneralizedArrow.
+
+Section GArrowFromReification.
+
+  Context  (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)).
+
+  Fixpoint garrow_fobj_ vk : C :=
+    match vk with
+    | T_Leaf None     => me_i C
+    | T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end
+    | t1,,t2          => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2))
+    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 (RepresentableFunctor C (me_i C)).
+    exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)).
+    abstract (exists (garrow_fobj vk); auto).
+    Defined.
+
+  Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (RepresentableFunctor 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 step1_functor : Functor (enr_v_mon K) (FullImage (RepresentableFunctor C (me_i C))) garrow_fobj'.
+    refine {| fmor := fun a b f => step1_mor f |}.
+    abstract (intros; unfold step1_mor; simpl;
+              apply comp_respects; try reflexivity;
+              apply comp_respects; try reflexivity;
+              apply fmor_respects; auto).
+    abstract (intros; unfold step1_mor; simpl;
+      setoid_rewrite fmor_preserves_id;
+      setoid_rewrite right_identity;
+      apply iso_comp2).
+    abstract (intros;
+      unfold step1_mor;
+      simpl;
+      repeat setoid_rewrite <- associativity;
+      apply comp_respects; try reflexivity;
+      repeat setoid_rewrite associativity;
+      apply comp_respects; try reflexivity;
+      setoid_rewrite juggle2;
+      set (iso_comp1 (homset_tensor_iso b)) as qqq;
+      setoid_rewrite qqq;
+      clear qqq;
+      setoid_rewrite right_identity;
+      apply (fmor_preserves_comp reification)).
+      Defined.
+
+  Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor 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).
+    Qed.
+    Opaque homset_tensor_iso.
+
+  Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C).
+
+  Definition garrow_functor := step1_functor >>>> step2_functor.
+
+  Definition garrow_from_reification : GeneralizedArrow K C.
+    refine {| ga_functor := garrow_functor |}.
+    admit.
+    Defined.
+
+End GArrowFromReification.
+Opaque homset_tensor_iso.

diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v
new file mode 100644 (file)
index 0000000..e324990
--- /dev/null
+++ b/src/HaskProofCategory.v
@@ -0,0 +1,284 @@
+(*********************************************************************************************************************************)
+(* HaskProofCategory:                                                                                                            *)
+(*                                                                                                                               *)
+(*    Natural Deduction proofs of the well-typedness of a Haskell term form a category                                           *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
+Require Import HaskLiteralsAndTyCons.
+Require Import HaskStrongTypes.
+Require Import HaskProof.
+Require Import NaturalDeduction.
+Require Import NaturalDeductionCategory.
+
+Section HaskProofCategory.
+(*
+
+  Context (flat_dynamic_semantics : @ND_Relation _ Rule).
+  Context (ml_dynamic_semantics   : @ND_Relation _ Rule).
+
+  Section SystemFC_Category.
+    Context (encodeTypeTree_reduce      : @LeveledHaskType V -> @LeveledHaskType V -> @LeveledHaskType V).
+    Context (encodeTypeTree_empty       : @LeveledHaskType V).
+    Context (encodeTypeTree_flat_empty  : @CoreType V).
+    Context (encodeTypeTree_flat_reduce : @CoreType V -> @CoreType V -> @CoreType V).
+  
+    Definition encodeTypeTree      :=
+      @treeReduce _ _ (fun x => match x with None => encodeTypeTree_empty | Some q => q end) encodeTypeTree_reduce.
+    Definition encodeTypeTree_flat :=
+      @treeReduce _ _ (fun x => match x with None => encodeTypeTree_flat_empty | Some q => q end) encodeTypeTree_flat_reduce.
+    (* the full category of judgments *)
+    Definition ob2judgment past :=
+      fun q:Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V)  =>
+        let (a,s):=q in (Γ > past : a |- (encodeTypeTree s) ).
+    Definition SystemFC_Cat past :=
+      @Judgments_Category_monoidal _ Rule
+        (@ml_dynamic_semantics V)
+        (Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V))
+        (ob2judgment past).
+  
+    (* the category of judgments with no variables or succedents in the "future" –- still may have code types *)
+    (* technically this should be a subcategory of SystemFC_Cat *)
+    Definition ob2judgment_flat past :=
+      fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V)  =>
+        let (a,s):=q in (Γ > past : ``a |- `(encodeTypeTree_flat s) ).
+    Definition SystemFC_Cat_Flat past :=
+      @Judgments_Category_monoidal _ Rule
+        (@flat_dynamic_semantics V)
+        (Tree ??(@CoreType V) * Tree ??(@CoreType V))
+        (ob2judgment_flat past).
+  
+    Section EscBrak_Functor.
+      Context
+        (past:@Past V)
+        (n:V)
+        (Σ₁:Tree ??(@LeveledHaskType V)).
+    
+      Definition EscBrak_Functor_Fobj
+        : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
+        := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
+          let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
+   
+      Definition append_brak
+      : forall {c}, ND_ML
+          (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        c )
+          (mapOptionTree (ob2judgment                   past )  (EscBrak_Functor_Fobj c)).
+        intros.
+        unfold ND_ML.
+        unfold EscBrak_Functor_Fobj.
+        rewrite mapOptionTree_comp.
+        simpl in *.
+        apply nd_replicate.
+        intro o; destruct o.
+        apply nd_rule.
+        apply MLRBrak.
+        Defined.
+    
+      Definition prepend_esc
+      : forall {h}, ND_ML
+          (mapOptionTree (ob2judgment                  past )  (EscBrak_Functor_Fobj h))
+          (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        h ).
+        intros.
+        unfold ND_ML.
+        unfold EscBrak_Functor_Fobj.
+        rewrite mapOptionTree_comp.
+        simpl in *.
+        apply nd_replicate.
+        intro o; destruct o.
+        apply nd_rule.
+        apply MLREsc.
+        Defined.
+    
+      Definition EscBrak_Functor_Fmor
+        : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b), 
+          (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
+        intros.
+        eapply nd_comp.
+        apply prepend_esc.
+        eapply nd_comp.
+        eapply Flat_to_ML.
+        apply f.
+        apply append_brak.
+        Defined.
+            
+      Lemma esc_then_brak_is_id : forall a,
+       ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
+         (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
+         admit.
+         Qed.
+    
+      Lemma brak_then_esc_is_id : forall a,
+       ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
+         (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
+         admit.
+         Qed.
+    
+      Instance EscBrak_Functor
+        : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
+        { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
+        intros; unfold EscBrak_Functor_Fmor; simpl in *.
+          apply ndr_comp_respects; try reflexivity.
+          apply ndr_comp_respects; try reflexivity.
+          auto.
+        intros; unfold EscBrak_Functor_Fmor; simpl in *.
+          set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
+          setoid_rewrite q.
+          apply esc_then_brak_is_id.
+        intros; unfold EscBrak_Functor_Fmor; simpl in *.
+          set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
+          repeat setoid_rewrite q.
+          apply ndr_comp_respects; try reflexivity.
+          apply ndr_comp_respects; try reflexivity.
+          repeat setoid_rewrite <- q.
+          apply ndr_comp_respects; try reflexivity.
+          setoid_rewrite brak_then_esc_is_id.
+          clear q.
+          set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
+          setoid_rewrite q.
+          reflexivity.
+        Defined.
+  
+    End EscBrak_Functor.
+  
+
+
+  Ltac rule_helper_tactic' :=
+    match goal with
+    | [ H : ?A = ?A |- _ ] => clear H
+    | [ H : [?A] = [] |- _ ] => inversion H; clear H
+    | [ H : [] = [?A] |- _ ] => inversion H; clear H
+    | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
+    | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
+    | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
+    | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
+    | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
+    | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
+(*  | [ H : Sequent T |- _ ] => destruct H *)
+(*  | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
+    | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
+    | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
+    | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
+    | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
+    end.
+
+  Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
+    admit.
+    Defined.
+
+  Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
+    admit.
+    Qed.
+
+  Definition append_brak_to_id : forall {c},
+  @ND_FC V
+      (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )
+      (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
+  admit.
+  Defined.
+
+  Definition append_brak : forall {h c}
+    (pf:@ND_FC V
+      h
+      (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )),
+    @ND_FC V
+       h
+      (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
+    
+      refine (fix append_brak h c nd {struct nd} :=
+       ((match nd
+            as nd'
+            in @ND _ _ H C
+            return
+            (H=h) ->
+            (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) -> 
+            ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
+          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_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_rule    _ _     rule    => let case_nd_rule    := tt in _
+          | nd_cancell _               => let case_nd_cancell := tt in _
+          | nd_cancelr _               => let case_nd_cancelr := tt in _
+          | nd_llecnac _               => let case_nd_llecnac := tt in _
+          | nd_rlecnac _               => let case_nd_rlecnac := tt in _
+          | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
+          | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
+        end) (refl_equal _) (refl_equal _)
+       ));
+       simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
+       destruct case_nd_id0. apply nd_id0.
+       destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
+       destruct case_nd_weak. apply nd_weak.
+
+       destruct case_nd_copy.
+         (*
+         destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
+         inversion H0; subst.
+         simpl.*)
+         idtac.
+         clear H0.
+         admit.
+
+       destruct case_nd_prod.
+         eapply nd_prod.
+         apply (append_brak _ _ lpf).
+         apply (append_brak _ _ rpf).
+
+       destruct case_nd_comp.
+         apply append_brak in bot.
+         apply (nd_comp top bot).
+
+       destruct case_nd_cancell.
+         eapply nd_comp; [ apply nd_cancell | idtac ].
+         apply append_brak_to_id.
+
+       destruct case_nd_cancelr.
+         eapply nd_comp; [ apply nd_cancelr | idtac ].
+         apply append_brak_to_id.
+
+       destruct case_nd_llecnac.
+         eapply nd_comp; [ idtac | apply nd_llecnac ].
+         apply append_brak_to_id.
+
+       destruct case_nd_rlecnac.
+         eapply nd_comp; [ idtac | apply nd_rlecnac ].
+         apply append_brak_to_id.
+
+       destruct case_nd_assoc.
+         eapply nd_comp; [ apply nd_assoc | idtac ].
+         repeat rewrite fixit.
+         apply append_brak_to_id.
+
+       destruct case_nd_cossa.
+         eapply nd_comp; [ idtac | apply nd_cossa ].
+         repeat rewrite fixit.
+         apply append_brak_to_id.
+
+       destruct case_nd_rule
+  
+
+
+    Defined.
+    
+  Definition append_brak {h c} : forall
+      pf:@ND_FC V
+        (fixify Γ ((⟨n, Σ₁ ⟩) :: past)                       h )
+        c,
+      @ND_FC V
+        (fixify Γ                past  (EscBrak_Functor_Fobj h))
+        c.
+    admit.
+    Defined.
+*)
+End HaskProofCategory.
\ No newline at end of file

diff --git a/src/HaskStrongCategory.v b/src/HaskStrongCategory.v
new file mode 100644 (file)
index 0000000..99772c7
--- /dev/null
+++ b/src/HaskStrongCategory.v
@@ -0,0 +1,127 @@
+(*********************************************************************************************************************************)
+(* HaskStrongCategory:                                                                                                           *)
+(*                                                                                                                               *)
+(*    Well-typed Haskell terms in a specific tyvar/covar context form a category                                                 *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
+Require Import HaskLiteralsAndTyCons.
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+
+(*  
+    (* the category of flat Haskell terms (n-ary) *)
+    Section HaskFlat.
+  
+      Context (past:@Past V).
+    
+      Lemma idmor   a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
+        (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
+        admit.
+        Defined.
+    
+      Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
+        admit.
+        Defined.
+      
+      Definition HaskFlat
+        : ECategory
+            (SystemFC_Cat_Flat past)
+            (Tree ??(@CoreType V))
+            (fun a s => [(a,s)]).
+        refine
+          {| eid   := fun a     => idmor   a
+           ; ecomp := fun a b c => compmor a b c
+          |}; intros; simpl in *; auto.
+        apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
+        apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
+        admit.
+        admit.
+        admit.
+        Defined.
+  
+      Definition HaskFlatEnrichment : SurjectiveEnrichment.
+        refine {| se_enr := {| enr_c := HaskFlat |} |}.
+        admit.
+        Defined.
+  
+    End HaskFlat.
+  
+    (* the category of multi-level Haskell terms (n-ary) with a given past *)
+    Section Hask.
+      Context (past:@Past V).
+  
+      Lemma idmor'   a : [] ~~{SystemFC_Cat past}~~> [(a,a)].
+        (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
+        admit.
+        Defined.
+    
+      Lemma compmor' a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat past}~~> [(a,c)].
+        admit.
+        Defined.
+  
+      Definition Hask
+        : ECategory
+            (SystemFC_Cat past)
+            (Tree ??(@LeveledHaskType V))
+            (fun a s => [(a,s)]).
+        refine
+          {| eid   := fun a     => idmor'   a
+           ; ecomp := fun a b c => compmor' a b c
+          |}; intros; simpl in *; auto.
+        apply (MonoidalCat_all_central (SystemFC_Cat past)).
+        apply (MonoidalCat_all_central (SystemFC_Cat past)).
+        admit.
+        admit.
+        admit.
+        Defined.
+  
+      Definition HaskEnrichmentMonoidal : MonoidalEnrichment.
+        refine {| me_enr := {| enr_c := Hask |} |}.
+        Admitted.
+  
+      Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment.
+        refine {| ffme_enr := HaskEnrichmentMonoidal |}.
+        admit.
+        admit.
+        admit.
+        Defined.
+    End Hask.
+  
+    Section ReificationAndGeneralizedArrow.
+      Context
+        (past:list ((Tree ??(@LeveledHaskType V)) * V))
+        (Σ:(Tree ??(@LeveledHaskType V)))
+        (n:V).
+    
+      Definition SystemFC_Reification 
+        : Reification
+        (HaskFlatEnrichment (((Σ,n)::past))) 
+        (HaskEnrichmentMonicMonoidal  (*past*))
+        (me_i (HaskEnrichmentMonicMonoidal (*past*))).
+        (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*)
+        admit.
+        Defined.
+(*    
+      Definition SystemFC_GArrow :=
+        garrow_from_reification
+        (HaskFlatEnrichment (((Σ,n)::past)))
+        (HaskEnrichmentMonicMonoidal (*past*))
+        SystemFC_Reification.
+  *)
+      (* I think we have to add a proof that the derived GArrow's range is in the "monoidal closure" of the reification functor;
+       * from there we can show that -- in the case of Hask and System FC -- that range is a retract of some other subcategory
+       * of Hask which consists of the (GArrow g => g a b) morphisms *)
+    
+    End ReificationAndGeneralizedArrow.
+*)  
+
+

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
new file mode 100644 (file)
index 0000000..23ddb56
--- /dev/null
+++ b/src/NaturalDeductionCategory.v
@@ -0,0 +1,178 @@
+(*********************************************************************************************************************************)
+(* NaturalDeductionCategory:                                                                                                     *)
+(*                                                                                                                               *)
+(*   Natural Deduction proofs form a category (under mild assumptions, see below)                                                *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+
+Require Import Algebras_ch4.
+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.
+
+Open Scope nd_scope.
+Open Scope pf_scope.
+
+(* proofs form a category, with judgment-trees as the objects *)
+Section Judgments_Category.
+
+  Context {Judgment : Type}.
+  Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
+  Context (nd_eqv   : @ND_Relation Judgment Rule).
+
+  (* actually you can use any type as the objects, so long as you give a mapping from that type to judgments *)
+  Context {Ob       : Type}.
+  Context (ob2judgment : Ob -> Judgment).
+  Coercion ob2judgment : Ob >-> Judgment.
+
+  Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
+
+  Instance Judgments_Category
+    : Category (Tree ??Ob) (fun h c => (mapOptionTree ob2judgment h) /⋯⋯/ (mapOptionTree ob2judgment c)) :=
+  { id   := fun h          => nd_id _
+  ; comp := fun a b c f g  => f ;; g
+  ; eqv  := fun a b f g    => f === g
+  }.
+  intros; apply Build_Equivalence;
+    [ unfold Reflexive; intros; reflexivity
+    | 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_comp_associativity.
+  Defined.
+
+  Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
+    (fun xy =>
+     match xy with
+     | pair_obj x y => T_Branch x y
+     end).
+  Definition Judgments_Category_monoidal_endofunctor_fmor :
+           forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) ->
+           ((Judgments_Category_monoidal_endofunctor_fobj a)
+           ~~{Judgments_Category}~~>
+           (Judgments_Category_monoidal_endofunctor_fobj b)).
+     intros.
+     destruct a.
+     destruct b.
+     destruct X.
+     exact (h**h0).
+     Defined.
+  Definition Judgments_Category_monoidal_endofunctor
+  : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj.
+    refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl.
+    abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto).
+    abstract (destruct a; simpl in *; reflexivity).
+    abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp).
+    Defined.
+
+  Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
+    apply (@Build_Isomorphic _ _ Judgments_Category _ _
+      (@nd_assoc _ Rule  (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c)
+        : (a,, b),, c ~~{Judgments_Category}~~> a,, (b,, c))
+      (@nd_cossa _ Rule  (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c)
+        : a,, (b,, c) ~~{Judgments_Category}~~> (a,, b),, c)); simpl; auto.
+    Defined.
+  Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
+    apply (@Build_Isomorphic _ _ Judgments_Category _ _
+      (@nd_cancelr _ Rule (mapOptionTree ob2judgment a) : a,,[] ~~{Judgments_Category}~~> a)
+      (@nd_rlecnac _ Rule (mapOptionTree ob2judgment a) : a     ~~{Judgments_Category}~~> a,,[])); simpl; auto.
+    Defined.
+  Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
+    apply (@Build_Isomorphic _ _ Judgments_Category _ _
+      (@nd_cancell _ Rule (mapOptionTree ob2judgment a) : [],,a ~~{Judgments_Category}~~> a)
+      (@nd_llecnac _ Rule (mapOptionTree ob2judgment a) : a     ~~{Judgments_Category}~~> [],,a)); simpl; auto.
+    Defined.
+
+  Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
+    refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl.
+    setoid_rewrite (ndr_prod_right_identity f).
+    repeat setoid_rewrite ndr_comp_associativity.
+    apply ndr_comp_respects; try reflexivity.
+    symmetry.
+    eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
+    apply ndr_comp_respects; try reflexivity; simpl; auto.
+    Defined.
+  Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
+    eapply Build_NaturalIsomorphism.
+    instantiate (1:=fun x => jud_cancell_iso x).
+    intros; simpl.
+    setoid_rewrite (ndr_prod_left_identity f).
+    repeat setoid_rewrite ndr_comp_associativity.
+    apply ndr_comp_respects; try reflexivity.
+    symmetry.
+    eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
+    apply ndr_comp_respects; try reflexivity; simpl; auto.
+    Defined.
+  Definition jud_mon_assoc_iso :
+    forall X, 
+      (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) X) ≅
+  (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor))) X.
+    intros.
+    destruct X as [a c].
+    destruct a as [a b].
+    apply (jud_assoc_iso a b c).
+    Defined.
+  Definition jud_mon_assoc   :
+    ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
+    <~~~>
+    func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
+    refine {| ni_iso := jud_mon_assoc_iso |}.
+    intros.
+    destruct A as [a1 a3]. destruct a1 as [a1 a2].
+    destruct B as [b1 b3]. destruct b1 as [b1 b2].
+    destruct f as [f1 f3]. destruct f1 as [f1 f2].
+    simpl.
+    setoid_rewrite ndr_prod_associativity.
+    setoid_rewrite ndr_comp_associativity.
+    setoid_rewrite ndr_comp_associativity.
+    apply ndr_comp_respects; try reflexivity.
+    symmetry.
+    eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
+    apply ndr_comp_respects; try reflexivity; simpl; auto.
+    Defined.
+
+  Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] :=
+  { mon_cancelr := jud_mon_cancelr
+  ; mon_cancell := jud_mon_cancell
+  ; mon_assoc   := jud_mon_assoc   }.
+    apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
+    apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; 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,,[]    )]
+  }.
+
+
+  (* Structure ExpressionAlgebra (sig:Signature) := *)
+
+End Judgments_Category.
+
+Close Scope pf_scope.
+Close Scope nd_scope.

diff --git a/src/Reification.v b/src/Reification.v
new file mode 100644 (file)
index 0000000..a56ded8
--- /dev/null
+++ b/src/Reification.v
@@ -0,0 +1,46 @@
+(*********************************************************************************************************************************)
+(* Reification:                                                                                                                  *)
+(*                                                                                                                               *)
+(*   A reification is a functor R from one enrichING category A to another enrichING category B which forms a commuting square   *)
+(*   with every pair of hom-functors Hom(X,-):a->A and Hom(Y,-):b->B up to natural isomorphism.                                  *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+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.
+
+Opaque RepresentableFunctor.
+Opaque functor_comp.
+Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
+{ reification_r_obj     : K -> K -> 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     :             MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
+; reification_commutes  : forall k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
+}.
+Transparent RepresentableFunctor.
+Transparent functor_comp.
+
+Coercion reification_rstar : Reification >-> MonoidalFunctor.
+Implicit Arguments Reification                [ ].
+Implicit Arguments reification_r_obj          [ K C CI ].
+Implicit Arguments reification_r              [ K C CI ].
+Implicit Arguments reification_rstar          [ K C CI ].
+Implicit Arguments reification_rstar_f        [ K C CI ].
+Implicit Arguments reification_commutes       [ K C CI ].
+Implicit Arguments reification_rstar_obj      [ K C CI ].

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
new file mode 100644 (file)
index 0000000..4d83b78
--- /dev/null
+++ b/src/ReificationCategory.v
@@ -0,0 +1,14 @@
+(*********************************************************************************************************************************)
+(* ReificationCategory:                                                                                                          *)
+(*                                                                                                                               *)
+(*   There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms                    *)
+(*   are reifications                                                                                                            *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
new file mode 100644 (file)
index 0000000..ed92c57
--- /dev/null
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -0,0 +1,37 @@
+(*********************************************************************************************************************************)
+(* ReificationFromGeneralizedArrow:                                                                                              *)
+(*                                                                                                                               *)
+(*   Turn a reification into a generalized arrow                                                                                 *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+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 Reification.
+Require Import GeneralizedArrow.
+
+Definition reification_from_garrow (K:Enrichment) (C:MonoidalEnrichment) (garrow : GeneralizedArrow K C)
+ : Reification K C (mon_i C).
+  refine
+  {| reification_r         := fun k:K => RepresentableFunctor K k >>>> garrow
+   ; reification_rstar_f   :=                                garrow >>>> me_mf C
+   ; reification_rstar     :=              MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C)
+   |}.
+   abstract (intros; set (@ni_associativity) as q; apply q).
+   Defined.
+
+

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
new file mode 100644 (file)
index 0000000..5b4c5ef
--- /dev/null
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -0,0 +1,86 @@
+(*********************************************************************************************************************************)
+(* ReificationsEquivalentToGeneralizedArrows:                                                                                    *)
+(*                                                                                                                               *)
+(*   The category of generalized arrows and the category of reifications are equivalent categories.                              *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+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 Reification.
+Require Import GeneralizedArrow.
+Require Import GArrowFromReification.
+Require Import ReificationFromGArrow.
+Require Import ReificationCategory.
+Require Import GeneralizedArrowCategory.
+
+Section ReificationsEquivalentToGeneralizedArrows.
+
+  Ltac if_transitive :=
+    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 _ _).
+    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_inv.
+    apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))).
+    apply if_respects.
+    apply ff_functor_section_splits_niso.
+    apply if_id.
+    Qed.
+
+  Definition roundtrip_lemma
+    (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C))
+    := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
+
+  Lemma roundtrip_reification_to_reification
+    (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C))
+    : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
+    simpl.
+    unfold mon_f.
+    unfold garrow_functor.
+    apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
+       apply step1_niso.
+       apply (if_inv (roundtrip_lemma K C reification)).
+    Qed.
+    (* FIXME: show that the R-functors are naturally isomorphic as well; should follow pretty easily from the proof for Rstar *)
+
+  Lemma roundtrip_garrow_to_garrow
+    (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (garrow : GeneralizedArrow K C)
+    : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
+    apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)).
+    apply if_inv.
+    apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
+           >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
+    unfold mf_f.
+    unfold garrow_from_reification.
+    unfold garrow_functor.
+    unfold step2_functor.
+    apply roundtrip_lemma.
+    apply if_inv.
+    apply (step1_niso K C (reification_from_garrow K C garrow)).
+    Qed.
+
+End ReificationsEquivalentToGeneralizedArrows.