typeclass inference problem

src/category_theory/functor_category.lean

@@ -36,12 +36,13 @@ section
 @[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟹ F).app X = 𝟙 (F.obj X) := rfl
 @[simp] lemma comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
   (α ≫ β).app X = α.app X ≫ β.app X := rfl
+
 end
 
 namespace nat_trans
 -- This section gives two lemmas about natural transformations
 -- between functors into functor categories,
--- spelling them out in components.
+-- spelling them out in components,
 
 include ℰ
 
@@ -53,6 +54,13 @@ lemma naturality_app {F G : C ⥤ (D ⥤ E)} (T : F ⟹ G) (Z : D) {X Y : C} (f
   ((F.map f).app Z) ≫ ((T.app Y).app Z) = ((T.app X).app Z) ≫ ((G.map f).app Z) :=
 congr_fun (congr_arg app (T.naturality f)) Z
 
+@[simp] lemma map_vcomp {F : (C ⥤ D) ⥤ E} {G H K : C ⥤ D} {α : G ⟹ H} {β : H ⟹ K} :
+  F.map(α ⊟ β) = F.map α ≫ F.map β :=
+begin
+  rw ←F.map_comp,
+  refl,
+end
+
 end nat_trans
 
 end functor.category

src/category_theory/instances/functor_ext.lean

@@ -0,0 +1,23 @@
+import category_theory.functor
+
+universes u₁ v₁ u₂
+
+open category_theory
+
+variables (C : Sort u₁) [𝒞 : category.{v₁} C]
+variables (D : Sort u₂) [𝒟 : category.{0} D]
+include 𝒞 𝒟
+
+namespace category_theory.functor
+
+/-- For functors into Prop-level categories, we can use extensionality. -/
+-- Look ma, no `eq.rec`!
+@[extensionality] lemma ext (F G : C ⥤ D) (w : ∀ X : C, F.obj X = G.obj X) : F = G :=
+begin
+  cases F, cases G,
+  congr,
+  funext,
+  exact w x,
+end
+
+end category_theory.functor

src/category_theory/instances/topological_spaces.lean

@@ -111,6 +111,10 @@ instance : category.{u+1} (opens X) :=
 { hom  := λ U V, ulift (plift (U ≥ V)),
   id   := λ X, ⟨ ⟨ le_refl X ⟩ ⟩,
   comp := λ X Y Z f g, ⟨ ⟨ ge_trans f.down.down g.down.down ⟩ ⟩ }
+-- instance : category.{0} (opens X) :=
+-- { hom  := λ U V, U ≥ V,
+--   id   := λ X, le_refl X,
+--   comp := λ X Y Z f g, ge_trans f g }
 
 def nbhds (x : X.α) := { U : opens X // x ∈ U }
 instance nbhds_category (x : X.α) : category (nbhds x) := begin unfold nbhds, apply_instance end
@@ -169,6 +173,8 @@ def map (x : X) : nbhds (f x) ⥤ nbhds x :=
 { obj := λ U, ⟨(opens.map f).obj U.1, by tidy⟩,
   map := λ U V i, (opens.map f).map i }
 
+@[simp] lemma map_id_obj (x : X) (U : nbhds x) : (map (𝟙 X) x).obj U = U := by tidy
+
 def inclusion_map_iso (x : X) : nbhds_inclusion (f x) ⋙ opens.map f ≅ map f x ⋙ nbhds_inclusion x :=
 nat_iso.of_components
   (λ U, begin split, exact 𝟙 _, exact 𝟙 _ end)

src/category_theory/limits/limits.lean

@@ -498,6 +498,19 @@ def colimit.desc (F : J ⥤ C) [has_colimit F] (c : cocone F) : colimit F ⟶ c.
   colimit.ι F j ≫ colimit.desc F c = c.ι.app j :=
 is_colimit.fac _ c j
 
+/--
+We have lots of lemmas describing how to simplify `colimit.ι F j ≫ _`,
+and combined with `colimit.ext` we rely on these lemmas for many calculations.
+
+However, since `category.assoc` is a `@[simp]` lemma, often expressions are
+right associated, and it's hard to apply these lemmas about `colimit.ι`.
+
+We thus define some additional `@[simp]` lemmas, with an arbitrary extra morphism.
+ -/
+@[simp] lemma colimit.ι_desc_assoc {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) {Y : C} (f : c.X ⟶ Y) :
+  colimit.ι F j ≫ colimit.desc F c ≫ f = c.ι.app j ≫ f :=
+by rw [←category.assoc, colimit.ι_desc]
+
 def colimit.cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) :
   cocone_morphism (colimit.cocone F) c :=
 (colimit.is_colimit F).desc_cocone_morphism c
@@ -541,6 +554,10 @@ colimit.desc (E ⋙ F)
 @[simp] lemma colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) :=
 by erw is_colimit.fac
 
