feat(category_theory/*): some lemmas about universes

category_theory/category.lean

@@ -118,12 +118,17 @@ end
 
 section
 variable (C : Type u)
-variable [small_category C]
+variable [category.{u v} C]
 
-instance : large_category (ulift.{(u+1)} C) :=
+universe u'
+
+instance ulift_category : category.{(max u u') v} (ulift.{u'} C) :=
 { hom  := λ X Y, (X.down ⟶ Y.down),
   id   := λ X, 𝟙 X.down,
-  comp := λ _ _ _ f g, f ≫ g }
+  comp := λ _ _ _ f g, f ≫ g }  
+
+-- We verify that this previous instance can lift small categories to large categories.
+example (D : Type u) [small_category D] : large_category (ulift.{u+1} D) := by apply_instance
 end
 
 variables (α : Type u)

category_theory/functor.lean

@@ -103,6 +103,19 @@ infixr ` ⋙ `:80 := comp
   (F ⋙ G).map f = G.map (F.map f) := rfl
 end
 
+section
+variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+@[simp] def ulift_down : (ulift.{u₂} C) ⥤ C :=
+{ obj := λ X, X.down,
+  map' := λ X Y f, f }
+
+@[simp] def ulift_up : C ⥤ (ulift.{u₂} C) :=
+{ obj := λ X, ⟨ X ⟩,
+  map' := λ X Y f, f }
+end
+
 end functor
 
 def bundled.map {c : Type u → Type v} {d : Type u → Type v} (f : Π{a}, c a → d a) (s : bundled c) : bundled d :=

category_theory/natural_isomorphism.lean

@@ -87,6 +87,7 @@ namespace category_theory.functor
 
 universes u₁ u₂ v₁ v₂
 
+section
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] 
           {D : Type u₂} [𝒟 : category.{u₂ v₂} D] 
 include 𝒞 𝒟
@@ -121,4 +122,20 @@ variables (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D)
 -- When it's time to define monoidal categories and 2-categories,
 -- we'll need to add lemmas relating these natural isomorphisms,
 -- in particular the pentagon for the associator.
+end
+
+section
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] 
+include 𝒞
+
+def ulift_down_up : ulift_down.{u₁ v₁ u₂} C ⋙ ulift_up C ≅ functor.id (ulift.{u₂} C) :=
+{ hom := { app := λ X, @category.id (ulift.{u₂} C) _ X },
+  inv := { app := λ X, @category.id (ulift.{u₂} C) _ X } }
+
+def ulift_up_down : ulift_up.{u₁ v₁ u₂} C ⋙ ulift_down C ≅ functor.id C :=
+{ hom := { app := λ X, 𝟙 X },
+  inv := { app := λ X, 𝟙 X } }
+
+end
+
 end category_theory.functor