refactor(category_theory/concrete_category): move bundled to own file

Author: rwbarton

src/category_theory/category.lean

@@ -80,49 +80,6 @@ A `small_category` has objects and morphisms in the same universe level.
 -/
 abbreviation small_category (C : Type u)     : Type (u+1) := category.{u} C
 
-structure bundled (c : Type u → Type v) :=
-(α : Type u)
-(str : c α)
-
-instance (c : Type u → Type v) : has_coe_to_sort (bundled c) :=
-{ S := Type u, coe := bundled.α }
-
-def mk_ob {c : Type u → Type v} (α : Type u) [str : c α] : bundled c :=
-@bundled.mk c α str
-
-/-- `concrete_category hom` collects the evidence that a type constructor `c` and a morphism
-predicate `hom` can be thought of as a concrete category.
-In a typical example, `c` is the type class `topological_space` and `hom` is `continuous`. -/
-structure concrete_category {c : Type u → Type v}
-  (hom : out_param $ ∀{α β : Type u}, c α → c β → (α → β) → Prop) :=
-(hom_id : ∀{α} (ia : c α), hom ia ia id)
-(hom_comp : ∀{α β γ} (ia : c α) (ib : c β) (ic : c γ) {f g},
-  hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))
-attribute [class] concrete_category
-
-section
-variables {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-variables [h : concrete_category @hom]
-include h
-
-instance : category (bundled c) :=
-{ hom   := λa b, subtype (hom a.2 b.2),
-  id    := λa, ⟨@id a.1, h.hom_id a.2⟩,
-  comp  := λa b c f g, ⟨g.1 ∘ f.1, h.hom_comp a.2 b.2 c.2 f.2 g.2⟩ }
-
-@[simp] lemma concrete_category_id (X : bundled c) : subtype.val (𝟙 X) = id := rfl
-@[simp] lemma concrete_category_comp {X Y Z : bundled c} (f : X ⟶ Y) (g : Y ⟶ Z) :
-  subtype.val (f ≫ g) = g.val ∘ f.val := rfl
-
-instance {X Y : bundled c} : has_coe_to_fun (X ⟶ Y) :=
-{ F := λ f, X → Y,
-  coe := λ f, f.1 }
-
-@[simp] lemma bundled_hom_coe {X Y : bundled c} (val : X → Y) (prop) (x : X) :
-  (⟨val, prop⟩ : X ⟶ Y) x = val x := rfl
-
-end
-
 section
 variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}
 include 𝒞