+@[simp] lemma colimit.ι_pre_assoc (k : K) {Z : C} (f : colimit F ⟶ Z):
+  colimit.ι (E ⋙ F) k ≫ (colimit.pre F E) ≫ f = ((colimit.ι F (E.obj k)) : (E ⋙ F).obj k ⟶ colimit F) ≫ f :=
+by rw [←category.assoc, colimit.ι_pre]
+
 @[simp] lemma colimit.pre_desc (c : cocone F) :
   colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) :=
 by ext; rw [←assoc, colimit.ι_pre]; simp
@@ -575,6 +592,10 @@ colimit.desc (F ⋙ G)
 @[simp] lemma colimit.ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G  = G.map (colimit.ι F j) :=
 by erw is_colimit.fac
 
+@[simp] lemma colimit.ι_post_assoc (j : J) {Y : D} (f : G.obj (colimit F) ⟶ Y):
+  colimit.ι (F ⋙ G) j ≫ colimit.post F G  ≫ f = G.map (colimit.ι F j) ≫ f :=
+by rw [←category.assoc, colimit.ι_post]
+
 @[simp] lemma colimit.post_desc (c : cocone F) :
   colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.map_cocone c) :=
 by ext; rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_desc, colimit.ι_desc]; refl
@@ -626,6 +647,10 @@ variables {F} {G : J ⥤ C} (α : F ⟹ G)
 @[simp] lemma colim.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j :=
 by apply is_colimit.fac
 
