diff -r 4eb6407c6ca3 Adjoint.v
--- a/Adjoint.v	Fri May 24 20:09:37 2013 -0400
+++ b/Adjoint.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,8 +11,8 @@
 Set Universe Polymorphism.
 
 Section Adjunction.
-  Context `{C : @SpecializedCategory objC}.
-  Context `{D : @SpecializedCategory objD}.
+  Context `{C : SpecializedCategory}.
+  Context `{D : SpecializedCategory}.
   Variable F : SpecializedFunctor C D.
   Variable G : SpecializedFunctor D C.
 
@@ -97,7 +97,7 @@
     simpl in *.
     match goal with
       | [ H : Compose ?x (?T ?A ?A') = Identity _ |- Compose _ ?x = _ ]
-        => eapply (@iso_is_epi _ _ _ _ (T A A')); [
+        => eapply (@iso_is_epi _ _ _ (T A A')); [
           exists x; hnf; eauto
           |
             repeat rewrite Associativity; find_composition_to_identity (* slow, but I don't have a better way to do it *); rewrite RightIdentity
@@ -105,7 +105,7 @@
     end.
     match goal with
       | [ H : Compose (?T ?A ?A') ?x = Identity _ |- _ = Compose ?x _ ]
-        => eapply (@iso_is_mono _ _ _ _ (T A A')); [
+        => eapply (@iso_is_mono _ _ _ (T A A')); [
           exists x; hnf; eauto
           |
             repeat rewrite <- Associativity; find_composition_to_identity; rewrite LeftIdentity
@@ -116,12 +116,12 @@
   Defined.
 End Adjunction.
 
-Arguments AComponentsOf {objC C objD D} [F G] T A A' _ : simpl nomatch.
-Arguments AIsomorphism {objC C objD D} [F G] T A A' : simpl nomatch.
+Arguments AComponentsOf {C D} [F G] T A A' _ : simpl nomatch.
+Arguments AIsomorphism {C D} [F G] T A A' : simpl nomatch.
 
 Section AdjunctionEquivalences.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor C D.
   Variable G : SpecializedFunctor D C.
 
@@ -134,7 +134,7 @@
     match goal with
       | [ |- SpecializedNaturalTransformation ?F ?G ] =>
         refine (Build_SpecializedNaturalTransformation F G
-          (fun cd : objC * objD => A.(AComponentsOf) (fst cd) (snd cd))
+          (fun cd : C * D => A.(AComponentsOf) (fst cd) (snd cd))
           _
         )
     end.
diff -r 4eb6407c6ca3 AdjointComposition.v
--- a/AdjointComposition.v	Fri May 24 20:09:37 2013 -0400
+++ b/AdjointComposition.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,9 +10,9 @@
 Set Universe Polymorphism.
 
 Section compose.
-  Context `(C : SpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
-  Context `(E : SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
 
   Variable F : SpecializedFunctor C D.
   Variable F' : SpecializedFunctor D E.
diff -r 4eb6407c6ca3 AdjointPointwise.v
--- a/AdjointPointwise.v	Fri May 24 20:09:37 2013 -0400
+++ b/AdjointPointwise.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,11 +10,11 @@
 Set Universe Polymorphism.
 
 Section AdjointPointwise.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
-  Context `(C' : @SpecializedCategory objC').
-  Context `(D' : @SpecializedCategory objD').
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
+  Context `(C' : SpecializedCategory).
+  Context `(D' : SpecializedCategory).
 
   Variable F : SpecializedFunctor C D.
   Variable G : SpecializedFunctor D C.
diff -r 4eb6407c6ca3 AdjointUniversalMorphisms.v
--- a/AdjointUniversalMorphisms.v	Fri May 24 20:09:37 2013 -0400
+++ b/AdjointUniversalMorphisms.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,8 +10,8 @@
 Set Universe Polymorphism.
 
 Section AdjunctionUniversal.
-  Context `{C : @SpecializedCategory objC}.
-  Context `{D : @SpecializedCategory objD}.
+  Context `{C : SpecializedCategory}.
+  Context `{D : SpecializedCategory}.
   Variable F : SpecializedFunctor C D.
   Variable G : SpecializedFunctor D C.
 
@@ -80,8 +80,8 @@
 End AdjunctionUniversal.
 
 Section AdjunctionFromUniversal.
-  Context `{C : @SpecializedCategory objC}.
-  Context `{D : @SpecializedCategory objD}.
+  Context `{C : SpecializedCategory}.
+  Context `{D : SpecializedCategory}.
 
   Local Ltac diagonal_transitivity_pre_then tac :=
     repeat rewrite AssociativityNoEvar by noEvar;
diff -r 4eb6407c6ca3 BoolCategory.v
--- a/BoolCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/BoolCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -29,8 +29,8 @@
   Global Arguments BoolCat_Compose [s d d'] m1 m2 : simpl never.
   Global Arguments BoolCat_Identity x : simpl never.
 
-  Definition BoolCat : @SpecializedCategory bool.
-    refine (@Build_SpecializedCategory _
+  Definition BoolCat : SpecializedCategory.
+    refine (@Build_SpecializedCategory bool
                                        mor
                                        BoolCat_Identity
                                        BoolCat_Compose
diff -r 4eb6407c6ca3 CanonicalStructureSimplification.v
--- a/CanonicalStructureSimplification.v	Fri May 24 20:09:37 2013 -0400
+++ b/CanonicalStructureSimplification.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,7 +11,7 @@
 
 Section SimplifiedMorphism.
   Section single_category.
-    Context `{C : SpecializedCategory objC}.
+    Context `{C : SpecializedCategory}.
 
     (* structure for packaging a morphism and its reification *)
 
@@ -52,13 +52,13 @@
                  reflexivity.
 
   Section more_single_category.
-    Context `{C : SpecializedCategory objC}.
+    Context `{C : SpecializedCategory}.
 
     Lemma reifyIdentity x : Identity x = ReifiedMorphismDenote (ReifiedIdentityMorphism C x). reflexivity. Qed.
     Canonical Structure reify_identity_morphism x := ReifyMorphism (identity_tag _) _ (reifyIdentity x).
 
     Lemma reifyCompose s d d'
-          `(m1' : @SimplifiedMorphism objC C d d') `(m2' : @SimplifiedMorphism objC C s d)
+          `(m1' : @SimplifiedMorphism C d d') `(m2' : @SimplifiedMorphism C s d)
     : Compose (untag (morphism_of m1')) (untag (morphism_of m2'))
       = ReifiedMorphismDenote (ReifiedComposedMorphism (reified_morphism_of m1') (reified_morphism_of m2')).
       t.
@@ -67,11 +67,11 @@
   End more_single_category.
 
   Section functor.
-    Context `{C : SpecializedCategory objC}.
-    Context `{D : SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
     Variable F : SpecializedFunctor C D.
 
-    Lemma reifyFunctor `(m' : @SimplifiedMorphism objC C s d)
+    Lemma reifyFunctor `(m' : @SimplifiedMorphism C s d)
     : MorphismOf F (untag (morphism_of m')) = ReifiedMorphismDenote (ReifiedFunctorMorphism F (reified_morphism_of m')).
       t.
     Qed.
@@ -79,8 +79,8 @@
   End functor.
 
   Section natural_transformation.
-    Context `{C : SpecializedCategory objC}.
-    Context `{D : SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
     Variables F G : SpecializedFunctor C D.
     Variable T : SpecializedNaturalTransformation F G.
 
@@ -88,7 +88,7 @@
     Canonical Structure reify_nt_morphism x := ReifyMorphism (nt_tag _) _ (@reifyNT x).
   End natural_transformation.
   Section generic.
-    Context `{C : SpecializedCategory objC}.
+    Context `{C : SpecializedCategory}.
 
     Lemma reifyGeneric s d (m : Morphism C s d) : m = ReifiedMorphismDenote (ReifiedGenericMorphism C s d m). reflexivity. Qed.
     Canonical Structure reify_generic_morphism s d m := ReifyMorphism (generic_tag m) _ (@reifyGeneric s d m).
@@ -113,8 +113,8 @@
 (*******************************************************************************)
 Section good_examples.
   Section id.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objC).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
     Variables F G : SpecializedFunctor C D.
     Variable T : SpecializedNaturalTransformation F G.
 
@@ -143,9 +143,9 @@
 Section bad_examples.
   Require Import SumCategory.
   Section bad_example_0001.
-    Context `(C0 : SpecializedCategory objC0).
-    Context `(C1 : SpecializedCategory objC1).
-    Context `(D : SpecializedCategory objD).
+    Context `(C0 : SpecializedCategory).
+    Context `(C1 : SpecializedCategory).
+    Context `(D : SpecializedCategory).
 
     Variables s d d' : C0.
     Variable m1 : Morphism C0 s d.
diff -r 4eb6407c6ca3 Category.v
--- a/Category.v	Fri May 24 20:09:37 2013 -0400
+++ b/Category.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,21 +10,15 @@
 Set Universe Polymorphism.
 
 Record > Category := {
-  CObject : Type;
-
-  UnderlyingCategory :> @SpecializedCategory CObject
+  UnderlyingCategory :> SpecializedCategory
 }.
 
 Record > SmallCategory := {
-  SObject : Set;
-
-  SUnderlyingCategory :> @SmallSpecializedCategory SObject
+  SUnderlyingCategory :> SmallSpecializedCategory
 }.
 
 Record > LocallySmallCategory := {
-  LSObject : Type;
-
-  LSUnderlyingCategory :> @LocallySmallSpecializedCategory LSObject
+  LSUnderlyingCategory :> LocallySmallSpecializedCategory
 }.
 
 Bind Scope category_scope with Category.
diff -r 4eb6407c6ca3 CategoryEquality.v
--- a/CategoryEquality.v	Fri May 24 20:09:37 2013 -0400
+++ b/CategoryEquality.v	Sat Jun 22 12:51:34 2013 -0400
@@ -16,8 +16,8 @@
   Lemma Category_eq : forall (A B : Category),
     Object A = Object B
     -> Morphism A == Morphism B
-    -> @Identity _ A == @Identity _ B
-    -> @Compose _ A == @Compose _ B
+    -> @Identity A == @Identity B
+    -> @Compose A == @Compose B
     -> A = B.
     unfold Object, Morphism, Identity, Compose; intros;
     destruct_type @Category; destruct_type @SpecializedCategory; simpl in *;
@@ -26,24 +26,24 @@
   Qed.
 
   Lemma SmallCategory_eq : forall (A B : SmallCategory),
-    SObject A = SObject B
+    Object A = Object B
     -> Morphism A == Morphism B
-    -> @Identity _ A == @Identity _ B
-    -> @Compose _ A == @Compose _ B
+    -> @Identity A == @Identity B
+    -> @Compose A == @Compose B
     -> A = B.
-    unfold SObject, Morphism, Identity, Compose; intros;
+    unfold Object, Morphism, Identity, Compose; intros;
     destruct_type @SmallCategory; destruct_type @SmallSpecializedCategory; simpl in *;
     subst_body; repeat (subst; JMeq_eq).
     repeat f_equal; apply proof_irrelevance.
   Qed.
 
   Lemma LocallySmallCategory_eq : forall (A B : LocallySmallCategory),
-    LSObject A = LSObject B
+    Object A = Object B
     -> Morphism A == Morphism B
-    -> @Identity _ A == @Identity _ B
-    -> @Compose _ A == @Compose _ B
+    -> @Identity A == @Identity B
+    -> @Compose A == @Compose B
     -> A = B.
-    unfold LSObject, Morphism, Identity, Compose; intros;
+    unfold Object, Morphism, Identity, Compose; intros;
     destruct_type @LocallySmallCategory; destruct_type @LocallySmallSpecializedCategory; simpl in *;
     subst_body; repeat (subst; JMeq_eq).
     repeat f_equal; apply proof_irrelevance.
@@ -61,14 +61,14 @@
 Ltac cat_eq := cat_eq_with idtac.
 
 Section RoundtripCat.
-  Context `(C : @SpecializedCategory obj).
+  Context `(C : SpecializedCategory).
   Variable C' : Category.
 
-  Lemma SpecializedCategory_Category_SpecializedCategory_Id : ((C : Category) : SpecializedCategory _) = C.
+  Lemma SpecializedCategory_Category_SpecializedCategory_Id : ((C : Category) : SpecializedCategory) = C.
     spcat_eq.
   Qed.
 
-  Lemma Category_SpecializedCategory_Category_Id : ((C' : SpecializedCategory _) : Category) = C'.
+  Lemma Category_SpecializedCategory_Category_Id : ((C' : SpecializedCategory) : Category) = C'.
     cat_eq.
   Qed.
 End RoundtripCat.
@@ -76,14 +76,14 @@
 Hint Rewrite @SpecializedCategory_Category_SpecializedCategory_Id @Category_SpecializedCategory_Category_Id : category.
 
 Section RoundtripLSCat.
-  Context `(C : @LocallySmallSpecializedCategory obj).
+  Context `(C : @LocallySmallSpecializedCategory).
   Variable C' : LocallySmallCategory.
 
-  Lemma LocallySmall_SpecializedCategory_Category_SpecializedCategory_Id : ((C : LocallySmallCategory) : LocallySmallSpecializedCategory _) = C.
+  Lemma LocallySmall_SpecializedCategory_Category_SpecializedCategory_Id : ((C : LocallySmallCategory) : LocallySmallSpecializedCategory) = C.
     spcat_eq.
   Qed.
 
-  Lemma LocallySmall_Category_SpecializedCategory_Category_Id : ((C' : LocallySmallSpecializedCategory _) : LocallySmallCategory) = C'.
+  Lemma LocallySmall_Category_SpecializedCategory_Category_Id : ((C' : LocallySmallSpecializedCategory) : LocallySmallCategory) = C'.
     cat_eq.
   Qed.
 End RoundtripLSCat.
@@ -91,14 +91,15 @@
 Hint Rewrite @LocallySmall_SpecializedCategory_Category_SpecializedCategory_Id LocallySmall_Category_SpecializedCategory_Category_Id : category.
 
 Section RoundtripSCat.
-  Context `(C : @SmallSpecializedCategory obj).
+  Context `(C : @SmallSpecializedCategory).
   Variable C' : SmallCategory.
 
-  Lemma Small_SpecializedCategory_Category_SpecializedCategory_Id : ((C : SmallCategory) : SmallSpecializedCategory _) = C.
+  Lemma Small_SpecializedCategory_Category_SpecializedCategory_Id : ((C : SmallCategory) : SmallSpecializedCategory) = C.
     spcat_eq.
   Qed.
 
-  Lemma Small_Category_SpecializedCategory_Category_Id : ((C' : SmallSpecializedCategory _) : SmallCategory) = C'.
+
+  Lemma Small_Category_SpecializedCategory_Category_Id : ((C' : SmallSpecializedCategory) : SmallCategory) = C'.
     cat_eq.
   Qed.
 End RoundtripSCat.
diff -r 4eb6407c6ca3 CategoryIsomorphisms.v
--- a/CategoryIsomorphisms.v	Fri May 24 20:09:37 2013 -0400
+++ b/CategoryIsomorphisms.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,7 +11,7 @@
 Set Universe Polymorphism.
 
 Section Category.
-  Context `{C : @SpecializedCategory obj}.
+  Context `{C : SpecializedCategory}.
 
   (* [m'] is the inverse of [m] if both compositions are
      equivalent to the relevant identity morphisms. *)
@@ -200,12 +200,12 @@
 
 Ltac eapply_by_compose H :=
   match goal with
-    | [ |- @eq (@Morphism ?obj ?mor ?C) _ _ ] => eapply (H obj mor C)
-    | [ |- @Compose ?obj ?mor ?C _ _ _ _ _ = _ ] => eapply (H obj mor C)
-    | [ |- _ = @Compose ?obj ?mor ?C _ _ _ _ _ ] => eapply (H obj mor C)
+    | [ |- @eq (@Morphism ?C) _ _ ] => eapply (H C)
+    | [ |- @Compose ?C _ _ _ _ _ = _ ] => eapply (H C)
+    | [ |- _ = @Compose ?C _ _ _ _ _ ] => eapply (H C)
     | _ => eapply H
-    | [ C : @SpecializedCategory ?obj ?mor |- _ ] => eapply (H obj mor C)
-    | [ C : ?T |- _ ] => match eval hnf in T with | @SpecializedCategory ?obj ?mor => eapply (H obj mor C) end
+    | [ C : SpecializedCategory |- _ ] => eapply (H C)
+    | [ C : ?T |- _ ] => match eval hnf in T with | SpecializedCategory => eapply (H C) end
   end.
 
 Ltac solve_isomorphism := destruct_hypotheses;
@@ -229,7 +229,7 @@
   [ solve_isomorphism | ].
 
 Section CategoryObjects1.
-  Context `(C : @SpecializedCategory obj).
+  Context `(C : SpecializedCategory).
 
   Definition UniqueUpToUniqueIsomorphism' (P : C.(Object) -> Prop) : Prop :=
     forall o, P o -> forall o', P o' -> exists m : C.(Morphism) o o', IsIsomorphism m /\ is_unique m.
@@ -247,7 +247,7 @@
 
     Record TerminalObject :=
       {
-        TerminalObject_Object' : obj;
+        TerminalObject_Object' : C;
         TerminalObject_Morphism : forall o, Morphism C o TerminalObject_Object';
         TerminalObject_Property : forall o, is_unique (TerminalObject_Morphism o)
       }.
@@ -276,7 +276,7 @@
 
     Record InitialObject :=
       {
-        InitialObject_Object' :> obj;
+        InitialObject_Object' :> C;
         InitialObject_Morphism : forall o, Morphism C InitialObject_Object' o;
         InitialObject_Property : forall o, is_unique (InitialObject_Morphism o)
       }.
@@ -296,14 +296,14 @@
   End initial.
 End CategoryObjects1.
 
-Arguments UniqueUpToUniqueIsomorphism {_ C} P.
-Arguments IsInitialObject' {_ C} o.
-Arguments IsInitialObject {_ C} o.
-Arguments IsTerminalObject' {_ C} o.
-Arguments IsTerminalObject {_ C} o.
+Arguments UniqueUpToUniqueIsomorphism {C} P.
+Arguments IsInitialObject' {C} o.
+Arguments IsInitialObject {C} o.
+Arguments IsTerminalObject' {C} o.
+Arguments IsTerminalObject {C} o.
 
 Section CategoryObjects2.
-  Context `(C : @SpecializedCategory obj).
+  Context `(C : SpecializedCategory).
 
   Ltac unique := hnf; intros; specialize_all_ways; destruct_sig;
     unfold is_unique, unique, uniqueness in *;
diff -r 4eb6407c6ca3 ChainCategory.v
--- a/ChainCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/ChainCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,8 +9,8 @@
 Set Universe Polymorphism.
 
 Section ChainCat.
-  Definition OmegaCategory : @SpecializedCategory nat.
-    refine (@Build_SpecializedCategory _
+  Definition OmegaCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory nat
                                        le
                                        le_refl
                                        (fun _ _ _ H0 H1 => le_trans H1 H0)
@@ -20,7 +20,7 @@
     abstract (intros; apply proof_irrelevance).
   Defined.
 
-  Let ChainCategory' n : @SpecializedCategory { m | m <= n }.
+  Let ChainCategory' (n : nat) : SpecializedCategory.
     simpl_definition_by_tac_and_exact (FullSubcategory OmegaCategory (fun m => m <= n)) ltac:(unfold Subcategory in *).
   Defined.
   Definition ChainCategory n := Eval cbv beta iota zeta delta [ChainCategory'] in ChainCategory' n.
diff -r 4eb6407c6ca3 Coend.v
--- a/Coend.v	Fri May 24 20:09:37 2013 -0400
+++ b/Coend.v	Sat Jun 22 12:51:34 2013 -0400
@@ -37,21 +37,27 @@
      ]]
      where the triangles denote induced colimit morphisms.
      *)
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Let COp := OppositeCategory C.
 
   Variable F : SpecializedFunctor (COp * C) D.
 
-  Let MorC := @MorphismFunctor _ _ (fun _ : unit => C) tt. (* [((c0, c1) & f : morC c0 c1)], the set of morphisms of C *)
+  Let MorC := @MorphismFunctor _ (fun _ : unit => C) tt. (* [((c0, c1) & f : morC c0 c1)], the set of morphisms of C *)
 
   Variable Fmor : ∐_{ c0c1f : MorC } (F (snd (projT1 c0c1f), fst (projT1 c0c1f)) : D).
   Variable Fob : ∐_{ c } (F (c, c) : D).
 
   (* There is a morphism in D from [Fmor] to [Fob] which takes the domain of the relevant morphism. *)
   Definition Coend_Fdom : Morphism D (ColimitObject Fmor) (ColimitObject Fob).
-    apply (InducedColimitMap (G := InducedDiscreteFunctor _ (DomainNaturalTransformation _ (fun _ => C) tt))).
+    refine (InducedColimitMap (D := D)
+                              (F1 := InducedDiscreteFunctor D _)
+                              (F2 := InducedDiscreteFunctor D (fun c : COp => F (c, c)))
+                              (G := InducedDiscreteFunctor (DiscreteCategory COp) (DomainNaturalTransformation (fun _ : unit => C) tt))
+                              _
+                              Fmor
+                              Fob);
     hnf; simpl.
     match goal with
       | [ |- SpecializedNaturalTransformation ?F0 ?G0 ] =>
@@ -65,7 +71,7 @@
 
   (* There is a morphism in D from [Fmor] to [Fob] which takes the codomain of the relevant morphism. *)
   Definition Coend_Fcod : Morphism D (ColimitObject Fmor) (ColimitObject Fob).
-    apply (InducedColimitMap (G := InducedDiscreteFunctor _ (CodomainNaturalTransformation _ (fun _ => C) tt))).
+    apply (InducedColimitMap (G := InducedDiscreteFunctor (DiscreteCategory COp) (CodomainNaturalTransformation (fun _ => C) tt))).
     hnf; simpl.
     match goal with
       | [ |- SpecializedNaturalTransformation ?F0 ?G0 ] =>
diff -r 4eb6407c6ca3 CoendFunctor.v
--- a/CoendFunctor.v	Fri May 24 20:09:37 2013 -0400
+++ b/CoendFunctor.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,11 +13,11 @@
 Local Open Scope type_scope.
 
 Section Coend.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Let COp := OppositeCategory C.
 
-  Definition CoendFunctor_Index_Object := { ds : objC * objC & Morphism C (snd ds) (fst ds) } + objC.
+  Definition CoendFunctor_Index_Object := { ds : C * C & Morphism C (snd ds) (fst ds) } + C.
 
   Global Arguments CoendFunctor_Index_Object /.
 
@@ -52,9 +52,9 @@
     end.
   Defined.
 
-  Definition CoendFunctor_Index : SpecializedCategory CoendFunctor_Index_Object.
+  Definition CoendFunctor_Index : SpecializedCategory.
   Proof.
-    refine (@Build_SpecializedCategory _
+    refine (@Build_SpecializedCategory CoendFunctor_Index_Object
                                        CoendFunctor_Index_Morphism
                                        CoendFunctor_Index_Identity
                                        CoendFunctor_Index_Compose
@@ -133,8 +133,8 @@
 End Coend.
 
 Section CoendFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Let COp := OppositeCategory C.
 
diff -r 4eb6407c6ca3 CommaCategory.v
--- a/CommaCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/CommaCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,7 +12,7 @@
 
 Local Ltac fold_functor := idtac. (*
   change CObject with (fun C => @Object (CObject C) C) in *;
-    change (@SpecializedFunctor) with (fun objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD) => @Functor C D) in *. *)
+    change (@SpecializedFunctor) with (fun objC (C : SpecializedCategory) objD (D : SpecializedCategory) => @Functor C D) in *. *)
 
 Section CommaCategory.
   (* [Definition]s are not sort-polymorphic, and it's too slow to not use
diff -r 4eb6407c6ca3 CommaCategoryFunctorProperties.v
--- a/CommaCategoryFunctorProperties.v	Fri May 24 20:09:37 2013 -0400
+++ b/CommaCategoryFunctorProperties.v	Sat Jun 22 12:51:34 2013 -0400
@@ -35,9 +35,9 @@
          end.
 
 Section FCompositionOf.
-  Context `(A : @SpecializedCategory objA).
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
+  Context `(A : SpecializedCategory).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
 
   Lemma CommaCategoryInducedFunctor_FCompositionOf s d d'
         (m1 : Morphism ((OppositeCategory (C ^ A)) * (C ^ B)) s d)
@@ -47,7 +47,7 @@
     Time slice_t. (* 44 s *)
   Qed.
 
-  Lemma CommaCategoryInducedFunctor_FIdentityOf (x : (OppositeCategory (C ^ A)) * (C ^ B)) :
+  Lemma CommaCategoryInducedFunctor_FIdentityOf (x : Object ((OppositeCategory (C ^ A)) * (C ^ B))) :
     CommaCategoryInducedFunctor (Identity x)
     = IdentityFunctor _.
     Time slice_t. (* 11 s *)
diff -r 4eb6407c6ca3 CommaCategoryInducedFunctors.v
--- a/CommaCategoryInducedFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/CommaCategoryInducedFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -76,9 +76,9 @@
   repeat induced_step.
 
 Section CommaCategoryInducedFunctor.
-  Context `(A : @SpecializedCategory objA).
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
+  Context `(A : SpecializedCategory).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
 
   Let CommaCategoryInducedFunctor_ObjectOf s d (m : Morphism ((OppositeCategory (C ^ A)) * (C ^ B)) s d)
       (x : fst s ↓ snd s) : (fst d ↓ snd d)
@@ -121,10 +121,10 @@
 End CommaCategoryInducedFunctor.
 
 Section SliceCategoryInducedFunctor.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Section Slice_Coslice.
-    Context `(D : @SpecializedCategory objD).
+    Context `(D : SpecializedCategory).
 
     (* TODO(jgross): See if this can be recast as an exponential law functor about how Cat ^ 1 is isomorphic to Cat, or something *)
     Definition SliceCategoryInducedFunctor_NT s d (m : Morphism D s d) :
diff -r 4eb6407c6ca3 CommaCategoryProjection.v
--- a/CommaCategoryProjection.v	Fri May 24 20:09:37 2013 -0400
+++ b/CommaCategoryProjection.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,9 +12,9 @@
 Local Open Scope category_scope.
 
 Section CommaCategory.
-  Context `(A : @SpecializedCategory objA).
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
+  Context `(A : SpecializedCategory).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
   Variable S : SpecializedFunctor A C.
   Variable T : SpecializedFunctor B C.
 
@@ -27,7 +27,7 @@
 End CommaCategory.
 
 Section SliceCategory.
-  Context `(A : @SpecializedCategory objA).
+  Context `(A : SpecializedCategory).
 
   Local Arguments ComposeFunctors' / .
 
@@ -41,7 +41,7 @@
     := ComposeFunctors' snd_Functor (CommaCategoryProjection _ (IdentityFunctor A)).
 
   Section Slice_Coslice.
-    Context `(C : @SpecializedCategory objC).
+    Context `(C : SpecializedCategory).
     Variable a : C.
     Variable S : SpecializedFunctor A C.
 
diff -r 4eb6407c6ca3 CommaCategoryProjectionFunctors.v
--- a/CommaCategoryProjectionFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/CommaCategoryProjectionFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -36,7 +36,6 @@
   destruct_head_hnf @CommaSpecializedCategory_Object;
   destruct_sig;
   subst_body;
-  unfold Object in *;
   simpl in *;
   trivial.
 
@@ -68,7 +67,6 @@
         end).
 
 Local Ltac induced_anihilate :=
-  unfold Object in *;
   simpl in *;
   destruct_head @prod;
   simpl in *;
@@ -76,23 +74,23 @@
   repeat induced_step.
 
 Section CommaCategoryProjectionFunctor.
-  Context `(A : LocallySmallSpecializedCategory objA).
-  Context `(B : LocallySmallSpecializedCategory objB).
-  Context `(C : SpecializedCategory objC).
+  Context `(A : LocallySmallSpecializedCategory).
+  Context `(B : LocallySmallSpecializedCategory).
+  Context `(C : SpecializedCategory).
 
   Definition CommaCategoryProjectionFunctor_ObjectOf (ST : (OppositeCategory (C ^ A)) * (C ^ B)) :
-    LocallySmallCat / (A * B : LocallySmallSpecializedCategory _)
+    LocallySmallCat / (A * B : LocallySmallSpecializedCategory)
     := let S := (fst ST) in
        let T := (snd ST) in
        existT _
-              ((S ↓ T : LocallySmallSpecializedCategory _) : LocallySmallCategory, tt)
+              ((S ↓ T : LocallySmallSpecializedCategory) : LocallySmallCategory, tt)
               (CommaCategoryProjection S T) :
          CommaSpecializedCategory_ObjectT (IdentityFunctor _)
                                           (FunctorFromTerminal LocallySmallCat
-                                                               (A * B : LocallySmallSpecializedCategory _)).
+                                                               (A * B : LocallySmallSpecializedCategory)).
 
   Definition CommaCategoryProjectionFunctor_MorphismOf s d (m : Morphism ((OppositeCategory (C ^ A)) * (C ^ B)) s d) :
-    Morphism (LocallySmallCat / (A * B : LocallySmallSpecializedCategory _))
+    Morphism (LocallySmallCat / (A * B : LocallySmallSpecializedCategory))
              (CommaCategoryProjectionFunctor_ObjectOf s)
              (CommaCategoryProjectionFunctor_ObjectOf d).
     hnf in *; constructor; simpl in *.
@@ -112,7 +110,7 @@
   Qed.
 
   Lemma CommaCategoryProjectionFunctor_FCompositionOf s d d' m m' :
-    CommaCategoryProjectionFunctor_MorphismOf (@Compose _ _ s d d' m m')
+    CommaCategoryProjectionFunctor_MorphismOf (Compose (s := s) (d := d) (d' := d') m m')
     = Compose (CommaCategoryProjectionFunctor_MorphismOf m)
               (CommaCategoryProjectionFunctor_MorphismOf m').
     (* admit. *) Time (expand; anihilate). (* 57 s  :-( :-( *)
@@ -120,9 +118,9 @@
 
   Definition CommaCategoryProjectionFunctor :
     SpecializedFunctor ((OppositeCategory (C ^ A)) * (C ^ B))
-                       (LocallySmallCat / (A * B : LocallySmallSpecializedCategory _)).
+                       (LocallySmallCat / (A * B : LocallySmallSpecializedCategory)).
     refine (Build_SpecializedFunctor ((OppositeCategory (C ^ A)) * (C ^ B))
-                                     (LocallySmallCat / (A * B : LocallySmallSpecializedCategory _))
+                                     (LocallySmallCat / (A * B : LocallySmallSpecializedCategory))
                                      CommaCategoryProjectionFunctor_ObjectOf
                                      CommaCategoryProjectionFunctor_MorphismOf
                                      _
@@ -134,8 +132,8 @@
 End CommaCategoryProjectionFunctor.
 
 Section SliceCategoryProjectionFunctor.
-  Context `(C : LocallySmallSpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
+  Context `(C : LocallySmallSpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Local Arguments ExponentialLaw4Functor_Inverse_ObjectOf_ObjectOf / .
   Local Arguments ComposeFunctors / .
@@ -153,9 +151,9 @@
 *)
 
   Definition SliceCategoryProjectionFunctor_pre_pre'
-    := Eval hnf in (LocallySmallCatOverInducedFunctor (ProductLaw1Functor C : Morphism LocallySmallCat (C * 1 : LocallySmallSpecializedCategory _) C)).
+    := Eval hnf in (LocallySmallCatOverInducedFunctor (ProductLaw1Functor C : Morphism LocallySmallCat (C * 1 : LocallySmallSpecializedCategory) C)).
 
-  Definition SliceCategoryProjectionFunctor_pre_pre : SpecializedFunctor (LocallySmallCat / (C * 1 : LocallySmallSpecializedCategory _)) (LocallySmallCat / C).
+  Definition SliceCategoryProjectionFunctor_pre_pre : SpecializedFunctor (LocallySmallCat / (C * 1 : LocallySmallSpecializedCategory)) (LocallySmallCat / C).
     functor_abstract_trailing_props SliceCategoryProjectionFunctor_pre_pre'.
   Defined.
 
@@ -180,14 +178,14 @@
   Definition SliceCategoryProjectionFunctor_pre' : ((LocallySmallCat / C) ^ (D * (OppositeCategory (D ^ C)))).
     refine (ComposeFunctors _ ((ExponentialLaw1Functor_Inverse D) * IdentityFunctor (OppositeCategory (D ^ C)))).
     refine (ComposeFunctors _ (SwapFunctor _ _)).
-    refine (ComposeFunctors _ (CommaCategoryProjectionFunctor (C : LocallySmallSpecializedCategory _) (1 : LocallySmallSpecializedCategory _) D)).
+    refine (ComposeFunctors _ (CommaCategoryProjectionFunctor (C : LocallySmallSpecializedCategory) (1 : LocallySmallSpecializedCategory) D)).
     (*
     refine_right_compose_functor_by_abstract ((ExponentialLaw1Functor_Inverse D) * IdentityFunctor (OppositeCategory (D ^ C)))%functor.
     refine_right_compose_functor_by_abstract (SwapFunctor (D ^ 1)%functor (OppositeCategory (D ^ C)%functor)).
-    refine_right_compose_functor_by_abstract (CommaCategoryProjectionFunctor (C : LocallySmallSpecializedCategory _) (1 : LocallySmallSpecializedCategory _) D).*)
+    refine_right_compose_functor_by_abstract (CommaCategoryProjectionFunctor (C : LocallySmallSpecializedCategory) (1 : LocallySmallSpecializedCategory) D).*)
     let F := (eval hnf in SliceCategoryProjectionFunctor_pre_pre) in
     exact F.
-(* (LocallySmallCatOverInducedFunctor (ProductLaw1Functor C : Morphism LocallySmallCat (C * 1 : LocallySmallSpecializedCategory _) (C : LocallySmallSpecializedCategory _))). *)
+(* (LocallySmallCatOverInducedFunctor (ProductLaw1Functor C : Morphism LocallySmallCat (C * 1 : LocallySmallSpecializedCategory) (C : LocallySmallSpecializedCategory))). *)
   Defined.
 
   Definition SliceCategoryProjectionFunctor_pre'' : ((LocallySmallCat / C) ^ (D * (OppositeCategory (D ^ C)))).
@@ -212,7 +210,7 @@
   Definition CosliceCategoryProjectionFunctor : ((LocallySmallCat / C) ^ (OppositeCategory D)) ^ (D ^ C).
     refine ((ExponentialLaw4Functor_Inverse _ _ _) _).
     refine (ComposeFunctors _ ((OppositeFunctor (ExponentialLaw1Functor_Inverse D)) * IdentityFunctor (D ^ C))).
-    refine (ComposeFunctors _ (CommaCategoryProjectionFunctor (1 : LocallySmallSpecializedCategory _) (C : LocallySmallSpecializedCategory _) D)).
+    refine (ComposeFunctors _ (CommaCategoryProjectionFunctor (1 : LocallySmallSpecializedCategory) (C : LocallySmallSpecializedCategory) D)).
     refine (LocallySmallCatOverInducedFunctor _).
     refine (ComposeFunctors _ (SwapFunctor _ _)).
     exact (ProductLaw1Functor _).
diff -r 4eb6407c6ca3 ComputableCategory.v
--- a/ComputableCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/ComputableCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,13 +9,12 @@
 
 Section ComputableCategory.
   Variable I : Type.
-  Variable Index2Object : I -> Type.
-  Variable Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i).
+  Variable Index2Cat : I -> SpecializedCategory.
 
   Local Coercion Index2Cat : I >-> SpecializedCategory.
 
-  Definition ComputableCategory : @SpecializedCategory I.
-    refine (@Build_SpecializedCategory _
+  Definition ComputableCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory I
                                        (fun C D : I => SpecializedFunctor C D)
                                        (fun o : I => IdentityFunctor o)
                                        (fun C D E : I => ComposeFunctors (C := C) (D := D) (E := E))
diff -r 4eb6407c6ca3 ComputableGraphCategory.v
--- a/ComputableGraphCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/ComputableGraphCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -14,7 +14,7 @@
 
   Local Coercion Index2Graph : I >-> Graph.
 
-  Definition ComputableGraphCategory : @SpecializedCategory I.
+  Definition ComputableGraphCategory : SpecializedCategory.
     refine (@Build_SpecializedCategory _
                                        (fun C D : I => GraphTranslation C D)
                                        (fun o : I => IdentityGraphTranslation o)
diff -r 4eb6407c6ca3 ComputableSchemaCategory.v
--- a/ComputableSchemaCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/ComputableSchemaCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -22,7 +22,7 @@
   Hint Rewrite ComposeSmallTranslationsAssociativity.
 
   (* XXX TODO: Automate this better. *)
-  Definition ComputableSchemaCategory : @SpecializedCategory O (fun s d : O => EquivalenceClass (@SmallTranslationsEquivalent s d)).
+  Definition ComputableSchemaCategory : SpecializedCategory (fun s d : O => EquivalenceClass (@SmallTranslationsEquivalent s d)).
     refine (Build_SpecializedCategory (fun s d : O => EquivalenceClass (@SmallTranslationsEquivalent s d))
       (fun o => @classOf _ _ (@SmallTranslationsEquivalent_rel _ _)
         (IdentitySmallTranslation o))
diff -r 4eb6407c6ca3 Correspondences.v
--- a/Correspondences.v	Fri May 24 20:09:37 2013 -0400
+++ b/Correspondences.v	Sat Jun 22 12:51:34 2013 -0400
@@ -72,8 +72,8 @@
      is a functor
      [[M: C^{op} × C' → Set.]]
      *)
-  Context `(C : @SpecializedCategory objC).
-  Context `(C' : @SpecializedCategory objC').
+  Context `(C : SpecializedCategory).
+  Context `(C' : SpecializedCategory).
 
   Let COp := OppositeCategory C.
 
@@ -120,8 +120,8 @@
   (* TODO: Figure out how to get Coq to do automatic type inference
      here, and simplify this proof *)
   (* TODO(jgross): Rewrite fg_equal_in using typeclasses? for speed *)
-  Definition CorrespondenceCategory : @SpecializedCategory (C + C')%type.
-    refine (@Build_SpecializedCategory _
+  Definition CorrespondenceCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory (C + C')%type
                                        CorrespondenceCategory_Morphism
                                        CorrespondenceCategory_Identity
                                        CorrespondenceCategory_Compose
@@ -152,7 +152,7 @@
      {0, 1}, regarded as a category in the obvious way), uniquely
      determined by the condition that [F⁻¹ {0} = C] and [F⁻¹ {1} = C'].
      *)
-  Context `(dummy : @CorrespondenceCategory objC C objC' C' M).
+  Context `(dummy : @CorrespondenceCategory C C' M).
 
   Let CorrespondenceCategoryFunctor_ObjectOf (x : C + C') : Object ([1]) := if x then false else true. (*
     match x with
@@ -191,7 +191,7 @@
      [F : M → [1] ], we can define [C = F⁻¹ {0}], [C' = F⁻¹ {1}], and a
      correspondence [M : C → C'] by the formula
      [M (X, Y) = Hom_{M} (X, Y)]. *)
-  Context `(M : @SpecializedCategory objM).
+  Context `(M : SpecializedCategory).
   Variable F : SpecializedFunctor M ([1]).
 
   (* Comments after these two are for if we want to use [ChainCategory] instead of [BoolCat]. *)
diff -r 4eb6407c6ca3 DataMigrationFunctorExamples.v
--- a/DataMigrationFunctorExamples.v	Fri May 24 20:09:37 2013 -0400
+++ b/DataMigrationFunctorExamples.v	Sat Jun 22 12:51:34 2013 -0400
@@ -256,9 +256,9 @@
         | _ => Empty_set
       end.
 
-    Example C_Category_Ex22 : LocallySmallSpecializedCategory _ := PathsCategory C_Edges_Ex22.
-    Example D_Category_Ex22 : LocallySmallSpecializedCategory _ := PathsCategory D_Edges_Ex22.
-    Example E_Category_Ex22 : LocallySmallSpecializedCategory _ := PathsCategory E_Edges_Ex22.
+    Example C_Category_Ex22 : LocallySmallSpecializedCategory := PathsCategory C_Edges_Ex22.
+    Example D_Category_Ex22 : LocallySmallSpecializedCategory := PathsCategory D_Edges_Ex22.
+    Example E_Category_Ex22 : LocallySmallSpecializedCategory := PathsCategory E_Edges_Ex22.
 
     Example F_Functor_Ex22_ObjectOf (x : C_Objects_Ex22) : D_Objects_Ex22 :=
       match x with
@@ -1088,7 +1088,7 @@
 
         Require Import InitialTerminalCategory ChainCategory DiscreteCategoryFunctors.
 
-        Definition F objC (C : SpecializedCategory objC) : SpecializedFunctor C TerminalCategory.
+        Definition F objC (C : SpecializedCategory) : SpecializedFunctor C TerminalCategory.
           clear.
           eexists; intros; simpl; eauto.
           Grab Existential Variables.
@@ -1096,9 +1096,9 @@
           intros; simpl; eauto.
         Defined.
 
-        Let Π_F_C objC (C : @LocallySmallSpecializedCategory objC) := Eval hnf in
+        Let Π_F_C objC (C : @LocallySmallSpecializedCategory) := Eval hnf in
                              (@RightPushforwardAlong C
-                                                     (TerminalCategory : LocallySmallSpecializedCategory _)
+                                                     (TerminalCategory : LocallySmallSpecializedCategory)
                                                      TypeCat
                                                      (@F objC C)
                                                      (fun (g : SpecializedFunctorToType _) d => @TypeLimit
@@ -1106,14 +1106,14 @@
                                                                                                   _
                                                                                                   (RightPushforwardAlong_pre_Functor
                                                                                                      C
-                                                                                                     (TerminalCategory : LocallySmallSpecializedCategory _)
+                                                                                                     (TerminalCategory : LocallySmallSpecializedCategory)
                                                                                                      TypeCat
                                                                                                      (@F objC C)
                                                                                                      (g : SpecializedFunctorToType _)
                                                                                                      d))).
 
-        Let Π_F_C'_ObjectOf objC C := Eval hnf in @ObjectOf _ _ _ _ (@Π_F_C objC C).
-        Let Π_F_C'_MorphismOf objC C := Eval simpl in @MorphismOf _ _ _ _ (@Π_F_C objC C).
+        Let Π_F_C'_ObjectOf C := Eval hnf in @ObjectOf _ _ _ _ (@Π_F_C objC C).
+        Let Π_F_C'_MorphismOf C := Eval simpl in @MorphismOf _ _ _ _ (@Π_F_C objC C).
 
         Require Import ProofIrrelevance.
 
@@ -1136,16 +1136,16 @@
         Defined.
 
         Let Π_F_01_F F := Eval hnf in
-                           (@RightPushforwardAlong ([0] : LocallySmallSpecializedCategory _)
-                                                   ([1] : LocallySmallSpecializedCategory _)
+                           (@RightPushforwardAlong ([0] : LocallySmallSpecializedCategory)
+                                                   ([1] : LocallySmallSpecializedCategory)
                                                    TypeCat
                                                    F
                                                    (fun (g : SpecializedFunctorToType _) d => @TypeLimit
                                                                                                 _
                                                                                                 _
                                                                                                 (RightPushforwardAlong_pre_Functor
-                                                                                                   ([0] : LocallySmallSpecializedCategory _)
-                                                                                                   ([1] : LocallySmallSpecializedCategory _)
+                                                                                                   ([0] : LocallySmallSpecializedCategory)
+                                                                                                   ([1] : LocallySmallSpecializedCategory)
                                                                                                    TypeCat
                                                                                                    F
                                                                                                    (g : SpecializedFunctorToType _)
@@ -1357,9 +1357,9 @@
 
         Print Π_F_01_F_ObjectOf.
 
-        Example Π_F_C'_ObjectOf objC C g : typeof (@Π_F_C'_ObjectOf objC C g).
+        Example Π_F_C'_ObjectOf C g : typeof (@Π_F_C'_ObjectOf C g).
         Proof.
-          pose (@Π_F_C'_ObjectOf objC C g) as f; hnf in f |- *; revert f; clear; intro.
+          pose (@Π_F_C'_ObjectOf C g) as f; hnf in f |- *; revert f; clear; intro.
           hnf in *.
           unfold Object in *.
           simpl in *.
@@ -1367,7 +1367,7 @@
             InducedLimitFunctors.InducedLimitFunctor_MorphismOf, LimitFunctorTheorems.InducedLimitMap, NTComposeT, NTComposeF in *;
             simpl in *.
         Print Π_F_C'_ObjectOf.
-        Example Π_F_C' objC C : typeof (@Π_F_C objC C).
+        Example Π_F_C' C : typeof (@Π_F_C objC C).
         pose (Π_F_C C) as Π_F_C''.
         hnf in Π_F_C'' |- *.
         revert Π_F_C''; clear; intro.
diff -r 4eb6407c6ca3 DataMigrationFunctors.v
--- a/DataMigrationFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/DataMigrationFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -65,9 +65,9 @@
          end.
 
 Section DataMigrationFunctors.
-  Context `(C : LocallySmallSpecializedCategory objC).
-  Context `(D : LocallySmallSpecializedCategory objD).
-  Context `(S : SpecializedCategory objS).
+  Context `(C : LocallySmallSpecializedCategory).
+  Context `(D : LocallySmallSpecializedCategory).
+  Context `(S : SpecializedCategory).
 
   Section Δ.
     Definition PullbackAlongFunctor : ((S ^ C) ^ (S ^ D)) ^ (D ^ C)
diff -r 4eb6407c6ca3 DataMigrationFunctorsAdjoint.v
--- a/DataMigrationFunctorsAdjoint.v	Fri May 24 20:09:37 2013 -0400
+++ b/DataMigrationFunctorsAdjoint.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,12 +12,12 @@
 (*
 Section coslice_initial.
   (* TODO(jgross): This should go elsewhere *)
-  Definition CosliceSpecializedCategory_InitialObject objC C objD D (F : @SpecializedFunctor objC C objD D) x :
+  Definition CosliceSpecializedCategory_InitialObject C D (F : SpecializedFunctor C D) x :
     { o : _ & @InitialObject _ (CosliceSpecializedCategory (F x) F) o }.
     unfold Object; simpl;
     match goal with
       | [ |- { o : CommaSpecializedCategory_Object ?A ?B & _ } ] =>
-        (exists (existT _ (tt, _) (@Identity _ D _) : CommaSpecializedCategory_ObjectT A B))
+        (exists (existT _ (tt, _) (@Identity D _) : CommaSpecializedCategory_ObjectT A B))
     end;
     simpl.
     intro o'; hnf; simpl.
@@ -134,7 +134,7 @@
                   reflexivity
                 | ];
                 (* do transitivity with the evar'd components *)
-                let A'' := context A'[@Build_SpecializedNaturalTransformation objC C objD D F G CO' Com'] in
+                let A'' := context A'[@Build_SpecializedNaturalTransformation C D F G CO' Com'] in
                 transitivity A''; subst Com' CO'
           end
       end.
@@ -235,7 +235,7 @@
       expand.
       match goal with
         | [ |- @eq (@SpecializedNaturalTransformation ?objC ?C ?objD ?D ?F ?G) _ _ ] =>
-          apply (@NaturalTransformation_eq objC C objD D F G)
+          apply (@NaturalTransformation_eq C D F G)
       end.
       nt_eq.
       assumption.
@@ -249,7 +249,7 @@
       etransitivity.
       mat
       - do 3 match goal with
-               | [ |- @Build_SpecializedNaturalTransformation ?objC ?C ?objD ?D ?F ?G _ _ = _ ] => (apply (@NaturalTransformation_eq objC C objD D F G); simpl) || fail 1 "Cannot apply NaturalTransformation_eq"
+               | [ |- @Build_SpecializedNaturalTransformation ?objC ?C ?objD ?D ?F ?G _ _ = _ ] => (apply (@NaturalTransformation_eq C D F G); simpl) || fail 1 "Cannot apply NaturalTransformation_eq"
                | [ |- appcontext[Build_SpecializedNaturalTransformation] ] => apply f_equal2 || apply f_equal || fail 1 "Cannot apply f_equal"
                | _ => reflexivity
              end.
@@ -859,8 +859,8 @@
       admit.
 
       (*
-      Definition Δ {objC C objD D} := @diagonal_functor_object_of objC C objD D.
-      Definition ΔMor {objC C objD D} o1 o2 := @diagonal_functor_morphism_of objC C objD D o1 o2.
+      Definition Δ {C D} := @diagonal_functor_object_of C D.
+      Definition ΔMor {C D} o1 o2 := @diagonal_functor_morphism_of C D o1 o2.
       Definition limo F x := TerminalMorphism_Object (HasLimits F x).
       Definition φ := TerminalMorphism_Morphism.
       Definition unique_m := @TerminalProperty_Morphism.
@@ -1147,7 +1147,7 @@
       apply functional_extensionality_dep.
       intro.
       Time step.
-      pose (fun I Index2Object Index2Cat objD D C => @FIdentityOf _ _ _ _ (@InducedLimitFunctor I Index2Object Index2Cat objD D C)) as a.
+      pose (fun I Index2Object Index2Cat D C => @FIdentityOf _ _ _ _ (@InducedLimitFunctor I Index2Object Index2Cat D C)) as a.
       unfold InducedLimitFunctor, InducedLimitFunctor_MorphismOf in a; simpl in a.
       unfold RightPushforwardAlong_MorphismOf.
       admit.
@@ -1423,7 +1423,7 @@
       apply functional_extensionality_dep.
       intro.
       Time step.
-      pose (fun I Index2Object Index2Cat objD D C => @FIdentityOf _ _ _ _ (@InducedColimitFunctor I Index2Object Index2Cat objD D C)) as a.
+      pose (fun I Index2Object Index2Cat D C => @FIdentityOf _ _ _ _ (@InducedColimitFunctor I Index2Object Index2Cat D C)) as a.
       unfold InducedColimitFunctor, InducedColimitFunctor_MorphismOf in a; simpl in a.
       unfold LeftPushforwardAlong_MorphismOf.
       admit.
diff -r 4eb6407c6ca3 DecidableComputableCategory.v
--- a/DecidableComputableCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/DecidableComputableCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,11 +10,11 @@
 
 Section ComputableCategory.
   Variable I : Type.
-  Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+  Variable Index2Cat : I -> SpecializedCategory.
 
   Local Coercion Index2Cat : I >-> SpecializedCategory.
 
-  Let eq_dec_on_cat `(C : @SpecializedCategory objC) := forall x y : objC, {x = y} + {x <> y}.
+  Let eq_dec_on_cat `(C : SpecializedCategory) := forall x y : C, {x = y} + {x <> y}.
 
-  Definition ComputableCategoryDec := @SpecializedCategory_sigT_obj _ (@ComputableCategory _ _ Index2Cat) (fun C => eq_dec_on_cat C).
+  Definition ComputableCategoryDec := @SpecializedCategory_sigT_obj (ComputableCategory Index2Cat) (fun C => eq_dec_on_cat C).
 End ComputableCategory.
diff -r 4eb6407c6ca3 DecidableDiscreteCategory.v
--- a/DecidableDiscreteCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/DecidableDiscreteCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -41,8 +41,8 @@
     simpl_eq_dec.
   Defined.
 
-  Definition DiscreteCategoryDec : @SpecializedCategory O.
-    refine (@Build_SpecializedCategory _
+  Definition DiscreteCategoryDec : SpecializedCategory.
+    refine (@Build_SpecializedCategory O
                                        DiscreteCategoryDec_Morphism
                                        DiscreteCategoryDec_Identity
                                        DiscreteCategoryDec_Compose
diff -r 4eb6407c6ca3 DecidableDiscreteCategoryFunctors.v
--- a/DecidableDiscreteCategoryFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/DecidableDiscreteCategoryFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -17,56 +17,32 @@
 End eq_dec_prop.
 
 Section Obj.
-  Local Ltac build_ob_functor Index2Object :=
-    match goal with
-      | [ |- SpecializedFunctor ?C ?D ] =>
-        refine (Build_SpecializedFunctor C D
-          (fun C' => existT _ (Index2Object (projT1 C')) (projT2 C'))
-          (fun _ _ F => ObjectOf F)
-          _
-          _
-        )
-    end;
-    intros; simpl in *; reflexivity.
+  Local Ltac build_ob_functor Index2Cat :=
+    let C := match goal with | [ |- SpecializedFunctor ?C ?D ] => constr:(C) end in
+    let D := match goal with | [ |- SpecializedFunctor ?C ?D ] => constr:(D) end in
+    refine (Build_SpecializedFunctor C D
+                                     (fun C' => existT _ (Object (Index2Cat (projT1 C'))) (projT2 C'))
+                                     (fun _ _ F => ObjectOf F)
+                                     _
+                                     _
+           );
+      intros; simpl in *; reflexivity.
 
   Section type.
     Variable I : Type.
-    Variable Index2Object : I -> Type.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+    Variable Index2Cat : I -> SpecializedCategory.
 
-    Definition ObjectFunctorDec : SpecializedFunctor (@ComputableCategoryDec _ _ Index2Cat) TypeCatDec.
-      build_ob_functor Index2Object.
+    Definition ObjectFunctorDec : SpecializedFunctor (@ComputableCategoryDec _ Index2Cat) TypeCatDec.
+      build_ob_functor Index2Cat.
     Defined.
   End type.
-
-  Section set.
-    Variable I : Type.
-    Variable Index2Object : I -> Set.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
-
-    Definition ObjectFunctorToSetDec : SpecializedFunctor (@ComputableCategoryDec _ _ Index2Cat) SetCatDec.
-      build_ob_functor Index2Object.
-    Defined.
-  End set.
-
-  Section prop.
-    Variable I : Type.
-    Variable Index2Object : I -> Prop.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
-
-    Definition ObjectFunctorToPropDec : SpecializedFunctor (@ComputableCategoryDec _ _ Index2Cat) PropCatDec.
-      build_ob_functor Index2Object.
-    Defined.
-  End prop.
 End Obj.
 
-Arguments ObjectFunctorDec {I Index2Object Index2Cat}.
-Arguments ObjectFunctorToSetDec {I Index2Object Index2Cat}.
-Arguments ObjectFunctorToPropDec {I Index2Object Index2Cat}.
+Arguments ObjectFunctorDec {I Index2Cat}.
 
 Section InducedFunctor.
   Variable O : Type.
-  Context `(O' : @SpecializedCategory obj).
+  Context `(O' : SpecializedCategory).
   Variable f : O -> O'.
   Variable eq_dec : forall x y : O, {x = y} + {x <> y}.
 
@@ -99,7 +75,7 @@
   Hint Unfold DiscreteCategoryDec_Compose.
   Hint Unfold eq_rect_r eq_rect eq_sym.
 
-  Local Arguments Compose {obj} [C s d d'] / _ _ : rename, simpl nomatch.
+  Local Arguments Compose [C s d d'] / _ _ : rename, simpl nomatch.
 
   Definition InducedDiscreteFunctorDec : SpecializedFunctor (DiscreteCategoryDec eq_dec) O'.
     match goal with
@@ -147,9 +123,9 @@
     refine (Build_SpecializedFunctor TypeCatDec LocallySmallCatDec
       (fun O => existT
         (fun C : LocallySmallCategory => forall x y : C, {x = y} + {x <> y})
-        (DiscreteCategoryDec (projT2 O) : LocallySmallSpecializedCategory _)
+        (DiscreteCategoryDec (projT2 O) : LocallySmallSpecializedCategory)
         (fun x y => projT2 O x y))
-      (fun s d f => InducedDiscreteFunctorDec _ f (projT2 s))
+      (fun s d f => InducedDiscreteFunctorDec (DiscreteCategoryDec (projT2 d)) f (projT2 s))
       _
       _
     );
@@ -231,9 +207,9 @@
     refine (Build_SpecializedFunctor SetCatDec SmallCatDec
       (fun O => existT
         (fun C : SmallCategory => forall x y : C, {x = y} + {x <> y})
-        (DiscreteCategoryDec (projT2 O) : SmallSpecializedCategory _)
+        (DiscreteCategoryDec (projT2 O) : SmallSpecializedCategory)
         (fun x y => projT2 O x y))
-      (fun s d f => InducedDiscreteFunctorDec _ f (projT2 s))
+      (fun s d f => InducedDiscreteFunctorDec (DiscreteCategoryDec (projT2 d)) f (projT2 s))
       _
       _
     );
diff -r 4eb6407c6ca3 DecidableSmallCat.v
--- a/DecidableSmallCat.v	Fri May 24 20:09:37 2013 -0400
+++ b/DecidableSmallCat.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,7 +9,7 @@
 Set Universe Polymorphism.
 
 Section SmallCat.
-  Let eq_dec_on_cat `(C : @SpecializedCategory objC) := forall x y : objC, {x = y} + {x <> y}.
+  Let eq_dec_on_cat `(C : SpecializedCategory) := forall x y : C, {x = y} + {x <> y}.
 
   Definition SmallCatDec := SpecializedCategory_sigT_obj SmallCat (fun C => eq_dec_on_cat C).
   Definition LocallySmallCatDec := SpecializedCategory_sigT_obj LocallySmallCat (fun C => eq_dec_on_cat C).
diff -r 4eb6407c6ca3 DiscreteCategory.v
--- a/DiscreteCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/DiscreteCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -30,8 +30,8 @@
   Global Arguments DiscreteCategory_Compose [s d d'] m m' /.
   Global Arguments DiscreteCategory_Identity o /.
 
-  Definition DiscreteCategory : @SpecializedCategory O.
-    refine (@Build_SpecializedCategory _
+  Definition DiscreteCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory O
                                        DiscreteCategory_Morphism
                                        DiscreteCategory_Identity
                                        DiscreteCategory_Compose
diff -r 4eb6407c6ca3 DiscreteCategoryFunctors.v
--- a/DiscreteCategoryFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/DiscreteCategoryFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,8 +12,8 @@
 
 Section FunctorFromDiscrete.
   Variable O : Type.
-  Context `(D : @SpecializedCategory objD).
-  Variable objOf : O -> objD.
+  Context `(D : SpecializedCategory).
+  Variable objOf : O -> D.
 
   Let FunctorFromDiscrete_MorphismOf s d (m : Morphism (DiscreteCategory O) s d) : Morphism D (objOf s) (objOf d)
     := match m with
@@ -22,7 +22,12 @@
 
   Definition FunctorFromDiscrete : SpecializedFunctor (DiscreteCategory O) D.
   Proof.
-    refine {| ObjectOf := objOf; MorphismOf := FunctorFromDiscrete_MorphismOf |};
+    refine (@Build_SpecializedFunctor (DiscreteCategory O)
+                                      D
+                                      objOf
+                                      FunctorFromDiscrete_MorphismOf
+                                      _
+                                      _);
       abstract (
         intros; hnf in *; subst; simpl;
           auto with category
@@ -31,59 +36,36 @@
 End FunctorFromDiscrete.
 
 Section Obj.
-  Local Ltac build_ob_functor Index2Object :=
+  Local Ltac build_ob_functor Index2Cat :=
     match goal with
       | [ |- SpecializedFunctor ?C ?D ] =>
-        refine (Build_SpecializedFunctor C D
-          (fun C' => Index2Object C')
-          (fun _ _ F => ObjectOf F)
-          _
-          _
-        )
+        refine (@Build_SpecializedFunctor C D
+                                          (fun C' => Object (Index2Cat C'))
+                                          (fun _ _ F => ObjectOf F)
+                                          _
+                                          _
+               )
     end;
     intros; simpl in *; reflexivity.
 
   Section type.
     Variable I : Type.
-    Variable Index2Object : I -> Type.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+    Variable Index2Cat : I -> SpecializedCategory.
 
-    Definition ObjectFunctor : SpecializedFunctor (@ComputableCategory _ _ Index2Cat) TypeCat.
-      build_ob_functor Index2Object.
+    Definition ObjectFunctor : SpecializedFunctor (ComputableCategory Index2Cat) TypeCat.
+      build_ob_functor Index2Cat.
     Defined.
   End type.
-
-  Section set.
-    Variable I : Type.
-    Variable Index2Object : I -> Set.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
-
-    Definition ObjectFunctorToSet : SpecializedFunctor (@ComputableCategory _ _ Index2Cat) SetCat.
-      build_ob_functor Index2Object.
-    Defined.
-  End set.
-
-  Section prop.
-    Variable I : Type.
-    Variable Index2Object : I -> Prop.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
-
-    Definition ObjectFunctorToProp : SpecializedFunctor (@ComputableCategory _ _ Index2Cat) PropCat.
-      build_ob_functor Index2Object.
-    Defined.
-  End prop.
 End Obj.
 
-Arguments ObjectFunctor {I Index2Object Index2Cat}.
-Arguments ObjectFunctorToSet {I Index2Object Index2Cat}.
-Arguments ObjectFunctorToProp {I Index2Object Index2Cat}.
+Arguments ObjectFunctor {I Index2Cat}.
 
 Section Mor.
-  Local Ltac build_mor_functor Index2Object Index2Cat :=
+  Local Ltac build_mor_functor Index2Cat :=
     match goal with
       | [ |- SpecializedFunctor ?C ?D ] =>
         refine (Build_SpecializedFunctor C D
-          (fun C' => { sd : Index2Object C' * Index2Object C' & (Index2Cat C').(Morphism) (fst sd) (snd sd) } )
+          (fun C' => { sd : Index2Cat C' * Index2Cat C' & (Index2Cat C').(Morphism) (fst sd) (snd sd) } )
           (fun _ _ F => (fun sdm =>
             existT (fun sd => Morphism _ (fst sd) (snd sd))
             (F (fst (projT1 sdm)), F (snd (projT1 sdm)))
@@ -100,16 +82,15 @@
 
   Section type.
     Variable I : Type.
-    Variable Index2Object : I -> Type.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+    Variable Index2Cat : I -> SpecializedCategory.
 
-    Definition MorphismFunctor : SpecializedFunctor (@ComputableCategory _ _ Index2Cat) TypeCat.
-      build_mor_functor Index2Object Index2Cat.
+    Definition MorphismFunctor : SpecializedFunctor (ComputableCategory Index2Cat) TypeCat.
+      build_mor_functor Index2Cat.
     Defined.
   End type.
 End Mor.
 
-Arguments MorphismFunctor {I Index2Object Index2Cat}.
+Arguments MorphismFunctor {I Index2Cat}.
 
 Section dom_cod.
   Local Ltac build_dom_cod fst_snd :=
@@ -124,14 +105,13 @@
 
   Section type.
     Variable I : Type.
-    Variable Index2Object : I -> Type.
-    Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+    Variable Index2Cat : I -> SpecializedCategory.
 
-    Definition DomainNaturalTransformation : SpecializedNaturalTransformation (@MorphismFunctor _ _ Index2Cat) ObjectFunctor.
+    Definition DomainNaturalTransformation : SpecializedNaturalTransformation (@MorphismFunctor _ Index2Cat) ObjectFunctor.
       build_dom_cod @fst.
     Defined.
 
-    Definition CodomainNaturalTransformation : SpecializedNaturalTransformation (@MorphismFunctor _ _ Index2Cat) ObjectFunctor.
+    Definition CodomainNaturalTransformation : SpecializedNaturalTransformation (@MorphismFunctor _ Index2Cat) ObjectFunctor.
       build_dom_cod @snd.
     Defined.
   End type.
@@ -139,7 +119,7 @@
 
 Section InducedFunctor.
   Variable O : Type.
-  Context `(O' : @SpecializedCategory obj).
+  Context `(O' : SpecializedCategory).
   Variable f : O -> O'.
 
   Definition InducedDiscreteFunctor : SpecializedFunctor (DiscreteCategory O) O'.
@@ -169,8 +149,8 @@
 
   Definition DiscreteFunctor : SpecializedFunctor TypeCat LocallySmallCat.
     refine (Build_SpecializedFunctor TypeCat LocallySmallCat
-      (fun O => DiscreteCategory O : LocallySmallSpecializedCategory _)
-      (fun s d f => InducedDiscreteFunctor _ f)
+      (fun O => DiscreteCategory O : LocallySmallSpecializedCategory)
+      (fun s d f => InducedDiscreteFunctor (DiscreteCategory d) f)
       _
       _
     );
@@ -179,8 +159,8 @@
 
   Definition DiscreteSetFunctor : SpecializedFunctor SetCat SmallCat.
     refine (Build_SpecializedFunctor SetCat SmallCat
-      (fun O => DiscreteCategory O : SmallSpecializedCategory _)
-      (fun s d f => InducedDiscreteFunctor _ f)
+      (fun O => DiscreteCategory O : SmallSpecializedCategory)
+      (fun s d f => InducedDiscreteFunctor (DiscreteCategory d) f)
       _
       _
     );
diff -r 4eb6407c6ca3 DualFunctor.v
--- a/DualFunctor.v	Fri May 24 20:09:37 2013 -0400
+++ b/DualFunctor.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,7 +9,7 @@
 Section OppositeCategory.
   Definition SmallOppositeFunctor : SpecializedFunctor SmallCat SmallCat.
     refine (Build_SpecializedFunctor SmallCat SmallCat
-                                     (fun x => OppositeCategory x : SmallSpecializedCategory _)
+                                     (fun x => OppositeCategory x : SmallSpecializedCategory)
                                      (fun _ _ m => OppositeFunctor m)
                                      _
                                      _);
@@ -18,7 +18,7 @@
 
   Definition LocallySmallOppositeFunctor : SpecializedFunctor LocallySmallCat LocallySmallCat.
     refine (Build_SpecializedFunctor LocallySmallCat LocallySmallCat
-                                     (fun x => OppositeCategory x : LocallySmallSpecializedCategory _)
+                                     (fun x => OppositeCategory x : LocallySmallSpecializedCategory)
                                      (fun _ _ m => OppositeFunctor m)
                                      _
                                      _);
diff -r 4eb6407c6ca3 Duals.v
--- a/Duals.v	Fri May 24 20:09:37 2013 -0400
+++ b/Duals.v	Sat Jun 22 12:51:34 2013 -0400
@@ -15,25 +15,25 @@
 Local Open Scope category_scope.
 
 Section OppositeCategory.
-  Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC
-    := @Build_SpecializedCategory' objC
+  Definition OppositeCategory `(C : SpecializedCategory) : SpecializedCategory
+    := @Build_SpecializedCategory' C
                                 (fun s d => Morphism C d s)
                                 (Identity (C := C))
                                 (fun _ _ _ m1 m2 => Compose m2 m1)
-                                (fun _ _ _ _ _ _ _ => @Associativity_sym _ _ _ _ _ _ _ _ _)
-                                (fun _ _ _ _ _ _ _ => @Associativity _ _ _ _ _ _ _ _ _)
-                                (fun _ _ => @RightIdentity _ _ _ _)
-                                (fun _ _ => @LeftIdentity _ _ _ _).
+                                (fun _ _ _ _ _ _ _ => @Associativity_sym _ _ _ _ _ _ _ _)
+                                (fun _ _ _ _ _ _ _ => @Associativity _ _ _ _ _ _ _ _)
+                                (fun _ _ => @RightIdentity _ _ _)
+                                (fun _ _ => @LeftIdentity _ _ _).
 End OppositeCategory.
 
 (*Notation "C ᵒᵖ" := (OppositeCategory C) : category_scope.*)
 
 Section DualCategories.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Lemma op_op_id : OppositeCategory (OppositeCategory C) = C.
-    clear D objD.
+    clear D.
     unfold OppositeCategory; simpl.
     repeat change (fun a => ?f a) with f.
     destruct C; intros; simpl; reflexivity.
@@ -47,7 +47,7 @@
 Hint Rewrite @op_op_id @op_distribute_prod : category.
 
 Section DualObjects.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition terminal_opposite_initial (o : C) : IsTerminalObject o -> IsInitialObject (C := OppositeCategory C) o
     := fun H o' => H o'.
@@ -65,8 +65,8 @@
 End DualObjects.
 
 Section OppositeFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor C D.
   Let COp := OppositeCategory C.
   Let DOp := OppositeCategory D.
@@ -84,8 +84,8 @@
 (*Notation "C ᵒᵖ" := (OppositeFunctor C) : functor_scope.*)
 
 Section OppositeFunctor_Id.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor C D.
 
   Lemma op_op_functor_id : OppositeFunctor (OppositeFunctor F) == F.
@@ -97,8 +97,8 @@
 (*Hint Rewrite op_op_functor_id.*)
 
 Section OppositeNaturalTransformation.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variables F G : SpecializedFunctor C D.
   Variable T : SpecializedNaturalTransformation F G.
   Let COp := OppositeCategory C.
@@ -117,8 +117,8 @@
 (*Notation "C ᵒᵖ" := (OppositeNaturalTransformation C) : natural_transformation_scope.*)
 
 Section OppositeNaturalTransformation_Id.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variables F G : SpecializedFunctor C D.
   Variable T : SpecializedNaturalTransformation F G.
 
diff -r 4eb6407c6ca3 EnrichedCategory.v
--- a/EnrichedCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/EnrichedCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,13 +13,13 @@
   (** Quoting Wikipedia:
      Let [(M, ⊗, I, α, λ, ρ)] be a monoidal category.
      *)
-  Context `(M : @MonoidalCategory objM).
+  Context `(M : MonoidalCategory).
 
-  Let src `{C : @SpecializedCategory objC} s d (_ : Morphism C s d) := s.
-  Let dst `{C : @SpecializedCategory objC} s d (_ : Morphism C s d) := d.
+  Let src `{C : SpecializedCategory} s d (_ : Morphism C s d) := s.
+  Let dst `{C : SpecializedCategory} s d (_ : Morphism C s d) := d.
 
-  Arguments src [objC C s d] _.
-  Arguments dst [objC C s d] _.
+  Arguments src [C s d] _.
+  Arguments dst [C s d] _.
 
   Local Notation "A ⊗ B" := (M.(TensorProduct) (A, B)).
   Local Notation "A ⊗m B" := (M.(TensorProduct).(MorphismOf) (s := (src A, src B)) (d := (dst A, dst B)) (A, B)%morphism).
@@ -140,10 +140,10 @@
 
   Local Notation "x ~> y" := (M.(Morphism) x y).
 
-  Record EnrichedCategory (objC : Type) := {
-    EnrichedObject :> _ := objC;
+  Record EnrichedCategory := {
+    EnrichedObject :> Type;
 
-    EnrichedMorphism : objC -> objC -> objM where "'C' ( A , B )" := (@EnrichedMorphism A B);
+    EnrichedMorphism : EnrichedObject -> EnrichedObject -> M where "'C' ( A , B )" := (@EnrichedMorphism A B);
     EnrichedIdentity : forall a, I ~> C (a, a) where "'id'" := EnrichedIdentity;
     EnrichedCompose : forall a b c, C(b, c) ⊗ C(a, b) ~> C(a, c) where "○_{ a , b , c }" := (@EnrichedCompose a b c);
 
@@ -167,9 +167,9 @@
      ]]
      *)
     EnrichedAssociativity : forall a b c d, (
-      (Compose ○_{a, b, d} (○_{b, c, d} ⊗m @Identity _ M C(a, b))) =
+      (Compose ○_{a, b, d} (○_{b, c, d} ⊗m @Identity M C(a, b))) =
       (Compose ○_{a, c, d}
-        (Compose ((@Identity _ M C(c, d)) ⊗m ○_{a, b, c})
+        (Compose ((@Identity M C(c, d)) ⊗m ○_{a, b, c})
           (α (C(c, d), C(b, c), C(a, b)))
         )
       )
@@ -190,7 +190,7 @@
      ]]
      *)
     EnrichedLeftIdentity : forall a b, (
-      Compose ○_{a, b, b} ((id b) ⊗m (@Identity _ M C(a, b))) =
+      Compose ○_{a, b, b} ((id b) ⊗m (@Identity M C(a, b))) =
       λ C(a, b)
     );
     (*
@@ -209,7 +209,7 @@
      ]]
      *)
     EnrichedRightIdentity : forall a b, (
-      Compose ○_{a, a, b} ((@Identity _ M C(a, b)) ⊗m (id a)) =
+      Compose ○_{a, a, b} ((@Identity M C(a, b)) ⊗m (id a)) =
       ρ C(a, b)
     )
   }.
diff -r 4eb6407c6ca3 Equalizer.v
--- a/Equalizer.v	Fri May 24 20:09:37 2013 -0400
+++ b/Equalizer.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,8 +10,8 @@
 Set Universe Polymorphism.
 
 Section Equalizer.
-  Context `(C : @SpecializedCategory objC).
-  Variables A B : objC.
+  Context `(C : SpecializedCategory).
+  Variables A B : C.
   Variables f g : C.(Morphism) A B.
 
   Inductive EqualizerTwo := EqualizerA | EqualizerB.
@@ -31,8 +31,8 @@
     destruct s, d, d'; simpl in *; trivial.
   Defined.
 
-  Definition EqualizerIndex : @SpecializedCategory EqualizerTwo.
-    refine (@Build_SpecializedCategory _
+  Definition EqualizerIndex : SpecializedCategory.
+    refine (@Build_SpecializedCategory EqualizerTwo
                                        EqualizerIndex_Morphism
                                        (fun x => match x with EqualizerA => tt | EqualizerB => tt end)
                                        EqualizerIndex_Compose
diff -r 4eb6407c6ca3 EqualizerFunctor.v
--- a/EqualizerFunctor.v	Fri May 24 20:09:37 2013 -0400
+++ b/EqualizerFunctor.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,7 +9,7 @@
 Set Universe Polymorphism.
 
 Section Equalizer.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Variable HasLimits : forall F : SpecializedFunctor EqualizerIndex C, Limit F.
   Variable HasColimits : forall F : SpecializedFunctor EqualizerIndex C, Colimit F.
diff -r 4eb6407c6ca3 ExponentialLaws.v
--- a/ExponentialLaws.v	Fri May 24 20:09:37 2013 -0400
+++ b/ExponentialLaws.v	Sat Jun 22 12:51:34 2013 -0400
@@ -19,12 +19,12 @@
       NaturalTransformation_JMeq eq_JMeq.
 
 Section Law0.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition ExponentialLaw0Functor : SpecializedFunctor (C ^ 0) 1
     := FunctorTo1 _.
   Definition ExponentialLaw0Functor_Inverse : SpecializedFunctor 1 (C ^ 0)
-    := FunctorFrom1 _ (FunctorFrom0 _).
+    := FunctorFrom1 (C ^ 0) (FunctorFrom0 _).
 
   Lemma ExponentialLaw0
   : ComposeFunctors ExponentialLaw0Functor ExponentialLaw0Functor_Inverse
@@ -33,15 +33,15 @@
        = IdentityFunctor _.
   Proof.
     split; auto.
-    apply Functor_eq; auto.
+    apply Functor_eq; auto;
     nt_eq; auto;
     destruct_head_hnf Empty_set.
   Qed.
 End Law0.
 
 Section Law0'.
-  Context `(C : @SpecializedCategory objC).
-  Variable c : objC.
+  Context `(C : SpecializedCategory).
+  Variable c : C.
 
   Definition ExponentialLaw0'Functor : SpecializedFunctor (0 ^ C) 0
     := Build_SpecializedFunctor (0 ^ C) 0
@@ -69,7 +69,7 @@
 End Law0'.
 
 Section Law1.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition ExponentialLaw1Functor : SpecializedFunctor (C ^ 1) C
     := Build_SpecializedFunctor (C ^ 1) C
@@ -105,7 +105,7 @@
   Proof.
     refine (Build_SpecializedFunctor
               C (C ^ 1)
-              (@FunctorFrom1 _ _)
+              (@FunctorFrom1 _)
               ExponentialLaw1Functor_Inverse_MorphismOf
               _
               _
@@ -131,7 +131,7 @@
 End Law1.
 
 Section Law1'.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition ExponentialLaw1'Functor : SpecializedFunctor (1 ^ C) 1
     := FunctorTo1 _.
@@ -158,15 +158,15 @@
     = IdentityFunctor _.
   Proof.
     split; auto.
-    apply Functor_eq; auto.
+    apply Functor_eq; auto;
     nt_eq; auto.
   Qed.
 End Law1'.
 
 Section Law2.
-  Context `(D : @SpecializedCategory objD).
-  Context `(C1 : @SpecializedCategory objC1).
-  Context `(C2 : @SpecializedCategory objC2).
+  Context `(D : SpecializedCategory).
+  Context `(C1 : SpecializedCategory).
+  Context `(C2 : SpecializedCategory).
 
   Definition ExponentialLaw2Functor
   : SpecializedFunctor (D ^ (C1 + C2)) ((D ^ C1) * (D ^ C2))
@@ -219,31 +219,30 @@
 End Law2.
 
 Section Law3.
-  Context `(C1 : @SpecializedCategory objC1).
-  Context `(C2 : @SpecializedCategory objC2).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C1 : SpecializedCategory).
+  Context `(C2 : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Definition ExponentialLaw3Functor
   : SpecializedFunctor ((C1 * C2) ^ D) (C1 ^ D * C2 ^ D).
-    match goal with
-      | [ |- SpecializedFunctor ?F ?G ] =>
-        refine (Build_SpecializedFunctor
-                  F G
-                  (fun H => (ComposeFunctors fst_Functor H,
-                             ComposeFunctors snd_Functor H))
-                  (fun s d m =>
-                     (MorphismOf (FunctorialComposition D (C1 * C2) C1)
-                                 (s := (_, _))
-                                 (d := (_, _))
-                                 (Identity fst_Functor, m),
-                      MorphismOf (FunctorialComposition D (C1 * C2) C2)
-                                 (s := (_, _))
-                                 (d := (_, _))
-                                 (Identity snd_Functor, m)))
-                  _
-                  _
-               )
-    end;
+    let F := match goal with | [ |- SpecializedFunctor ?F ?G ] => constr:(F) end in
+    let G := match goal with | [ |- SpecializedFunctor ?F ?G ] => constr:(G) end in
+    refine (Build_SpecializedFunctor
+              F G
+              (fun H => (ComposeFunctors fst_Functor H,
+                         ComposeFunctors snd_Functor H))
+              (fun s d m =>
+                 (MorphismOf (FunctorialComposition D (C1 * C2) C1)
+                             (s := (_, _))
+                             (d := (_, _))
+                             (Identity (C := _ ^ _) fst_Functor, m),
+                  MorphismOf (FunctorialComposition D (C1 * C2) C2)
+                             (s := (_, _))
+                             (d := (_, _))
+                             (Identity (C := _ ^ _) snd_Functor, m)))
+              _
+              _
+           );
     abstract (
         intros;
         simpl;
@@ -263,8 +262,8 @@
     refine (Build_SpecializedFunctor
               (fst FG) (snd FG)
               (fun H => FunctorProduct
-                          (@fst_Functor _ (C1 ^ D) _ (C2 ^ D) H)
-                          (@snd_Functor _ (C1 ^ D) _ (C2 ^ D) H))
+                          (@fst_Functor (C1 ^ D) (C2 ^ D) H)
+                          (@snd_Functor (C1 ^ D) (C2 ^ D) H))
               (fun _ _ m => FunctorProductFunctorial (fst m) (snd m))
               _
               _);
@@ -300,9 +299,9 @@
 End Law3.
 
 Section Law4.
-  Context `(C1 : @SpecializedCategory objC1).
-  Context `(C2 : @SpecializedCategory objC2).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C1 : SpecializedCategory).
+  Context `(C2 : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Section functor.
     Local Ltac do_exponential4 := intros; simpl;
diff -r 4eb6407c6ca3 Functor.v
--- a/Functor.v	Fri May 24 20:09:37 2013 -0400
+++ b/Functor.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,8 +13,8 @@
 Local Infix "==" := JMeq.
 
 Section SpecializedFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   (**
      Quoting from the lecture notes for 18.705, Commutative Algebra:
@@ -28,7 +28,7 @@
      **)
   Record SpecializedFunctor :=
     {
-      ObjectOf :> objC -> objD;
+      ObjectOf :> C -> D;
       MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
       FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
                           MorphismOf _ _ (Compose m2 m1) = Compose (MorphismOf _ _ m2) (MorphismOf _ _ m1);
@@ -49,21 +49,21 @@
 Create HintDb functor discriminated.
 
 Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
-Definition GeneralizeFunctor objC C objD D (F : @SpecializedFunctor objC C objD D) : Functor C D := F.
+Definition GeneralizeFunctor C D (F : SpecializedFunctor C D) : Functor C D := F.
 Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.
 
 (* try to always unfold [GeneralizeFunctor]; it's in there
    only for coercions *)
-Arguments GeneralizeFunctor [objC C objD D] F /.
+Arguments GeneralizeFunctor [C D] F /.
 Hint Extern 0 => unfold GeneralizeFunctor : category functor.
 
-Arguments SpecializedFunctor {objC} C {objD} D.
+Arguments SpecializedFunctor C D.
 Arguments Functor C D.
-Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch.
-Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+Arguments ObjectOf {C%category D%category} F%functor c%object : rename, simpl nomatch.
+Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
 
-Arguments FCompositionOf [objC C objD D] F _ _ _ _ _ : rename.
-Arguments FIdentityOf [objC C objD D] F _ : rename.
+Arguments FCompositionOf [C D] F _ _ _ _ _ : rename.
+Arguments FIdentityOf [C D] F _ : rename.
 
 Hint Resolve @FCompositionOf @FIdentityOf : category functor.
 Hint Rewrite @FIdentityOf : category.
@@ -88,13 +88,13 @@
     hnf in H;
     revert H; clear; intro H; clear H;
     match F'' with
-      | @Build_SpecializedFunctor ?objC ?C
-                                  ?objD ?D
+      | @Build_SpecializedFunctor ?C
+                                  ?D
                                   ?OO
                                   ?MO
                                   ?FCO
                                   ?FIO =>
-        refine (@Build_SpecializedFunctor objC C objD D
+        refine (@Build_SpecializedFunctor C D
                                           OO
                                           MO
                                           _
@@ -105,7 +105,7 @@
 Ltac functor_simpl_abstract_trailing_props F := functor_tac_abstract_trailing_props F ltac:(fun F' => let F'' := eval simpl in F' in F'').
 
 Section Functors_Equal.
-  Lemma Functor_contr_eq' objC C objD D (F G : @SpecializedFunctor objC C objD D)
+  Lemma Functor_contr_eq' C D (F G : SpecializedFunctor C D)
         (D_morphism_proof_irrelevance
          : forall s d (m1 m2 : Morphism D s d) (pf1 pf2 : m1 = m2),
              pf1 = pf2)
@@ -122,7 +122,7 @@
       trivial.
   Qed.
 
-  Lemma Functor_contr_eq objC C objD D (F G : @SpecializedFunctor objC C objD D)
+  Lemma Functor_contr_eq C D (F G : SpecializedFunctor C D)
         (D_object_proof_irrelevance
          : forall (x : D) (pf : x = x),
              pf = eq_refl)
@@ -149,7 +149,7 @@
     reflexivity.
   Qed.
 
-  Lemma Functor_eq' objC C objD D : forall (F G : @SpecializedFunctor objC C objD D),
+  Lemma Functor_eq' C D : forall (F G : SpecializedFunctor C D),
     ObjectOf F = ObjectOf G
     -> MorphismOf F == MorphismOf G
     -> F = G.
@@ -157,8 +157,8 @@
       f_equal; apply proof_irrelevance.
   Qed.
 
-  Lemma Functor_eq objC C objD D :
-    forall (F G : @SpecializedFunctor objC C objD D),
+  Lemma Functor_eq C D :
+    forall (F G : SpecializedFunctor C D),
       (forall x, ObjectOf F x = ObjectOf G x)
       -> (forall s d m, MorphismOf F (s := s) (d := d) m == MorphismOf G (s := s) (d := d) m)
       -> F = G.
@@ -168,12 +168,10 @@
     try apply JMeq_eq; trivial.
   Qed.
 
-  Lemma Functor_JMeq objC C objD D objC' C' objD' D' :
-    forall (F : @SpecializedFunctor objC C objD D) (G : @SpecializedFunctor objC' C' objD' D'),
-      objC = objC'
-      -> objD = objD'
-      -> C == C'
-      -> D == D'
+  Lemma Functor_JMeq C D C' D' :
+    forall (F : SpecializedFunctor C D) (G : SpecializedFunctor C' D'),
+      C = C'
+      -> D = D'
       -> ObjectOf F == ObjectOf G
       -> MorphismOf F == MorphismOf G
       -> F == G.
@@ -199,8 +197,8 @@
     hnf in H;
     revert H; clear; intro H; clear H;
     match F'' with
-      | @Build_SpecializedFunctor ?objC ?C
-                                  ?objD ?D
+      | @Build_SpecializedFunctor ?C
+                                  ?D
                                   ?OO
                                   ?MO
                                   ?FCO
@@ -213,7 +211,7 @@
         let FIOT := (eval simpl in FIOT') in
         assert (FCO' : FCOT) by abstract exact FCO;
           assert (FIO' : FIOT) by (clear FCO'; abstract exact FIO);
-          exists (@Build_SpecializedFunctor objC C objD D
+          exists (@Build_SpecializedFunctor C D
                                             OO
                                             MO
                                             FCO'
@@ -233,10 +231,10 @@
 Ltac functor_simpl_abstract_trailing_props_with_equality := functor_tac_abstract_trailing_props_with_equality ltac:(fun F' => let F'' := eval simpl in F' in F'').
 
 Section FunctorComposition.
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
   Variable G : SpecializedFunctor D E.
   Variable F : SpecializedFunctor C D.
 
@@ -284,7 +282,7 @@
 End FunctorComposition.
 
 Section IdentityFunctor.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   (** There is an identity functor.  It does the obvious thing. *)
   Definition IdentityFunctor : SpecializedFunctor C C
@@ -296,8 +294,8 @@
 End IdentityFunctor.
 
 Section IdentityFunctorLemmas.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Lemma LeftIdentityFunctor (F : SpecializedFunctor D C) : ComposeFunctors (IdentityFunctor _) F = F.
     functor_eq.
@@ -313,10 +311,10 @@
 Hint Immediate @LeftIdentityFunctor @RightIdentityFunctor : category functor.
 
 Section FunctorCompositionLemmas.
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
 
   Lemma ComposeFunctorsAssociativity (F : SpecializedFunctor B C) (G : SpecializedFunctor C D) (H : SpecializedFunctor D E) :
     ComposeFunctors (ComposeFunctors H G) F = ComposeFunctors H (ComposeFunctors G F).
diff -r 4eb6407c6ca3 FunctorAttributes.v
--- a/FunctorAttributes.v	Fri May 24 20:09:37 2013 -0400
+++ b/FunctorAttributes.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,10 +13,10 @@
 Local Open Scope category_scope.
 
 Section FullFaithful.
-  Context `(C : @SpecializedCategory objC).
-  Context `(C' : @LocallySmallSpecializedCategory objC').
-  Context `(D : @SpecializedCategory objD).
-  Context `(D' : @LocallySmallSpecializedCategory objD').
+  Context `(C : SpecializedCategory).
+  Context `(C' : @LocallySmallSpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(D' : @LocallySmallSpecializedCategory).
   Variable F : SpecializedFunctor C D.
   Variable F' : SpecializedFunctor C' D'.
   Let COp := OppositeCategory C.
diff -r 4eb6407c6ca3 FunctorCategory.v
--- a/FunctorCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/FunctorCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,14 +10,14 @@
 Set Universe Polymorphism.
 
 Section FunctorCategory.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   (*
      There is a category Fun(C, D) of functors from [C] to [D].
    *)
-  Definition FunctorCategory : @SpecializedCategory (SpecializedFunctor C D).
-    refine (@Build_SpecializedCategory _
+  Definition FunctorCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory (SpecializedFunctor C D)
                                        (SpecializedNaturalTransformation (C := C) (D := D))
                                        (IdentityNaturalTransformation (C := C) (D := D))
                                        (NTComposeT (C := C) (D := D))
diff -r 4eb6407c6ca3 FunctorCategoryFunctorial.v
--- a/FunctorCategoryFunctorial.v	Fri May 24 20:09:37 2013 -0400
+++ b/FunctorCategoryFunctorial.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,10 +13,10 @@
 
 Section FunctorCategoryParts.
   Section MorphismOf.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-    Context `(C' : @SpecializedCategory objC').
-    Context `(D' : @SpecializedCategory objD').
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
+    Context `(C' : SpecializedCategory).
+    Context `(D' : SpecializedCategory).
 
     Variable F : SpecializedFunctor C C'.
     Variable G : SpecializedFunctor D' D.
@@ -49,8 +49,8 @@
   End MorphismOf.
 
   Section FIdentityOf.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
 
     Lemma FunctorCategoryFunctor_FIdentityOf : FunctorCategoryFunctor_MorphismOf (IdentityFunctor C) (IdentityFunctor D) = IdentityFunctor _.
       repeat (intro || apply Functor_eq || nt_eq); simpl; subst; JMeq_eq; rsimplify_morphisms; reflexivity.
@@ -58,12 +58,12 @@
   End FIdentityOf.
 
   Section FCompositionOf.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-    Context `(C' : @SpecializedCategory objC').
-    Context `(D' : @SpecializedCategory objD').
-    Context `(C'' : @SpecializedCategory objC'').
-    Context `(D'' : @SpecializedCategory objD'').
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
+    Context `(C' : SpecializedCategory).
+    Context `(D' : SpecializedCategory).
+    Context `(C'' : SpecializedCategory).
+    Context `(D'' : SpecializedCategory).
 
     Variable F' : SpecializedFunctor C' C''.
     Variable G : SpecializedFunctor D D'.
@@ -80,7 +80,7 @@
 Section FunctorCategoryFunctor.
   Definition FunctorCategoryFunctor : SpecializedFunctor (LocallySmallCat * (OppositeCategory LocallySmallCat)) LocallySmallCat.
     refine (Build_SpecializedFunctor (LocallySmallCat * (OppositeCategory LocallySmallCat)) LocallySmallCat
-                                     (fun CD => (fst CD) ^ (snd CD) : LocallySmallSpecializedCategory _)
+                                     (fun CD => (fst CD) ^ (snd CD) : LocallySmallSpecializedCategory)
                                      (fun s d m => FunctorCategoryFunctor_MorphismOf (fst m) (snd m))
                                      _
                                      _);
@@ -95,10 +95,10 @@
 Notation "F ^ G" := (FunctorCategoryFunctor_MorphismOf F G) : functor_scope.
 
 Section NaturalTransformation.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(C' : @SpecializedCategory objC').
-  Context `(D' : @SpecializedCategory objD').
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(C' : SpecializedCategory).
+  Context `(D' : SpecializedCategory).
 
   Variables F G : SpecializedFunctor C D.
   Variables F' G' : SpecializedFunctor C' D'.
@@ -134,8 +134,8 @@
 
 Section NaturalTransformation_Properties.
   Section identity.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
 
     Local Ltac t := intros; simpl; nt_eq; rsimplify_morphisms; try reflexivity.
 
@@ -201,12 +201,12 @@
   End identity.
 
   Section compose.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-    Context `(E : @SpecializedCategory objE).
-    Context `(C' : @SpecializedCategory objC').
-    Context `(D' : @SpecializedCategory objD').
-    Context `(E' : @SpecializedCategory objE').
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
+    Context `(E : SpecializedCategory).
+    Context `(C' : SpecializedCategory).
+    Context `(D' : SpecializedCategory).
+    Context `(E' : SpecializedCategory).
 
     Variable G : SpecializedFunctor D E.
     Variable F : SpecializedFunctor C D.
diff -r 4eb6407c6ca3 FunctorIsomorphisms.v
--- a/FunctorIsomorphisms.v	Fri May 24 20:09:37 2013 -0400
+++ b/FunctorIsomorphisms.v	Sat Jun 22 12:51:34 2013 -0400
@@ -16,8 +16,8 @@
   (* Copy definitions from CategoryIsomorphisms.v *)
 
   Section FunctorIsInverseOf.
-    Context `{C : @SpecializedCategory objC}.
-    Context `{D : @SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
 
     Definition FunctorIsInverseOf1 (F : SpecializedFunctor C D) (G : SpecializedFunctor D C) : Prop :=
       ComposeFunctors G F = IdentityFunctor C.
@@ -31,14 +31,14 @@
       FunctorIsInverseOf1 F G /\ FunctorIsInverseOf2 F G.
   End FunctorIsInverseOf.
 
-  Lemma FunctorIsInverseOf_sym `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD}
+  Lemma FunctorIsInverseOf_sym `{C : SpecializedCategory} `{D : SpecializedCategory}
     (F : SpecializedFunctor C D) (G : SpecializedFunctor D C) :
     FunctorIsInverseOf F G -> FunctorIsInverseOf G F.
     intros; hnf in *; split_and; split; trivial.
   Qed.
 
   Section FunctorIsomorphismOf.
-    Record FunctorIsomorphismOf `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD} (F : SpecializedFunctor C D) := {
+    Record FunctorIsomorphismOf `{C : SpecializedCategory} `{D : SpecializedCategory} (F : SpecializedFunctor C D) := {
       FunctorIsomorphismOf_Functor :> _ := F;
       InverseFunctor : SpecializedFunctor D C;
       LeftInverseFunctor : ComposeFunctors InverseFunctor F = IdentityFunctor C;
@@ -48,16 +48,16 @@
     Hint Resolve RightInverseFunctor LeftInverseFunctor : category.
     Hint Resolve RightInverseFunctor LeftInverseFunctor : functor.
 
-    Definition FunctorIsomorphismOf_Identity `(C : @SpecializedCategory objC) : FunctorIsomorphismOf (IdentityFunctor C).
+    Definition FunctorIsomorphismOf_Identity `(C : SpecializedCategory) : FunctorIsomorphismOf (IdentityFunctor C).
       exists (IdentityFunctor _); eauto with functor.
     Defined.
 
-    Definition InverseOfFunctor `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD} (F : SpecializedFunctor C D)
+    Definition InverseOfFunctor `{C : SpecializedCategory} `{D : SpecializedCategory} (F : SpecializedFunctor C D)
       (i : FunctorIsomorphismOf F) : FunctorIsomorphismOf (InverseFunctor i).
       exists i; auto with functor.
     Defined.
 
-    Definition ComposeFunctorIsmorphismOf `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD} `{E : @SpecializedCategory objE}
+    Definition ComposeFunctorIsmorphismOf `{C : SpecializedCategory} `{D : SpecializedCategory} `{E : SpecializedCategory}
       {F : SpecializedFunctor D E} {G : SpecializedFunctor C D} (i1 : FunctorIsomorphismOf F) (i2 : FunctorIsomorphismOf G) :
       FunctorIsomorphismOf (ComposeFunctors F G).
       exists (ComposeFunctors (InverseFunctor i2) (InverseFunctor i1));
@@ -75,7 +75,7 @@
   End FunctorIsomorphismOf.
 
   Section IsomorphismOfCategories.
-    Record IsomorphismOfCategories `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) := {
+    Record IsomorphismOfCategories `(C : SpecializedCategory) `(D : SpecializedCategory) := {
       IsomorphismOfCategories_Functor : SpecializedFunctor C D;
       IsomorphismOfCategories_Of :> FunctorIsomorphismOf IsomorphismOfCategories_Functor
     }.
@@ -84,10 +84,10 @@
   End IsomorphismOfCategories.
 
   Section FunctorIsIsomorphism.
-    Definition FunctorIsIsomorphism `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD} (F : SpecializedFunctor C D) : Prop :=
+    Definition FunctorIsIsomorphism `{C : SpecializedCategory} `{D : SpecializedCategory} (F : SpecializedFunctor C D) : Prop :=
       exists G, FunctorIsInverseOf F G.
 
-    Lemma FunctorIsmorphismOf_FunctorIsIsomorphism `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD} (F : SpecializedFunctor C D) :
+    Lemma FunctorIsmorphismOf_FunctorIsIsomorphism `{C : SpecializedCategory} `{D : SpecializedCategory} (F : SpecializedFunctor C D) :
       FunctorIsomorphismOf F -> FunctorIsIsomorphism F.
       intro i; hnf.
       exists (InverseFunctor i);
@@ -96,7 +96,7 @@
         assumption.
     Qed.
 
-    Lemma FunctorIsIsomorphism_FunctorIsmorphismOf `{C : @SpecializedCategory objC} `{D : @SpecializedCategory objD} (F : SpecializedFunctor C D) :
+    Lemma FunctorIsIsomorphism_FunctorIsmorphismOf `{C : SpecializedCategory} `{D : SpecializedCategory} (F : SpecializedFunctor C D) :
       FunctorIsIsomorphism F -> exists _ : FunctorIsomorphismOf F, True.
       intro i; destruct_hypotheses.
       destruct_exists; trivial.
@@ -108,7 +108,7 @@
     Definition CategoriesIsomorphic (C D : Category) : Prop :=
       exists (F : SpecializedFunctor C D) (G : SpecializedFunctor D C), FunctorIsInverseOf F G.
 
-    Lemma IsmorphismOfCategories_CategoriesIsomorphic `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :
+    Lemma IsmorphismOfCategories_CategoriesIsomorphic `(C : SpecializedCategory) `(D : SpecializedCategory) :
       IsomorphismOfCategories C D -> CategoriesIsomorphic C D.
       intro i; destruct i as [ m i ].
       exists m.
@@ -163,8 +163,8 @@
 End FunctorIsomorphism.
 
 Section Functor_preserves_isomorphism.
-  Context `(C : SpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor C D.
 
   Hint Rewrite <- FCompositionOf : functor.
diff -r 4eb6407c6ca3 FunctorProduct.v
--- a/FunctorProduct.v	Fri May 24 20:09:37 2013 -0400
+++ b/FunctorProduct.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,9 +10,9 @@
 Set Universe Polymorphism.
 
 Section FunctorProduct.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(D' : @SpecializedCategory objD').
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(D' : SpecializedCategory).
 
   Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D').
     match goal with
@@ -44,10 +44,10 @@
 End FunctorProduct.
 
 Section FunctorProduct'.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(C' : @SpecializedCategory objC').
-  Context `(D' : @SpecializedCategory objD').
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(C' : SpecializedCategory).
+  Context `(D' : SpecializedCategory).
   Variable F : Functor C D.
   Variable F' : Functor C' D'.
 
diff -r 4eb6407c6ca3 FunctorialComposition.v
--- a/FunctorialComposition.v	Fri May 24 20:09:37 2013 -0400
+++ b/FunctorialComposition.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,9 +10,9 @@
 Set Universe Polymorphism.
 
 Section FunctorialComposition.
-  Context `(C : SpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
-  Context `(E : SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
 
   Definition FunctorialComposition : SpecializedFunctor ((E ^ D) * (D ^ C)) (E ^ C).
   Proof.
diff -r 4eb6407c6ca3 Graphs.v
--- a/Graphs.v	Fri May 24 20:09:37 2013 -0400
+++ b/Graphs.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,7 +11,7 @@
 Set Universe Polymorphism.
 
 Section GraphObj.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.
 
@@ -30,8 +30,8 @@
     destruct s, d, d'; simpl in *; trivial.
   Defined.
 
-  Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
-    refine (@Build_SpecializedCategory _
+  Definition GraphIndexingCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory GraphIndex
                                        GraphIndex_Morphism
                                        (fun x => match x with GraphIndexSource => tt | GraphIndexTarget => tt end)
                                        GraphIndex_Compose
@@ -45,8 +45,8 @@
 
   Definition UnderlyingGraph_ObjectOf x :=
     match x with
-      | GraphIndexSource => { sd : objC * objC & C.(Morphism) (fst sd) (snd sd) }
-      | GraphIndexTarget => objC
+      | GraphIndexSource => { sd : C * C & C.(Morphism) (fst sd) (snd sd) }
+      | GraphIndexTarget => Object C
     end.
 
   Global Arguments UnderlyingGraph_ObjectOf x /.
@@ -92,7 +92,7 @@
     UnderlyingGraph C.
 
   Local Ltac t :=
-    intros; destruct_head GraphIndex;
+    intros; destruct_head_hnf GraphIndex;
       repeat match goal with
                | [ H : Empty_set |- _ ] => destruct H
                | _  => reflexivity
@@ -143,7 +143,7 @@
 
   Hint Rewrite concatenate_p_noedges concatenate_noedges_p concatenate_associative.
 
-  Definition FreeCategory : SpecializedCategory vertices.
+  Definition FreeCategory : SpecializedCategory.
   Proof.
     refine (@Build_SpecializedCategory
               vertices
diff -r 4eb6407c6ca3 Grothendieck.v
--- a/Grothendieck.v	Fri May 24 20:09:37 2013 -0400
+++ b/Grothendieck.v	Sat Jun 22 12:51:34 2013 -0400
@@ -24,12 +24,12 @@
      [Hom (Γ F) (c1, x1) (c2, x2)] is the set of morphisms
      [f : c1 -> c2] in [C] such that [F.(MorphismOf) f x1 = x2].
      *)
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Variable F : SpecializedFunctor C TypeCat.
   Variable F' : SpecializedFunctor C SetCat.
 
   Record GrothendieckPair := {
-    GrothendieckC' : objC;
+    GrothendieckC' : C;
     GrothendieckX' : F GrothendieckC'
   }.
 
@@ -45,7 +45,7 @@
   Qed.
 
   Record SetGrothendieckPair := {
-    SetGrothendieckC' : objC;
+    SetGrothendieckC' : C;
     SetGrothendieckX' : F' SetGrothendieckC'
   }.
 
@@ -86,8 +86,8 @@
 
   Hint Extern 1 (@eq (sig _) _ _) => simpl_eq : category.
 
-  Definition CategoryOfElements : @SpecializedCategory GrothendieckPair.
-    refine (@Build_SpecializedCategory _
+  Definition CategoryOfElements : SpecializedCategory.
+    refine (@Build_SpecializedCategory GrothendieckPair
                                        (fun s d =>
                                           { f : C.(Morphism) (GrothendieckC s) (GrothendieckC d) | F.(MorphismOf) f (GrothendieckX s) = (GrothendieckX d) })
                                        (fun o => GrothendieckIdentity (GrothendieckC o) (GrothendieckX o))
@@ -109,7 +109,7 @@
 End Grothendieck.
 
 Section SetGrothendieckCoercion.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Variable F : SpecializedFunctor C SetCat.
   Let F' := (F : SpecializedFunctorToSet _) : SpecializedFunctorToType _.
 
diff -r 4eb6407c6ca3 GrothendieckCat.v
--- a/GrothendieckCat.v	Fri May 24 20:09:37 2013 -0400
+++ b/GrothendieckCat.v	Sat Jun 22 12:51:34 2013 -0400
@@ -29,11 +29,11 @@
      [Hom (Γ F) (c1, x1) (c2, x2)] is the set of morphisms
      [f : c1 -> c2] in [C] such that [F.(MorphismOf) f x1 = x2].
      *)
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Variable F : SpecializedFunctor C Cat.
 
   Record CatGrothendieckPair := {
-    CatGrothendieckC' : objC;
+    CatGrothendieckC' : C;
     CatGrothendieckX' : F CatGrothendieckC'
   }.
 
diff -r 4eb6407c6ca3 GrothendieckFunctorial.v
--- a/GrothendieckFunctorial.v	Fri May 24 20:09:37 2013 -0400
+++ b/GrothendieckFunctorial.v	Sat Jun 22 12:51:34 2013 -0400
@@ -14,7 +14,7 @@
   Local Open Scope category_scope.
   Local Notation "Cat / C" := (SliceSpecializedCategoryOver Cat C).
 
-  Context `(C : @LocallySmallSpecializedCategory objC).
+  Context `(C : @LocallySmallSpecializedCategory).
 
   Let Cat := LocallySmallCat.
 
@@ -29,7 +29,7 @@
         end.
         hnf; simpl.
         exists (((CategoryOfElements x
-                  : LocallySmallSpecializedCategory _)
+                  : LocallySmallSpecializedCategory)
                  : LocallySmallCategory),
                tt).
         exact (GrothendieckFunctor _).
@@ -103,7 +103,7 @@
     Definition CategoryOfElementsFunctorial'
     : SpecializedFunctor (TypeCat ^ C) Cat.
       refine (Build_SpecializedFunctor (TypeCat ^ C) Cat
-                                       (fun x => CategoryOfElements x : LocallySmallSpecializedCategory _)
+                                       (fun x => CategoryOfElements x : LocallySmallSpecializedCategory)
                                        CategoryOfElementsFunctorial'_MorphismOf
                                        _
                                        _);
diff -r 4eb6407c6ca3 GroupCategory.v
--- a/GroupCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/GroupCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -24,7 +24,7 @@
 Ltac destruct_Trues := destruct_singleton_constructor I.
 
 Section as_category.
-  Definition CategoryOfGroup (G : Group) : SpecializedCategory unit.
+  Definition CategoryOfGroup (G : Group) : SpecializedCategory.
     refine (@Build_SpecializedCategory unit
                                        (fun _ _ => G)
                                        (fun _ => @GroupIdentity G)
@@ -39,8 +39,8 @@
 Coercion CategoryOfGroup : Group >-> SpecializedCategory.
 
 Section category_of_groups.
-  Definition GroupCat : SpecializedCategory Group
-    := Eval unfold ComputableCategory in ComputableCategory _ CategoryOfGroup.
+  Definition GroupCat : SpecializedCategory
+    := Eval unfold ComputableCategory in ComputableCategory CategoryOfGroup.
 End category_of_groups.
 
 Section forgetful_functor.
diff -r 4eb6407c6ca3 Groupoid.v
--- a/Groupoid.v	Fri May 24 20:09:37 2013 -0400
+++ b/Groupoid.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,9 +11,9 @@
 Set Universe Polymorphism.
 
 Section GroupoidOf.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
-  Inductive GroupoidOf_Morphism (s d : objC) :=
+  Inductive GroupoidOf_Morphism (s d : C) :=
   | hasMorphism : C.(Morphism) s d -> GroupoidOf_Morphism s d
   | hasInverse : C.(Morphism) d s -> GroupoidOf_Morphism s d
   | byComposition : forall e, GroupoidOf_Morphism e d -> GroupoidOf_Morphism s e -> GroupoidOf_Morphism s d.
@@ -28,7 +28,7 @@
   (** Quoting Wikipedia:
      A groupoid is a small category in which every morphism is an isomorphism, and hence invertible.
      *)
-  Definition GroupoidOf : @SpecializedCategory objC.
+  Definition GroupoidOf : SpecializedCategory.
     refine (@Build_SpecializedCategory _
                                        (fun s d => inhabited (GroupoidOf_Morphism s d))
                                        (fun o : C => inhabits (hasMorphism _ _ (Identity o)))
@@ -46,7 +46,7 @@
 Hint Constructors GroupoidOf_Morphism : category.
 
 Section Groupoid.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Lemma GroupoidOf_Groupoid : CategoryIsGroupoid (GroupoidOf C).
     hnf; intros s d m; hnf; destruct m as [ m ]; induction m;
diff -r 4eb6407c6ca3 Hom.v
--- a/Hom.v	Fri May 24 20:09:37 2013 -0400
+++ b/Hom.v	Sat Jun 22 12:51:34 2013 -0400
@@ -17,12 +17,12 @@
 
 Section covariant_contravariant.
   Local Arguments InducedProductSndFunctor / _ _ _ _ _ _ _ _ _ _ _.
-  Definition CovariantHomFunctor `(C : @SpecializedCategory objC) (A : OppositeCategory C) :=
+  Definition CovariantHomFunctor `(C : SpecializedCategory) (A : OppositeCategory C) :=
     Eval simpl in ((HomFunctor C) [ A, - ])%functor.
-  Definition ContravariantHomFunctor `(C : @SpecializedCategory objC) (A : C) := ((HomFunctor C) [ -, A ])%functor.
+  Definition ContravariantHomFunctor `(C : SpecializedCategory) (A : C) := ((HomFunctor C) [ -, A ])%functor.
 
-  Definition CovariantHomSetFunctor `(C : @LocallySmallSpecializedCategory objC morC) (A : OppositeCategory C) := ((HomSetFunctor C) [ A, - ])%functor.
-  Definition ContravariantHomSetFunctor `(C : @LocallySmallSpecializedCategory objC morC) (A : C) := ((HomSetFunctor C) [ -, A ])%functor.
+  Definition CovariantHomSetFunctor `(C : @LocallySmallSpecializedCategory morC) (A : OppositeCategory C) := ((HomSetFunctor C) [ A, - ])%functor.
+  Definition ContravariantHomSetFunctor `(C : @LocallySmallSpecializedCategory morC) (A : C) := ((HomSetFunctor C) [ -, A ])%functor.
 End covariant_contravariant.
 
 but that would introduce an extra identity morphism which some tactics
@@ -30,7 +30,7 @@
 *)
 
 Section HomFunctor.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Let COp := OppositeCategory C.
 
   Section Covariant.
@@ -89,7 +89,7 @@
 End HomFunctor.
 
 Section SplitHomFunctor.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Let COp := OppositeCategory C.
 
   Lemma SplitHom (X Y : COp * C) : forall gh,
diff -r 4eb6407c6ca3 IndiscreteCategory.v
--- a/IndiscreteCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/IndiscreteCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,7 +13,7 @@
   (** The indiscrete category has exactly one morphism between any two objects. *)
   Variable O : Type.
 
-  Definition IndiscreteCategory : @SpecializedCategory O
+  Definition IndiscreteCategory : SpecializedCategory
     := @Build_SpecializedCategory O
                                   (fun _ _ => unit)
                                   (fun _ => tt)
@@ -25,8 +25,8 @@
 
 Section FunctorToIndiscrete.
   Variable O : Type.
-  Context `(C : @SpecializedCategory objC).
-  Variable objOf : objC -> O.
+  Context `(C : SpecializedCategory).
+  Variable objOf : C -> O.
 
   Definition FunctorToIndiscrete : SpecializedFunctor C (IndiscreteCategory O)
     := Build_SpecializedFunctor C (IndiscreteCategory O)
diff -r 4eb6407c6ca3 InducedLimitFunctors.v
--- a/InducedLimitFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/InducedLimitFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -14,14 +14,14 @@
      a category that we're coming from.  So prove them separately, so
      we can use them elsewhere, without assuming a full [HasLimits]. *)
   Variable I : Type.
-  Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+  Variable Index2Cat : I -> SpecializedCategory.
 
   Local Coercion Index2Cat : I >-> SpecializedCategory.
 
-  Local Notation "'CAT' ⇑ D" := (@LaxCosliceSpecializedCategory _ _ Index2Cat _ D).
-  Local Notation "'CAT' ⇓ D" := (@LaxSliceSpecializedCategory _ _ Index2Cat _ D).
+  Local Notation "'CAT' ⇑ D" := (@LaxCosliceSpecializedCategory _ Index2Cat D).
+  Local Notation "'CAT' ⇓ D" := (@LaxSliceSpecializedCategory _ Index2Cat D).
 
-  Context `(D : @SpecializedCategory objD).
+  Context `(D : SpecializedCategory).
   Let DOp := OppositeCategory D.
 
   Section Limit.
diff -r 4eb6407c6ca3 InitialTerminalCategory.v
--- a/InitialTerminalCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/InitialTerminalCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,19 +10,19 @@
 Set Universe Polymorphism.
 
 Section InitialTerminal.
-   Definition InitialCategory : SmallSpecializedCategory _ := 0.
-   Definition TerminalCategory : SmallSpecializedCategory _ := 1.
+   Definition InitialCategory : SmallSpecializedCategory := 0.
+   Definition TerminalCategory : SmallSpecializedCategory := 1.
 End InitialTerminal.
 
 Section Functors.
-  Context `(C : SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition FunctorTo1 : SpecializedFunctor C 1
     := Build_SpecializedFunctor C 1 (fun _ => tt) (fun _ _ _ => eq_refl) (fun _ _ _ _ _ => eq_refl) (fun _ => eq_refl).
   Definition FunctorToTerminal : SpecializedFunctor C TerminalCategory := FunctorTo1.
 
   Definition FunctorFrom1 (c : C) : SpecializedFunctor 1 C
-    := Build_SpecializedFunctor 1 C (fun _ => c) (fun _ _ _ => Identity c) (fun _ _ _ _ _ => eq_sym (@RightIdentity _ _ _ _ _)) (fun _ => eq_refl).
+    := Build_SpecializedFunctor 1 C (fun _ => c) (fun _ _ _ => Identity c) (fun _ _ _ _ _ => eq_sym (@RightIdentity _ _ _ _)) (fun _ => eq_refl).
   Definition FunctorFromTerminal (c : C) : SpecializedFunctor TerminalCategory C := FunctorFrom1 c.
 
   Definition FunctorFrom0 : SpecializedFunctor 0 C
@@ -31,7 +31,7 @@
 End Functors.
 
 Section FunctorsUnique.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Lemma InitialCategoryFunctorUnique
   : forall F F' : SpecializedFunctor InitialCategory C,
diff -r 4eb6407c6ca3 LaxCommaCategory.v
--- a/LaxCommaCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/LaxCommaCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,8 +13,8 @@
 Local Open Scope category_scope.
 
 Local Ltac fold_functor := idtac. (*
-  change (@SpecializedFunctor) with (fun objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD) => @Functor C D) in *;
-    change (@SpecializedNaturalTransformation) with (fun objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD)
+  change (@SpecializedFunctor) with (fun objC (C : SpecializedCategory) objD (D : SpecializedCategory) => @Functor C D) in *;
+    change (@SpecializedNaturalTransformation) with (fun objC (C : SpecializedCategory) objD (D : SpecializedCategory)
       (F G : SpecializedFunctor C D)
       => @NaturalTransformation C D F G) in *. *)
 
@@ -26,7 +26,7 @@
 
   Local Coercion Index2Cat : I >-> Category.
 
-  Let Cat := ComputableCategory _ Index2Cat.
+  Let Cat := ComputableCategory Index2Cat.
 
   Variable C : Category.
 
@@ -34,20 +34,20 @@
      removing [Specialized], so that we have smaller definitions.
      *)
 
-  Let LaxSliceCategory_Object' := Eval hnf in LaxSliceSpecializedCategory_ObjectT _ Index2Cat C.
+  Let LaxSliceCategory_Object' := Eval hnf in LaxSliceSpecializedCategory_ObjectT Index2Cat C.
   Let LaxSliceCategory_Object'' : Type.
     simpl_definition_by_tac_and_exact LaxSliceCategory_Object' ltac:(simpl in *; fold_functor; simpl in *).
   Defined.
   Definition LaxSliceCategory_Object := Eval hnf in LaxSliceCategory_Object''.
 
-  Let LaxSliceCategory_Morphism' (XG X'G' : LaxSliceCategory_Object) := Eval hnf in @LaxSliceSpecializedCategory_MorphismT _ _ Index2Cat _ C XG X'G'.
+  Let LaxSliceCategory_Morphism' (XG X'G' : LaxSliceCategory_Object) := Eval hnf in @LaxSliceSpecializedCategory_MorphismT _ Index2Cat C XG X'G'.
   Let LaxSliceCategory_Morphism'' (XG X'G' : LaxSliceCategory_Object) : Type.
     simpl_definition_by_tac_and_exact (LaxSliceCategory_Morphism' XG X'G') ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
   Defined.
   Definition LaxSliceCategory_Morphism (XG X'G' : LaxSliceCategory_Object) := Eval hnf in LaxSliceCategory_Morphism'' XG X'G'.
 
   Let LaxSliceCategory_Compose' s d d' Fα F'α'
-    := Eval hnf in @LaxSliceSpecializedCategory_Compose _ _ Index2Cat _ C s d d' Fα F'α'.
+    := Eval hnf in @LaxSliceSpecializedCategory_Compose _ Index2Cat C s d d' Fα F'α'.
   Let LaxSliceCategory_Compose'' s d d' (Fα : LaxSliceCategory_Morphism d d') (F'α' : LaxSliceCategory_Morphism s d) :
     LaxSliceCategory_Morphism s d'.
     simpl_definition_by_tac_and_exact (@LaxSliceCategory_Compose' s d d' Fα F'α') ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
@@ -56,7 +56,7 @@
     LaxSliceCategory_Morphism s d'
     := Eval hnf in @LaxSliceCategory_Compose'' s d d' Fα F'α'.
 
-  Let LaxSliceCategory_Identity' o := Eval hnf in @LaxSliceSpecializedCategory_Identity _ _ Index2Cat _ C o.
+  Let LaxSliceCategory_Identity' o := Eval hnf in @LaxSliceSpecializedCategory_Identity _ Index2Cat C o.
   Let LaxSliceCategory_Identity'' (o : LaxSliceCategory_Object) : LaxSliceCategory_Morphism o o.
     simpl_definition_by_tac_and_exact (@LaxSliceCategory_Identity' o) ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
   Defined.
@@ -68,19 +68,19 @@
 
   Lemma LaxSliceCategory_Associativity o1 o2 o3 o4 (m1 : LaxSliceCategory_Morphism o1 o2) (m2 : LaxSliceCategory_Morphism o2 o3) (m3 : LaxSliceCategory_Morphism o3 o4) :
     LaxSliceCategory_Compose (LaxSliceCategory_Compose m3 m2) m1 = LaxSliceCategory_Compose m3 (LaxSliceCategory_Compose m2 m1).
-    abstract apply (@LaxSliceSpecializedCategory_Associativity _ _ Index2Cat _ C o1 o2 o3 o4 m1 m2 m3).
+    abstract apply (@LaxSliceSpecializedCategory_Associativity _ Index2Cat C o1 o2 o3 o4 m1 m2 m3).
   Qed.
 
   Lemma LaxSliceCategory_LeftIdentity (a b : LaxSliceCategory_Object) (f : LaxSliceCategory_Morphism a b) :
     LaxSliceCategory_Compose (LaxSliceCategory_Identity b) f = f.
   Proof.
-    abstract apply (@LaxSliceSpecializedCategory_LeftIdentity _ _ Index2Cat _ C a b f).
+    abstract apply (@LaxSliceSpecializedCategory_LeftIdentity _ Index2Cat C a b f).
   Qed.
 
   Lemma LaxSliceCategory_RightIdentity (a b : LaxSliceCategory_Object) (f : LaxSliceCategory_Morphism a b) :
     LaxSliceCategory_Compose f (LaxSliceCategory_Identity a) = f.
   Proof.
-    abstract apply (@LaxSliceSpecializedCategory_RightIdentity _ _ Index2Cat _ C a b f).
+    abstract apply (@LaxSliceSpecializedCategory_RightIdentity _ Index2Cat C a b f).
   Qed.
 
   Definition LaxSliceCategory : Category.
@@ -104,7 +104,7 @@
 
   Local Coercion Index2Cat : I >-> Category.
 
-  Let Cat := ComputableCategory _ Index2Cat.
+  Let Cat := ComputableCategory Index2Cat.
 
   Variable C : Category.
 
@@ -114,14 +114,14 @@
   Defined.
   Definition LaxCosliceCategory_Object := Eval hnf in LaxCosliceCategory_Object''.
 
-  Let LaxCosliceCategory_Morphism' (XG X'G' : LaxCosliceCategory_Object) := Eval hnf in @LaxCosliceSpecializedCategory_MorphismT _ _ Index2Cat _ C XG X'G'.
+  Let LaxCosliceCategory_Morphism' (XG X'G' : LaxCosliceCategory_Object) := Eval hnf in @LaxCosliceSpecializedCategory_MorphismT _ Index2Cat C XG X'G'.
   Let LaxCosliceCategory_Morphism'' (XG X'G' : LaxCosliceCategory_Object) : Type.
     simpl_definition_by_tac_and_exact (LaxCosliceCategory_Morphism' XG X'G') ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
   Defined.
   Definition LaxCosliceCategory_Morphism (XG X'G' : LaxCosliceCategory_Object) := Eval hnf in LaxCosliceCategory_Morphism'' XG X'G'.
 
   Let LaxCosliceCategory_Compose' s d d' Fα F'α'
-    := Eval hnf in @LaxCosliceSpecializedCategory_Compose _ _ Index2Cat _ C s d d' Fα F'α'.
+    := Eval hnf in @LaxCosliceSpecializedCategory_Compose _ Index2Cat C s d d' Fα F'α'.
   Let LaxCosliceCategory_Compose'' s d d' (Fα : LaxCosliceCategory_Morphism d d') (F'α' : LaxCosliceCategory_Morphism s d) :
     LaxCosliceCategory_Morphism s d'.
     simpl_definition_by_tac_and_exact (@LaxCosliceCategory_Compose' s d d' Fα F'α') ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
@@ -130,7 +130,7 @@
     LaxCosliceCategory_Morphism s d'
     := Eval hnf in @LaxCosliceCategory_Compose'' s d d' Fα F'α'.
 
-  Let LaxCosliceCategory_Identity' o := Eval hnf in @LaxCosliceSpecializedCategory_Identity _ _ Index2Cat _ C o.
+  Let LaxCosliceCategory_Identity' o := Eval hnf in @LaxCosliceSpecializedCategory_Identity _ Index2Cat C o.
   Let LaxCosliceCategory_Identity'' (o : LaxCosliceCategory_Object) : LaxCosliceCategory_Morphism o o.
     simpl_definition_by_tac_and_exact (@LaxCosliceCategory_Identity' o) ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
   Defined.
@@ -142,19 +142,19 @@
 
   Lemma LaxCosliceCategory_Associativity o1 o2 o3 o4 (m1 : LaxCosliceCategory_Morphism o1 o2) (m2 : LaxCosliceCategory_Morphism o2 o3) (m3 : LaxCosliceCategory_Morphism o3 o4) :
     LaxCosliceCategory_Compose (LaxCosliceCategory_Compose m3 m2) m1 = LaxCosliceCategory_Compose m3 (LaxCosliceCategory_Compose m2 m1).
-    abstract apply (@LaxCosliceSpecializedCategory_Associativity _ _ Index2Cat _ C o1 o2 o3 o4 m1 m2 m3).
+    abstract apply (@LaxCosliceSpecializedCategory_Associativity _ Index2Cat C o1 o2 o3 o4 m1 m2 m3).
   Qed.
 
   Lemma LaxCosliceCategory_LeftIdentity (a b : LaxCosliceCategory_Object) (f : LaxCosliceCategory_Morphism a b) :
     LaxCosliceCategory_Compose (LaxCosliceCategory_Identity b) f = f.
   Proof.
-    abstract apply (@LaxCosliceSpecializedCategory_LeftIdentity _ _ Index2Cat _ C a b f).
+    abstract apply (@LaxCosliceSpecializedCategory_LeftIdentity _ Index2Cat C a b f).
   Qed.
 
   Lemma LaxCosliceCategory_RightIdentity (a b : LaxCosliceCategory_Object) (f : LaxCosliceCategory_Morphism a b) :
     LaxCosliceCategory_Compose f (LaxCosliceCategory_Identity a) = f.
   Proof.
-    abstract apply (@LaxCosliceSpecializedCategory_RightIdentity _ _ Index2Cat _ C a b f).
+    abstract apply (@LaxCosliceSpecializedCategory_RightIdentity _ Index2Cat C a b f).
   Qed.
 
   Definition LaxCosliceCategory : Category.
diff -r 4eb6407c6ca3 LimitFunctorTheorems.v
--- a/LimitFunctorTheorems.v	Fri May 24 20:09:37 2013 -0400
+++ b/LimitFunctorTheorems.v	Sat Jun 22 12:51:34 2013 -0400
@@ -34,9 +34,9 @@
      injects one set into its union with another and [lim G] projects a
      product of two sets onto one factor.
      *)
-  Context `(C1 : @SpecializedCategory objC1).
-  Context `(C2 : @SpecializedCategory objC2).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C1 : SpecializedCategory).
+  Context `(C2 : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F1 : SpecializedFunctor C1 D.
   Variable F2 : SpecializedFunctor C2 D.
   Variable G : SpecializedFunctor C1 C2.
diff -r 4eb6407c6ca3 LimitFunctors.v
--- a/LimitFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/LimitFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,8 +12,8 @@
 Local Open Scope category_scope.
 
 Section LimitFunctors.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Definition HasLimits' := forall F : SpecializedFunctor D C, exists _ : Limit F, True.
   Definition HasLimits := forall F : SpecializedFunctor D C, Limit F.
@@ -25,9 +25,9 @@
   Hypothesis HC : HasColimits.
 
   Definition LimitFunctor : SpecializedFunctor (C ^ D) C
-    := Eval unfold AdjointFunctorOfTerminalMorphism in AdjointFunctorOfTerminalMorphism HL.
+    := Eval unfold AdjointFunctorOfTerminalMorphism in AdjointFunctorOfTerminalMorphism (D := C ^ D) HL.
   Definition ColimitFunctor : SpecializedFunctor (C ^ D) C
-    := Eval unfold AdjointFunctorOfInitialMorphism in AdjointFunctorOfInitialMorphism HC.
+    := Eval unfold AdjointFunctorOfInitialMorphism in AdjointFunctorOfInitialMorphism (C := C ^ D) HC.
 
   Definition LimitAdjunction : Adjunction (DiagonalFunctor C D) LimitFunctor
     := AdjunctionOfTerminalMorphism _.
diff -r 4eb6407c6ca3 Limits.v
--- a/Limits.v	Fri May 24 20:09:37 2013 -0400
+++ b/Limits.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,8 +12,8 @@
 Local Open Scope category_scope.
 
 Section DiagonalFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   (**
      Quoting Dwyer and Spalinski:
@@ -63,9 +63,9 @@
 End DiagonalFunctor.
 
 Section DiagonalFunctorLemmas.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(D' : @SpecializedCategory objD').
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(D' : SpecializedCategory).
 
   Lemma Compose_DiagonalFunctor x (F : SpecializedFunctor D' D) :
     ComposeFunctors (DiagonalFunctor C D x) F = DiagonalFunctor _ _ x.
@@ -83,8 +83,8 @@
 Hint Rewrite @Compose_DiagonalFunctor.
 
 Section Limit.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor D C.
 
   (**
@@ -160,8 +160,8 @@
 End Limit.
 
 Section LimitMorphisms.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor D C.
 
   Definition MorphismBetweenLimits (L L' : Limit F) : C.(Morphism) (LimitObject L) (LimitObject L').
diff -r 4eb6407c6ca3 LtacReifiedSimplification.v
--- a/LtacReifiedSimplification.v	Fri May 24 20:09:37 2013 -0400
+++ b/LtacReifiedSimplification.v	Sat Jun 22 12:51:34 2013 -0400
@@ -18,70 +18,69 @@
     repeat rewrite ?FCompositionOf.
 
 Section ReifiedMorphism.
-  Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
-  | ReifiedIdentityMorphism : forall objC C x, @ReifiedMorphism objC C x x
-  | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'
-  | ReifiedNaturalTransformationMorphism : forall objB (B : SpecializedCategory objB)
-                                                  objC (C : SpecializedCategory objC)
+  Inductive ReifiedMorphism : forall (C : SpecializedCategory), C -> C -> Type :=
+  | ReifiedIdentityMorphism : forall C x, @ReifiedMorphism C x x
+  | ReifiedComposedMorphism : forall C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism C s d'
+  | ReifiedNaturalTransformationMorphism : forall (B : SpecializedCategory)
+                                                  (C : SpecializedCategory)
                                                   (F G : SpecializedFunctor B C)
                                                   (T : SpecializedNaturalTransformation F G)
                                                   x,
                                              ReifiedMorphism C (F x) (G x)
-  | ReifiedFunctorMorphism : forall objB (B : SpecializedCategory objB)
-                                    objC (C : SpecializedCategory objC)
+  | ReifiedFunctorMorphism : forall (B : SpecializedCategory)
+                                    (C : SpecializedCategory)
                                     (F : SpecializedFunctor B C)
                                     s d,
-                               @ReifiedMorphism objB B s d -> @ReifiedMorphism objC C (F s) (F d)
-  | ReifiedGenericMorphism : forall objC (C : SpecializedCategory objC) s d, Morphism C s d -> @ReifiedMorphism objC C s d.
+                               @ReifiedMorphism B s d -> @ReifiedMorphism C (F s) (F d)
+  | ReifiedGenericMorphism : forall (C : SpecializedCategory) s d, Morphism C s d -> @ReifiedMorphism C s d.
 
-  Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
-    match m in @ReifiedMorphism objC C s d return Morphism C s d with
-      | ReifiedIdentityMorphism _ _ x => Identity x
-      | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
-                                                           (@ReifiedMorphismDenote _ _ _ _ m2)
-      | ReifiedNaturalTransformationMorphism _ _ _ _ _ _ T x => T x
-      | ReifiedFunctorMorphism _ _ _ _ F _ _ m => MorphismOf F (@ReifiedMorphismDenote _ _ _ _ m)
-      | ReifiedGenericMorphism _ _ _ _ m => m
+  Fixpoint ReifiedMorphismDenote C s d (m : @ReifiedMorphism C s d) : Morphism C s d :=
+    match m in @ReifiedMorphism C s d return Morphism C s d with
+      | ReifiedIdentityMorphism _ x => Identity x
+      | ReifiedComposedMorphism _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ m1)
+                                                           (@ReifiedMorphismDenote _ _ _ m2)
+      | ReifiedNaturalTransformationMorphism _ _ _ _ T x => T x
+      | ReifiedFunctorMorphism _ _ F _ _ m => MorphismOf F (@ReifiedMorphismDenote _ _ _ m)
+      | ReifiedGenericMorphism _ _ _ m => m
     end.
 End ReifiedMorphism.
 
 Ltac Ltac_reify_morphism m :=
-  let objC := match type of m with @Morphism ?objC _ ?s ?d => constr:(objC) end in
-  let C := match type of m with @Morphism ?objC ?C ?s ?d => constr:(C) end in
-  let s := match type of m with @Morphism ?objC _ ?s ?d => constr:(s) end in
-  let d := match type of m with @Morphism ?objC _ ?s ?d => constr:(d) end in
+  let C := match type of m with @Morphism ?C ?s ?d => constr:(C) end in
+  let s := match type of m with @Morphism ?C ?s ?d => constr:(s) end in
+  let d := match type of m with @Morphism ?C ?s ?d => constr:(d) end in
   match m with
-    | @Identity _ _ ?x => constr:(@ReifiedIdentityMorphism _ C x)
+    | @Identity _ ?x => constr:(@ReifiedIdentityMorphism C x)
     | Compose ?m1 ?m2 => let m1' := Ltac_reify_morphism m1 in
                          let m2' := Ltac_reify_morphism m2 in
-                         constr:(@ReifiedComposedMorphism _ _ _ _ _ m1' m2')
-    | ComponentsOf ?T ?x => constr:(@ReifiedNaturalTransformationMorphism _ _ _ _ _ _ T x)
+                         constr:(@ReifiedComposedMorphism _ _ _ _ m1' m2')
+    | ComponentsOf ?T ?x => constr:(@ReifiedNaturalTransformationMorphism _ _ _ _ T x)
     | MorphismOf ?F ?m => let m' := Ltac_reify_morphism m in
-                          constr:(@ReifiedFunctorMorphism _ _ _ _ F _ _ m')
+                          constr:(@ReifiedFunctorMorphism _ _ F _ _ m')
     | ReifiedMorphismDenote ?m' => constr:(m')
-    | _ => constr:(@ReifiedGenericMorphism objC C s d m)
+    | _ => constr:(@ReifiedGenericMorphism C s d m)
   end.
 
 Section SimplifiedMorphism.
-  Fixpoint ReifiedHasIdentities `(m : @ReifiedMorphism objC C s d) : bool
+  Fixpoint ReifiedHasIdentities `(m : @ReifiedMorphism C s d) : bool
     := match m with
-         | ReifiedIdentityMorphism _ _ _ => true
-         | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => orb (@ReifiedHasIdentities _ _ _ _ m1) (@ReifiedHasIdentities _ _ _ _ m2)
-         | ReifiedNaturalTransformationMorphism _ _ _ _ _ _ _ _ => false
-         | ReifiedFunctorMorphism _ _ _ _ _ _ _ m0 => (@ReifiedHasIdentities _ _ _ _ m0)
-         | ReifiedGenericMorphism _ _ _ _ _ => false
+         | ReifiedIdentityMorphism _ _ => true
+         | ReifiedComposedMorphism _ _ _ _ m1 m2 => orb (@ReifiedHasIdentities _ _ _ m1) (@ReifiedHasIdentities _ _ _ m2)
+         | ReifiedNaturalTransformationMorphism _ _ _ _ _ _ => false
+         | ReifiedFunctorMorphism _ _ _ _ _ m0 => (@ReifiedHasIdentities _ _ _ m0)
+         | ReifiedGenericMorphism _ _ _ _ => false
        end.
 
-  Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d) {struct m}
+  Fixpoint ReifiedMorphismSimplifyWithProof C s d (m : @ReifiedMorphism C s d) {struct m}
   : { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
   refine match m with
-           | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
-           | ReifiedFunctorMorphism _ _ _ _ F _ _ m' => _
-           | ReifiedIdentityMorphism _ _ x => exist _ _ eq_refl
-           | ReifiedNaturalTransformationMorphism _ _ _ _ _ _ T x => exist _ _ eq_refl
-           | ReifiedGenericMorphism _ _ _ _ m => exist _ _ eq_refl
+           | ReifiedComposedMorphism _ s0 d0 d0' m1 m2 => _
+           | ReifiedFunctorMorphism _ _ F _ _ m' => _
+           | ReifiedIdentityMorphism _ x => exist _ _ eq_refl
+           | ReifiedNaturalTransformationMorphism _ _ _ _ T x => exist _ _ eq_refl
+           | ReifiedGenericMorphism _ _ _ m => exist _ _ eq_refl
          end; clear m;
-  [ destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ m1' H1 ], (@ReifiedMorphismSimplifyWithProof _ _ _ _ m2) as [ m2' H2 ];
+  [ destruct (@ReifiedMorphismSimplifyWithProof _ _ _ m1) as [ m1' H1 ], (@ReifiedMorphismSimplifyWithProof _ _ _ m2) as [ m2' H2 ];
     clear ReifiedMorphismSimplifyWithProof;
     destruct m1';
     ((destruct m2')
@@ -97,42 +96,40 @@
          match type of m2' with
            | ReifiedMorphism _ _ (?f ?x) => generalize dependent (f x); intros; destruct m2'
          end))
-    | destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m') as [ m'' ? ];
+    | destruct (@ReifiedMorphismSimplifyWithProof _ _ _ m') as [ m'' ? ];
       clear ReifiedMorphismSimplifyWithProof;
       destruct m''];
   simpl in *;
-  match goal with
-    | [ |- { m' : _ | ?m'' = ReifiedMorphismDenote m' } ]
-      => let T := type of m'' in
-         let t := fresh in
-         let H := fresh in
-         evar (t : T);
-           assert (H : t = m'');
-           [ repeat match goal with
-                      | [ H : ReifiedMorphismDenote _ = _ |- _ ] => rewrite H; clear H
-                    end;
-             do_simplification;
-             subst t;
-             reflexivity
-           | ];
-           instantiate;
-           let m := (eval unfold t in t) in
-           let m' := Ltac_reify_morphism m in
-           (exists m');
-             clear H t
-  end;
-  repeat match goal with
-           | [ H : _ = _ |- _ ] => revert H
-           | _ => clear
-         end;
-  intros;
-  abstract (
-      repeat match goal with
+  let m'' := match goal with | [ |- { m' : _ | ?m'' = ReifiedMorphismDenote m' } ] => constr:(m'') end in
+  let T := type of m'' in
+  let t := fresh in
+  let H := fresh in
+  evar (t : T);
+    assert (H : t = m'');
+    [ repeat match goal with
                | [ H : ReifiedMorphismDenote _ = _ |- _ ] => rewrite H; clear H
              end;
       do_simplification;
+      subst t;
       reflexivity
-    ).
+    | ];
+    instantiate;
+    let m := (eval unfold t in t) in
+    let m' := Ltac_reify_morphism m in
+    (exists m');
+      clear H t;
+      repeat match goal with
+               | [ H : _ = _ |- _ ] => revert H
+               | _ => clear
+             end;
+      intros;
+      abstract (
+          repeat match goal with
+                   | [ H : ReifiedMorphismDenote _ = _ |- _ ] => rewrite H; clear H
+                 end;
+          do_simplification;
+          reflexivity
+        ).
   Defined.
 
   Local Ltac solve_t :=
@@ -179,16 +176,16 @@
       destruct H';
       simpl in H.
 
-  Fixpoint ReifiedMorphismSimplifyWithProofNoIdentity `(C : @SpecializedCategory objC) s d
+  Fixpoint ReifiedMorphismSimplifyWithProofNoIdentity `(C : SpecializedCategory) s d
            (m : ReifiedMorphism C s d)
   : {ReifiedHasIdentities (proj1_sig (ReifiedMorphismSimplifyWithProof m)) = false}
     + { exists H : s = d, proj1_sig (ReifiedMorphismSimplifyWithProof m) = match H with eq_refl => ReifiedIdentityMorphism C s end }.
   destruct m;
   try solve [ right; clear; abstract (exists eq_refl; subst; reflexivity)
             | left; clear; reflexivity ];
-  [ destruct (@ReifiedMorphismSimplifyWithProofNoIdentity _ _ _ _ m1), (@ReifiedMorphismSimplifyWithProofNoIdentity _ _ _ _ m2);
+  [ destruct (@ReifiedMorphismSimplifyWithProofNoIdentity _ _ _ m1), (@ReifiedMorphismSimplifyWithProofNoIdentity _ _ _ m2);
     [ left | left | left | right ]
-  | destruct (@ReifiedMorphismSimplifyWithProofNoIdentity _ _ _ _ m);
+  | destruct (@ReifiedMorphismSimplifyWithProofNoIdentity _ _ _ m);
     [ left | right ] ];
   clear ReifiedMorphismSimplifyWithProofNoIdentity;
   try abstract (
@@ -211,14 +208,14 @@
   Section ReifiedMorphismSimplify.
     Local Arguments ReifiedMorphismSimplifyWithProof / .
 
-    Definition ReifiedMorphismSimplify objC C s d (m : @ReifiedMorphism objC C s d)
+    Definition ReifiedMorphismSimplify C s d (m : @ReifiedMorphism C s d)
     : ReifiedMorphism C s d
       := Eval simpl in proj1_sig (ReifiedMorphismSimplifyWithProof m).
 
     (*Local Arguments ReifiedMorphismSimplify / .*)
   End ReifiedMorphismSimplify.
 
-  Lemma ReifiedMorphismSimplifyOk objC C s d (m : @ReifiedMorphism objC C s d)
+  Lemma ReifiedMorphismSimplifyOk C s d (m : @ReifiedMorphism C s d)
   : ReifiedMorphismDenote m =
     ReifiedMorphismDenote (ReifiedMorphismSimplify m).
   Proof.
@@ -227,7 +224,7 @@
 
   Local Arguments ReifiedMorphismSimplifyWithProofNoIdentity / .
 
-  Definition ReifiedMorphismSimplifyNoIdentity `(C : @SpecializedCategory objC) s d
+  Definition ReifiedMorphismSimplifyNoIdentity `(C : SpecializedCategory) s d
              (m : ReifiedMorphism C s d)
   : {ReifiedHasIdentities (ReifiedMorphismSimplify m) = false}
     + { exists H : s = d, ReifiedMorphismSimplify m = match H with eq_refl => ReifiedIdentityMorphism C s end }
@@ -252,8 +249,8 @@
 (*******************************************************************************)
 Section good_examples.
   Section id.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objC).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
     Variables F G : SpecializedFunctor C D.
     Variable T : SpecializedNaturalTransformation F G.
 
@@ -276,13 +273,13 @@
   End id.
 
   Lemma good_example_00004
-  : forall (objC : Type) (C : SpecializedCategory objC)
-           (objD : Type) (D : SpecializedCategory objD) (objC' : Type)
-           (C' : SpecializedCategory objC') (objD' : Type)
-           (D' : SpecializedCategory objD') (F : SpecializedFunctor C C')
+  : forall (C : SpecializedCategory)
+           (D : SpecializedCategory)
+           (C' : SpecializedCategory)
+           (D' : SpecializedCategory) (F : SpecializedFunctor C C')
            (G : SpecializedFunctor D' D) (s d d' : SpecializedFunctor D C)
            (m1 : SpecializedNaturalTransformation s d)
-           (m2 : SpecializedNaturalTransformation d d') (x : objD'),
+           (m2 : SpecializedNaturalTransformation d d') (x : D'),
       Compose (MorphismOf F (m2 (G x))) (MorphismOf F (m1 (G x))) =
       Compose
         (Compose
@@ -294,13 +291,13 @@
   Qed.
 
   Lemma good_example_00005
-  : forall (objC : Type) (C : SpecializedCategory objC)
-           (objD : Type) (D : SpecializedCategory objD) (objC' : Type)
-           (C' : SpecializedCategory objC') (objD' : Type)
-           (D' : SpecializedCategory objD') (F : SpecializedFunctor C C')
+  : forall (objC : Type) (C : SpecializedCategory)
+           (objD : Type) (D : SpecializedCategory) (objC' : Type)
+           (C' : SpecializedCategory) (objD' : Type)
+           (D' : SpecializedCategory) (F : SpecializedFunctor C C')
            (G : SpecializedFunctor D' D) (s d d' : SpecializedFunctor D C)
            (m1 : SpecializedNaturalTransformation s d)
-           (m2 : SpecializedNaturalTransformation d d') (x : objD'),
+           (m2 : SpecializedNaturalTransformation d d') (x : D'),
       Compose
         (MorphismOf F
                     (Compose (MorphismOf d' (Identity (G x)))
@@ -324,9 +321,9 @@
 Section bad_examples.
   Require Import SumCategory.
   Section bad_example_0001.
-    Context `(C0 : SpecializedCategory objC0).
-    Context `(C1 : SpecializedCategory objC1).
-    Context `(D : SpecializedCategory objD).
+    Context `(C0 : SpecializedCategory).
+    Context `(C1 : SpecializedCategory).
+    Context `(D : SpecializedCategory).
 
     Variables s d d' : C0.
     Variable m1 : Morphism C0 s d.
diff -r 4eb6407c6ca3 MonoidalCategory.v
--- a/MonoidalCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/MonoidalCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -17,7 +17,7 @@
   (** Quoting Wikipedia:
      A  monoidal category is a category [C] equipped with
      *)
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   (**
      - a bifunctor [ ⊗ : C × C -> C] called the tensor product or
          monoidal product,
@@ -299,7 +299,6 @@
 End PreMonoidalCategory.
 
 Section MonoidalCategory.
-  Variable objC : Type.
   (** Quoting Wikipedia:
      A  monoidal category is a category [C] equipped with
      - a bifunctor [ ⊗ : C × C -> C] called the tensor product or
@@ -357,18 +356,18 @@
   Local Reserved Notation "'λ'".
   Local Reserved Notation "'ρ'".
 
-  Let src (C : @SpecializedCategory objC) {s d} (_ : Morphism C s d) := s.
-  Let dst (C : @SpecializedCategory objC) s d (_ : Morphism C s d) := d.
+  Let src (C : SpecializedCategory) {s d} (_ : Morphism C s d) := s.
+  Let dst (C : SpecializedCategory) s d (_ : Morphism C s d) := d.
 
   Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
   Let UnitorCoherenceCondition' := Eval unfold UnitorCoherenceCondition in @UnitorCoherenceCondition.
 
   Record MonoidalCategory := {
-    MonoidalUnderlyingCategory :> @SpecializedCategory objC;
+    MonoidalUnderlyingCategory :> SpecializedCategory;
     TensorProduct : SpecializedFunctor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory
       where "A ⊗ B" := (TensorProduct (A, B)) and "A ⊗m B" := (TensorProduct.(MorphismOf) (s := (@src _ _ _ A, @src _ _ _ B)) (d := (@dst _ _ _ A, @dst _ _ _ B)) (A, B)%morphism);
 
-    IdentityObject : objC where "'I'" := IdentityObject;
+    IdentityObject : MonoidalUnderlyingCategory where "'I'" := IdentityObject;
 
     Associator : NaturalIsomorphism (TriMonoidalProductL TensorProduct) (TriMonoidalProductR TensorProduct) where "'α'" := Associator;
     LeftUnitor : NaturalIsomorphism (LeftUnitorFunctor TensorProduct I)  (IdentityFunctor _) where "'λ'" := LeftUnitor;
diff -r 4eb6407c6ca3 NaturalEquivalence.v
--- a/NaturalEquivalence.v	Fri May 24 20:09:37 2013 -0400
+++ b/NaturalEquivalence.v	Sat Jun 22 12:51:34 2013 -0400
@@ -17,20 +17,20 @@
 
 Section NaturalIsomorphism.
   Section NaturalIsomorphism.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
     Variables F G : SpecializedFunctor C D.
 
     Record NaturalIsomorphism :=
       {
         NaturalIsomorphism_Transformation :> SpecializedNaturalTransformation F G;
-        NaturalIsomorphism_Isomorphism : forall x : objC, IsomorphismOf (NaturalIsomorphism_Transformation x)
+        NaturalIsomorphism_Isomorphism : forall x : C, IsomorphismOf (NaturalIsomorphism_Transformation x)
       }.
   End NaturalIsomorphism.
 
   Section Inverse.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
     Variables F G : SpecializedFunctor C D.
 
     Definition InverseNaturalIsomorphism_NT (T : NaturalIsomorphism F G) : NaturalTransformation G F.
@@ -56,9 +56,9 @@
   End Inverse.
 
   Section Composition.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-    Context `(E : @SpecializedCategory objE).
+    Context `(C : SpecializedCategory).
+    Context `(D : SpecializedCategory).
+    Context `(E : SpecializedCategory).
     Variables F F' F'' : SpecializedFunctor C D.
     Variables G G' : SpecializedFunctor D E.
 
@@ -94,8 +94,8 @@
 End NaturalIsomorphism.
 
 Section NaturalIsomorphismOfCategories.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Local Reserved Notation "'F'".
   Local Reserved Notation "'G'".
@@ -135,8 +135,8 @@
 Arguments FunctorsNaturallyEquivalent [C D] F G.
 
 Section Coercions.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variables F G : SpecializedFunctor C D.
   Variable C' : Category.
   Variable D' : Category.
diff -r 4eb6407c6ca3 NaturalNumbersObject.v
--- a/NaturalNumbersObject.v	Fri May 24 20:09:37 2013 -0400
+++ b/NaturalNumbersObject.v	Sat Jun 22 12:51:34 2013 -0400
@@ -90,7 +90,7 @@
           [NaturalNumbersPreObject], to make the distinction slightly
           more obvious. *)
 
-  Context `(E : SpecializedCategory objE).
+  Context `(E : SpecializedCategory).
 
   Local Reserved Notation "'ℕ'".
   Local Reserved Notation "'S'".
diff -r 4eb6407c6ca3 NaturalTransformation.v
--- a/NaturalTransformation.v	Fri May 24 20:09:37 2013 -0400
+++ b/NaturalTransformation.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,8 +13,8 @@
 Local Infix "==" := JMeq.
 
 Section SpecializedNaturalTransformation.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variables F G : SpecializedFunctor C D.
 
   (**
@@ -55,19 +55,19 @@
 
 Create HintDb natural_transformation discriminated.
 
-Arguments ComponentsOf {objC%type C%category objD%type D%category F%functor G%functor} T%natural_transformation c%object : rename, simpl nomatch.
-Arguments Commutes [objC C objD D F G] T _ _ _ : rename.
+Arguments ComponentsOf {C%category D%category F%functor G%functor} T%natural_transformation c%object : rename, simpl nomatch.
+Arguments Commutes [C D F G] T _ _ _ : rename.
 
 Identity Coercion NaturalTransformation_SpecializedNaturalTransformation_Id : NaturalTransformation >-> SpecializedNaturalTransformation.
-Definition GeneralizeNaturalTransformation `(T : @SpecializedNaturalTransformation objC C objD D F G) :
+Definition GeneralizeNaturalTransformation `(T : @SpecializedNaturalTransformation C D F G) :
   NaturalTransformation F G := T.
 Global Coercion GeneralizeNaturalTransformation : SpecializedNaturalTransformation >-> NaturalTransformation.
 
-Arguments GeneralizeNaturalTransformation [objC C objD D F G] T /.
+Arguments GeneralizeNaturalTransformation [C D F G] T /.
 Hint Extern 0 => unfold GeneralizeNaturalTransformation : category natural_transformation.
 Ltac fold_NT :=
   change @SpecializedNaturalTransformation with
-    (fun objC (C : SpecializedCategory objC) objD (D : SpecializedCategory objD) => @NaturalTransformation C D) in *; simpl in *.
+    (fun (C : SpecializedCategory) (D : SpecializedCategory) => @NaturalTransformation C D) in *; simpl in *.
 
 Hint Resolve @Commutes : category natural_transformation.
 
@@ -88,13 +88,13 @@
     hnf in H;
     revert H; clear; intro H; clear H;
     match T'' with
-      | @Build_SpecializedNaturalTransformation ?objC ?C
-                                                ?objD ?D
+      | @Build_SpecializedNaturalTransformation ?C
+                                                ?D
                                                 ?F
                                                 ?G
                                                 ?CO
                                                 ?COM =>
-        refine (@Build_SpecializedNaturalTransformation objC C objD D F G
+        refine (@Build_SpecializedNaturalTransformation C D F G
                                                         CO
                                                         _);
           abstract exact COM
@@ -103,8 +103,8 @@
 Ltac nt_simpl_abstract_trailing_props T := nt_tac_abstract_trailing_props T ltac:(fun T' => let T'' := eval simpl in T' in T'').
 
 Section NaturalTransformations_Equal.
-  Lemma NaturalTransformation_contr_eq' objC C objD D F G
-        (T U : @SpecializedNaturalTransformation objC C objD D F G)
+  Lemma NaturalTransformation_contr_eq' C D F G
+        (T U : @SpecializedNaturalTransformation C D F G)
         (D_morphism_proof_irrelevance
          : forall s d (m1 m2 : Morphism D s d) (pf1 pf2 : m1 = m2),
              pf1 = pf2)
@@ -116,8 +116,8 @@
     trivial.
   Qed.
 
-  Lemma NaturalTransformation_contr_eq objC C objD D F G
-        (T U : @SpecializedNaturalTransformation objC C objD D F G)
+  Lemma NaturalTransformation_contr_eq C D F G
+        (T U : @SpecializedNaturalTransformation C D F G)
         (D_morphism_proof_irrelevance
          : forall s d (m1 m2 : Morphism D s d) (pf1 pf2 : m1 = m2),
              pf1 = pf2)
@@ -129,8 +129,8 @@
     trivial.
   Qed.
 
-  Lemma NaturalTransformation_eq' objC C objD D F G :
-    forall (T U : @SpecializedNaturalTransformation objC C objD D F G),
+  Lemma NaturalTransformation_eq' C D F G :
+    forall (T U : @SpecializedNaturalTransformation C D F G),
     ComponentsOf T = ComponentsOf U
     -> T = U.
     intros T U.
@@ -138,8 +138,8 @@
     intros; apply proof_irrelevance.
   Qed.
 
-  Lemma NaturalTransformation_eq objC C objD D F G :
-    forall (T U : @SpecializedNaturalTransformation objC C objD D F G),
+  Lemma NaturalTransformation_eq C D F G :
+    forall (T U : @SpecializedNaturalTransformation C D F G),
     (forall x, ComponentsOf T x = ComponentsOf U x)
     -> T = U.
     intros T U.
@@ -147,13 +147,11 @@
     intros; apply proof_irrelevance.
   Qed.
 
-  Lemma NaturalTransformation_JMeq' objC C objD D objC' C' objD' D' :
+  Lemma NaturalTransformation_JMeq' C D C' D' :
     forall F G F' G'
-      (T : @SpecializedNaturalTransformation objC C objD D F G) (U : @SpecializedNaturalTransformation objC' C' objD' D' F' G'),
-      objC = objC'
-      -> objD = objD'
-      -> C == C'
-      -> D == D'
+      (T : @SpecializedNaturalTransformation C D F G) (U : @SpecializedNaturalTransformation C' D' F' G'),
+      C = C'
+      -> D = D'
       -> F == F'
       -> G == G'
       -> ComponentsOf T == ComponentsOf U
@@ -162,13 +160,11 @@
       JMeq_eq.
     f_equal; apply proof_irrelevance.
   Qed.
-  Lemma NaturalTransformation_JMeq objC C objD D objC' C' objD' D' :
+  Lemma NaturalTransformation_JMeq C D C' D' :
     forall F G F' G'
-      (T : @SpecializedNaturalTransformation objC C objD D F G) (U : @SpecializedNaturalTransformation objC' C' objD' D' F' G'),
-      objC = objC'
-      -> objD = objD'
-      -> C == C'
-      -> D == D'
+      (T : @SpecializedNaturalTransformation C D F G) (U : @SpecializedNaturalTransformation C' D' F' G'),
+      C = C'
+      -> D = D'
       -> F == F'
       -> G == G'
       -> (forall x x', x == x' -> ComponentsOf T x == ComponentsOf U x')
@@ -207,7 +203,7 @@
         let COMT' := type of COM in
         let COMT := (eval simpl in COMT') in
         assert (COM' : COMT) by abstract exact COM;
-          exists (@Build_SpecializedNaturalTransformation objC C objD D F G
+          exists (@Build_SpecializedNaturalTransformation C D F G
                                                           CO
                                                           COM');
           expand; abstract (apply thm; reflexivity) || (apply thm; try reflexivity)
@@ -224,9 +220,9 @@
 Ltac nt_simpl_abstract_trailing_props_with_equality := nt_tac_abstract_trailing_props_with_equality ltac:(fun T' => let T'' := eval simpl in T' in T'').
 
 Section NaturalTransformationComposition.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
   Variables F F' F'' : SpecializedFunctor C D.
   Variables G G' : SpecializedFunctor D E.
 
@@ -309,7 +305,7 @@
   Hint Resolve f_equal2 : natural_transformation.
   Hint Extern 1 (_ = _) => apply @FCompositionOf : natural_transformation.
 
-  Lemma FCompositionOf2 : forall `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD)
+  Lemma FCompositionOf2 : forall `(C : SpecializedCategory) `(D : SpecializedCategory)
     (F : SpecializedFunctor C D) x y z u (m1 : C.(Morphism) x z) (m2 : C.(Morphism) y x) (m3 : D.(Morphism) u _),
     Compose (MorphismOf F m1) (Compose (MorphismOf F m2) m3) = Compose (MorphismOf F (Compose m1 m2)) m3.
     intros; symmetry; try_associativity ltac:(eauto with natural_transformation).
@@ -329,8 +325,8 @@
 End NaturalTransformationComposition.
 
 Section IdentityNaturalTransformation.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor C D.
 
   (* There is an identity natrual transformation. *)
@@ -354,9 +350,9 @@
 Hint Rewrite @LeftIdentityNaturalTransformation @RightIdentityNaturalTransformation : natural_transformation.
 
 Section IdentityNaturalTransformationF.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
   Variable G : SpecializedFunctor D E.
   Variable F : SpecializedFunctor C D.
 
@@ -371,10 +367,10 @@
 Hint Rewrite @NTComposeFIdentityNaturalTransformation : natural_transformation.
 
 Section Associativity.
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
   Variable F : SpecializedFunctor D E.
   Variable G : SpecializedFunctor C D.
   Variable H : SpecializedFunctor B C.
@@ -406,8 +402,8 @@
 End Associativity.
 
 Section IdentityFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Local Ltac t :=
     repeat match goal with
@@ -447,9 +443,9 @@
 End IdentityFunctor.
 
 Section NaturalTransformationExchangeLaw.
-  Context `(C : SpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
-  Context `(E : SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
 
   Variables F G H : SpecializedFunctor C D.
   Variables F' G' H' : SpecializedFunctor D E.
diff -r 4eb6407c6ca3 PathsCategory.v
--- a/PathsCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/PathsCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -14,8 +14,8 @@
   Hint Immediate concatenate_associative.
   Hint Rewrite concatenate_associative.
 
-  Definition PathsCategory : @SpecializedCategory V.
-    refine (@Build_SpecializedCategory _
+  Definition PathsCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory V
                                        (@path V E)
                                        (@NoEdges _ _)
                                        (fun _ _ _ p p' => concatenate p' p)
diff -r 4eb6407c6ca3 PathsCategoryFunctors.v
--- a/PathsCategoryFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/PathsCategoryFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,8 +13,8 @@
 Section FunctorFromPaths.
   Variable V : Type.
   Variable E : V -> V -> Type.
-  Context `(D : @SpecializedCategory objD).
-  Variable objOf : V -> objD.
+  Context `(D : SpecializedCategory).
+  Variable objOf : V -> D.
   Variable morOf : forall s d, E s d -> Morphism D (objOf s) (objOf d).
 
   Fixpoint path_compose s d (m : Morphism (PathsCategory E) s d) : Morphism D (objOf s) (objOf d) :=
@@ -31,15 +31,15 @@
 
   Definition FunctorFromPaths : SpecializedFunctor (PathsCategory E) D.
   Proof.
-    refine {|
-      ObjectOf := objOf;
-      MorphismOf := path_compose;
-      FCompositionOf := FunctorFromPaths_FCompositionOf
-    |};
+    refine (Build_SpecializedFunctor (PathsCategory E) D
+                                     objOf
+                                     path_compose
+                                     FunctorFromPaths_FCompositionOf
+                                     _);
     abstract intuition.
   Defined.
 End FunctorFromPaths.
 
 Section Underlying.
-  Definition UnderlyingGraph `(C : @SpecializedCategory objC) := @PathsCategory objC (Morphism C).
+  Definition UnderlyingGraph `(C : SpecializedCategory) := @PathsCategory _ (Morphism C).
 End Underlying.
diff -r 4eb6407c6ca3 ProductCategory.v
--- a/ProductCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/ProductCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,11 +10,11 @@
 Set Universe Polymorphism.
 
 Section ProductCategory.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
-  Definition ProductCategory : @SpecializedCategory (objC * objD)%type.
-    refine (@Build_SpecializedCategory _
+  Definition ProductCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory (C * D)%type
                                        (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
                                        (fun o => (Identity (fst o), Identity (snd o)))
                                        (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))
@@ -28,8 +28,8 @@
 Infix "*" := ProductCategory : category_scope.
 
 Section ProductCategoryFunctors.
-  Context `{C : @SpecializedCategory objC}.
-  Context `{D : @SpecializedCategory objD}.
+  Context `{C : SpecializedCategory}.
+  Context `{D : SpecializedCategory}.
 
   Definition fst_Functor : SpecializedFunctor (C * D) C
     := Build_SpecializedFunctor (C * D) C
diff -r 4eb6407c6ca3 ProductFunctors.v
--- a/ProductFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/ProductFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,7 +10,7 @@
 Set Universe Polymorphism.
 
 Section Products.
-  Context `{C : @SpecializedCategory objC}.
+  Context `{C : SpecializedCategory}.
   Variable I : Type.
 
   Variable HasLimits : forall F : SpecializedFunctor (DiscreteCategory I) C, Limit F.
diff -r 4eb6407c6ca3 ProductInducedFunctors.v
--- a/ProductInducedFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/ProductInducedFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -15,9 +15,9 @@
   reflexivity.
 
 Section ProductInducedFunctors.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
 
   Variable F : SpecializedFunctor (C * D) E.
 
@@ -40,9 +40,9 @@
 Notation "F ⟨ - , d ⟩" := (InducedProductFstFunctor F d) : functor_scope.
 
 Section ProductInducedNaturalTransformations.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
 
   Variable F : SpecializedFunctor (C * D) E.
 
diff -r 4eb6407c6ca3 ProductLaws.v
--- a/ProductLaws.v	Fri May 24 20:09:37 2013 -0400
+++ b/ProductLaws.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,7 +12,7 @@
 Local Open Scope category_scope.
 
 Section swap.
-  Definition SwapFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD)
+  Definition SwapFunctor `(C : SpecializedCategory) `(D : SpecializedCategory)
   : SpecializedFunctor (C * D) (D * C)
     := Build_SpecializedFunctor (C * D) (D * C)
                                 (fun cd => (snd cd, fst cd))
@@ -20,14 +20,14 @@
                                 (fun _ _ _ _ _ => eq_refl)
                                 (fun _ => eq_refl).
 
-  Lemma ProductLawSwap `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD)
+  Lemma ProductLawSwap `(C : SpecializedCategory) `(D : SpecializedCategory)
   : ComposeFunctors (SwapFunctor C D) (SwapFunctor D C) = IdentityFunctor _.
     functor_eq; intuition.
   Qed.
 End swap.
 
 Section Law0.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition ProductLaw0Functor : SpecializedFunctor (C * 0) 0.
     refine (Build_SpecializedFunctor (C * 0) 0
@@ -60,7 +60,7 @@
 End Law0.
 
 Section Law0'.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Let ProductLaw0'Functor' : SpecializedFunctor (0 * C) 0.
     functor_simpl_abstract_trailing_props (ComposeFunctors (ProductLaw0Functor C) (SwapFunctor _ _)).
@@ -82,7 +82,7 @@
 End Law0'.
 
 Section Law1.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Let ProductLaw1Functor' : SpecializedFunctor (C * 1) C.
     functor_simpl_abstract_trailing_props (fst_Functor (C := C) (D := 1)).
@@ -113,7 +113,7 @@
 End Law1.
 
 Section Law1'.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition ProductLaw1'Functor' : SpecializedFunctor (1 * C) C.
     functor_simpl_abstract_trailing_props (ComposeFunctors (ProductLaw1Functor C) (SwapFunctor _ _)).
diff -r 4eb6407c6ca3 ProductNaturalTransformation.v
--- a/ProductNaturalTransformation.v	Fri May 24 20:09:37 2013 -0400
+++ b/ProductNaturalTransformation.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,10 +10,10 @@
 Set Universe Polymorphism.
 
 Section ProductNaturalTransformation.
-  Context `{A : @SpecializedCategory objA}.
-  Context `{B : @SpecializedCategory objB}.
-  Context `{C : @SpecializedCategory objC}.
-  Context `{D : @SpecializedCategory objD}.
+  Context `{A : SpecializedCategory}.
+  Context `{B : SpecializedCategory}.
+  Context `{C : SpecializedCategory}.
+  Context `{D : SpecializedCategory}.
   Variables F F' : SpecializedFunctor A B.
   Variables G G' : SpecializedFunctor C D.
   Variable T : SpecializedNaturalTransformation F F'.
diff -r 4eb6407c6ca3 Products.v
--- a/Products.v	Fri May 24 20:09:37 2013 -0400
+++ b/Products.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,7 +10,7 @@
 Set Universe Polymorphism.
 
 Section Products.
-  Context `{C : @SpecializedCategory objC}.
+  Context `{C : SpecializedCategory}.
   Variable I : Type.
   Variable f : I -> C.
 
@@ -19,7 +19,7 @@
 End Products.
 
 (* XXX: [Reserved Notation] doesn't work here? *)
-Notation "∏_{ x } f" := (@Product _ _ _ (fun x => f)) (at level 0, x at level 99).
-Notation "∏_{ x : A } f" := (@Product _ _ A (fun x : A => f)) (at level 0, x at level 99).
-Notation "∐_{ x } f" := (@Coproduct _ _ _ (fun x => f)) (at level 0, x at level 99).
-Notation "∐_{ x : A } f" := (@Coproduct _ _ A (fun x : A => f)) (at level 0, x at level 99).
+Notation "∏_{ x } f" := (@Product _ _ (fun x => f)) (at level 0, x at level 99).
+Notation "∏_{ x : A } f" := (@Product _ A (fun x : A => f)) (at level 0, x at level 99).
+Notation "∐_{ x } f" := (@Coproduct _ _ (fun x => f)) (at level 0, x at level 99).
+Notation "∐_{ x : A } f" := (@Coproduct _ A (fun x : A => f)) (at level 0, x at level 99).
diff -r 4eb6407c6ca3 Pullback.v
--- a/Pullback.v	Fri May 24 20:09:37 2013 -0400
+++ b/Pullback.v	Sat Jun 22 12:51:34 2013 -0400
@@ -24,9 +24,9 @@
      ]]
    *)
 
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Section pullback.
-    Variables a b c : objC.
+    Variables a b c : C.
     Variable f : C.(Morphism) a c.
     Variable g : C.(Morphism) b c.
 
@@ -49,8 +49,8 @@
              destruct s, d, d'; simpl in *; trivial.
            Defined.
 
-    Definition PullbackIndex : @SpecializedCategory PullbackThree.
-      refine (@Build_SpecializedCategory _
+    Definition PullbackIndex : SpecializedCategory.
+      refine (@Build_SpecializedCategory PullbackThree
                                          PullbackIndex_Morphism
                                          (fun x => match x as p return (PullbackIndex_Morphism p p) with
                                                        PullbackA => tt | PullbackB => tt | PullbackC => tt
@@ -153,7 +153,7 @@
   End pullback_functorial.
 
   Section pushout.
-    Variables a b c : objC.
+    Variables a b c : C.
     Variable f : C.(Morphism) c a.
     Variable g : C.(Morphism) c b.
 
@@ -242,8 +242,8 @@
 End Pullback.
 
 Section PullbackObjects.
-  Context `{C : @SpecializedCategory objC}.
-  Variables a b c : objC.
+  Context `{C : SpecializedCategory}.
+  Variables a b c : C.
 
   (** Does an object [d] together with the functions [i] and [j]
     fit into a pullback diagram?
@@ -279,7 +279,7 @@
                             (FunctorCategory.FunctorCategory PullbackIndex C)
                             (PullbackDiagram C a b c f g)).
     exists (PullbackObject, tt).
-    exists (fun x => match x as x return (Morphism C PullbackObject (PullbackDiagram_ObjectOf a b c x)) with
+    exists (fun x => match x as x return (Morphism C PullbackObject (PullbackDiagram_ObjectOf C a b c x)) with
                        | PullbackA => i
                        | PullbackB => j
                        | PullbackC => Compose f i
@@ -295,7 +295,7 @@
              (i : Morphism C PullbackObject a)
              (j : Morphism C PullbackObject b)
              (PullbackCompatible : Compose f i = Compose g j)
-    := @IsPullback _ _ a b c f g (IsPullbackGivenMorphisms_Object f g PullbackObject i j PullbackCompatible).
+    := @IsPullback _ a b c f g (IsPullbackGivenMorphisms_Object f g PullbackObject i j PullbackCompatible).
 
   Definition IsPushoutGivenMorphisms_Object
              (f : Morphism C c a)
@@ -309,7 +309,7 @@
                             (PushoutDiagram C a b c f g))
                          (DiagonalFunctor C PushoutIndex).
     exists (tt, PushoutObject).
-    exists (fun x => match x as x return (Morphism C (PushoutDiagram_ObjectOf a b c x) PushoutObject) with
+    exists (fun x => match x as x return (Morphism C (PushoutDiagram_ObjectOf C a b c x) PushoutObject) with
                        | PullbackA => i
                        | PullbackB => j
                        | PullbackC => Compose i f
@@ -325,5 +325,5 @@
              (i : Morphism C a PushoutObject)
              (j : Morphism C b PushoutObject)
              (PushoutCompatible : Compose j g = Compose i f)
-    := @IsPushout _ _ a b c f g (IsPushoutGivenMorphisms_Object f g PushoutObject i j PushoutCompatible).
+    := @IsPushout _ a b c f g (IsPushoutGivenMorphisms_Object f g PushoutObject i j PushoutCompatible).
 End PullbackObjects.
diff -r 4eb6407c6ca3 PullbackFunctor.v
--- a/PullbackFunctor.v	Fri May 24 20:09:37 2013 -0400
+++ b/PullbackFunctor.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,7 +9,7 @@
 Set Universe Polymorphism.
 
 Section Equalizer.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Variable HasLimits : forall F : SpecializedFunctor PullbackIndex C, Limit F.
   Variable HasColimits : forall F : SpecializedFunctor PushoutIndex C, Colimit F.
diff -r 4eb6407c6ca3 SemiSimplicialSets.v
--- a/SemiSimplicialSets.v	Fri May 24 20:09:37 2013 -0400
+++ b/SemiSimplicialSets.v	Sat Jun 22 12:51:34 2013 -0400
@@ -21,8 +21,8 @@
      which we will use to make simplicial sets without having to worry
      about "degneracies". *)
 
-  Definition SemiSimplexCategory : SpecializedCategory nat.
-    eapply (WideSubcategory Δ (@IsMonomorphism _ _));
+  Definition SemiSimplexCategory : SpecializedCategory.
+    eapply (WideSubcategory Δ (@IsMonomorphism _));
     abstract eauto with morphism.
   Defined.
 
@@ -31,7 +31,7 @@
   Definition SemiSimplexCategoryInclusionFunctor : SpecializedFunctor Γ Δ
     := WideSubcategoryInclusionFunctor _ _ _ _.
 
-  Definition SemiSimplicialCategory `(C : SpecializedCategory objC) := (C ^ (OppositeCategory Γ))%category.
+  Definition SemiSimplicialCategory `(C : SpecializedCategory) := (C ^ (OppositeCategory Γ))%category.
 
   Definition SemiSimplicialSet := SemiSimplicialCategory SetCat.
   Definition SemiSimplicialType := SemiSimplicialCategory TypeCat.
diff -r 4eb6407c6ca3 SetCategory.v
--- a/SetCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SetCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -23,15 +23,15 @@
 
 (* There is a category [Set], where the objects are sets and the morphisms are set morphisms *)
 Section CSet.
-  Definition TypeCat : @SpecializedCategory Type := Eval cbv beta in CatOf Type.
-  Definition SetCat : @SpecializedCategory Set := Eval cbv beta in CatOf Set.
-  Definition PropCat : @SpecializedCategory Prop := Eval cbv beta in CatOf Prop.
+  Definition TypeCat : SpecializedCategory := Eval cbv beta in CatOf Type.
+  Definition SetCat : SpecializedCategory := Eval cbv beta in CatOf Set.
+  Definition PropCat : SpecializedCategory := Eval cbv beta in CatOf Prop.
 
   Definition IndexedTypeCat (Index : Type) (Index2Object : Index -> Type) := Eval cbv beta in IndexedCatOf Index Index2Object.
 End CSet.
 
 Section SetCoercionsDefinitions.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition SpecializedFunctorToProp := SpecializedFunctor C PropCat.
   Definition SpecializedFunctorToSet := SpecializedFunctor C SetCat.
@@ -50,7 +50,7 @@
 Identity Coercion SpecializedFunctorFromType_Id : SpecializedFunctorFromType >-> SpecializedFunctor.
 
 Section SetCoercions.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Local Notation BuildFunctor C D F :=
     (Build_SpecializedFunctor C D
@@ -94,10 +94,10 @@
                                                                          (fun _ _ _ _ _ => eq_refl)
                                                                          (fun _ => eq_refl)).
 
-  Definition PointedTypeCat : @SpecializedCategory { A : Type & A } := Eval cbv beta zeta in PointedCatOf Type.
+  Definition PointedTypeCat : SpecializedCategory := Eval cbv beta zeta in PointedCatOf Type.
   Definition PointedTypeProjection : SpecializedFunctor PointedTypeCat TypeCat := PointedCatProjectionOf Type.
-  Definition PointedSetCat : @SpecializedCategory { A : Set & A } := Eval cbv beta zeta in PointedCatOf Set.
+  Definition PointedSetCat : SpecializedCategory := Eval cbv beta zeta in PointedCatOf Set.
   Definition PointedSetProjection : SpecializedFunctor PointedSetCat SetCat := PointedCatProjectionOf Set.
-  Definition PointedPropCat : @SpecializedCategory { A : Prop & A } := Eval cbv beta zeta in PointedCatOf Prop.
+  Definition PointedPropCat : SpecializedCategory := Eval cbv beta zeta in PointedCatOf Prop.
   Definition PointedPropProjection : SpecializedFunctor PointedPropCat PropCat := PointedCatProjectionOf Prop.
 End PointedSet.
diff -r 4eb6407c6ca3 SetCategoryFacts.v
--- a/SetCategoryFacts.v	Fri May 24 20:09:37 2013 -0400
+++ b/SetCategoryFacts.v	Sat Jun 22 12:51:34 2013 -0400
@@ -148,7 +148,7 @@
     congruence.
 
   Local Notation PartialBuild_NaturalNumbersPreObject T Cat :=
-    (fun pf => @Build_NaturalNumbersPreObject T Cat
+    (fun pf => @Build_NaturalNumbersPreObject Cat
                                               nat
                                               (UnitTerminalOf T)
                                               (fun _ => 0)
diff -r 4eb6407c6ca3 SetCategoryProductFunctor.v
--- a/SetCategoryProductFunctor.v	Fri May 24 20:09:37 2013 -0400
+++ b/SetCategoryProductFunctor.v	Sat Jun 22 12:51:34 2013 -0400
@@ -16,15 +16,14 @@
 
   Local Ltac build_functor :=
     hnf;
-    match goal with
-      | [ |- @SpecializedFunctor ?objC ?C ?objD ?D ] =>
-        refine (@Build_SpecializedFunctor objC C objD D
-                                          (fun ab => (fst ab) * (snd ab))
-                                          (fun _ _ fg => (fun xy => ((fst fg) (fst xy), (snd fg) (snd xy))))
-                                          _
-                                          _);
-          abstract eauto
-    end.
+    let C := match goal with | [ |- SpecializedFunctor ?C ?D ] => constr:(C) end in
+    let D := match goal with | [ |- SpecializedFunctor ?C ?D ] => constr:(D) end in
+    refine (@Build_SpecializedFunctor C D
+                                      (fun ab => (fst ab) * (snd ab))
+                                      (fun _ _ fg => (fun xy => ((fst fg) (fst xy), (snd fg) (snd xy))))
+                                      _
+                                      _);
+      simpl; abstract (intros; eauto).
 
   Definition TypeProductFunctor : SpecializedFunctor (TypeCat * TypeCat) TypeCat. build_functor. Defined.
   Definition SetProductFunctor  : SpecializedFunctor (SetCat * SetCat) SetCat. build_functor. Defined.
diff -r 4eb6407c6ca3 SetColimits.v
--- a/SetColimits.v	Fri May 24 20:09:37 2013 -0400
+++ b/SetColimits.v	Sat Jun 22 12:51:34 2013 -0400
@@ -46,11 +46,11 @@
   (* An element of the colimit is an pair [c : C] and [x : F c] with
      (c, x) ~ (c', x') an equivalence relation generated by the
      existance of a morphism [m : c -> c'] with m c x = m c x'. *)
-  Context `(C : @SmallSpecializedCategory objC).
+  Context `(C : @SmallSpecializedCategory).
   Variable F : SpecializedFunctor C SetCat.
   Let F' : SpecializedFunctorToType _ := F : SpecializedFunctorToSet _.
 
-  Definition SetColimit_Object_pre := SetGrothendieckPair F. (* { c : objC & F.(ObjectOf) c }.*)
+  Definition SetColimit_Object_pre := SetGrothendieckPair F. (* { c : C & F.(ObjectOf) c }.*)
   Global Arguments SetColimit_Object_pre /.
   Definition SetColimit_Object_equiv_sig :=
     generateEquivalence (fun x y : SetColimit_Object_pre => inhabited (Morphism (CategoryOfElements F') x y)).
@@ -99,7 +99,7 @@
       match goal with
         | [ |- SpecializedNaturalTransformation ?F ?G ] =>
           refine (Build_SpecializedNaturalTransformation F G
-            (fun c : objC =>
+            (fun c : C =>
               (fun S : F c =>
                 chooser' (Build_SetGrothendieckPair F c S)
               )
@@ -172,10 +172,10 @@
   (* An element of the colimit is an pair [c : C] and [x : F c] with
      (c, x) ~ (c', x') an equivalence relation generated by the
      existance of a morphism [m : c -> c'] with m c x = m c x'. *)
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Variable F : SpecializedFunctor C TypeCat.
 
-  Definition TypeColimit_Object_pre := GrothendieckPair F. (* { c : objC & F.(ObjectOf) c }. *)
+  Definition TypeColimit_Object_pre := GrothendieckPair F. (* { c : C & F.(ObjectOf) c }. *)
   Global Arguments TypeColimit_Object_pre /.
   Definition TypeColimit_Object_equiv_sig :=
     generateEquivalence (fun x y : TypeColimit_Object_pre => inhabited (Morphism (CategoryOfElements F) x y)).
@@ -224,7 +224,7 @@
       match goal with
         | [ |- SpecializedNaturalTransformation ?F ?G ] =>
           refine (Build_SpecializedNaturalTransformation F G
-            (fun c : objC =>
+            (fun c : C =>
               (fun S : F c =>
                 chooser' (Build_GrothendieckPair F c S)
               )
diff -r 4eb6407c6ca3 SetLimits.v
--- a/SetLimits.v	Fri May 24 20:09:37 2013 -0400
+++ b/SetLimits.v	Sat Jun 22 12:51:34 2013 -0400
@@ -27,7 +27,7 @@
   trivial; t_with t'; intuition.
 
 Section SetLimits.
-  Context `(C : @SmallSpecializedCategory objC).
+  Context `(C : @SmallSpecializedCategory).
   Variable F : SpecializedFunctor C SetCat.
 
   (* Quoting David:
@@ -35,7 +35,7 @@
      one for each c in C, such that under every arrow g: c-->c' in C, x_c is sent to x_{c'}.
      *)
   Definition SetLimit_Object : SetCat :=
-    { S : forall c : objC, F c | forall c c' (g : C.(Morphism) c c'), F.(MorphismOf) g (S c) = (S c') }.
+    { S : forall c : C, F c | forall c c' (g : C.(Morphism) c c'), F.(MorphismOf) g (S c) = (S c') }.
 
   Definition SetLimit_Morphism : SpecializedNaturalTransformation
                                    ((DiagonalFunctor SetCat C) SetLimit_Object)
@@ -43,7 +43,7 @@
     match goal with
       | [ |- SpecializedNaturalTransformation ?F ?G ] =>
         refine (Build_SpecializedNaturalTransformation F G
-          (fun c : objC => (fun S => (proj1_sig S) c))
+          (fun c : C => (fun S => (proj1_sig S) c))
           _
         )
     end.
@@ -67,7 +67,7 @@
 End SetLimits.
 
 Section TypeLimits.
-  Context `(C : @SmallSpecializedCategory objC).
+  Context `(C : @SmallSpecializedCategory).
   Variable F : SpecializedFunctor C TypeCat.
 
   (* Quoting David:
@@ -75,7 +75,7 @@
      one for each c in C, such that under every arrow g: c-->c' in C, x_c is sent to x_{c'}.
      *)
   Definition TypeLimit_Object : TypeCat :=
-    { S : forall c : objC, F c | forall c c' (g : C.(Morphism) c c'), F.(MorphismOf) g (S c) = (S c') }.
+    { S : forall c : C, F c | forall c c' (g : C.(Morphism) c c'), F.(MorphismOf) g (S c) = (S c') }.
 
   Definition TypeLimit_Morphism : SpecializedNaturalTransformation
                                    ((DiagonalFunctor TypeCat C) TypeLimit_Object)
@@ -83,7 +83,7 @@
     match goal with
       | [ |- SpecializedNaturalTransformation ?F ?G ] =>
         refine (Build_SpecializedNaturalTransformation F G
-          (fun c : objC => (fun S => (proj1_sig S) c))
+          (fun c : C => (fun S => (proj1_sig S) c))
           _
         )
     end.
diff -r 4eb6407c6ca3 SigCategory.v
--- a/SigCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SigCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -23,24 +23,22 @@
           end).
 
 Section sig_obj_mor.
-  Context `(A : @SpecializedCategory objA).
-  Variable Pobj : objA -> Prop.
+  Context `(A : SpecializedCategory).
+  Variable Pobj : A -> Prop.
   Variable Pmor : forall s d : sig Pobj, A.(Morphism) (proj1_sig s) (proj1_sig d) -> Prop.
   Variable Pidentity : forall x, @Pmor x x (Identity (C := A) _).
   Variable Pcompose : forall s d d', forall m1 m2, @Pmor d d' m1 -> @Pmor s d m2 -> @Pmor s d' (Compose (C := A) m1 m2).
 
-  Definition SpecializedCategory_sig : @SpecializedCategory (sig Pobj).
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => sig (@Pmor s d))
-          (fun x => exist _ _ (Pidentity x))
-          (fun s d d' m1 m2 => exist _ _ (Pcompose (proj2_sig m1) (proj2_sig m2)))
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sig : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              (sig Pobj)
+              (fun s d => sig (@Pmor s d))
+              (fun x => exist _ _ (Pidentity x))
+              (fun s d d' m1 m2 => exist _ _ (Pcompose (proj2_sig m1) (proj2_sig m2)))
+              _
+              _
+              _
+           );
     abstract (intros; simpl_eq; auto with category).
   Defined.
 
@@ -56,24 +54,22 @@
   Qed.
 End sig_obj_mor.
 
-Arguments proj1_sig_functor {objA A Pobj Pmor Pidentity Pcompose}.
+Arguments proj1_sig_functor {A Pobj Pmor Pidentity Pcompose}.
 
 Section sig_obj.
-  Context `(A : @SpecializedCategory objA).
-  Variable Pobj : objA -> Prop.
+  Context `(A : SpecializedCategory).
+  Variable Pobj : A -> Prop.
 
-  Definition SpecializedCategory_sig_obj : @SpecializedCategory (sig Pobj).
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => A.(Morphism) (proj1_sig s) (proj1_sig d))
-          (fun x => Identity (C := A) (proj1_sig x))
-          (fun s d d' m1 m2 => Compose (C := A) m1 m2)
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sig_obj : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              (sig Pobj)
+              (fun s d => A.(Morphism) (proj1_sig s) (proj1_sig d))
+              (fun x => Identity (C := A) (proj1_sig x))
+              (fun s d d' m1 m2 => Compose (C := A) m1 m2)
+              _
+              _
+              _
+           );
     abstract (intros; destruct_sig; simpl; auto with category).
   Defined.
 
@@ -84,8 +80,8 @@
                                 (fun _ _ _ _ _ => eq_refl)
                                 (fun _ => eq_refl).
 
-  Definition SpecializedCategory_sig_obj_as_sig : @SpecializedCategory (sig Pobj)
-    := @SpecializedCategory_sig _ A Pobj (fun _ _ _ => True) (fun _ => I) (fun _ _ _ _ _ _ _ => I).
+  Definition SpecializedCategory_sig_obj_as_sig : SpecializedCategory
+    := @SpecializedCategory_sig A Pobj (fun _ _ _ => True) (fun _ => I) (fun _ _ _ _ _ _ _ => I).
 
   Definition sig_functor_obj : SpecializedFunctor SpecializedCategory_sig_obj_as_sig SpecializedCategory_sig_obj
     := Build_SpecializedFunctor SpecializedCategory_sig_obj_as_sig SpecializedCategory_sig_obj
@@ -114,27 +110,25 @@
   Qed.
 End sig_obj.
 
-Arguments proj1_sig_obj_functor {objA A Pobj}.
+Arguments proj1_sig_obj_functor {A Pobj}.
 
 Section sig_mor.
-  Context `(A : @SpecializedCategory objA).
+  Context `(A : SpecializedCategory).
   Variable Pmor : forall s d, A.(Morphism) s d -> Prop.
 
   Variable Pidentity : forall x, @Pmor x x (Identity (C := A) _).
   Variable Pcompose : forall s d d', forall m1 m2, @Pmor d d' m1 -> @Pmor s d m2 -> @Pmor s d' (Compose (C := A) m1 m2).
 
-  Definition SpecializedCategory_sig_mor : @SpecializedCategory objA.
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => sig (@Pmor s d))
-          (fun x => exist _ (Identity (C := A) x) (Pidentity x))
-          (fun s d d' m1 m2 => exist _ (Compose (proj1_sig m1) (proj1_sig m2)) (Pcompose (proj2_sig m1) (proj2_sig m2)))
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sig_mor : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              A
+              (fun s d => sig (@Pmor s d))
+              (fun x => exist _ (Identity (C := A) x) (Pidentity x))
+              (fun s d d' m1 m2 => exist _ (Compose (proj1_sig m1) (proj1_sig m2)) (Pcompose (proj2_sig m1) (proj2_sig m2)))
+              _
+              _
+              _
+           );
     abstract (intros; simpl_eq; auto with category).
   Defined.
 
@@ -145,8 +139,8 @@
                                 (fun _ _ _ _ _ => eq_refl)
                                 (fun _ => eq_refl).
 
-  Definition SpecializedCategory_sig_mor_as_sig : @SpecializedCategory (sig (fun _ : objA => True))
-    := @SpecializedCategory_sig _ A _ (fun s d => @Pmor (proj1_sig s) (proj1_sig d)) (fun _ => Pidentity _) (fun _ _ _ _ _ m1 m2 => Pcompose m1 m2).
+  Definition SpecializedCategory_sig_mor_as_sig : SpecializedCategory
+    := @SpecializedCategory_sig A (fun _ => True) (fun s d => @Pmor (proj1_sig s) (proj1_sig d)) (fun _ => Pidentity _) (fun _ _ _ _ _ m1 m2 => Pcompose m1 m2).
 
   Definition sig_functor_mor : SpecializedFunctor SpecializedCategory_sig_mor_as_sig SpecializedCategory_sig_mor
     := Build_SpecializedFunctor SpecializedCategory_sig_mor_as_sig SpecializedCategory_sig_mor
@@ -175,4 +169,4 @@
   Qed.
 End sig_mor.
 
-Arguments proj1_sig_mor_functor {objA A Pmor Pidentity Pcompose}.
+Arguments proj1_sig_mor_functor {A Pmor Pidentity Pcompose}.
diff -r 4eb6407c6ca3 SigSigTCategory.v
--- a/SigSigTCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SigSigTCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,8 +13,8 @@
 Local Infix "==" := JMeq.
 
 Section sig_sigT_obj_mor.
-  Context `(A : @SpecializedCategory objA).
-  Variable Pobj : objA -> Prop.
+  Context `(A : SpecializedCategory).
+  Variable Pobj : A -> Prop.
   Variable Pmor : forall s d : sig Pobj, A.(Morphism) (proj1_sig s) (proj1_sig d) -> Type.
 
   Variable Pidentity : forall x, @Pmor x x (Identity (C := A) _).
@@ -32,18 +32,16 @@
     @Pcompose a a b f _ f' (@Pidentity a) ==
     f'.
 
-  Definition SpecializedCategory_sig_sigT : @SpecializedCategory (sig Pobj).
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => sigT (@Pmor s d))
-          (fun x => existT _ (Identity (C := A) (proj1_sig x)) (Pidentity x))
-          (fun s d d' m1 m2 => existT _ (Compose (C := A) (projT1 m1) (projT1 m2)) (Pcompose (projT2 m1) (projT2 m2)))
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sig_sigT : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              (sig Pobj)
+              (fun s d => sigT (@Pmor s d))
+              (fun x => existT _ (Identity (C := A) (proj1_sig x)) (Pidentity x))
+              (fun s d d' m1 m2 => existT _ (Compose (C := A) (projT1 m1) (projT1 m2)) (Pcompose (projT2 m1) (projT2 m2)))
+              _
+              _
+              _
+           );
     abstract (intros; simpl_eq; auto with category).
   Defined.
 
@@ -67,13 +65,13 @@
     f'
     := P_RightIdentity f'.
 
-  Let SpecializedCategory_sig_sigT_as_sigT : @SpecializedCategory (sigT Pobj).
-    eapply (@SpecializedCategory_sigT _ A
-      Pobj
-      Pmor'
-      Pidentity'
-      Pcompose'
-    );
+  Let SpecializedCategory_sig_sigT_as_sigT : SpecializedCategory.
+    eapply (@SpecializedCategory_sigT A
+                                      Pobj
+                                      Pmor'
+                                      Pidentity'
+                                      Pcompose'
+           );
     trivial.
   Defined.
 
diff -r 4eb6407c6ca3 SigTCategory.v
--- a/SigTCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SigTCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -27,8 +27,8 @@
           end).
 
 Section sigT_obj_mor.
-  Context `(A : @SpecializedCategory objA).
-  Variable Pobj : objA -> Type.
+  Context `(A : SpecializedCategory).
+  Variable Pobj : A -> Type.
   Variable Pmor : forall s d : sigT Pobj, A.(Morphism) (projT1 s) (projT1 d) -> Type.
 
   Variable Pidentity : forall x, @Pmor x x (Identity (C := A) _).
@@ -46,18 +46,16 @@
     @Pcompose a a b f _ f' (@Pidentity a) ==
     f'.
 
-  Definition SpecializedCategory_sigT : @SpecializedCategory (sigT Pobj).
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => sigT (@Pmor s d))
-          (fun x => existT _ (Identity (C := A) (projT1 x)) (Pidentity x))
-          (fun s d d' m1 m2 => existT _ (Compose (C := A) (projT1 m1) (projT1 m2)) (Pcompose (projT2 m1) (projT2 m2)))
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sigT : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              (sigT Pobj)
+              (fun s d => sigT (@Pmor s d))
+              (fun x => existT _ (Identity (C := A) (projT1 x)) (Pidentity x))
+              (fun s d d' m1 m2 => existT _ (Compose (C := A) (projT1 m1) (projT1 m2)) (Pcompose (projT2 m1) (projT2 m2)))
+              _
+              _
+              _
+           );
     abstract (intros; simpl_eq; auto with category).
   Defined.
 
@@ -69,24 +67,22 @@
                                 (fun _ => eq_refl).
 End sigT_obj_mor.
 
-Arguments projT1_functor {objA A Pobj Pmor Pidentity Pcompose P_Associativity P_LeftIdentity P_RightIdentity}.
+Arguments projT1_functor {A Pobj Pmor Pidentity Pcompose P_Associativity P_LeftIdentity P_RightIdentity}.
 
 Section sigT_obj.
-  Context `(A : @SpecializedCategory objA).
-  Variable Pobj : objA -> Type.
+  Context `(A : SpecializedCategory).
+  Variable Pobj : A -> Type.
 
-  Definition SpecializedCategory_sigT_obj : @SpecializedCategory (sigT Pobj).
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => A.(Morphism) (projT1 s) (projT1 d))
-          (fun x => Identity (C := A) (projT1 x))
-          (fun s d d' m1 m2 => Compose (C := A) m1 m2)
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sigT_obj : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              (sigT Pobj)
+              (fun s d => A.(Morphism) (projT1 s) (projT1 d))
+              (fun x => Identity (C := A) (projT1 x))
+              (fun s d d' m1 m2 => Compose (C := A) m1 m2)
+              _
+              _
+              _
+           );
     abstract (intros; destruct_sig; simpl; auto with category).
   Defined.
 
@@ -97,8 +93,8 @@
                                 (fun _ _ _ _ _ => eq_refl)
                                 (fun _ => eq_refl).
 
-  Definition SpecializedCategory_sigT_obj_as_sigT : @SpecializedCategory (sigT Pobj).
-    refine (@SpecializedCategory_sigT _ A Pobj (fun _ _ _ => unit) (fun _ => tt) (fun _ _ _ _ _ _ _ => tt) _ _ _);
+  Definition SpecializedCategory_sigT_obj_as_sigT : SpecializedCategory.
+    refine (@SpecializedCategory_sigT A Pobj (fun _ _ _ => unit) (fun _ => tt) (fun _ _ _ _ _ _ _ => tt) _ _ _);
     abstract (simpl; intros; trivial).
   Defined.
 
@@ -125,10 +121,10 @@
   Qed.
 End sigT_obj.
 
-Arguments projT1_obj_functor {objA A Pobj}.
+Arguments projT1_obj_functor {A Pobj}.
 
 Section sigT_mor.
-  Context `(A : @SpecializedCategory objA).
+  Context `(A : SpecializedCategory).
   Variable Pmor : forall s d, A.(Morphism) s d -> Type.
 
   Variable Pidentity : forall x, @Pmor x x (Identity (C := A) _).
@@ -146,18 +142,16 @@
     @Pcompose a a b f _ f' (@Pidentity a) ==
     f'.
 
-  Definition SpecializedCategory_sigT_mor : @SpecializedCategory objA.
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => sigT (@Pmor s d))
-          (fun x => existT _ (Identity (C := A) x) (Pidentity x))
-          (fun s d d' m1 m2 => existT _ (Compose (C := A) (projT1 m1) (projT1 m2)) (Pcompose (projT2 m1) (projT2 m2)))
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sigT_mor : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              _
+              (fun s d => sigT (@Pmor s d))
+              (fun x => existT _ (Identity (C := A) x) (Pidentity x))
+              (fun s d d' m1 m2 => existT _ (Compose (C := A) (projT1 m1) (projT1 m2)) (Pcompose (projT2 m1) (projT2 m2)))
+              _
+              _
+              _
+           );
     abstract (intros; simpl_eq; auto with category).
   Defined.
 
@@ -171,8 +165,8 @@
     intros; reflexivity.
   Defined.
 
-  Definition SpecializedCategory_sigT_mor_as_sigT : @SpecializedCategory (sigT (fun _ : objA => unit)).
-    apply (@SpecializedCategory_sigT _ A _ (fun s d => @Pmor (projT1 s) (projT1 d)) (fun _ => Pidentity _) (fun _ _ _ _ _ m1 m2 => Pcompose m1 m2));
+  Definition SpecializedCategory_sigT_mor_as_sigT : SpecializedCategory.
+    apply (@SpecializedCategory_sigT A (fun _ => unit) (fun s d => @Pmor (projT1 s) (projT1 d)) (fun _ => Pidentity _) (fun _ _ _ _ _ m1 m2 => Pcompose m1 m2));
       abstract (intros; trivial).
   Defined.
 
@@ -211,4 +205,4 @@
   Qed.
 End sigT_mor.
 
-Arguments projT1_mor_functor {objA A Pmor Pidentity Pcompose P_Associativity P_LeftIdentity P_RightIdentity}.
+Arguments projT1_mor_functor {A Pmor Pidentity Pcompose P_Associativity P_LeftIdentity P_RightIdentity}.
diff -r 4eb6407c6ca3 SigTInducedFunctors.v
--- a/SigTInducedFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/SigTInducedFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,11 +12,11 @@
 Section T2.
   (* use dummy variables so we don't have to specify the types of
      all these hypotheses *)
-  Context `(dummy0 : @SpecializedCategory_sigT objA A Pobj0 Pmor0 Pidentity0 Pcompose0 P_Associativity0 P_LeftIdentity0 P_RightIdentity0).
-  Context `(dummy1 : @SpecializedCategory_sigT objA A Pobj1 Pmor1 Pidentity1 Pcompose1 P_Associativity1 P_LeftIdentity1 P_RightIdentity1).
+  Context `(dummy0 : @SpecializedCategory_sigT A Pobj0 Pmor0 Pidentity0 Pcompose0 P_Associativity0 P_LeftIdentity0 P_RightIdentity0).
+  Context `(dummy1 : @SpecializedCategory_sigT A Pobj1 Pmor1 Pidentity1 Pcompose1 P_Associativity1 P_LeftIdentity1 P_RightIdentity1).
 
-  Let sigT_cat0 := @SpecializedCategory_sigT objA A Pobj0 Pmor0 Pidentity0 Pcompose0 P_Associativity0 P_LeftIdentity0 P_RightIdentity0.
-  Let sigT_cat1 := @SpecializedCategory_sigT objA A Pobj1 Pmor1 Pidentity1 Pcompose1 P_Associativity1 P_LeftIdentity1 P_RightIdentity1.
+  Let sigT_cat0 := @SpecializedCategory_sigT A Pobj0 Pmor0 Pidentity0 Pcompose0 P_Associativity0 P_LeftIdentity0 P_RightIdentity0.
+  Let sigT_cat1 := @SpecializedCategory_sigT A Pobj1 Pmor1 Pidentity1 Pcompose1 P_Associativity1 P_LeftIdentity1 P_RightIdentity1.
 
   Variable P_ObjectOf : forall x, Pobj0 x -> Pobj1 x.
 
diff -r 4eb6407c6ca3 SigTSigCategory.v
--- a/SigTSigCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SigTSigCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,30 +13,28 @@
 Local Infix "==" := JMeq.
 
 Section sigT_sig_obj_mor.
-  Context `(A : @SpecializedCategory objA).
-  Variable Pobj : objA -> Type.
+  Context `(A : SpecializedCategory).
+  Variable Pobj : A -> Type.
   Variable Pmor : forall s d : sigT Pobj, A.(Morphism) (projT1 s) (projT1 d) -> Prop.
 
   Variable Pidentity : forall x, @Pmor x x (Identity (C := A) _).
   Variable Pcompose : forall s d d', forall m1 m2, @Pmor d d' m1 -> @Pmor s d m2 -> @Pmor s d' (Compose (C := A) m1 m2).
 
-  Definition SpecializedCategory_sigT_sig : @SpecializedCategory (sigT Pobj).
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          (fun s d => sig (@Pmor s d))
-          (fun x => existT _ (Identity (C := A) (projT1 x)) (Pidentity x))
-          (fun s d d' m1 m2 => existT _ (Compose (C := A) (proj1_sig m1) (proj1_sig m2)) (Pcompose (proj2_sig m1) (proj2_sig m2)))
-          _
-          _
-          _
-        )
-    end;
+  Definition SpecializedCategory_sigT_sig : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              (sigT Pobj)
+              (fun s d => sig (@Pmor s d))
+              (fun x => existT _ (Identity (C := A) (projT1 x)) (Pidentity x))
+              (fun s d d' m1 m2 => existT _ (Compose (C := A) (proj1_sig m1) (proj1_sig m2)) (Pcompose (proj2_sig m1) (proj2_sig m2)))
+              _
+              _
+              _
+           );
     abstract (intros; simpl_eq; auto with category).
   Defined.
 
-  Let SpecializedCategory_sigT_sig_as_sigT : @SpecializedCategory (sigT Pobj).
-    apply (@SpecializedCategory_sigT _ A _ _ Pidentity Pcompose);
+  Let SpecializedCategory_sigT_sig_as_sigT : SpecializedCategory.
+    apply (@SpecializedCategory_sigT A Pobj _ Pidentity Pcompose);
       abstract (
         simpl; intros;
           match goal with
diff -r 4eb6407c6ca3 SigTSigInducedFunctors.v
--- a/SigTSigInducedFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/SigTSigInducedFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -13,11 +13,11 @@
 Section T2.
   (* use dummy variables so we don't have to specify the types of
      all these hypotheses *)
-  Context `(dummy0 : @SpecializedCategory_sigT_sig objA A Pobj0 Pmor0 Pidentity0 Pcompose0).
-  Context `(dummy1 : @SpecializedCategory_sigT_sig objA A Pobj1 Pmor1 Pidentity1 Pcompose1).
+  Context `(dummy0 : @SpecializedCategory_sigT_sig A Pobj0 Pmor0 Pidentity0 Pcompose0).
+  Context `(dummy1 : @SpecializedCategory_sigT_sig A Pobj1 Pmor1 Pidentity1 Pcompose1).
 
-  Let sigT_sig_cat0 := @SpecializedCategory_sigT_sig objA A Pobj0 Pmor0 Pidentity0 Pcompose0.
-  Let sigT_sig_cat1 := @SpecializedCategory_sigT_sig objA A Pobj1 Pmor1 Pidentity1 Pcompose1.
+  Let sigT_sig_cat0 := @SpecializedCategory_sigT_sig A Pobj0 Pmor0 Pidentity0 Pcompose0.
+  Let sigT_sig_cat1 := @SpecializedCategory_sigT_sig A Pobj1 Pmor1 Pidentity1 Pcompose1.
 
   Variable P_ObjectOf : forall x, Pobj0 x -> Pobj1 x.
 
@@ -40,7 +40,7 @@
   Definition InducedT2Functor_sigT_sig : SpecializedFunctor sigT_sig_cat0 sigT_sig_cat1.
     eapply (ComposeFunctors (sigT_functor_sigT_sig _ _ _ _) (ComposeFunctors _ (sigT_sig_functor_sigT _ _ _ _))).
     Grab Existential Variables.
-    eapply (@InducedT2Functor_sigT _ A Pobj0 Pmor0 Pidentity0 Pcompose0 _ _ _ Pobj1 Pmor1 Pidentity1 Pcompose1 _ _ _
+    eapply (@InducedT2Functor_sigT A Pobj0 Pmor0 Pidentity0 Pcompose0 _ _ _ Pobj1 Pmor1 Pidentity1 Pcompose1 _ _ _
       P_ObjectOf (fun s d m => @P_MorphismOf s d (sig_of_sigT' m)));
     subst_body;
     abstract (simpl; intros; apply proof_irrelevance).
diff -r 4eb6407c6ca3 SimplicialSets.v
--- a/SimplicialSets.v	Fri May 24 20:09:37 2013 -0400
+++ b/SimplicialSets.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,10 +10,10 @@
 Set Universe Polymorphism.
 
 Section SimplicialSets.
-  Definition SimplexCategory := @ComputableCategory nat _ (fun n => [n])%category.
+  Definition SimplexCategory := ComputableCategory (fun n : nat => [n])%category.
   Local Notation Δ := SimplexCategory.
 
-  Definition SimplicialCategory `(C : SpecializedCategory objC) := (C ^ (OppositeCategory Δ))%category.
+  Definition SimplicialCategory `(C : SpecializedCategory) := (C ^ (OppositeCategory Δ))%category.
 
   Definition SimplicialSet := SimplicialCategory SetCat.
   Definition SimplicialType := SimplicialCategory TypeCat.
diff -r 4eb6407c6ca3 SmallCat.v
--- a/SmallCat.v	Fri May 24 20:09:37 2013 -0400
+++ b/SmallCat.v	Sat Jun 22 12:51:34 2013 -0400
@@ -9,8 +9,8 @@
 Set Universe Polymorphism.
 
 Section SmallCat.
-  Definition SmallCat := ComputableCategory _ SUnderlyingCategory.
-  Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory.
+  Definition SmallCat := ComputableCategory SUnderlyingCategory.
+  Definition LocallySmallCat := ComputableCategory LSUnderlyingCategory.
 End SmallCat.
 
 Local Ltac destruct_simple_types :=
@@ -26,8 +26,8 @@
 Section Objects.
   Hint Unfold Morphism Object.
 
-  Local Arguments Object / {obj} C : rename.
-  Local Arguments Morphism / {obj} _ _ _ : rename.
+  Local Arguments Object / C : rename.
+  Local Arguments Morphism / _ _ _ : rename.
 
   Hint Extern 1 => destruct_simple_types.
   Hint Extern 3 => destruct_to_empty_set.
diff -r 4eb6407c6ca3 SpecializedCategory.v
--- a/SpecializedCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SpecializedCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -12,10 +12,10 @@
 
 Local Infix "==" := JMeq.
 
-Record SpecializedCategory (obj : Type) :=
+Record SpecializedCategory :=
   Build_SpecializedCategory' {
-      Object :> _ := obj;
-      Morphism : obj -> obj -> Type;
+      Object :> Type;
+      Morphism : Object -> Object -> Type;
 
       Identity : forall x, Morphism x x;
       Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d';
@@ -39,10 +39,10 @@
 Bind Scope object_scope with Object.
 Bind Scope morphism_scope with Morphism.
 
-Arguments Object {obj%type} C%category / : rename.
-Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
-Arguments Identity {obj%type} [!C%category] x%object : rename.
-Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+Arguments Object C%category : rename.
+Arguments Morphism !C%category s d : rename. (* , simpl nomatch. *)
+Arguments Identity [!C%category] x%object : rename.
+Arguments Compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
 
 Section SpecializedCategoryInterface.
   Definition Build_SpecializedCategory (obj : Type)
@@ -53,7 +53,7 @@
                                  Compose' o1 o2 o4 (Compose' o2 o3 o4 m3 m2) m1 = Compose' o1 o3 o4 m3 (Compose' o1 o2 o3 m2 m1))
              (LeftIdentity' : forall (a b : obj) (f : Morphism a b), Compose' a b b (Identity' b) f = f)
              (RightIdentity' : forall (a b : obj) (f : Morphism a b), Compose' a a b f (Identity' a) = f)
-  : @SpecializedCategory obj
+  : SpecializedCategory
     := @Build_SpecializedCategory' obj
                                    Morphism
                                    Identity'
@@ -87,103 +87,130 @@
 Hint Rewrite @LeftIdentity @RightIdentity : morphism.
 
 (* eh, I'm not terribly happy.  meh. *)
-Definition LocallySmallSpecializedCategory (obj : Type) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
-Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
+Definition LocallySmallSpecializedCategory (*obj : Type*) (*mor : obj -> obj -> Set*) := SpecializedCategory.
+Definition SmallSpecializedCategory (*obj : Set*) (*mor : obj -> obj -> Set*) := SpecializedCategory.
 Identity Coercion LocallySmallSpecializedCategory_SpecializedCategory_Id : LocallySmallSpecializedCategory >-> SpecializedCategory.
 Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.
 
 Section Categories_Equal.
-  Lemma SpecializedCategory_contr_eq' `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC)
-        (C_morphism_proof_irrelevance
-         : forall s d (m1 m2 : Morphism C s d) (pf1 pf2 : m1 = m2),
-             pf1 = pf2)
-  : forall (HM : @Morphism _ C = @Morphism _ D),
-      match HM in (_ = y) return (forall x : objC, y x x) with
-        | eq_refl => Identity (C := C)
-      end = Identity (C := D)
-      -> match
-        HM in (_ = y) return (forall s d d' : objC, y d d' -> y s d -> y s d')
-      with
-        | eq_refl => Compose (C := C)
-      end = Compose (C := D)
-      -> C = D.
-    intros.
-    destruct C, D;
-      subst_body;
-      intros;
-      simpl in *.
-    subst.
-    repeat f_equal;
-      repeat (apply functional_extensionality_dep; intro);
-      trivial.
-  Qed.
+  Section contr_eq.
+    Variables C D : SpecializedCategory.
+    Section contr_eq'.
+      Hypothesis C_morphism_proof_irrelevance
+      : forall s d (m1 m2 : Morphism C s d) (pf1 pf2 : m1 = m2),
+          pf1 = pf2.
+      Hypothesis HO : Object C = Object D.
+      Hypothesis HM : match HO in (_ = y) return (y -> y -> Type) with
+                        | eq_refl => Morphism C
+                      end = Morphism D.
 
-  Lemma SpecializedCategory_contr_eq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC)
-        (C_morphism_proof_irrelevance
-         : forall s d (m1 m2 : Morphism C s d) (pf1 pf2 : m1 = m2),
-             pf1 = pf2)
-        (C_morphism_type_contr
-         : forall s d (pf1 pf2 : Morphism C s d = Morphism C s d),
-             pf1 = pf2)
-  : forall (HM : forall s d, @Morphism _ C s d = @Morphism _ D s d),
-      (forall x,
-         match HM x x in (_ = y) return y with
-           | eq_refl => Identity (C := C) x
-         end = Identity (C := D) x)
-      -> (forall s d d' (m : Morphism D d d') (m' : Morphism D s d),
-            match HM s d' in (_ = y) return y with
-              | eq_refl =>
-                match HM s d in (_ = y) return (y -> Morphism C s d') with
-                  | eq_refl =>
-                    match
-                      HM d d' in (_ = y) return (y -> Morphism C s d -> Morphism C s d')
-                    with
-                      | eq_refl => Compose (d':=d')
-                    end m
-                end m'
-            end = Compose m m')
-      -> C = D.
-    intros HM HI HC.
-    assert (HM' : @Morphism _ C = @Morphism _ D)
-      by (repeat (apply functional_extensionality_dep; intro); trivial).
-    apply (SpecializedCategory_contr_eq' _ _ C_morphism_proof_irrelevance HM');
-      revert HI HC C_morphism_proof_irrelevance C_morphism_type_contr;
-      destruct C, D; simpl in *; clear;
-      intros;
-      subst_body;
-      simpl in *;
-      repeat (subst || intro || apply functional_extensionality_dep);
-      rewrite_rev_hyp;
-      generalize_eq_match;
-      subst_eq_refl_dec;
-      trivial.
-  Qed.
+      Let HIdT : Prop.
+        refine (_ = Identity (C := D)).
+        case HM; clear HM.
+        case HO; clear HO.
+        exact (Identity (C := C)).
+      Defined.
+      Hypothesis HId : HIdT.
 
-  Lemma SpecializedCategory_eq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC) :
-    @Morphism _ C = @Morphism _ D
-    -> @Identity _ C == @Identity _ D
-    -> @Compose _ C == @Compose _ D
+      Let HCoT : Prop.
+        refine (_ = Compose (C := D)).
+        clear HId HIdT.
+        case HM; clear HM.
+        case HO; clear HO.
+        exact (Compose (C := C)).
+      Defined.
+      Hypothesis HCo : HCoT.
+
+      Lemma SpecializedCategory_contr_eq' : C = D.
+      Proof.
+        hnf in *.
+        destruct C, D.
+        subst_body.
+        simpl in *.
+        repeat subst.
+        f_equal;
+          repeat (apply functional_extensionality_dep; intro);
+          trivial.
+      Qed.
+    End contr_eq'.
+
+    Section contr_eq.
+      Hypothesis C_morphism_proof_irrelevance
+      : forall s d (m1 m2 : Morphism C s d) (pf1 pf2 : m1 = m2),
+          pf1 = pf2.
+
+      (* presumably this can be proven from the above by univalence,
+         and turning equalities into equivalences *)
+      Hypothesis C_morphism_type_contr
+      : forall s d (pf1 pf2 : Morphism C s d = Morphism C s d),
+          pf1 = pf2.
+
+      Hypothesis HO : Object C = Object D.
+      Hypothesis HM : forall s d,
+                        match HO in (_ = y) return (y -> y -> Type) with
+                          | eq_refl => Morphism C
+                        end s d = Morphism D s d.
+
+      Let HIdT : forall x : D, Prop.
+        intro x.
+        refine (_ = Identity x).
+        case (HM x x); clear HM.
+        revert x; case HO; clear HO; intro x.
+        exact (Identity x).
+      Defined.
+      Hypothesis HId : forall x, HIdT x.
+
+      Let HCoT s d d' (m1 : Morphism D d d') (m2 : Morphism D s d) : Prop.
+        refine (_ = Compose m1 m2).
+        clear HId HIdT.
+        revert m1 m2.
+        case (HM s d'), (HM d d'), (HM s d); clear HM.
+        revert s d d'.
+        case HO; clear HO.
+        exact (Compose (C := C)).
+      Defined.
+      Hypothesis HCo : forall s d d' m1 m2, @HCoT s d d' m1 m2.
+
+      Lemma SpecializedCategory_contr_eq : C = D.
+      Proof.
+        let f := match type of HM with forall s d, ?f s d = ?f' s d => constr:(f) end in
+        let f' := match type of HM with forall s d, ?f s d = ?f' s d => constr:(f') end in
+        assert (HM' : f = f')
+          by (repeat (apply functional_extensionality_dep; intro); trivial).
+        apply (SpecializedCategory_contr_eq' C_morphism_proof_irrelevance HO HM');
+          repeat (apply functional_extensionality_dep; intro);
+          destruct C, D;
+          subst_body;
+          simpl in *;
+          repeat (subst || intro || apply functional_extensionality_dep);
+          etransitivity;
+          try match goal with
+                | [ H : _ |- _ ] => solve [ apply H ]
+              end;
+          [|];
+          instantiate;
+          generalize_eq_match;
+          subst_eq_refl_dec;
+          trivial.
+      Qed.
+    End contr_eq.
+  End contr_eq.
+
+  Lemma SpecializedCategory_eq `(C : SpecializedCategory) `(D : SpecializedCategory) :
+    @Object C = @Object D
+    -> @Morphism C == @Morphism D
+    -> @Identity C == @Identity D
+    -> @Compose C == @Compose D
     -> C = D.
     intros.
     destruct_head @SpecializedCategory;
     simpl in *; repeat subst;
     f_equal; apply proof_irrelevance.
   Qed.
-
-  Lemma SpecializedCategory_JMeq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :
-    objC = objD
-    -> @Morphism _ C == @Morphism _ D
-    -> @Identity _ C == @Identity _ D
-    -> @Compose _ C == @Compose _ D
-    -> C == D.
-    intros; destruct_head @SpecializedCategory;
-    simpl in *; repeat subst; JMeq_eq;
-    f_equal; apply proof_irrelevance.
-  Qed.
 End Categories_Equal.
 
 Ltac spcat_eq_step_with tac :=
-  structures_eq_step_with_tac ltac:(apply SpecializedCategory_eq || apply SpecializedCategory_JMeq) tac.
+  structures_eq_step_with_tac ltac:(apply SpecializedCategory_eq) tac.
 
 Ltac spcat_eq_with tac := repeat spcat_eq_step_with tac.
 
@@ -192,11 +219,11 @@
 
 Ltac solve_for_identity :=
   match goal with
-    | [ |- @Compose _ ?C ?s ?s ?d ?a ?b = ?b ]
-      => cut (a = @Identity _ C s);
+    | [ |- @Compose ?C ?s ?s ?d ?a ?b = ?b ]
+      => cut (a = @Identity C s);
         [ try solve [ let H := fresh in intro H; rewrite H; apply LeftIdentity ] | ]
-    | [ |- @Compose _ ?C ?s ?d ?d ?a ?b = ?a ]
-      => cut (b = @Identity _ C d );
+    | [ |- @Compose ?C ?s ?d ?d ?a ?b = ?a ]
+      => cut (b = @Identity C d );
         [ try solve [ let H := fresh in intro H; rewrite H; apply RightIdentity ] | ]
   end.
 
@@ -204,7 +231,7 @@
 
 Definition NoEvar T (_ : T) := True.
 
-Lemma AssociativityNoEvar `(C : @SpecializedCategory obj) : forall (o1 o2 o3 o4 : C) (m1 : C.(Morphism) o1 o2)
+Lemma AssociativityNoEvar `(C : SpecializedCategory) : forall (o1 o2 o3 o4 : C) (m1 : C.(Morphism) o1 o2)
   (m2 : C.(Morphism) o2 o3) (m3 : C.(Morphism) o3 o4),
   NoEvar (m1, m2) \/ NoEvar (m2, m3) \/ NoEvar (m1, m3)
   -> Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1).
@@ -224,10 +251,10 @@
 
 Ltac find_composition_to_identity :=
   match goal with
-    | [ H : @Compose _ _ _ _ _ ?a ?b = @Identity _ _ _ |- context[@Compose ?A ?B ?C ?D ?E ?c ?d] ]
+    | [ H : @Compose _ _ _ _ ?a ?b = @Identity _ _ |- context[@Compose ?B ?C ?D ?E ?c ?d] ]
       => let H' := fresh in
         assert (H' : b = d /\ a = c) by (split; reflexivity); clear H';
-          assert (H' : @Compose A B C D E c d = @Identity _ _ _) by (
+          assert (H' : @Compose B C D E c d = @Identity _ _) by (
             exact H ||
               (unfold Object; simpl in H |- *; exact H || (rewrite H; reflexivity))
           );
@@ -241,7 +268,7 @@
 (** * Back to the main content.... *)
 
 Section Category.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   (* Quoting Wikipedia,
     In category theory, an epimorphism (also called an epic
@@ -293,11 +320,11 @@
 
 Hint Immediate @IdentityIsEpimorphism @IdentityIsMonomorphism @MonomorphismComposition @EpimorphismComposition : category morphism.
 
-Arguments IsEpimorphism {objC} [C x y] m.
-Arguments IsMonomorphism {objC} [C x y] m.
+Arguments IsEpimorphism [C x y] m.
+Arguments IsMonomorphism [C x y] m.
 
 Section AssociativityComposition.
-  Context `(C : @SpecializedCategory obj).
+  Context `(C : SpecializedCategory).
   Variables o0 o1 o2 o3 o4 : C.
 
   Lemma compose4associativity_helper
diff -r 4eb6407c6ca3 SpecializedCommaCategory.v
--- a/SpecializedCommaCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SpecializedCommaCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -16,9 +16,9 @@
 
 Section CommaSpecializedCategory.
   (* [Definition]s are not sort-polymorphic. *)
-  Context `(A : @SpecializedCategory objA).
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
+  Context `(A : SpecializedCategory).
+  Context `(B : SpecializedCategory).
+  Context `(C : SpecializedCategory).
   Variable S : SpecializedFunctor A C.
   Variable T : SpecializedFunctor B C.
 
@@ -54,7 +54,7 @@
      up significantly.  We unfold the definitions at the very end with
      [Eval]. *)
   (* stupid lack of sort-polymorphism in definitions... *)
-  Record CommaSpecializedCategory_Object := { CommaSpecializedCategory_Object_Member :> { αβ : objA * objB & C.(Morphism) (S (fst αβ)) (T (snd αβ)) } }.
+  Record CommaSpecializedCategory_Object := { CommaSpecializedCategory_Object_Member :> { αβ : A * B & C.(Morphism) (S (fst αβ)) (T (snd αβ)) } }.
 
   Let SortPolymorphic_Helper (A T : Type) (Build_T : A -> T) := A.
 
@@ -152,16 +152,14 @@
     abstract comma_t.
   Qed.
 
-  Definition CommaSpecializedCategory : @SpecializedCategory CommaSpecializedCategory_Object.
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          CommaSpecializedCategory_Morphism
-          CommaSpecializedCategory_Identity
-          CommaSpecializedCategory_Compose
-          _ _ _
-        )
-    end;
+  Definition CommaSpecializedCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              CommaSpecializedCategory_Object
+              CommaSpecializedCategory_Morphism
+              CommaSpecializedCategory_Identity
+              CommaSpecializedCategory_Compose
+              _ _ _
+           );
     abstract (
       intros;
         destruct_type' @CommaSpecializedCategory_Morphism;
@@ -178,8 +176,8 @@
 Hint Constructors CommaSpecializedCategory_Morphism CommaSpecializedCategory_Object : category.
 
 Section SliceSpecializedCategory.
-  Context `(A : @SpecializedCategory objA).
-  Context `(C : @SpecializedCategory objC).
+  Context `(A : SpecializedCategory).
+  Context `(C : SpecializedCategory).
   Variable a : C.
   Variable S : SpecializedFunctor A C.
 
@@ -190,7 +188,7 @@
 End SliceSpecializedCategory.
 
 Section SliceSpecializedCategoryOver.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Variable a : C.
 
   Definition SliceSpecializedCategoryOver := SliceSpecializedCategory a (IdentityFunctor C).
@@ -198,16 +196,16 @@
 End SliceSpecializedCategoryOver.
 
 Section ArrowSpecializedCategory.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition ArrowSpecializedCategory := CommaSpecializedCategory (IdentityFunctor C) (IdentityFunctor C).
 End ArrowSpecializedCategory.
 
-Notation "C / a" := (@SliceSpecializedCategoryOver _ C a) : category_scope.
-Notation "a \ C" := (@CosliceSpecializedCategoryOver _ C a) (at level 70) : category_scope.
+Notation "C / a" := (@SliceSpecializedCategoryOver C a) : category_scope.
+Notation "a \ C" := (@CosliceSpecializedCategoryOver C a) (at level 70) : category_scope.
 
-Definition CC_SpecializedFunctor' `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) := SpecializedFunctor C D.
-Coercion CC_FunctorFromTerminal' `(C : @SpecializedCategory objC) (x : C) : CC_SpecializedFunctor' TerminalCategory C := FunctorFromTerminal C x.
+Definition CC_SpecializedFunctor' `(C : SpecializedCategory) `(D : SpecializedCategory) := SpecializedFunctor C D.
+Coercion CC_FunctorFromTerminal' `(C : SpecializedCategory) (x : C) : CC_SpecializedFunctor' TerminalCategory C := FunctorFromTerminal C x.
 Arguments CC_SpecializedFunctor' / .
 Arguments CC_FunctorFromTerminal' / .
 
@@ -219,5 +217,5 @@
 Notation "S ↓ T" := (CommaSpecializedCategory (S : CC_SpecializedFunctor' _ _)
                                               (T : CC_SpecializedFunctor' _ _)) : category_scope.
 (*Set Printing All.
-Check (fun `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) `(E : @SpecializedCategory objE) (S : SpecializedFunctor C D) (T : SpecializedFunctor E D) => (S ↓ T)%category).
-Check (fun `(D : @SpecializedCategory objD) `(E : @SpecializedCategory objE) (S : SpecializedFunctor E D) (x : D) => (x ↓ S)%category).*)
+Check (fun `(C : SpecializedCategory) `(D : SpecializedCategory) `(E : SpecializedCategory) (S : SpecializedFunctor C D) (T : SpecializedFunctor E D) => (S ↓ T)%category).
+Check (fun `(D : SpecializedCategory) `(E : SpecializedCategory) (S : SpecializedFunctor E D) (x : D) => (x ↓ S)%category).*)
diff -r 4eb6407c6ca3 SpecializedLaxCommaCategory.v
--- a/SpecializedLaxCommaCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SpecializedLaxCommaCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -16,14 +16,13 @@
   (* [Definition]s are not sort-polymorphic. *)
 
   Variable I : Type.
-  Variable Index2Object : I -> Type.
-  Variable Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i).
+  Variable Index2Cat : I -> SpecializedCategory.
 
   Local Coercion Index2Cat : I >-> SpecializedCategory.
 
-  Let Cat := ComputableCategory Index2Object Index2Cat.
+  Let Cat := ComputableCategory Index2Cat.
 
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   (** Quoting David Spivak:
      David: ok
@@ -183,18 +182,16 @@
     abstract lax_slice_t.
   Qed.
 
-  Definition LaxSliceSpecializedCategory : @SpecializedCategory LaxSliceSpecializedCategory_Object.
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          LaxSliceSpecializedCategory_Morphism
-          LaxSliceSpecializedCategory_Identity
-          LaxSliceSpecializedCategory_Compose
-          _
-          _
-          _
-        )
-    end;
+  Definition LaxSliceSpecializedCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              LaxSliceSpecializedCategory_Object
+              LaxSliceSpecializedCategory_Morphism
+              LaxSliceSpecializedCategory_Identity
+              LaxSliceSpecializedCategory_Compose
+              _
+              _
+              _
+           );
     abstract (
       repeat (
         let H := fresh in intro H; destruct H as [ ]; simpl in * |-
@@ -216,13 +213,13 @@
   (* [Definition]s are not sort-polymorphic. *)
 
   Variable I : Type.
-  Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
+  Variable Index2Cat : I -> SpecializedCategory.
 
   Local Coercion Index2Cat : I >-> SpecializedCategory.
 
-  Let Cat := ComputableCategory Index2Object Index2Cat.
+  Let Cat := ComputableCategory Index2Cat.
 
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Record LaxCosliceSpecializedCategory_Object := { LaxCosliceSpecializedCategory_Object_Member :> { X : unit * I & SpecializedFunctor (snd X) C } }.
 
@@ -358,18 +355,16 @@
     abstract lax_coslice_t.
   Qed.
 
-  Definition LaxCosliceSpecializedCategory : @SpecializedCategory LaxCosliceSpecializedCategory_Object.
-    match goal with
-      | [ |- @SpecializedCategory ?obj ] =>
-        refine (@Build_SpecializedCategory obj
-          LaxCosliceSpecializedCategory_Morphism
-          LaxCosliceSpecializedCategory_Identity
-          LaxCosliceSpecializedCategory_Compose
-          _
-          _
-          _
-        )
-    end;
+  Definition LaxCosliceSpecializedCategory : SpecializedCategory.
+    refine (@Build_SpecializedCategory
+              LaxCosliceSpecializedCategory_Object
+              LaxCosliceSpecializedCategory_Morphism
+              LaxCosliceSpecializedCategory_Identity
+              LaxCosliceSpecializedCategory_Compose
+              _
+              _
+              _
+           );
     abstract (
       repeat (
         let H := fresh in intro H; destruct H as [ ]; simpl in * |-
diff -r 4eb6407c6ca3 SubobjectClassifier.v
--- a/SubobjectClassifier.v	Fri May 24 20:09:37 2013 -0400
+++ b/SubobjectClassifier.v	Sat Jun 22 12:51:34 2013 -0400
@@ -62,7 +62,7 @@
    See for instance (MacLane-Moerdijk, p. 22).
    *)
 
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Local Reserved Notation "'Ω'".
 
diff -r 4eb6407c6ca3 SumCategory.v
--- a/SumCategory.v	Fri May 24 20:09:37 2013 -0400
+++ b/SumCategory.v	Sat Jun 22 12:51:34 2013 -0400
@@ -10,10 +10,10 @@
 Set Universe Polymorphism.
 
 Section SumCategory.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
-  Definition SumCategory_Morphism (s d : objC + objD) : Type
+  Definition SumCategory_Morphism (s d : C + D) : Type
     := match (s, d) with
          | (inl s, inl d) => C.(Morphism) s d
          | (inr s, inr d) => D.(Morphism) s d
@@ -38,7 +38,7 @@
 
   Global Arguments SumCategory_Compose [_ _ _] _ _ /.
 
-  Definition SumCategory : @SpecializedCategory (objC + objD)%type.
+  Definition SumCategory : SpecializedCategory.
     refine (@Build_SpecializedCategory _
                                        SumCategory_Morphism
                                        SumCategory_Identity
@@ -59,8 +59,8 @@
 Infix "+" := SumCategory : category_scope.
 
 Section SumCategoryFunctors.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
 
   Definition inl_Functor : SpecializedFunctor C (C + D)
     := Build_SpecializedFunctor C (C + D)
diff -r 4eb6407c6ca3 SumInducedFunctors.v
--- a/SumInducedFunctors.v	Fri May 24 20:09:37 2013 -0400
+++ b/SumInducedFunctors.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,9 +11,9 @@
 
 Section SumCategoryFunctors.
   Section sum_functor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(C' : @SpecializedCategory objC').
-    Context `(D : @SpecializedCategory objD).
+    Context `(C : SpecializedCategory).
+    Context `(C' : SpecializedCategory).
+    Context `(D : SpecializedCategory).
 
     Definition sum_Functor (F : SpecializedFunctor C D) (F' : SpecializedFunctor C' D)
     : SpecializedFunctor (C + C') D.
@@ -65,14 +65,14 @@
 
   Section swap_functor.
     Definition sum_swap_Functor
-               `(C : @SpecializedCategory objC)
-               `(D : @SpecializedCategory objD)
+               `(C : SpecializedCategory)
+               `(D : SpecializedCategory)
     : SpecializedFunctor (C + D) (D + C)
       := sum_Functor (inr_Functor _ _) (inl_Functor _ _).
 
     Lemma sum_swap_swap_id
-          `(C : @SpecializedCategory objC)
-          `(D : @SpecializedCategory objD)
+          `(C : SpecializedCategory)
+          `(D : SpecializedCategory)
     : ComposeFunctors (sum_swap_Functor C D) (sum_swap_Functor D C) = IdentityFunctor _.
       apply Functor_eq; repeat intros [?|?]; simpl; trivial.
     Qed.
diff -r 4eb6407c6ca3 TypeclassSimplification.v
--- a/TypeclassSimplification.v	Fri May 24 20:09:37 2013 -0400
+++ b/TypeclassSimplification.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,7 +11,7 @@
 
 Section SimplifiedMorphism.
   Section single_category.
-    Context `{C : SpecializedCategory objC}.
+    Context `{C : SpecializedCategory}.
 
     Class SimplifiedMorphism {s d} (m : Morphism C s d) :=
       SimplifyMorphism { reified_morphism : ReifiedMorphism C s d;
@@ -43,11 +43,11 @@
   End single_category.
 
   Section functor.
-    Context `{C : SpecializedCategory objC}.
-    Context `{D : SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
     Variable F : SpecializedFunctor C D.
 
-    Global Instance functor_morphism `(@SimplifiedMorphism objC C s d m)
+    Global Instance functor_morphism `(@SimplifiedMorphism C s d m)
     : SimplifiedMorphism (MorphismOf F m) | 50
       := SimplifyMorphism (m := MorphismOf F m)
                           (ReifiedFunctorMorphism F (reified_morphism (m := m)))
@@ -55,8 +55,8 @@
   End functor.
 
   Section natural_transformation.
-    Context `{C : SpecializedCategory objC}.
-    Context `{D : SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
     Variables F G : SpecializedFunctor C D.
     Variable T : SpecializedNaturalTransformation F G.
 
diff -r 4eb6407c6ca3 TypeclassUnreifiedSimplification.v
--- a/TypeclassUnreifiedSimplification.v	Fri May 24 20:09:37 2013 -0400
+++ b/TypeclassUnreifiedSimplification.v	Sat Jun 22 12:51:34 2013 -0400
@@ -11,7 +11,7 @@
 
 Section SimplifiedMorphism.
   Section single_category_definition.
-    Context `{C : SpecializedCategory objC}.
+    Context `{C : SpecializedCategory}.
 
     Class > MorphismSimplifiesTo {s d} (m_orig m_simpl : Morphism C s d) :=
       simplified_morphism_ok :> m_orig = m_simpl.
@@ -29,38 +29,38 @@
     trivial.
 
   Section single_category_instances.
-    Context `{C : SpecializedCategory objC}.
+    Context `{C : SpecializedCategory}.
 
     Global Instance LeftIdentitySimplify
-           `(@MorphismSimplifiesTo _ C s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ C _ _ m2_orig (Identity _))
+           `(@MorphismSimplifiesTo C s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo C _ _ m2_orig (Identity _))
     : MorphismSimplifiesTo (Compose m2_orig m1_orig) m1_simpl | 10.
     t.
     Qed.
 
     Global Instance RightIdentitySimplify
-           `(@MorphismSimplifiesTo _ C s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ C _ _ m2_orig (Identity _))
+           `(@MorphismSimplifiesTo C s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo C _ _ m2_orig (Identity _))
     : MorphismSimplifiesTo (Compose m1_orig m2_orig) m1_simpl | 10.
     t.
     Qed.
 
     Global Instance ComposeToIdentitySimplify
-           `(@MorphismSimplifiesTo _ C s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ C d s m2_orig m2_simpl)
+           `(@MorphismSimplifiesTo C s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo C d s m2_orig m2_simpl)
            `(Compose m2_simpl m1_simpl = Identity _)
     : MorphismSimplifiesTo (Compose m2_orig m1_orig) (Identity _) | 20.
     t.
     Qed.
 
-    Global Instance AssociativitySimplify `(@MorphismSimplifiesTo _ C _ _ (@Compose _ C _ c d m3 (@Compose _ C a b c m2 m1)) m_simpl)
+    Global Instance AssociativitySimplify `(@MorphismSimplifiesTo C _ _ (@Compose C _ c d m3 (@Compose C a b c m2 m1)) m_simpl)
     : MorphismSimplifiesTo (Compose (Compose m3 m2) m1) m_simpl | 1000.
     t.
     Qed.
 
     Global Instance ComposeSimplify
-           `(@MorphismSimplifiesTo _ C s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ C d d' m2_orig m2_simpl)
+           `(@MorphismSimplifiesTo C s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo C d d' m2_orig m2_simpl)
     : MorphismSimplifiesTo (Compose m2_orig m1_orig) (Compose m2_simpl m1_simpl) | 5000.
     t.
     Qed.
@@ -71,40 +71,40 @@
   End single_category_instances.
 
   Section sum_prod_category_instances.
-    Context `{C : SpecializedCategory objC}.
-    Context `{D : SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
 
     Global Instance SumCategorySimplify_inl
-           `(@MorphismSimplifiesTo _ C s d m_orig m_simpl)
-    : @MorphismSimplifiesTo _ (C + D) (inl s) (inl d) m_orig m_simpl | 100.
+           `(@MorphismSimplifiesTo C s d m_orig m_simpl)
+    : @MorphismSimplifiesTo (C + D) (inl s) (inl d) m_orig m_simpl | 100.
     t.
     Qed.
 
     Global Instance SumCategorySimplify_inr
-           `(@MorphismSimplifiesTo _ D s d m_orig m_simpl)
-    : @MorphismSimplifiesTo _ (C + D) (inr s) (inr d) m_orig m_simpl | 100.
+           `(@MorphismSimplifiesTo D s d m_orig m_simpl)
+    : @MorphismSimplifiesTo (C + D) (inr s) (inr d) m_orig m_simpl | 100.
     t.
     Qed.
 
     Global Instance SumComposeSimplify_inl
-           `(@MorphismSimplifiesTo _ C s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ C d d' m2_orig m2_simpl)
-    : MorphismSimplifiesTo (@Compose _ (C + D) (inl s) (inl d) (inl d') m2_orig m1_orig)
-                           (@Compose _ (C + D) (inl s) (inl d) (inl d') m2_simpl m1_simpl) | 50.
+           `(@MorphismSimplifiesTo C s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo C d d' m2_orig m2_simpl)
+    : MorphismSimplifiesTo (@Compose (C + D) (inl s) (inl d) (inl d') m2_orig m1_orig)
+                           (@Compose (C + D) (inl s) (inl d) (inl d') m2_simpl m1_simpl) | 50.
     t.
     Qed.
 
     Global Instance SumComposeSimplify_inr
-           `(@MorphismSimplifiesTo _ D s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ D d d' m2_orig m2_simpl)
-    : MorphismSimplifiesTo (@Compose _ (C + D) (inr s) (inr d) (inr d') m2_orig m1_orig)
-                           (@Compose _ (C + D) (inr s) (inr d) (inr d') m2_simpl m1_simpl) | 50.
+           `(@MorphismSimplifiesTo D s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo D d d' m2_orig m2_simpl)
+    : MorphismSimplifiesTo (@Compose (C + D) (inr s) (inr d) (inr d') m2_orig m1_orig)
+                           (@Compose (C + D) (inr s) (inr d) (inr d') m2_simpl m1_simpl) | 50.
     t.
     Qed.
 
     (*Global Instance ProductCategorySimplify
-           `(@MorphismSimplifiesTo _ C s d m_orig m_simpl)
-           `(@MorphismSimplifiesTo _ D s' d' m'_orig m'_simpl)
+           `(@MorphismSimplifiesTo C s d m_orig m_simpl)
+           `(@MorphismSimplifiesTo D s' d' m'_orig m'_simpl)
     : @MorphismSimplifiesTo _
                             (C * D)
                             (s, s')
@@ -118,20 +118,20 @@
 
 
   Section functor_instances.
-    Context `{C : SpecializedCategory objC}.
-    Context `{D : SpecializedCategory objD}.
+    Context `{C : SpecializedCategory}.
+    Context `{D : SpecializedCategory}.
     Variable F : SpecializedFunctor C D.
 
-    Global Instance FIdentityOfSimplify `(@MorphismSimplifiesTo _ C x x m_orig (Identity _))
+    Global Instance FIdentityOfSimplify `(@MorphismSimplifiesTo C x x m_orig (Identity _))
     : MorphismSimplifiesTo (MorphismOf F m_orig) (Identity _) | 30.
     t.
     Qed.
 
     Global Instance FCompositionOfSimplify
-           `(@MorphismSimplifiesTo _ C s d m1_orig m1_simpl)
-           `(@MorphismSimplifiesTo _ C d d' m2_orig m2_simpl)
-           `(@MorphismSimplifiesTo _ _ _ _ (Compose m2_simpl m1_simpl) m_comp)
-           `(@MorphismSimplifiesTo _ _ _ _ (MorphismOf F m_comp) m_Fcomp)
+           `(@MorphismSimplifiesTo C s d m1_orig m1_simpl)
+           `(@MorphismSimplifiesTo C d d' m2_orig m2_simpl)
+           `(@MorphismSimplifiesTo _ _ _ (Compose m2_simpl m1_simpl) m_comp)
+           `(@MorphismSimplifiesTo _ _ _ (MorphismOf F m_comp) m_Fcomp)
     : MorphismSimplifiesTo (Compose (MorphismOf F m2_orig) (MorphismOf F m1_orig))
                            m_Fcomp | 30.
     t.
@@ -139,15 +139,15 @@
 
     (** TODO(jgross): Remove this kludge *)
     Global Instance FunctorComposeToIdentitySimplify
-           `(@MorphismSimplifiesTo _ D (F s) (F d) m1_orig (MorphismOf F m1_simpl))
-           `(@MorphismSimplifiesTo _ D (F d) (F s) m2_orig (MorphismOf F m2_simpl))
+           `(@MorphismSimplifiesTo D (F s) (F d) m1_orig (MorphismOf F m1_simpl))
+           `(@MorphismSimplifiesTo D (F d) (F s) m2_orig (MorphismOf F m2_simpl))
            `(Compose m2_simpl m1_simpl = Identity _)
     : MorphismSimplifiesTo (Compose m2_orig m1_orig) (Identity _) | 20.
     t.
     Qed.
 
     Global Instance FunctorNoSimplify
-           `(@MorphismSimplifiesTo _ C s d m_orig m_simpl)
+           `(@MorphismSimplifiesTo C s d m_orig m_simpl)
     : MorphismSimplifiesTo (MorphismOf F m_orig) (MorphismOf F m_simpl) | 5000.
     t.
     Qed.
@@ -190,9 +190,9 @@
 (**                Goals which aren't yet solved by [rsimplify_morphisms]     **)
 (*******************************************************************************)
 Section bad1.
-  Context `(C : SpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
-  Context `(E : SpecializedCategory objE).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
+  Context `(E : SpecializedCategory).
   Variable s : SpecializedFunctor D E.
   Variable s8 : SpecializedFunctor C D.
   Variable s6 : SpecializedFunctor D E.
@@ -203,7 +203,7 @@
   Variable s3 : SpecializedNaturalTransformation s8 s7.
   Variable s0 : SpecializedNaturalTransformation s6 s4.
   Variable s1 : SpecializedNaturalTransformation s7 s5.
-  Variable x : objC.
+  Variable x : C.
 
   Goal
     (Compose (MorphismOf s4 (Compose (s1 x) (s3 x)))
@@ -221,13 +221,13 @@
 
 
 Section bad2.
-  Context `(C : SpecializedCategory objC).
-  Context `(D : SpecializedCategory objD).
+  Context `(C : SpecializedCategory).
+  Context `(D : SpecializedCategory).
   Variable F : SpecializedFunctor C D.
-  Variable o1 : objC.
-  Variable o2 : objC.
-  Variable o : objC.
-  Variable o0 : objC.
+  Variable o1 : C.
+  Variable o2 : C.
+  Variable o : C.
+  Variable o0 : C.
   Variable m : Morphism C o o1.
   Variable m0 : Morphism C o2 o0.
   Variable x : Morphism C o1 o2.
diff -r 4eb6407c6ca3 Yoneda.v
--- a/Yoneda.v	Fri May 24 20:09:37 2013 -0400
+++ b/Yoneda.v	Sat Jun 22 12:51:34 2013 -0400
@@ -22,7 +22,7 @@
     end.
 
 Section Yoneda.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Let COp := OppositeCategory C.
 
   Section Yoneda.
@@ -77,8 +77,8 @@
 End Yoneda.
 
 Section YonedaLemma.
-  Context `(C : @SpecializedCategory objC).
-  Let COp := OppositeCategory C : SpecializedCategory _.
+  Context `(C : SpecializedCategory).
+  Let COp := OppositeCategory C.
 
   (* Note: If we use [Yoneda _ c] instead, we get Universe Inconsistencies.  Hmm... *)
   Definition YonedaLemmaMorphism (c : C) (X : TypeCat ^ C) : Morphism TypeCat (Morphism (TypeCat ^ C) (Yoneda C c) X) (X c).
@@ -117,7 +117,7 @@
 End YonedaLemma.
 
 Section CoYonedaLemma.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
   Let COp := OppositeCategory C.
 
   Definition CoYonedaLemmaMorphism (c : C) (X : TypeCat ^ COp)
@@ -158,12 +158,12 @@
 End CoYonedaLemma.
 
 Section FullyFaithful.
-  Context `(C : @SpecializedCategory objC).
+  Context `(C : SpecializedCategory).
 
   Definition YonedaEmbedding : FunctorFullyFaithful (Yoneda C).
     unfold FunctorFullyFaithful.
     intros c c'.
-    destruct (@YonedaLemma _ C c (CovariantHomFunctor C c')) as [ m i ].
+    destruct (YonedaLemma (C := C) c (CovariantHomFunctor C c')) as [ m i ].
     exists (YonedaLemmaMorphism (X := CovariantHomFunctor C c')).
     t_with t'; nt_eq; autorewrite with morphism; trivial.
     apply_commutes_by_transitivity_and_solve_with ltac:(rewrite_hyp; autorewrite with morphism; trivial).
@@ -172,7 +172,7 @@
   Definition CoYonedaEmbedding : FunctorFullyFaithful (CoYoneda C).
     unfold FunctorFullyFaithful.
     intros c c'.
-    destruct (@CoYonedaLemma _ C c (ContravariantHomFunctor C c')) as [ m i ].
+    destruct (CoYonedaLemma (C := C) c (ContravariantHomFunctor C c')) as [ m i ].
     exists (CoYonedaLemmaMorphism (X := ContravariantHomFunctor C c')).
     t_with t'; nt_eq; autorewrite with morphism; trivial.
     unfold CoYonedaLemmaMorphism, CoYonedaLemmaMorphismInverse;