updated encatI.v

Author: Paolo Torrini

theories/encatI.v

@@ -101,8 +101,6 @@ Set Universe Checking.
 
 (*** CATEGORIES WITH PULLBACKS *)
 
-(* Local Open Scope type_scope. *)
-
 (* category with all prepullbacks *)
 (* Ideally span is in fact expanded and the final mixin has
 a pb : forall A B, cospan A B -> C
@@ -590,7 +588,8 @@ Lemma jm_pbsquare_universal {C: cat} (A B T P0 P1 P2 : C)
   (e: P0 = P2) :
   sigma m: P1 ~> P2, f = m \;;_e p1 /\ g = m \;;_e p2. 
   unfold jmcomp.
-  dependent destruction e.
+  destruct e.
+(*  dependent destruction e. *)
   eapply pbsquare_universal; eauto.
 Qed.  
 
@@ -778,7 +777,10 @@ Program Definition ipairC {C : pbcat} {C0 : C} {x0 x1 x2 x3 : iHom C0}
     subst prj21 prj22.
 
     (* surprisingly, this does not work with pbsquare_is_pulback_sym *)
-    (* rewrite <- pbsquare_is_pullback_sym. *)
+    (* rewrite - pbsquare_is_pullback_sym. 
+       Set Printing All. 
+    *)
+
     rewrite pbsquare_is_pullback.
     inversion HeqCsp2; subst.
     subst Sp2.
@@ -960,10 +962,11 @@ assert (forall (e2: ((c2 *_C0 c3) :> C) = Pb23),
     j33L \; (j12R \; src2) = m23 \;;_e2 j23L \; src2) as M23_E1.
 { intros e2.
   unfold jmcomp.
-  dependent destruction e2.
+  destruct e2.
+(*  dependent destruction e2. *)
   rewrite compoA.
   rewrite m23_E.
-  unfold jmcomp.
+  unfold jmcomp.  
   dependent destruction E23.
   rewrite compoA; auto.
 }  
@@ -973,7 +976,8 @@ assert (forall (e3: ((c2 *_C0 c3) :> C) = Pb23),
 { intros e3.
   specialize (M23_E1 E23).
   unfold jmcomp in M23_E1.
-  dependent destruction E23.
+  destruct E23.
+(*  dependent destruction E23. *)
   unfold jmcomp.
   dependent destruction e3.
   setoid_rewrite <- compoA.
@@ -999,7 +1003,7 @@ assert (pbsquare j15L j15R tgt1 src23) as pbsq15.
 }
 
 assert ((j33L \; j12L) \; tgt1 = m23 \; src23) as sqM23.
-{ specialize (M23_E2 E23).
+{ specialize (M23_E2 E23).  
   dependent destruction E23.
   exact M23_E2.
 }
@@ -1019,12 +1023,13 @@ assert (
   eapply (@pbsquare_universal C _ _ _ _ _ _ _ _ _ (j33L \; j12L) m23).
   exact pbsq15.
   exact sqM23.
-}
-  
+}  
 destruct (X E33) as [mm R].
 exact mm.
 Qed. 
 
+Print Assumptions iprodCAsc.
+
 (* An internal precategory is an internal category with two operators
    that must be src and tgt preserving, i.e. iHom morphisms: identity
    : C0 -> C1 (corresponding to horizontal 1-morphism identity in
@@ -1903,6 +1908,9 @@ Obligation 1.
 refine (@existT (D1hom h0 k0) _ hh0 (@existT (D1hom h1 k1) _ hh1 k)).
 Defined.
 
+(*HB.builders Context (T : obj cat) (f : IsInternalCat cat T).*)
+(* Context (f : doublecat). *)
+  
 (* hcomp (hm, hu) = prj1 (hm, hu) = hm   
    hcomp (hu, hm) = prj2 (hu, hm) = hm 
    (hm1 * hm2) * hm3 ~> hm1 * (hm2 * hm3)
@@ -1921,12 +1929,6 @@ HB.mixin Record IsDCat_UA T of CFunctor T := {
                        (@HO T (@hhom T) a0 a3 hh1)
 }. 
 *)
-(*
-Class pip (Y: Type) := {}.
-Class pip2 (T: Type) := {}.
-
-Instance pipO (T1 T2: Type) : pip T1 -> pip T2 -> pip2 (T1 + T2)%type. 
-*)
 
 (*********************************************************************)
 
@@ -2182,3 +2184,5 @@ Program Definition pb_cat (A B: cat) (H: cospan A B) : cat.
   destruct c as [a1 a2 a3].
   econstructor.  
 *)  
+
+