+@[simp] lemma colim.ι_map_assoc (j : J) {Y : C} (f : colimit G ⟶ Y):
+  colimit.ι F j ≫ colim.map α ≫ f = α.app j ≫ colimit.ι G j ≫ f :=
+by rw [←category.assoc, colim.ι_map, category.assoc]
+
 @[simp] lemma colimit.map_desc (c : cocone G) :
   colim.map α ≫ colimit.desc G c = colimit.desc F ((cocones.precompose α).obj c) :=
 by ext; rw [←assoc, colim.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl

src/category_theory/natural_isomorphism.lean

@@ -4,12 +4,13 @@
 
 import category_theory.isomorphism
 import category_theory.functor_category
+import category_theory.whiskering
 
 open category_theory
 
-namespace category_theory.nat_iso
+universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+namespace category_theory.nat_iso
 
 variables {C : Sort u₁} [𝒞 : category.{v₁} C] {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
@@ -92,15 +93,38 @@ by tidy
 
 end category_theory.nat_iso
 
-namespace category_theory.functor
+open category_theory
 
-universes u₁ u₂ v₁ v₂
+namespace category_theory.functor
 
 section
 variables {C : Sort u₁} [𝒞 : category.{v₁} C]
           {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
 
+section
+variables {E : Sort u₃} [ℰ : category.{v₃} E]
+include ℰ
+
+-- TODO rename functor.on_iso to functor.map_iso?
+
+def map_nat_iso {F G : C ⥤ D} (K : D ⥤ E) (α : F ≅ G) : (F ⋙ K) ≅ (G ⋙ K) :=
+nat_iso.of_components
+(λ X, K.on_iso (nat_iso.app α X))
+(λ X Y f,
+  begin
+    dsimp,
+    rw [←functor.map_comp, nat_trans.naturality, functor.map_comp],
+  end)
+
+@[simp] def map_nat_iso_hom {F G : C ⥤ D} (K : D ⥤ E) (α : F ≅ G) : (K.map_nat_iso α).hom = whisker_right α.hom K :=
+rfl
+@[simp] def map_nat_iso_inv {F G : C ⥤ D} (K : D ⥤ E) (α : F ≅ G) : (K.map_nat_iso α).inv = whisker_right α.inv K :=
+rfl
+
+-- TODO lemmas relating this to whiskering? rename this to something with `whiskering` in it?
+end
+
 @[simp] protected def id_comp (F : C ⥤ D) : functor.id C ⋙ F ≅ F :=
 { hom := { app := λ X, 𝟙 (F.obj X) },
   inv := { app := λ X, 𝟙 (F.obj X) } }

src/category_theory/preordered_stalks.lean

@@ -6,22 +6,22 @@ open category_theory.limits
 
 namespace category_theory
 
-structure PreorderPresheaf extends Presheaf.{v} (Type v) :=
-(preorder : Π x : X, preorder (to_Presheaf.stalk x))
+structure PreorderPresheaf extends PresheafedSpace.{v} (Type v) :=
+(preorder : Π x : X, preorder (to_PresheafedSpace.stalk x))
 
-instance (F : PreorderPresheaf.{v}) (x : F.X) : preorder (F.to_Presheaf.stalk x) :=
+instance (F : PreorderPresheaf.{v}) (x : F.X) : preorder (F.to_PresheafedSpace.stalk x) :=
 F.preorder x
 
 namespace PreorderPresheaf
 
 -- what's going on with the @s !?
 structure hom (F G : PreorderPresheaf.{v}) :=
-(hom : F.to_Presheaf ⟶ G.to_Presheaf)
-(monotone : Π (x : F.X) (a b : @Presheaf.stalk (Type v) _ _ G.to_Presheaf (Presheaf.hom.f hom x)),
-   (a ≤ b) → ((@Presheaf.stalk_map (Type v) _ _ _ _ hom x) a ≤ (@Presheaf.stalk_map (Type v) _ _ _ _ hom x) b))
+(hom : F.to_PresheafedSpace ⟶ G.to_PresheafedSpace)
+(monotone : Π (x : F.X) (a b : @PresheafedSpace.stalk (Type v) _ _ G.to_PresheafedSpace (PresheafedSpace.hom.f hom x)),
+   (a ≤ b) → ((@PresheafedSpace.stalk_map (Type v) _ _ _ _ hom x) a ≤ (@PresheafedSpace.stalk_map (Type v) _ _ _ _ hom x) b))
 
 def id (F : PreorderPresheaf.{v}) : hom F F :=
-{ hom := 𝟙 F.to_Presheaf,
+{ hom := 𝟙 F.to_PresheafedSpace,
   monotone := λ x a b h, begin simp, end  }
 
 end PreorderPresheaf

src/category_theory/presheaf.lean

@@ -21,33 +21,66 @@ include 𝒞
 
 def presheaf (X : Top.{v}) := opens X ⥤ C
 
+instance category_presheaf (X : Top.{v}) : category (presheaf C X) :=
+by dsimp [presheaf]; apply_instance
+
 namespace presheaf
 variables {C}
+
 @[simp] def pushforward {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : presheaf C X) : presheaf C Y :=
 (opens.map f) ⋙ ℱ
+
+def pushforward_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : presheaf C X) :
+  ℱ.pushforward f ≅ ℱ.pushforward g :=
+ℱ.map_nat_iso (opens.map_iso f g h)
+def pushforward_eq_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h₁ h₂ : f = g) (ℱ : presheaf C X) :
+  ℱ.pushforward_eq h₁ = ℱ.pushforward_eq h₂ :=
+rfl
+
+namespace pushforward
+def id {X : Top.{v}} (ℱ : presheaf C X) : ℱ.pushforward (𝟙 X) ≅ ℱ :=
+ℱ.map_nat_iso (opens.map_id X) ≪≫ functor.left_unitor _
+
+def comp {X Y Z : Top.{v}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : presheaf C X) : ℱ.pushforward (f ≫ g) ≅ (ℱ.pushforward f).pushforward g :=
+ℱ.map_nat_iso (opens.map_comp f g)
+
+@[simp] lemma comp_id {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : presheaf C X) :
+  comp f (𝟙 Y) ℱ = ℱ.pushforward_eq (category.comp_id Top.{v} f) :=
+begin
+  dsimp [id, comp],
+  tidy,
+end
+
+@[simp] lemma id_comp {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : presheaf C X) :
+  comp (𝟙 X) f ℱ = ℱ.pushforward_eq (category.id_comp Top.{v} f) :=
+begin
+  dsimp [id, comp],
+  tidy,
+end
+-- TODO a lemma about assoc?
+end pushforward
+
 end presheaf
 
-instance category_presheaf (X : Top.{v}) : category (presheaf C X) :=
-by dsimp [presheaf]; apply_instance
 
-structure Presheaf :=
+structure PresheafedSpace :=
 (X : Top.{v})
 (𝒪 : presheaf C X)
 
-instance : has_coe_to_sort (Presheaf.{v} C) :=
+instance : has_coe_to_sort (PresheafedSpace.{v} C) :=
 { S := Type v, coe := λ F, F.X.α }
 
 variables {C}
 
-namespace Presheaf
+namespace PresheafedSpace
 
-instance underlying_space (F : Presheaf.{v} C) : topological_space F := F.X.str
+instance underlying_space (F : PresheafedSpace.{v} C) : topological_space F := F.X.str
 
-structure hom (F G : Presheaf.{v} C) :=
+structure hom (F G : PresheafedSpace.{v} C) :=
 (f : F.X ⟶ G.X)
 (c : G.𝒪 ⟹ F.𝒪.pushforward f)
 
-@[extensionality] lemma ext {F G : Presheaf.{v} C} (α β : hom F G)
+@[extensionality] lemma ext {F G : PresheafedSpace.{v} C} (α β : hom F G)
   (w : α.f = β.f) (h : α.c ⊟ (whisker_right (opens.map_iso _ _ w).hom F.𝒪) = β.c) :
   α = β :=
 begin
@@ -57,48 +90,56 @@ begin
 end
 .
 
-@[simp] def id (F : Presheaf.{v} C) : hom F F :=
+@[simp] def id (F : PresheafedSpace.{v} C) : hom F F :=
 { f := 𝟙 F.X,
   c := ((functor.id_comp _).inv) ⊟ (whisker_right (opens.map_id _).inv _) }
 
-@[simp] def comp (F G H : Presheaf.{v} C) (α : hom F G) (β : hom G H) : hom F H :=
+@[simp] def comp (F G H : PresheafedSpace.{v} C) (α : hom F G) (β : hom G H) : hom F H :=
 { f := α.f ≫ β.f,
   c := β.c ⊟ (whisker_left (opens.map β.f) α.c) }
 
 variables (C)
 
-instance category_of_presheaves : category (Presheaf.{v} C) :=
+instance category_of_presheaves : category (PresheafedSpace.{v} C) :=
 { hom  := hom,
   id   := id,
   comp := comp, }.
 
 variables {C}
 
-@[simp] lemma id_f (F : Presheaf.{v} C) : ((𝟙 F) : F ⟶ F).f = 𝟙 F.X := rfl
-@[simp] lemma id_c (F : Presheaf.{v} C) :
+@[simp] lemma id_f (F : PresheafedSpace.{v} C) : ((𝟙 F) : F ⟶ F).f = 𝟙 F.X := rfl
+@[simp] lemma id_c (F : PresheafedSpace.{v} C) :
   ((𝟙 F) : F ⟶ F).c = (((functor.id_comp _).inv) ⊟ (whisker_right (opens.map_id _).inv _)) :=
 rfl
-@[simp] lemma comp_f {F G H : Presheaf.{v} C} (α : F ⟶ G) (β : G ⟶ H) :
+@[simp] lemma comp_f {F G H : PresheafedSpace.{v} C} (α : F ⟶ G) (β : G ⟶ H) :
   (α ≫ β).f = α.f ≫ β.f :=
 rfl
-@[simp] lemma comp_c {F G H : Presheaf.{v} C} (α : F ⟶ G) (β : G ⟶ H) :
+@[simp] lemma comp_c {F G H : PresheafedSpace.{v} C} (α : F ⟶ G) (β : G ⟶ H) :
   (α ≫ β).c = (β.c ⊟ (whisker_left (opens.map β.f) α.c)) :=
 rfl
-end Presheaf
+end PresheafedSpace
 
 attribute [simp] set.preimage_id -- TODO mathlib?
 
 variables {D : Type u} [𝒟 : category.{v+1} D]
 include 𝒟
 
-def functor.map_presheaf (F : C ⥤ D) : Presheaf.{v} C ⥤ Presheaf.{v} D :=
+def functor.map_presheaf (F : C ⥤ D) : PresheafedSpace.{v} C ⥤ PresheafedSpace.{v} D :=
 { obj := λ X, { X := X.X, 𝒪 := X.𝒪 ⋙ F },
   map := λ X Y f, { f := f.f, c := whisker_right f.c F } }.
 
-@[simp] lemma functor.map_presheaf_obj_X (F : C ⥤ D) (X : Presheaf.{v} C) : (F.map_presheaf.obj X).X = X.X := rfl
-@[simp] lemma functor.map_presheaf_obj_𝒪 (F : C ⥤ D) (X : Presheaf.{v} C) : (F.map_presheaf.obj X).𝒪 = X.𝒪 ⋙ F := rfl
-@[simp] lemma functor.map_presheaf_map_f (F : C ⥤ D) {X Y : Presheaf.{v} C} (f : X ⟶ Y) : (F.map_presheaf.map f).f = f.f := rfl
-@[simp] lemma functor.map_presheaf_map_c (F : C ⥤ D) {X Y : Presheaf.{v} C} (f : X ⟶ Y) : (F.map_presheaf.map f).c = whisker_right f.c F := rfl
+@[simp] lemma functor.map_presheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
+  (F.map_presheaf.obj X).X = X.X :=
+rfl
+@[simp] lemma functor.map_presheaf_obj_𝒪 (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
+  (F.map_presheaf.obj X).𝒪 = X.𝒪 ⋙ F :=
+rfl
+@[simp] lemma functor.map_presheaf_map_f (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
+  (F.map_presheaf.map f).f = f.f :=
+rfl
+@[simp] lemma functor.map_presheaf_map_c (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
+  (F.map_presheaf.map f).c = whisker_right f.c F :=
+rfl
 
 def nat_trans.on_presheaf {F G : C ⥤ D} (α : F ⟹ G) : G.map_presheaf ⟹ F.map_presheaf :=
 { app := λ X,