feat(category_theory): opposites, and the category of types

category_theory/functor.lean

@@ -84,7 +84,7 @@ def comp (F : C ↝ D) (G : D ↝ E) : C ↝ E :=
 
 infixr ` ⋙ `:80 := comp
 
-@[simp] lemma comp_obj (F : C ↝ D) (G : D ↝ E) (X : C) : (F ⋙ G).obj X = G.obj (F.obj X) := rfl
+@[simp] lemma comp_obj (F : C ↝ D) (G : D ↝ E) (X : C) : (F ⋙ G) X = G (F X) := rfl
 @[simp] lemma comp_map (F : C ↝ D) (G : D ↝ E) (X Y : C) (f : X ⟶ Y) : (F ⋙ G).map f = G.map (F.map f) := rfl
 end
 

category_theory/opposites.lean

@@ -0,0 +1,55 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Stephen Morgan, Scott Morrison
+
+import category_theory.functor
+import category_theory.products
+import category_theory.types
+
+namespace category_theory
+
+universes u₁ v₁ u₂ v₂
+
+def op (C : Type u₁) : Type u₁ := C
+
+notation C `ᵒᵖ` := op C
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+instance opposite : category.{u₁ v₁} (Cᵒᵖ) := 
+{ Hom     := λ X Y : C, Y ⟶ X,
+  comp    := λ _ _ _ f g, g ≫ f,
+  id      := λ X, 𝟙 X,
+  id_comp := begin /- `obviously'` says: -/ intros, simp end,
+  comp_id := begin /- `obviously'` says: -/ intros, simp end,
+  assoc   := begin /- `obviously'` says: -/ intros, simp end }
+
+namespace functor
+
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+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 }
+
+@[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
+
+end functor
+
+variable (C)
+
+definition hom_pairing : (Cᵒᵖ × C) ↝ (Type v₁) := 
+{ obj      := λ p, @category.Hom C _ p.1 p.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 }
+
+@[simp] lemma hom_pairing_obj (X : Cᵒᵖ × C) : (hom_pairing C) X = @category.Hom C _ X.1 X.2 := rfl
+@[simp] lemma hom_pairing_map {X Y : Cᵒᵖ × C} (f : X ⟶ Y) : (hom_pairing C).map f = λ h, f.1 ≫ h ≫ f.2 := rfl
+
+end category_theory

category_theory/products.lean

@@ -8,42 +8,37 @@ namespace category_theory
 universes u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄
 
 section
-variables (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D]
+variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
+include 𝒞 𝒟
 
 /--
 `prod.category C D` gives the cartesian product of two categories.
 -/
-instance prod.category : category.{(max u₁ u₂) (max v₁ v₂)} (C × D) :=
+instance prod : category.{(max u₁ u₂) (max v₁ v₂)} (C × D) :=
 { Hom     := λ X Y, ((X.1) ⟶ (Y.1)) × ((X.2) ⟶ (Y.2)),
   id      := λ X, ⟨ 𝟙 (X.1), 𝟙 (X.2) ⟩,
   comp    := λ _ _ _ f g, (f.1 ≫ g.1, f.2 ≫ g.2),
-  id_comp := begin  /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end,
+  id_comp := begin /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end,
   comp_id := begin /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end,
   assoc   := begin /- `obviously'` says: -/ intros, cases W, cases X, cases Y, cases Z, cases f, cases g, cases h, dsimp at *, simp end }
-end
-
-namespace prod.category
-
-section -- rfl lemmas for prod.category
-variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
-include 𝒞 𝒟
 
-@[simp, ematch] lemma id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) := rfl
-@[simp, ematch] lemma comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl
+-- rfl lemmas for category.prod
+@[simp, ematch] lemma prod_id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) := rfl
+@[simp, ematch] lemma prod_comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl
 end
 
 section
 variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₁) [𝒟 : category.{u₁ v₁} D]
-include 𝒞 𝒟
-
+include 𝒞 𝒟 
 /--
 `prod.category.uniform C D` is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.
 -/
-instance uniform : category (C × D) := prod.category C D
+instance uniform_prod : category (C × D) := category_theory.prod C D
 end
-
 -- Next we define the natural functors into and out of product categories. For now this doesn't address the universal properties.
 
