refactor(category_theory/category): split off has_hom

This gives a little more flexibility when defining a category,
which will be used for opposite categories. It should also be
useful for defining the free category on a graph.

Author: rwbarton

src/category_theory/category.lean

@@ -33,14 +33,17 @@ powerful tactics.
 def_replacer obviously
 @[obviously] meta def obviously' := tactic.tidy
 
+class has_hom (obj : Type u) : Type (max u (v+1)) :=
+(hom : obj → obj → Type v)
+
+infixr ` ⟶ `:10 := has_hom.hom -- type as \h
+
 /--
 The typeclass `category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
 -/
-class category (obj : Type u) : Type (max u (v+1)) :=
-(hom      : obj → obj → Type v)
-(infixr ` ⟶ `:10 := hom)
+class category (obj : Type u) extends has_hom.{v} obj : Type (max u (v+1)) :=
 (id       : Π X : obj, X ⟶ X)
 (notation `𝟙` := id)
 (comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
@@ -52,7 +55,6 @@ class category (obj : Type u) : Type (max u (v+1)) :=
 
 notation `𝟙` := category.id -- type as \b1
 infixr ` ≫ `:80 := category.comp -- type as \gg
-infixr ` ⟶ `:10 := category.hom -- type as \h
 
 -- `restate_axiom` is a command that creates a lemma from a structure field,
 -- discarding any auto_param wrappers from the type.

src/category_theory/opposites.lean

@@ -103,12 +103,12 @@ variable (C)
 
 /-- `functor.hom` is the hom-pairing, sending (X,Y) to X → Y, contravariant in X and covariant in Y. -/
 definition hom : Cᵒᵖ × C ⥤ Type v₁ :=
-{ obj       := λ p, @category.hom C _ p.1 p.2,
+{ obj       := λ p, @has_hom.hom C _ p.1 p.2,
   map       := λ X Y f, λ h, f.1 ≫ h ≫ f.2,
   map_id'   := by intros; ext; dsimp [category_theory.opposite]; simp,
   map_comp' := by intros; ext; dsimp [category_theory.opposite]; simp }
 
-@[simp] lemma hom_obj (X : Cᵒᵖ × C) : (functor.hom C).obj X = @category.hom C _ X.1 X.2 := rfl
+@[simp] lemma hom_obj (X : Cᵒᵖ × C) : (functor.hom C).obj X = @has_hom.hom C _ X.1 X.2 := rfl
 @[simp] lemma hom_pairing_map {X Y : Cᵒᵖ × C} (f : X ⟶ Y) :
   (functor.hom C).map f = λ h, f.1 ≫ h ≫ f.2 := rfl