Merge branch 'master' of http://git.megacz.com/coq-hetmet
authorAdam Megacz <megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 19:37:04 +0000 (19:37 +0000)
committerAdam Megacz <megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 19:37:04 +0000 (19:37 +0000)
Makefile
src/ExtractionMain.v
src/GeneralizedArrowCategory.v
src/GeneralizedArrowFromReification.v
src/PreCategory.v [new file with mode: 0644]
src/Reification.v
src/ReificationCategory.v
src/ReificationsIsomorphicToGeneralizedArrows.v
src/WeakFunctorCategory.v
src/categories

index 2d65894..d8bc76a 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ default: build/CoqPass.hs
 
 build/CoqPass.hs: $(allfiles)
        make build/Makefile.coq
-       cd build; make -f Makefile.coq OPTS=-dont-load-proofs ExtractionMain.vo
+       cd build; make -f Makefile.coq OPT=-dont-load-proofs ExtractionMain.vo
        cd build; make -f Makefile.coq Extraction.vo
        cat src/Extraction-prefix.hs                                     > build/CoqPass.hs
        cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs
index 05d059a..dbeb3cc 100644 (file)
@@ -40,7 +40,7 @@ Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
 *)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.
index a9bedbb..3ec6660 100644 (file)
@@ -26,19 +26,36 @@ Require Import GeneralizedArrow.
 Require Import WeakFunctorCategory.
 Require Import SmallSMMEs.
 
+(*
+ * Technically reifications form merely a *semicategory* (no identity
+ * maps), but one can always freely adjoin identity maps (and nothing
+ * else) to a semicategory to get a category whose non-identity-map
+ * portion is identical to the original semicategory
+ *
+ * Also, technically this category has ALL enrichments (not just the
+ * surjective monic monoidal ones), though there maps OUT OF only the
+ * surjective enrichments and INTO only the monic monoidal
+ * enrichments.  It's a big pain to do this in Coq, but sort of might
+ * matter in real life: a language with really severe substructural
+ * restrictions might fail to be monoidally enriched, meaning we can't
+ * use it as a host language.  But that's for the next paper...
+ *)
 Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
   | gaoi_id   : forall smme:SMMEs,                             GeneralizedArrowOrIdentity smme smme
   | gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2  -> GeneralizedArrowOrIdentity s1   s2.
 
-Definition generalizedArrowOrIdentityFunc
-  : forall s1 s2, GeneralizedArrowOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
-  intros.
-  destruct X.
-  exists (fun x => x).
-  apply functor_id.
-  eapply existT.
-  apply (g >>>> RepresentableFunctor s2 (mon_i s2)).
-  Defined.
+Definition generalizedArrowOrIdentityFobj (s1 s2:SMMEs) (f:GeneralizedArrowOrIdentity s1 s2) : s1 -> s2 :=
+  match f in GeneralizedArrowOrIdentity S1 S2 return S1 -> S2 with
+  | gaoi_id  s       => fun x => x
+  | gaoi_ga s1 s2 f  => fun a => ehom(ECategory:=s2) (mon_i (smme_mon s2)) (ga_functor_obj f a)
+  end.
+
+Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 s2)
+  : Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) :=
+  match f with
+  | gaoi_id  s       => functor_id _
+  | gaoi_ga s1 s2 f  => ga_functor f >>>> RepresentableFunctor s2 (mon_i s2)
+  end.
 
 Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
   GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
@@ -66,7 +83,7 @@ Definition generalizedArrowOrIdentityComp
 Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
   refine {| small_func      := GeneralizedArrowOrIdentity
           ; small_func_id   := fun s => gaoi_id s
-          ; small_func_func := fun smme1 smme2 f => projT2 (generalizedArrowOrIdentityFunc _ _ f)
+          ; small_func_func := fun smme1 smme2 f => generalizedArrowOrIdentityFunc _ _ f
           ; small_func_comp := generalizedArrowOrIdentityComp
          |}; intros; simpl.
   apply if_id.