src/category_theory/concrete_category.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2018 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather
+
+Bundled type and structure.
+-/
+import category_theory.functor
+import category_theory.types
+
+universes u v
+
+namespace category_theory
+variables {c d : Type u → Type v} {α : Type u}
+
+/--
+`concrete_category @hom` collects the evidence that a type constructor `c` and a
+morphism predicate `hom` can be thought of as a concrete category.
+
+In a typical example, `c` is the type class `topological_space` and `hom` is
+`continuous`.
+-/
+structure concrete_category (hom : out_param $ ∀ {α β}, c α → c β → (α → β) → Prop) :=
+(hom_id : ∀ {α} (ia : c α), hom ia ia id)
+(hom_comp : ∀ {α β γ} (ia : c α) (ib : c β) (ic : c γ) {f g}, hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))
+
+attribute [class] concrete_category
+
+/-- `bundled` is a type bundled with a type class instance for that type. Only
+the type class is exposed as a parameter. -/
+structure bundled (c : Type u → Type v) : Type (max (u+1) v) :=
+(α : Type u)
+(str : c α)
+
+def mk_ob {c : Type u → Type v} (α : Type u) [str : c α] : bundled c := ⟨α, str⟩
+
+namespace bundled
+
+instance : has_coe_to_sort (bundled c) :=
+{ S := Type u, coe := bundled.α }
+
+/-- Map over the bundled structure -/
+def map (f : ∀ {α}, c α → d α) (b : bundled c) : bundled d :=
+⟨b.α, f b.str⟩
+
+section concrete_category
+variables (hom : ∀ {α β : Type u}, c α → c β → (α → β) → Prop)
+variables [h : concrete_category @hom]
+include h
+
+instance : category (bundled c) :=
+{ hom   := λ a b, subtype (hom a.2 b.2),
+  id    := λ a, ⟨@id a.1, h.hom_id a.2⟩,
+  comp  := λ a b c f g, ⟨g.1 ∘ f.1, h.hom_comp a.2 b.2 c.2 f.2 g.2⟩ }
+
+variables {X Y Z : bundled c}
+
+@[simp] lemma concrete_category_id (X : bundled c) : subtype.val (𝟙 X) = id :=
+rfl
+
+@[simp] lemma concrete_category_comp (f : X ⟶ Y) (g : Y ⟶ Z) :
+  subtype.val (f ≫ g) = g.val ∘ f.val :=
+rfl
+
+instance : has_coe_to_fun (X ⟶ Y) :=
+{ F   := λ f, X → Y,
+  coe := λ f, f.1 }
+
+@[simp] lemma bundled_hom_coe {X Y : bundled c} (val : X → Y) (prop) (x : X) :
+  (⟨val, prop⟩ : X ⟶ Y) x = val x := rfl
+
+end concrete_category
+
+end bundled
+
+def concrete_functor
+  {C : Type u → Type v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC]
+  {D : Type u → Type v} {hD : ∀{α β}, D α → D β → (α → β) → Prop} [concrete_category @hD]
+  (m : ∀{α}, C α → D α) (h : ∀{α β} {ia : C α} {ib : C β} {f}, hC ia ib f → hD (m ia) (m ib) f) :
+  bundled C ⥤ bundled D :=
+{ obj := bundled.map @m,
+  map := λ X Y f, ⟨ f, h f.2 ⟩}
+
+section forget
+variables {C : Type u → Type v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
+include i
+
+/-- The forgetful functor from a bundled category to `Type`. -/
+def forget : bundled C ⥤ Type u := { obj := bundled.α, map := λa b h, h.1 }
+
+instance forget.faithful : faithful (forget : bundled C ⥤ Type u) := {}
+
+end forget
+
+end category_theory

src/category_theory/examples/measurable_space.lean

@@ -6,7 +6,6 @@ Basic setup for measurable spaces.
 -/
 
 import category_theory.examples.topological_spaces
-import category_theory.types
 import measure_theory.borel_space
 
 open category_theory

src/category_theory/examples/monoids.lean

@@ -7,8 +7,8 @@ Introduce Mon -- the category of monoids.
 Currently only the basic setup.
 -/
 
+import category_theory.concrete_category
 import category_theory.fully_faithful
-import category_theory.types
 import category_theory.adjunction
 import data.finsupp
 

src/category_theory/examples/rings.lean

@@ -7,6 +7,7 @@ Introduce CommRing -- the category of commutative rings.
 Currently only the basic setup.
 -/
 
+import category_theory.concrete_category
 import category_theory.examples.monoids
 import category_theory.fully_faithful
 import category_theory.adjunction

src/category_theory/examples/topological_spaces.lean

@@ -2,6 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Patrick Massot, Scott Morrison, Mario Carneiro
 
+import category_theory.concrete_category
 import category_theory.full_subcategory
 import category_theory.functor_category
 import category_theory.adjunction
@@ -135,4 +136,4 @@ nat_iso.of_components (λ U, eq_to_iso (congr_fun (congr_arg _ (congr_arg _ h))
 
 @[simp] def map_iso_id {X : Top.{u}} (h) : map_iso (𝟙 X) (𝟙 X) h = iso.refl (map _) := rfl
 
-end topological_space.opens
+end topological_space.opens

src/category_theory/functor.lean

@@ -97,16 +97,4 @@ 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 :=
-{ α := s.α, str := f s.str }
-
-def concrete_functor
-  {C : Type u → Type v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC]
-  {D : Type u → Type v} {hD : ∀{α β}, D α → D β → (α → β) → Prop} [concrete_category @hD]
-  (m : ∀{α}, C α → D α) (h : ∀{α β} {ia : C α} {ib : C β} {f}, hC ia ib f → hD (m ia) (m ib) f) :
-  bundled C ⥤ bundled D :=
-{ obj := bundled.map @m,
-  map := λ X Y f, ⟨ f, h f.2 ⟩}
-
 end category_theory

src/category_theory/types.lean

@@ -54,15 +54,4 @@ instance ulift_functor_faithful : fully_faithful ulift_functor :=
   injectivity' := λ X Y f g p, funext $ λ x,
     congr_arg ulift.down ((congr_fun p (ulift.up x)) : ((ulift.up (f x)) = (ulift.up (g x)))) }
 
-section forget
-variables {C : Type u → Type v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
-include i
-
-/-- The forgetful functor from a bundled category to `Type`. -/
-def forget : bundled C ⥤ Type u := { obj := bundled.α, map := λa b h, h.1 }
-
-instance forget.faithful : faithful (forget : bundled C ⥤ Type u) := {}
-
-end forget
-
 end category_theory