+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),
@@ -72,21 +67,21 @@ def snd (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [catego
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
-end prod.category
+end prod
 
 variables {A : Type u₁} [𝒜 : category.{u₁ v₁} A] {B : Type u₂} [ℬ : category.{u₂ v₂} B] {C : Type u₃} [𝒞 : category.{u₃ v₃} C] {D : Type u₄} [𝒟 : category.{u₄ v₄} D]
 include 𝒜 ℬ 𝒞 𝒟
 
 namespace functor
-/-- The cartesion product of two functors. -/
+/-- 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_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 }
 
-@[simp, ematch] lemma prod_obj (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : F.prod G (a, c) = (F a, G c) := rfl
-@[simp, ematch] lemma prod_map (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (F.prod G).map f = (F.map f.1, G.map f.2) := rfl
+@[simp, ematch] lemma prod_obj  (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : (functor.prod F G)     (a, c) = (F a, G c) := rfl
+@[simp, ematch] lemma prod_map  (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (functor.prod F G).map f = (F.map f.1, G.map f.2) := rfl
 end functor
 
 namespace nat_trans
@@ -96,7 +91,7 @@ def prod {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) : F.prod
 { app        := λ X, (α X.1, β X.2),
   naturality := begin /- `obviously'` says: -/ intros, cases f, cases Y, cases X, dsimp at *, simp, split, rw naturality_lemma, rw naturality_lemma end }
 
-@[simp, ematch] lemma prod_app {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) (a : A) (c : C) : α.prod β (a, c) = (α a, β c) := rfl
+@[simp, ematch] lemma prod_app  {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) (a : A) (c : C) : (nat_trans.prod α β)     (a, c) = (α a, β c) := rfl
 end nat_trans
 
 end category_theory

category_theory/types.lean

@@ -0,0 +1,51 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Stephen Morgan, Scott Morrison
+
+import category_theory.functor_category
+
+namespace category_theory
+
+universes u v u' v' w
+
+instance types : large_category (Type u) :=
+{ Hom     := λ a b, (a → b),
+  id      := λ a, id,
+  comp    := λ _ _ _ f g, g ∘ f,
+  id_comp := begin /- `obviously'` says: -/ intros, refl  end,
+  comp_id := begin /- `obviously'` says: -/ intros, refl end,
+  assoc   := begin /- `obviously'` says: -/ intros, refl end }
+
+@[simp] lemma types_Hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl  
+@[simp] lemma types_id {α : Type u} (a : α) : (𝟙 α : α → α) a = a := rfl
+@[simp] lemma types_comp {α β γ : Type u} (f : α → β) (g : β → γ) (a : α) : (((f : α ⟶ β) ≫ (g : β ⟶ γ)) : α ⟶ γ) a = g (f a) := rfl
+
+namespace functor_to_types
+variables {C : Type u} [𝒞 : category.{u v} C] (F G H : C ↝ (Type w)) {X Y Z : C} 
+include 𝒞
+variables (σ : F ⟹ G) (τ : G ⟹ H) 
+
+@[simp,ematch] lemma map_comp (f : X ⟶ Y) (g : Y ⟶ Z) (a : F X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) :=
+begin /- `obviously'` says: -/ simp end
+
+@[simp,ematch] lemma map_id (a : F X) : (F.map (𝟙 X)) a = a := 
+begin /- `obviously'` says: -/ simp end
+
+@[ematch] lemma naturality (f : X ⟶ Y) (x : F X) : σ Y ((F.map f) x) = (G.map f) (σ X x) := 
+congr_fun (σ.naturality_lemma f) x
+
+@[simp] lemma vcomp (x : F X) : (σ ⊟ τ) X x = τ X (σ X x) := rfl
+
+variables {D : Type u'} [𝒟 : category.{u' v'} D] (I J : D ↝ C) (ρ : I ⟹ J) {W : D}
+
+@[simp] lemma hcomp (x : (I ⋙ F) W) : (ρ ◫ σ) W x = (G.map (ρ W)) (σ (I W) x) := rfl
+
+end functor_to_types
+
+definition type_lift : (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_id   := begin /- `obviously'` says: -/ intros, ext, refl end,
+  map_comp := begin /- `obviously'` says: -/ intros, refl end }
+
+end category_theory

tactic/ext.lean

@@ -1,6 +1,8 @@
 
 import tactic.basic
 
+universes u₁ u₂
+
 /--
  Tag lemmas of the form:
 
@@ -17,6 +19,13 @@ meta def extensional_attribute : user_attribute :=
 
 attribute [extensionality] _root_.funext array.ext
 
+namespace ulift
+@[extensionality] lemma ext {α : Type u₁} (X Y : ulift.{u₂} α) (w : X.down = Y.down) : X = Y :=
+begin
+  cases X, cases Y, dsimp at w, rw w,
+end
+end ulift
+
 namespace tactic
 open interactive interactive.types
 open lean.parser nat