restating functor.map and nat_trans.app, and removing rfl lemmas for …

…coercions

category_theory/functor.lean

@@ -29,16 +29,16 @@ The axiom `map_id_lemma` expresses preservation of identities, and
 -/
 structure functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : Type (max u₁ v₁ u₂ v₂) :=
 (obj      : C → D)
-(map      : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
-(map_id   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
-(map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)
-
-restate_axiom functor.map_id
-restate_axiom functor.map_comp
-attribute [simp,ematch] functor.map_id_lemma functor.map_comp_lemma
+(map'     : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
+(map_id   : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X) . obviously)
+(map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = (map' f) ≫ (map' g) . obviously)
 
 infixr ` ↝ `:70 := functor       -- type as \lea --
 
+-- restate_axiom functor.map_id
+-- restate_axiom functor.map_comp
+-- attribute [simp,ematch] functor.map_comp_lemma
+
 namespace functor
 
 section
@@ -49,7 +49,14 @@ instance : has_coe_to_fun (C ↝ D) :=
 { F   := λ F, C → D,
   coe := λ F, F.obj }
 
-@[simp] lemma coe_def (F : C ↝ D) (X : C) : F X = F.obj X := rfl
+def map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F X) ⟶ (F Y) := F.map' f
+
+@[simp,ematch] lemma map_id_lemma (F : C ↝ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) := begin unfold functor.map, erw F.map_id, refl end
+@[simp,ematch] lemma map_comp_lemma (F : C ↝ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : F.map (f ≫ g) = F.map f ≫ F.map g := begin unfold functor.map, erw F.map_comp end
+
+@[simp] lemma obj_explicit (o : C → D) (m : _) (mi : _) (mc : _) (X : C) : ({ functor . obj := o, map' := m, map_id := mi, map_comp := mc } : C ↝ D) X = o X := rfl
+@[simp] lemma map_explicit (o : C → D) (m : _) (mi : _) (mc : _) {X Y : C} (f : X ⟶ Y) : functor.map { functor . obj := o, map' := m, map_id := mi, map_comp := mc } f = m f := rfl
+-- @[simp] lemma coe_def (F : C ↝ D) (X : C) : F X = F.obj X := rfl
 end
 
 section
@@ -59,7 +66,7 @@ include 𝒞
 /-- `functor.id C` is the identity functor on a category `C`. -/
 protected def id : C ↝ C :=
 { obj      := λ X, X,
-  map      := λ _ _ f, f,
+  map'      := λ _ _ f, f,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
@@ -77,8 +84,8 @@ include 𝒞 𝒟 ℰ
 `F ⋙ G` is the composition of a functor `F` and a functor `G` (`F` first, then `G`).
 -/
 def comp (F : C ↝ D) (G : D ↝ E) : C ↝ E :=
-{ obj      := λ X, G.obj (F.obj X),
-  map      := λ _ _ f, G.map (F.map f),
+{ obj      := λ X, G (F X),
+  map'      := λ _ _ f, G.map (F.map f),
   map_id   := begin /- `obviously'` says: -/ intros, simp end,
   map_comp := begin /- `obviously'` says: -/ intros, simp end }
 

category_theory/natural_transformation.lean

@@ -33,8 +33,8 @@ structure nat_trans (F G : C ↝ D) : Type (max u₁ v₂) :=
 (app : Π X : C, (F X) ⟶ (G X))
 (naturality : ∀ {X Y : C} (f : X ⟶ Y), (F.map f) ≫ (app Y) = (app X) ≫ (G.map f) . obviously)
 
-restate_axiom nat_trans.naturality
-attribute [ematch] nat_trans.naturality_lemma
+-- restate_axiom nat_trans.naturality
+-- attribute [ematch] nat_trans.naturality_lemma
 
 infixr ` ⟹ `:50  := nat_trans             -- type as \==> or ⟹
 
@@ -44,12 +44,19 @@ instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
 { F   := λ α, Π X : C, (F X) ⟶ (G X),
   coe := λ α, α.app }
 
-@[simp] lemma coe_def {F G : C ↝ D} (α : F ⟹ G) (X : C) : α X = α.app X := rfl
+-- @[simp] lemma coe_def {F G : C ↝ D} (α : F ⟹ G) (X : C) : α X = α.app X := rfl
+
+@[simp] lemma coe_explicit_def {F G : C ↝ D} (app : Π X : C, (F X) ⟶ (G X)) (naturality : _) (X : C) : { nat_trans . app := app, naturality := naturality } X = app X := rfl 
+
+@[ematch] lemma naturality_lemma {F G : C ↝ D} (α : F ⟹ G) {X Y : C} (f : X ⟶ Y) : (F.map f) ≫ (α Y) = (α X) ≫ (G.map f) := 
+begin 
+erw nat_trans.naturality, refl
+end
 
 /-- `nat_trans.id F` is the identity natural transformation on a functor `F`. -/
 protected def id (F : C ↝ D) : F ⟹ F :=
 { app        := λ X, 𝟙 (F X),
-  naturality := begin /- `obviously'` says: -/ intros, dsimp, simp end }
+  naturality := begin /- `obviously'` says: -/ intros, simp end }
 
 @[simp] lemma id_app (F : C ↝ D) (X : C) : (nat_trans.id F) X = 𝟙 (F X) := rfl
 

category_theory/opposites.lean

@@ -33,9 +33,9 @@ include 𝒟
 
 protected definition op (F : C ↝ D) : (Cᵒᵖ) ↝ (Dᵒᵖ) := 
 { obj      := λ X, F X,
-  map      := λ X Y f, F.map f,
-  map_id   := begin /- `obviously'` says: -/ intros, erw [map_id], refl, end,
-  map_comp := begin /- `obviously'` says: -/ intros, erw [map_comp], refl end }
+  map'     := λ X Y f, F.map f,
+  map_id   := begin /- `obviously'` says: -/ intros, erw [map_id_lemma], refl, end,
+  map_comp := begin /- `obviously'` says: -/ intros, erw [map_comp_lemma], refl end }
 
 @[simp] lemma opposite_obj (F : C ↝ D) (X : C) : (F.op) X = F X := rfl
 @[simp] lemma opposite_map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F.op).map f = F.map f := rfl
@@ -46,7 +46,7 @@ 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,
-  map      := λ X Y f, λ h, f.1 ≫ h ≫ f.2,
+  map'     := λ X Y f, λ h, f.1 ≫ h ≫ f.2,
   map_id   := begin /- `obviously'` says: -/ intros, ext, intros, cases X, dsimp at *, simp, erw [category.id_comp_lemma] end,
   map_comp := begin /- `obviously'` says: -/ intros, ext, intros, cases f, cases g, cases X, cases Y, cases Z, dsimp at *, simp, erw [category.assoc] end }
 

category_theory/products.lean

@@ -43,28 +43,28 @@ namespace prod
 /-- `inl C Z` is the functor `X ↦ (X, Z)`. -/
 def inl (C : Type u₁) [category.{u₁ v₁} C] {D : Type u₁} [category.{u₁ v₁} D] (Z : D) : C ↝ (C × D) :=
 { obj      := λ X, (X, Z),
-  map      := λ X Y f, (f, 𝟙 Z),
+  map'     := λ X Y f, (f, 𝟙 Z),
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
 /-- `inr D Z` is the functor `X ↦ (Z, X)`. -/
 def inr {C : Type u₁} [category.{u₁ v₁} C] (D : Type u₁) [category.{u₁ v₁} D] (Z : C) : D ↝ (C × D) :=
 { obj      := λ X, (Z, X),
-  map      := λ X Y f, (𝟙 Z, f),
+  map'     := λ X Y f, (𝟙 Z, f),
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
 /-- `fst` is the functor `(X, Y) ↦ X`. -/
 def fst (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ C :=
 { obj      := λ X, X.1,
-  map      := λ X Y f, f.1,
+  map'     := λ X Y f, f.1,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
 /-- `snd` is the functor `(X, Y) ↦ Y`. -/
 def snd (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ D :=
 { obj      := λ X, X.2,
-  map      := λ X Y f, f.2,
+  map'     := λ X Y f, f.2,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
@@ -77,7 +77,7 @@ namespace functor
 /-- The cartesian product of two functors. -/
 def prod (F : A ↝ B) (G : C ↝ D) : (A × C) ↝ (B × D) :=
 { obj := λ X, (F X.1, G X.2),
-  map := λ _ _ f, (F.map f.1, G.map f.2),
+  map':= λ _ _ f, (F.map f.1, G.map f.2),
   map_id   := begin /- `obviously'` says: -/ intros, cases X, dsimp, rw map_id_lemma, rw map_id_lemma end,
   map_comp := begin /- `obviously'` says: -/ intros, cases Z, cases Y, cases X, cases f, cases g, dsimp at *, rw map_comp_lemma, rw map_comp_lemma end }
 

category_theory/types.lean

@@ -44,7 +44,7 @@ end functor_to_types
 
 definition ulift : (Type u) ↝ (Type (max u v)) := 
 { obj      := λ X, ulift.{v} X,
-  map      := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down),
+  map'     := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down),
   map_id   := begin /- `obviously'` says: -/ intros, ext, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }