add HaskXXXXCategory, generalized arrows, and reifications

[coq-hetmet.git] / src / GeneralizedArrowFromReification.v

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.