index e6d3cbd..627aa22 100644 (file)
@@ -122,9 +122,29 @@ Section GArrowFromReification.
 
   Definition garrow_functor := step1_functor >>>> step2_functor.
 
-  Definition garrow_from_reification : GeneralizedArrow K C.
-    refine {| ga_functor := garrow_functor |}.
+  Lemma garrow_functor_monoidal_niso
+    : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+    admit.
+    Defined.
+  Lemma garrow_functor_monoidal_iso
+    : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
+    admit.
+    Defined.
+
+  Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
+    { mf_coherence := garrow_functor_monoidal_niso
+    ; mf_id        := garrow_functor_monoidal_iso
+    }.
     admit.
+    admit.
+    admit.
+    Defined.
+
+  Definition garrow_from_reification : GeneralizedArrow K C.
+    refine
+      {| ga_functor          := garrow_functor
+       ; ga_functor_monoidal := garrow_functor_monoidal
+      |}.
     Defined.
 
 End GArrowFromReification.
diff --git a/src/PreCategory.v b/src/PreCategory.v
new file mode 100644 (file)
index 0000000..7418261
--- /dev/null
@@ -0,0 +1,93 @@
+(*********************************************************************************************************************************)
+(* SemiCategory:                                                                                                                 *)
+(*                                                                                                                               *)
+(*   Same as a category, but without identity maps.   See                                                                        *)
+(*                                                                                                                               *)
+(*       http://ncatlab.org/nlab/show/semicategory                                                                               *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+Class SemiCategory (Ob:Type)(Hom:Ob->Ob->Type) :=
+{ semi_hom              := Hom
+; semi_ob               := Ob
+; semi_comp             :  forall  {a}{b}{c}, Hom a b -> Hom b c -> Hom a c
+; semi_eqv              :  forall  a b,   (Hom a b) -> (Hom a b) -> Prop
+; semi_eqv_equivalence  :  forall  a b,   Equivalence (semi_eqv a b)
+; semi_comp_respects    :  forall  a b c, Proper (semi_eqv a b ==> semi_eqv b c ==> semi_eqv a c) (@semi_comp _ _ _)
+; semi_associativity    :
+       forall `(f:Hom a b)`(g:Hom b c)`(h:Hom c d), semi_eqv _ _ (semi_comp (semi_comp f g) h) (semi_comp f (semi_comp g h))
+}.
+Coercion semi_ob : SemiCategory >-> Sortclass.
+
+Notation "a ~->   b" := (@semi_hom  _ _ _       a b) (at level 70).
+Notation "f ~-~   g" := (@semi_eqv  _ _ _ _ _   f g) (at level 54).
+Notation "f >>->> g" := (@semi_comp _ _ _ _ _ _ f g) (at level 45).
+
+Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:SemiCategory Ob Hom)(a b:Ob) : (semi_hom a b) (semi_eqv a b)
+  reflexivity proved by  (@Equivalence_Reflexive  _ _ (semi_eqv_equivalence a b))
+  symmetry proved by     (@Equivalence_Symmetric  _ _ (semi_eqv_equivalence a b))
+  transitivity proved by (@Equivalence_Transitive _ _ (semi_eqv_equivalence a b))
+  as parametric_relation_semi_eqv.
+  Add Parametric Morphism `(c:SemiCategory Ob Hom)(a b c:Ob) : (@semi_comp _ _ _ a b c)
+  with signature (semi_eqv _ _ ==> semi_eqv _ _ ==> semi_eqv _ _) as parametric_morphism_semi_comp.
+    intros.
+    apply semi_comp_respects; auto.
+  Defined.
+
+Class SemiFunctor
+`( c1                 : SemiCategory                           )
+`( c2                 : SemiCategory                           )
+( fobj                : c1 -> c2                               ) :=
+{ semifunctor_fobj         := fobj
+; semi_fmor                : forall {a b}, (a~->b) -> (fobj a)~->(fobj b)
+; semi_fmor_respects       : forall a b (f f':a~->b),   (f ~-~ f') ->        (semi_fmor f ~-~ semi_fmor f')
+; semi_fmor_preserves_comp : forall `(f:a~->b)`(g:b~->c), (semi_fmor f) >>->> (semi_fmor g) ~-~ semi_fmor (f >>->> g)
+}.
+Implicit Arguments semi_fmor [[Ob][Hom][c1][Ob0][Hom0][c2][fobj][a][b]].
+
+  (* register "fmor" so we can rewrite through it *)
+  Implicit Arguments semi_fmor                [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+  Implicit Arguments semi_fmor_respects       [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+  Implicit Arguments semi_fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
+  Notation "F \- f" := (semi_fmor F f) (at level 20)  : category_scope.
+  Add Parametric Morphism `(C1:SemiCategory)`(C2:SemiCategory)
+    (Fobj:C1->C2)
+    (F:SemiFunctor C1 C2 Fobj)
+    (a b:C1)
+  : (@semi_fmor _ _ C1 _ _ C2 Fobj F a b)
+  with signature ((@semi_eqv C1 _ C1 a b) ==> (@semi_eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_semi_fmor'.
+  intros; apply (@semi_fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
+  Defined.
+  Coercion semifunctor_fobj : SemiFunctor >-> Funclass.
+
+Definition semifunctor_comp
+  `(C1:SemiCategory)
+  `(C2:SemiCategory)
+  `(C3:SemiCategory)
+  `(F:@SemiFunctor _ _ C1 _ _ C2 Fobj)`(G:@SemiFunctor _ _ C2 _ _ C3 Gobj) : SemiFunctor C1 C3 (Gobj ○ Fobj).
+  intros. apply (Build_SemiFunctor _ _ _ _ _ _ _ (fun a b m => semi_fmor G (semi_fmor F m))).
+  intros.
+  setoid_rewrite H.
+  reflexivity.
+  intros.
+  setoid_rewrite semi_fmor_preserves_comp; auto.
+  setoid_rewrite semi_fmor_preserves_comp; auto.
+  reflexivity.
+  Defined.
+Notation "f >>>–>>> g" := (@semifunctor_comp _ _ _ _ _ _ _ _ _ _ f _ g) (at level 20)  : category_scope.
+
+Class IsomorphicSemiCategories `(C:SemiCategory)`(D:SemiCategory) :=
+{ isc_f_obj    : C -> D
+; isc_g_obj    : D -> C
+; isc_f        : SemiFunctor C D isc_f_obj
+; isc_g        : SemiFunctor D C isc_g_obj
+; isc_forward  : forall a b (f:a~->b), semi_fmor isc_f  (semi_fmor isc_g  f) ~-~ f
+}.
+; isc_backward : isc_g >>>> isc_f ~~~~ functor_id D
+}.
+
+
index a56ded8..2f2ba67 100644 (file)
@@ -31,7 +31,7 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI: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
+; reification_commutes : ∀ k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
 }.
 Transparent RepresentableFunctor.
 Transparent functor_comp.
index b4d444a..0227f60 100644 (file)
@@ -26,25 +26,44 @@ Require Import Reification.
 Require Import WeakFunctorCategory.
 Require Import SmallSMMEs.
 
+(* Technically reifications form merely a *semicategory* (no identity
+ * maps), but one can always freely adjoin identity maps (and nothing
+ * else) to a semicategory to get a category whose non-identity-map
+ * portion is identical to the original semicategory
+ *
+ * Also, technically this category has ALL enrichments (not just the
+ * surjective monic monoidal ones), though there maps OUT OF only the
+ * surjective enrichments and INTO only the monic monoidal
+ * enrichments.  It's a big pain to do this in Coq, but sort of might
+ * matter in real life: a language with really severe substructural
+ * restrictions might fail to be monoidally enriched, meaning we can't
+ * use it as a host language.  But that's for the next paper...
+ *)
 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
   | roi_id   : forall smme:SMMEs,                                  ReificationOrIdentity smme smme
   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1   s2.
 
+Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
+  match f with
+  | roi_id   s       => (fun x => x)
+  | roi_reif s1 s2 f => reification_rstar_obj f
+  end.
+
 Definition reificationOrIdentityFunc
-  : forall s1 s2, ReificationOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
+  : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
   intros.
-  destruct X.
-  exists (fun x => x).
+  destruct f.
   apply functor_id.
-  exists (reification_rstar_obj r).
-  apply r.
+  unfold reificationOrIdentityFobj.
+  apply (reification_rstar_f r).
   Defined.
 
 Definition compose_reifications (s0 s1 s2:SMMEs) :
   Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
   intros.
   refine
-    {| reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
+    {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
+     ; reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
     |}.
   intro K.
@@ -54,7 +73,28 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   clear q.
   set (reification_commutes X K) as comm1.
   set (reification_commutes X0 (mon_i s1)) as comm2.
-  admit.
+  set (RepresentableFunctor s0 K) as a in *.
+  set (reification_rstar_f X) as a' in *.
+  set (reification_rstar_f X0) as x in *.
+  set (reification_r X K) as b in *.
+  set (reification_r X0 (mon_i s1)) as c in *.
+  set (RepresentableFunctor s2 (mon_i s2)) as c' in *.
+  set (RepresentableFunctor s1 (mon_i s1)) as b' in *.
+  apply (ni_comp(F2:=b >>>> (b' >>>> x))).
+  apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
+  apply ni_id.
+  apply comm2.
+  eapply ni_comp.
+  eapply ni_inv.
+  apply (ni_associativity b b' x).
+  eapply ni_inv.
+  eapply ni_comp.
+  eapply ni_inv.
+  apply (ni_associativity a a' x).
+  apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
+  apply ni_inv.
+  apply comm1.
+  apply ni_id.
   Defined.
 
 Definition reificationOrIdentityComp
@@ -70,7 +110,7 @@ Definition reificationOrIdentityComp
 Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs.
   refine {| small_func      := ReificationOrIdentity
           ; small_func_id   := fun s => roi_id s
-          ; small_func_func := fun smme1 smme2 f => projT2 (reificationOrIdentityFunc _ _ f)
+          ; small_func_func := fun smme1 smme2 f => reificationOrIdentityFunc _ _ f
           ; small_func_comp := reificationOrIdentityComp
          |}; intros; simpl.
   apply if_id.
index db11897..5163c26 100644 (file)
@@ -32,4 +32,162 @@ Require Import WeakFunctorCategory.
 
 Section ReificationsIsomorphicToGeneralizedArrows.
 
+    Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
+      (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
+      (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
+      intro GA.
+      destruct GA; [ apply roi_id | idtac ].
+      apply roi_reif.
+      apply reification_from_garrow.
+      apply g.
+      Defined.
+
+    Lemma invert_ga : forall (a: SMME)
+      (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
+      (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
+      admit.
+      Qed.
+
+    Lemma invert_reif : forall (a: SMME)
+      (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
+      (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
+      admit.
+      Qed.
+
+    Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
+      refine {| fmor := fun a b f => M1 f |}.
+      intros.
+        unfold hom in *.
+        unfold eqv in *.
+        simpl in *.
+        destruct f.
+        set (invert_ga _ f') as q.
+        destruct q; subst.
+        apply if_id.
+        simpl in *.
+        destruct H0; subst.
+        apply H.
+        simpl in *.
+        destruct f'; simpl in *.
+        apply H.
+        apply H.
+      intros; simpl.
+        apply if_id.
+      intros.
+        simpl.
+        destruct f; simpl.
+        apply if_id.
+        destruct g; simpl.
+        apply if_id.
+        unfold mf_f; simpl.
+        apply (if_associativity 
+          ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
+        Defined.
+
+    Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
+      (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
+      (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
+      intro RE.
+      destruct RE; [ apply gaoi_id | idtac ].
+      apply gaoi_ga.
+      apply (garrow_from_reification s1 s2 r).
+      Defined.
+
+    Lemma M2_respects :
+      forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
+         f ~~ f' ->
+         M2 a b f ~~ M2 a b f'.
+      intros.
+        unfold hom in *.
+        unfold eqv in *.
+        simpl in *.
+        destruct f.
+        set (invert_reif _ f') as q.
+        destruct q; subst.
+        apply if_id.
+        simpl in *.
+        destruct H0; subst.
+        simpl in *.
+        unfold garrow_functor.
+        unfold step2_functor.
+        apply (if_comp H).
+        clear H.
+        apply (if_comp (@step1_niso _ smme _ _ smme x)).
+        apply if_inv.
+        apply (@roundtrip_lemma _ smme _ _ smme x).
+      simpl in *.
+        destruct f'; simpl in *.
+        apply if_inv.
+        apply if_inv in H.
+        apply (if_comp H).
+        clear H.
+        unfold garrow_functor.
+        unfold step2_functor.
+        apply (if_comp (@step1_niso _ smme _ _ smme r)).
+        apply if_inv.
+        apply (@roundtrip_lemma _ smme _ _ smme r).
+      simpl in *.
+        unfold garrow_functor.
+        unfold step2_functor.
+        apply if_inv in H.
+        set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
+        set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
+        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
+        apply if_inv.
+        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
+        apply yy'.
+        Qed.
+
+    Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
+      refine {| fmor := fun a b f => M2 _ _ f |}.
+      apply M2_respects.
+      intros; simpl; apply if_id.
+      intros.
+        simpl.
+        destruct f; simpl.
+        apply if_id.
+        destruct g; simpl.
+        apply if_id.
+        unfold mf_f; simpl.
+        apply (if_respects
+          (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
+          (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
+          (G0:=(RepresentableFunctor s2 (mon_i s2)))
+          (G1:=(RepresentableFunctor s2 (mon_i s2))));
+        [ idtac | apply if_id ].
+        admit.
+        Defined.
+
+    Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
+      refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
+      unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+        unfold hom in *.
+        set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
+        destruct f; simpl in *.
+        apply H.
+        apply if_inv.
+        apply (if_comp (if_inv H)).
+        clear H.
+        unfold mf_f in q.
+        apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
+          (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
+        apply q.
+        apply if_id.
+        
+      unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+        unfold hom in *.
+        set (@roundtrip_reification_to_reification _ a _ _ b) as q.
+        destruct f; simpl.
+        apply H.
+        apply if_inv.
+        apply (if_comp (if_inv H)).
+        clear H.
+        simpl.
+        unfold mf_f; simpl.
+        simpl in q.
+        unfold mf_f in q.
+        simpl in q.
+        apply q.
+        Qed.
+
 End ReificationsIsomorphicToGeneralizedArrows.
index 49a5189..85ade61 100644 (file)
@@ -192,8 +192,8 @@ Section WeakFunctorCategoryIsomorphism.
         apply q.
         Defined.
 
-    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
-      apply Build_IsomorphicCategories.
+    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
+      refine {| ic_f := F1 ; ic_g := F2 |}.
       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
         eapply if_comp.
         apply m1_m2_id.
index cc0b469..1ab46a0 160000 (submodule)
@@ -1 +1 @@
-Subproject commit cc0b4696c2cfc23bdff6ded347478510ccf014c9
+Subproject commit 1ab46a0e579ec1964ae0ab3cadb64f6a77db8d30