diff --git a/src/algebra/category/FinVect.lean b/src/algebra/category/FinVect.lean
index f78a110c0bf5d..39dd0267240df 100644
--- a/src/algebra/category/FinVect.lean
+++ b/src/algebra/category/FinVect.lean
@@ -32,21 +32,15 @@ instance monoidal_predicate_finite_dimensional :
   prop_tensor' := λ X Y hX hY, by exactI module.finite.tensor_product K X Y }
 
 /-- Define `FinVect` as the subtype of `Module.{u} K` of finite dimensional vector spaces. -/
-@[derive [large_category, λ α, has_coe_to_sort α (Sort*), concrete_category, monoidal_category,
-  symmetric_category]]
-def FinVect := { V : Module.{u} K // finite_dimensional K V }
+@[derive [large_category, concrete_category, monoidal_category, symmetric_category]]
+def FinVect := full_subcategory (λ (V : Module.{u} K), finite_dimensional K V)
 
 namespace FinVect
 
-instance finite_dimensional (V : FinVect K) : finite_dimensional K V := V.prop
+instance finite_dimensional (V : FinVect K) : finite_dimensional K V.obj := V.property
 
 instance : inhabited (FinVect K) := ⟨⟨Module.of K K, finite_dimensional.finite_dimensional_self K⟩⟩
 
-instance : has_coe (FinVect.{u} K) (Module.{u} K) := { coe := λ V, V.1, }
-
-protected lemma coe_comp {U V W : FinVect K} (f : U ⟶ V) (g : V ⟶ W) :
-  ((f ≫ g) : U → W) = (g : V → W) ∘ (f : U → V) := rfl
-
 /-- Lift an unbundled vector space to `FinVect K`. -/
 def of (V : Type u) [add_comm_group V] [module K V] [finite_dimensional K V] : FinVect K :=
 ⟨Module.of K V, by { change finite_dimensional K V, apply_instance }⟩
@@ -61,42 +55,39 @@ variables (V : FinVect K)
 
 /-- The dual module is the dual in the rigid monoidal category `FinVect K`. -/
 def FinVect_dual : FinVect K :=
-⟨Module.of K (module.dual K V), subspace.module.dual.finite_dimensional⟩
-
-instance : has_coe_to_fun (FinVect_dual K V) (λ _, V → K) :=
-{ coe := λ v, by { change V →ₗ[K] K at v, exact v, } }
+⟨Module.of K (module.dual K V.obj), subspace.module.dual.finite_dimensional⟩
 
 open category_theory.monoidal_category
 
 /-- The coevaluation map is defined in `linear_algebra.coevaluation`. -/
 def FinVect_coevaluation : 𝟙_ (FinVect K) ⟶ V ⊗ (FinVect_dual K V) :=
-by apply coevaluation K V
+by apply coevaluation K V.obj
 
 lemma FinVect_coevaluation_apply_one : FinVect_coevaluation K V (1 : K) =
-   ∑ (i : basis.of_vector_space_index K V),
-    (basis.of_vector_space K V) i ⊗ₜ[K] (basis.of_vector_space K V).coord i :=
-by apply coevaluation_apply_one K V
+   ∑ (i : basis.of_vector_space_index K V.obj),
+    (basis.of_vector_space K V.obj) i ⊗ₜ[K] (basis.of_vector_space K V.obj).coord i :=
+by apply coevaluation_apply_one K V.obj
 
 /-- The evaluation morphism is given by the contraction map. -/
 def FinVect_evaluation : (FinVect_dual K V) ⊗ V ⟶ 𝟙_ (FinVect K) :=
-by apply contract_left K V
+by apply contract_left K V.obj
 
 @[simp]
-lemma FinVect_evaluation_apply (f : (FinVect_dual K V)) (x : V) :
-  (FinVect_evaluation K V) (f ⊗ₜ x) = f x :=
+lemma FinVect_evaluation_apply (f : (FinVect_dual K V).obj) (x : V.obj) :
+  (FinVect_evaluation K V) (f ⊗ₜ x) = f.to_fun x :=
 by apply contract_left_apply f x
 
 private theorem coevaluation_evaluation :
   let V' : FinVect K := FinVect_dual K V in
   (𝟙 V' ⊗ (FinVect_coevaluation K V)) ≫ (α_ V' V V').inv ≫ (FinVect_evaluation K V ⊗ 𝟙 V')
   = (ρ_ V').hom ≫ (λ_ V').inv :=
-by apply contract_left_assoc_coevaluation K V
+by apply contract_left_assoc_coevaluation K V.obj
 
 private theorem evaluation_coevaluation :
   (FinVect_coevaluation K V ⊗ 𝟙 V)
   ≫ (α_ V (FinVect_dual K V) V).hom ≫ (𝟙 V ⊗ FinVect_evaluation K V)
   = (λ_ V).hom ≫ (ρ_ V).inv :=
-by apply contract_left_assoc_coevaluation' K V
+by apply contract_left_assoc_coevaluation' K V.obj
 
 instance exact_pairing : exact_pairing V (FinVect_dual K V) :=
 { coevaluation := FinVect_coevaluation K V,
@@ -112,7 +103,7 @@ variables {K V} (W : FinVect K)
 
 /-- Converts and isomorphism in the category `FinVect` to a `linear_equiv` between the underlying
 vector spaces. -/
-def iso_to_linear_equiv {V W : FinVect K} (i : V ≅ W) : V ≃ₗ[K] W :=
+def iso_to_linear_equiv {V W : FinVect K} (i : V ≅ W) : V.obj ≃ₗ[K] W.obj :=
   ((forget₂ (FinVect.{u} K) (Module.{u} K)).map_iso i).to_linear_equiv
 
 lemma iso.conj_eq_conj {V W : FinVect K} (i : V ≅ W) (f : End V) :
diff --git a/src/algebra/category/FinVect/limits.lean b/src/algebra/category/FinVect/limits.lean
index e27d7c05aa3c2..70188668e71db 100644
--- a/src/algebra/category/FinVect/limits.lean
+++ b/src/algebra/category/FinVect/limits.lean
@@ -48,7 +48,7 @@ instance (F : J ⥤ FinVect k) :
   finite_dimensional k (limit (F ⋙ forget₂ (FinVect k) (Module.{v} k)) : Module.{v} k) :=
 begin
   haveI : ∀ j, finite_dimensional k ((F ⋙ forget₂ (FinVect k) (Module.{v} k)).obj j),
-  { intro j, change finite_dimensional k (F.obj j), apply_instance, },
+  { intro j, change finite_dimensional k (F.obj j).obj, apply_instance, },
   exact finite_dimensional.of_injective
     (limit_subobject_product (F ⋙ forget₂ (FinVect k) (Module.{v} k)))
     ((Module.mono_iff_injective _).1 (by apply_instance)),
diff --git a/src/algebraic_geometry/AffineScheme.lean b/src/algebraic_geometry/AffineScheme.lean
index 4444625b845fe..fb26ada924bac 100644
--- a/src/algebraic_geometry/AffineScheme.lean
+++ b/src/algebraic_geometry/AffineScheme.lean
@@ -41,7 +41,8 @@ namespace algebraic_geometry
 open Spec (structure_sheaf)
 
 /-- The category of affine schemes -/
-def AffineScheme := Scheme.Spec.ess_image
+@[derive category, nolint has_nonempty_instance]
+def AffineScheme := Scheme.Spec.ess_image_subcategory
 
 /-- A Scheme is affine if the canonical map `X ⟶ Spec Γ(X)` is an isomorphism. -/
 class is_affine (X : Scheme) : Prop :=
@@ -54,18 +55,23 @@ def Scheme.iso_Spec (X : Scheme) [is_affine X] :
   X ≅ Scheme.Spec.obj (op $ Scheme.Γ.obj $ op X) :=
 as_iso (Γ_Spec.adjunction.unit.app X)
 
-lemma mem_AffineScheme (X : Scheme) : X ∈ AffineScheme ↔ is_affine X :=
+/-- Construct an affine scheme from a scheme and the information that it is affine. -/
+@[simps]
+def AffineScheme.mk (X : Scheme) (h : is_affine X) : AffineScheme :=
+⟨X, @@mem_ess_image_of_unit_is_iso _ _ _ _ h.1⟩
+
+lemma mem_Spec_ess_image (X : Scheme) : X ∈ Scheme.Spec.ess_image ↔ is_affine X :=
 ⟨λ h, ⟨functor.ess_image.unit_is_iso h⟩, λ h, @@mem_ess_image_of_unit_is_iso _ _ _ X h.1⟩
 
-instance is_affine_AffineScheme (X : AffineScheme.{u}) : is_affine (X : Scheme.{u}) :=
-(mem_AffineScheme _).mp X.prop
+instance is_affine_AffineScheme (X : AffineScheme.{u}) : is_affine X.obj :=
+⟨functor.ess_image.unit_is_iso X.property⟩
 
 instance Spec_is_affine (R : CommRingᵒᵖ) : is_affine (Scheme.Spec.obj R) :=
-(mem_AffineScheme _).mp (Scheme.Spec.obj_mem_ess_image R)
+algebraic_geometry.is_affine_AffineScheme ⟨_, Scheme.Spec.obj_mem_ess_image R⟩
 
 lemma is_affine_of_iso {X Y : Scheme} (f : X ⟶ Y) [is_iso f] [h : is_affine Y] :
   is_affine X :=
-by { rw [← mem_AffineScheme] at h ⊢, exact functor.ess_image.of_iso (as_iso f).symm h }
+by { rw [← mem_Spec_ess_image] at h ⊢, exact functor.ess_image.of_iso (as_iso f).symm h }
 
 namespace AffineScheme
 
diff --git a/src/algebraic_geometry/properties.lean b/src/algebraic_geometry/properties.lean
index 4043ecffb4a34..a942db176b528 100644
--- a/src/algebraic_geometry/properties.lean
+++ b/src/algebraic_geometry/properties.lean
@@ -34,7 +34,7 @@ begin
   rw t0_space_iff_inseparable,
   intros x y h,
   obtain ⟨U, R, ⟨e⟩⟩ := X.local_affine x,
-  have hy : y ∈ U.val := (h.mem_open_iff U.1.2).1 U.2,
+  have hy : y ∈ U.obj := (h.mem_open_iff U.1.2).1 U.2,
   erw ← subtype_inseparable_iff (⟨x, U.2⟩ : U.1.1) (⟨y, hy⟩ : U.1.1) at h,
   let e' : U.1 ≃ₜ prime_spectrum R :=
     homeo_of_iso ((LocallyRingedSpace.forget_to_SheafedSpace ⋙ SheafedSpace.forget _).map_iso e),
diff --git a/src/algebraic_topology/simplex_category.lean b/src/algebraic_topology/simplex_category.lean
index 0dc093321ccff..335a502fd6a9d 100644
--- a/src/algebraic_topology/simplex_category.lean
+++ b/src/algebraic_topology/simplex_category.lean
@@ -382,7 +382,7 @@ def is_skeleton_of : is_skeleton_of NonemptyFinLinOrd simplex_category skeletal_
 
 /-- The truncated simplex category. -/
 @[derive small_category]
-def truncated (n : ℕ) := {a : simplex_category // a.len ≤ n}
+def truncated (n : ℕ) := full_subcategory (λ a : simplex_category, a.len ≤ n)
 
 namespace truncated
 
diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean
index 67ce6368ea73d..39f172553e620 100644
--- a/src/category_theory/adjunction/reflective.lean
+++ b/src/category_theory/adjunction/reflective.lean
@@ -156,17 +156,19 @@ by rw [←equiv.eq_symm_apply, unit_comp_partial_bijective_symm_natural A h, equ
 /-- If `i : D ⥤ C` is reflective, the inverse functor of `i ≌ F.ess_image` can be explicitly
 defined by the reflector. -/
 @[simps]
-def equiv_ess_image_of_reflective [reflective i] : D ≌ i.ess_image :=
+def equiv_ess_image_of_reflective [reflective i] : D ≌ i.ess_image_subcategory :=
 { functor := i.to_ess_image,
   inverse := i.ess_image_inclusion ⋙ (left_adjoint i : _),
   unit_iso := nat_iso.of_components (λ X, (as_iso $ (of_right_adjoint i).counit.app X).symm)
     (by { intros X Y f, dsimp, simp only [is_iso.eq_inv_comp, is_iso.comp_inv_eq, category.assoc],
       exact ((of_right_adjoint i).counit.naturality _).symm }),
-  counit_iso := nat_iso.of_components
-    (λ X, by { refine (iso.symm $ as_iso _), exact (of_right_adjoint i).unit.app X,
+  counit_iso :=
+  nat_iso.of_components
+    (λ X, by { refine (iso.symm $ as_iso _), exact (of_right_adjoint i).unit.app X.obj,
       apply_with (is_iso_of_reflects_iso _ i.ess_image_inclusion) { instances := ff },
-      exact functor.ess_image.unit_is_iso X.prop })
-    (by { intros X Y f, dsimp, simp only [is_iso.eq_inv_comp, is_iso.comp_inv_eq, category.assoc],
-      exact ((of_right_adjoint i).unit.naturality f).symm }) }
+      exact functor.ess_image.unit_is_iso X.property })
+    (by { intros X Y f, dsimp, rw [is_iso.comp_inv_eq, assoc],
+      have h := ((of_right_adjoint i).unit.naturality f).symm,
+      rw [functor.id_map] at h, erw [← h, is_iso.inv_hom_id_assoc, functor.comp_map] }) }
 
 end category_theory
diff --git a/src/category_theory/concrete_category/basic.lean b/src/category_theory/concrete_category/basic.lean
index bf12a8c81f664..29e9eb2079c0b 100644
--- a/src/category_theory/concrete_category/basic.lean
+++ b/src/category_theory/concrete_category/basic.lean
@@ -171,11 +171,11 @@ instance induced_category.has_forget₂ {C : Type v} {D : Type v'} [category D]
   forget_comp := rfl }
 
 instance full_subcategory.concrete_category {C : Type v} [category C] [concrete_category C]
-  (Z : C → Prop) : concrete_category {X : C // Z X} :=
+  (Z : C → Prop) : concrete_category (full_subcategory Z) :=
 { forget := full_subcategory_inclusion Z ⋙ forget C }
 
 instance full_subcategory.has_forget₂ {C : Type v} [category C] [concrete_category C]
-  (Z : C → Prop) : has_forget₂ {X : C // Z X} C :=
+  (Z : C → Prop) : has_forget₂ (full_subcategory Z) C :=
 { forget₂ := full_subcategory_inclusion Z,
   forget_comp := rfl }
 
diff --git a/src/category_theory/connected_components.lean b/src/category_theory/connected_components.lean
index e4f1e2bc3d2f1..ba3c0b93c162f 100644
--- a/src/category_theory/connected_components.lean
+++ b/src/category_theory/connected_components.lean
@@ -41,7 +41,7 @@ instance [inhabited J] : inhabited (connected_components J) := ⟨quotient.mk' d
 
 /-- Given an index for a connected component, produce the actual component as a full subcategory. -/
 @[derive category]
-def component (j : connected_components J) : Type u₁ := {k : J // quotient.mk' k = j}
+def component (j : connected_components J) : Type u₁ := full_subcategory (λ k, quotient.mk' k = j)
 
 /-- The inclusion functor from a connected component to the whole category. -/
 @[derive [full, faithful], simps {rhs_md := semireducible}]
@@ -82,7 +82,7 @@ begin
   { refine @@list.chain_pmap_of_chain _ _ _ f (λ x y _ _ h, _) hl₁ h₁₂ _,
     exact zag_of_zag_obj (component.ι _) h },
   { erw list.last_pmap _ f (j₁ :: l) (by simpa [h₁₂] using hf) (list.cons_ne_nil _ _),
-    exact subtype.ext hl₂ },
+    exact full_subcategory.ext _ _ hl₂ },
 end
 
 /--
diff --git a/src/category_theory/essential_image.lean b/src/category_theory/essential_image.lean
index 7a832885783c3..e5cbab18144e6 100644
--- a/src/category_theory/essential_image.lean
+++ b/src/category_theory/essential_image.lean
@@ -66,11 +66,13 @@ set.ext $ λ A, ⟨ess_image.of_nat_iso h, ess_image.of_nat_iso h.symm⟩
 /-- An object in the image is in the essential image. -/
 lemma obj_mem_ess_image (F : D ⥤ C) (Y : D) : F.obj Y ∈ ess_image F := ⟨Y, ⟨iso.refl _⟩⟩
 
-instance : category F.ess_image := category_theory.full_subcategory _
+/-- The essential image of a functor, interpreted of a full subcategory of the target category. -/
+@[derive category, nolint has_nonempty_instance]
+def ess_image_subcategory (F : C ⥤ D) := full_subcategory F.ess_image
 
 /-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
 @[derive [full, faithful], simps]
-def ess_image_inclusion (F : C ⥤ D) : F.ess_image ⥤ D :=
+def ess_image_inclusion (F : C ⥤ D) : F.ess_image_subcategory ⥤ D :=
 full_subcategory_inclusion _
 
 /--
@@ -78,9 +80,8 @@ Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from
 image of `F`.
 -/
 @[simps]
-def to_ess_image (F : C ⥤ D) : C ⥤ F.ess_image :=
-{ obj := λ X, ⟨_, obj_mem_ess_image _ X⟩,
-  map := λ X Y f, (ess_image_inclusion F).preimage (F.map f) }
+def to_ess_image (F : C ⥤ D) : C ⥤ F.ess_image_subcategory :=
+full_subcategory.lift _ F (obj_mem_ess_image _)
 
 /--
 The functor `F` factorises through its essential image, where the first functor is essentially
@@ -89,7 +90,7 @@ surjective and the second is fully faithful.
 @[simps]
 def to_ess_image_comp_essential_image_inclusion (F : C ⥤ D) :
   F.to_ess_image ⋙ F.ess_image_inclusion ≅ F :=
-nat_iso.of_components (λ X, iso.refl _) (by tidy)
+full_subcategory.lift_comp_inclusion _ _ _
 
 end functor
 
diff --git a/src/category_theory/full_subcategory.lean b/src/category_theory/full_subcategory.lean
index e34c71dcd3e33..52397e39da4f6 100644
--- a/src/category_theory/full_subcategory.lean
+++ b/src/category_theory/full_subcategory.lean
@@ -81,35 +81,41 @@ variables {C : Type u₁} [category.{v} C]
 variables (Z : C → Prop)
 
 /--
-The category structure on a subtype; morphisms just ignore the property.
+A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use
+actual subtypes since the simp-normal form `↑X` of `X.val` does not work well for full
+subcategories.
 
 See <https://stacks.math.columbia.edu/tag/001D>. We do not define 'strictly full' subcategories.
 -/
-instance full_subcategory : category.{v} {X : C // Z X} :=
-induced_category.category subtype.val
+@[ext, nolint has_nonempty_instance] structure full_subcategory :=
+(obj : C)
+(property : Z obj)
+
+instance full_subcategory.category : category.{v} (full_subcategory Z) :=
+induced_category.category full_subcategory.obj
 
 /--
 The forgetful functor from a full subcategory into the original category
 ("forgetting" the condition).
 -/
-def full_subcategory_inclusion : {X : C // Z X} ⥤ C :=
-induced_functor subtype.val
+def full_subcategory_inclusion : full_subcategory Z ⥤ C :=
+induced_functor full_subcategory.obj
 
 @[simp] lemma full_subcategory_inclusion.obj {X} :
-  (full_subcategory_inclusion Z).obj X = X.val := rfl
+  (full_subcategory_inclusion Z).obj X = X.obj := rfl
 @[simp] lemma full_subcategory_inclusion.map {X Y} {f : X ⟶ Y} :
   (full_subcategory_inclusion Z).map f = f := rfl
 
 instance full_subcategory.full : full (full_subcategory_inclusion Z) :=
-induced_category.full subtype.val
+induced_category.full _
 instance full_subcategory.faithful : faithful (full_subcategory_inclusion Z) :=
-induced_category.faithful subtype.val
+induced_category.faithful _
 
 variables {Z} {Z' : C → Prop}
 
 /-- An implication of predicates `Z → Z'` induces a functor between full subcategories. -/
 @[simps]
-def full_subcategory.map (h : ∀ ⦃X⦄, Z X → Z' X) : {X // Z X} ⥤ {X // Z' X} :=
+def full_subcategory.map (h : ∀ ⦃X⦄, Z X → Z' X) : full_subcategory Z ⥤ full_subcategory Z' :=
 { obj := λ X, ⟨X.1, h X.2⟩,
   map := λ X Y f, f }
 
@@ -128,7 +134,7 @@ variables {D : Type u₂} [category.{v₂} D] (P Q : D → Prop)
 /-- A functor which maps objects to objects satisfying a certain property induces a lift through
     the full subcategory of objects satisfying that property. -/
 @[simps]
-def full_subcategory.lift (F : C ⥤ D) (hF : ∀ X, P (F.obj X)) : C ⥤ {X // P X} :=
+def full_subcategory.lift (F : C ⥤ D) (hF : ∀ X, P (F.obj X)) : C ⥤ full_subcategory P :=
 { obj := λ X, ⟨F.obj X, hF X⟩,
   map := λ X Y f, F.map f }
 
diff --git a/src/category_theory/monoidal/subcategory.lean b/src/category_theory/monoidal/subcategory.lean
index 8fef005cad002..2944ad4c599d5 100644
--- a/src/category_theory/monoidal/subcategory.lean
+++ b/src/category_theory/monoidal/subcategory.lean
@@ -45,11 +45,11 @@ open monoidal_predicate
 variables [monoidal_predicate P]
 
 /--
-When `P` is a monoidal predicate, the full subcategory `{X : C // P X}` inherits the monoidal
-structure of `C`
+When `P` is a monoidal predicate, the full subcategory for `P` inherits the monoidal structure of
+  `C`.
 -/
-instance full_monoidal_subcategory : monoidal_category {X : C // P X} :=
-{ tensor_obj := λ X Y, ⟨X ⊗ Y, prop_tensor X.2 Y.2⟩,
+instance full_monoidal_subcategory : monoidal_category (full_subcategory P) :=
+{ tensor_obj := λ X Y, ⟨X.1 ⊗ Y.1, prop_tensor X.2 Y.2⟩,
   tensor_hom := λ X₁ Y₁ X₂ Y₂ f g, by { change X₁.1 ⊗ X₂.1 ⟶ Y₁.1 ⊗ Y₂.1,
     change X₁.1 ⟶ Y₁.1 at f, change X₂.1 ⟶ Y₂.1 at g, exact f ⊗ g },
   tensor_unit := ⟨𝟙_ C, prop_id⟩,
@@ -71,7 +71,7 @@ The forgetful monoidal functor from a full monoidal subcategory into the origina
 ("forgetting" the condition).
 -/
 @[simps]
-def full_monoidal_subcategory_inclusion : monoidal_functor {X : C // P X} C :=
+def full_monoidal_subcategory_inclusion : monoidal_functor (full_subcategory P) C :=
 { to_functor := full_subcategory_inclusion P,
   ε := 𝟙 _,
   μ := λ X Y, 𝟙 _ }
@@ -87,7 +87,7 @@ variables {P} {P' : C → Prop} [monoidal_predicate P']
 subcategories. -/
 @[simps]
 def full_monoidal_subcategory.map (h : ∀ ⦃X⦄, P X → P' X) :
-  monoidal_functor {X : C // P X} {X : C // P' X}  :=
+  monoidal_functor (full_subcategory P) (full_subcategory P')  :=
 { to_functor := full_subcategory.map h,
   ε := 𝟙 _,
   μ := λ X Y, 𝟙 _ }
@@ -102,9 +102,9 @@ section braided
 variables (P) [braided_category C]
 
 /--
-The braided structure on `{X : C // P X}` inherited by the braided structure on `C`.
+The braided structure on a full subcategory inherited by the braided structure on `C`.
 -/
-instance full_braided_subcategory : braided_category {X : C // P X} :=
+instance full_braided_subcategory : braided_category (full_subcategory P) :=
 braided_category_of_faithful (full_monoidal_subcategory_inclusion P)
   (λ X Y, ⟨(β_ X.1 Y.1).hom, (β_ X.1 Y.1).inv, (β_ X.1 Y.1).hom_inv_id, (β_ X.1 Y.1).inv_hom_id⟩)
   (λ X Y, by tidy)
@@ -114,7 +114,7 @@ The forgetful braided functor from a full braided subcategory into the original
 ("forgetting" the condition).
 -/
 @[simps]
-def full_braided_subcategory_inclusion : braided_functor {X : C // P X} C :=
+def full_braided_subcategory_inclusion : braided_functor (full_subcategory P) C :=
 { to_monoidal_functor := full_monoidal_subcategory_inclusion P,
   braided' := λ X Y, by { rw [is_iso.eq_inv_comp], tidy } }
 
@@ -129,7 +129,7 @@ variables {P}
 subcategories. -/
 @[simps]
 def full_braided_subcategory.map (h : ∀ ⦃X⦄, P X → P' X) :
-  braided_functor {X : C // P X} {X : C // P' X}  :=
+  braided_functor (full_subcategory P) (full_subcategory P')  :=
 { to_monoidal_functor := full_monoidal_subcategory.map h,
   braided' := λ X Y, by { rw [is_iso.eq_inv_comp], tidy }  }
 
@@ -144,7 +144,7 @@ section symmetric
 
 variables (P) [symmetric_category C]
 
-instance full_symmetric_subcategory : symmetric_category {X : C // P X} :=
+instance full_symmetric_subcategory : symmetric_category (full_subcategory P) :=
 symmetric_category_of_faithful (full_braided_subcategory_inclusion P)
 
 end symmetric
diff --git a/src/category_theory/preadditive/additive_functor.lean b/src/category_theory/preadditive/additive_functor.lean
index bf80733103044..d5119cad4094f 100644
--- a/src/category_theory/preadditive/additive_functor.lean
+++ b/src/category_theory/preadditive/additive_functor.lean
@@ -147,7 +147,7 @@ variables (C D : Type*) [category C] [category D] [preadditive C] [preadditive D
 /-- Bundled additive functors. -/
 @[derive category, nolint has_nonempty_instance]
 def AdditiveFunctor :=
-{ F : C ⥤ D // functor.additive F }
+full_subcategory (λ (F : C ⥤ D), F.additive)
 
 infixr ` ⥤+ `:26 := AdditiveFunctor
 
diff --git a/src/category_theory/sites/sieves.lean b/src/category_theory/sites/sieves.lean
index 0eaba6acc1718..f0453fb0c5c4d 100644
--- a/src/category_theory/sites/sieves.lean
+++ b/src/category_theory/sites/sieves.lean
@@ -44,7 +44,7 @@ instance : inhabited (presieve X) := ⟨⊤⟩
 /-- Given a sieve `S` on `X : C`, its associated diagram `S.diagram` is defined to be
     the natural functor from the full subcategory of the over category `C/X` consisting
     of arrows in `S` to `C`. -/
-abbreviation diagram (S : presieve X) : {f : over X // S f.hom} ⥤ C :=
+abbreviation diagram (S : presieve X) : full_subcategory (λ (f : over X), S f.hom) ⥤ C :=
 full_subcategory_inclusion _ ⋙ over.forget X
 
 /-- Given a sieve `S` on `X : C`, its associated cocone `S.cocone` is defined to be
diff --git a/src/category_theory/subobject/basic.lean b/src/category_theory/subobject/basic.lean
index 5a8913a0d8811..46565079d87dd 100644
--- a/src/category_theory/subobject/basic.lean
+++ b/src/category_theory/subobject/basic.lean
@@ -149,7 +149,7 @@ The morphism in `C` from the arbitrarily chosen underlying object to the ambient
 -/
 noncomputable
 def arrow {X : C} (Y : subobject X) : (Y : C) ⟶ X :=
-(representative.obj Y).val.hom
+(representative.obj Y).obj.hom
 
 instance arrow_mono {X : C} (Y : subobject X) : mono (Y.arrow) :=
 (representative.obj Y).property
diff --git a/src/category_theory/subobject/mono_over.lean b/src/category_theory/subobject/mono_over.lean
index 0325ade408c04..98ccbe1a4b4e1 100644
--- a/src/category_theory/subobject/mono_over.lean
+++ b/src/category_theory/subobject/mono_over.lean
@@ -49,19 +49,19 @@ This isn't skeletal, so it's not a partial order.
 Later we define `subobject X` as the quotient of this by isomorphisms.
 -/
 @[derive [category]]
-def mono_over (X : C) := {f : over X // mono f.hom}
+def mono_over (X : C) := full_subcategory (λ (f : over X), mono f.hom)
 
 namespace mono_over
 
 /-- Construct a `mono_over X`. -/
 @[simps]
-def mk' {X A : C} (f : A ⟶ X) [hf : mono f] : mono_over X := { val := over.mk f, property := hf }
+def mk' {X A : C} (f : A ⟶ X) [hf : mono f] : mono_over X := { obj := over.mk f, property := hf }
 
 /-- The inclusion from monomorphisms over X to morphisms over X. -/
 def forget (X : C) : mono_over X ⥤ over X := full_subcategory_inclusion _
 
 instance : has_coe (mono_over X) C :=
-{ coe := λ Y, Y.val.left, }
+{ coe := λ Y, Y.obj.left, }
 
 @[simp]
 lemma forget_obj_left {f} : ((forget X).obj f).left = (f : C) := rfl
@@ -93,13 +93,13 @@ end⟩
 @[reassoc] lemma w {f g : mono_over X} (k : f ⟶ g) : k.left ≫ g.arrow = f.arrow := over.w _
 
 /-- Convenience constructor for a morphism in monomorphisms over `X`. -/
-abbreviation hom_mk {f g : mono_over X} (h : f.val.left ⟶ g.val.left) (w : h ≫ g.arrow = f.arrow) :
+abbreviation hom_mk {f g : mono_over X} (h : f.obj.left ⟶ g.obj.left) (w : h ≫ g.arrow = f.arrow) :
   f ⟶ g :=
 over.hom_mk h w
 
 /-- Convenience constructor for an isomorphism in monomorphisms over `X`. -/
 @[simps]
-def iso_mk {f g : mono_over X} (h : f.val.left ≅ g.val.left) (w : h.hom ≫ g.arrow = f.arrow) :
+def iso_mk {f g : mono_over X} (h : f.obj.left ≅ g.obj.left) (w : h.hom ≫ g.arrow = f.arrow) :
   f ≅ g :=
 { hom := hom_mk h.hom w,
   inv := hom_mk h.inv (by rw [h.inv_comp_eq, w]) }
@@ -217,7 +217,7 @@ def map_id : map (𝟙 X) ≅ 𝟭 _ :=
 lift_iso _ _ over.map_id ≪≫ lift_id
 
 @[simp] lemma map_obj_left (f : X ⟶ Y) [mono f] (g : mono_over X) :
-  (((map f).obj g) : C) = g.val.left :=
+  (((map f).obj g) : C) = g.obj.left :=
 rfl
 
 @[simp]
@@ -324,7 +324,7 @@ adjunction.mk_of_hom_equiv
     inv_fun := λ k,
     begin
       refine over.hom_mk _ _,
-      refine image.lift {I := g.val.left, m := g.arrow, e := k.left, fac' := over.w k},
+      refine image.lift {I := g.obj.left, m := g.arrow, e := k.left, fac' := over.w k},
       apply image.lift_fac,
     end,
     left_inv := λ k, subsingleton.elim _ _,
diff --git a/src/category_theory/subterminal.lean b/src/category_theory/subterminal.lean
index ddf8015a321e3..5adb0eedb5aae 100644
--- a/src/category_theory/subterminal.lean
+++ b/src/category_theory/subterminal.lean
@@ -117,7 +117,7 @@ to the lattice of open subsets of `X`. More generally, if `C` is a topos, this i
 -/
 @[derive category]
 def subterminals (C : Type u₁) [category.{v₁} C] :=
-{A : C // is_subterminal A}
+full_subcategory (λ (A : C), is_subterminal A)
 
 instance [has_terminal C] : inhabited (subterminals C) :=
 ⟨⟨⊤_ C, is_subterminal_of_terminal⟩⟩
@@ -140,7 +140,7 @@ def subterminals_equiv_mono_over_terminal [has_terminal C] :
   { obj := λ X, ⟨over.mk (terminal.from X.1), X.2.mono_terminal_from⟩,
     map := λ X Y f, mono_over.hom_mk f (by ext1 ⟨⟨⟩⟩) },
   inverse :=
-  { obj := λ X, ⟨X.val.left, λ Z f g, by { rw ← cancel_mono X.arrow, apply subsingleton.elim }⟩,
+  { obj := λ X, ⟨X.obj.left, λ Z f g, by { rw ← cancel_mono X.arrow, apply subsingleton.elim }⟩,
     map := λ X Y f, f.1 },
   unit_iso :=
   { hom := { app := λ X, 𝟙 _ },
diff --git a/src/representation_theory/fdRep.lean b/src/representation_theory/fdRep.lean
index bdc8703f7707c..054983741e6a1 100644
--- a/src/representation_theory/fdRep.lean
+++ b/src/representation_theory/fdRep.lean
@@ -43,13 +43,13 @@ variables {k G : Type u} [field k] [monoid G]
 instance : has_coe_to_sort (fdRep k G) (Type u) := concrete_category.has_coe_to_sort _
 
 instance (V : fdRep k G) : add_comm_group V :=
-by { change add_comm_group ((forget₂ (fdRep k G) (FinVect k)).obj V), apply_instance, }
+by { change add_comm_group ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_instance, }
 
 instance (V : fdRep k G) : module k V :=
-by { change module k ((forget₂ (fdRep k G) (FinVect k)).obj V), apply_instance, }
+by { change module k ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_instance, }
 
 instance (V : fdRep k G) : finite_dimensional k V :=
-by { change finite_dimensional k ((forget₂ (fdRep k G) (FinVect k)).obj V), apply_instance, }
+by { change finite_dimensional k ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_instance, }
 
 /-- The monoid homomorphism corresponding to the action of `G` onto `V : fdRep k G`. -/
 def ρ (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ
diff --git a/src/topology/category/Top/open_nhds.lean b/src/topology/category/Top/open_nhds.lean
index 5fad2e3daddcc..19d3a759f5b6c 100644
--- a/src/topology/category/Top/open_nhds.lean
+++ b/src/topology/category/Top/open_nhds.lean
@@ -35,7 +35,7 @@ variables {X Y : Top.{u}} (f : X ⟶ Y)
 namespace topological_space
 
 /-- The type of open neighbourhoods of a point `x` in a (bundled) topological space. -/
-def open_nhds (x : X) := { U : opens X // x ∈ U }
+def open_nhds (x : X) := full_subcategory (λ (U : opens X), x ∈ U)
 
 namespace open_nhds
 
@@ -43,7 +43,7 @@ instance (x : X) : partial_order (open_nhds x) :=
 { le := λ U V, U.1 ≤ V.1,
   le_refl := λ _, le_rfl,
   le_trans := λ _ _ _, le_trans,
-  le_antisymm := λ _ _ i j, subtype.eq $ le_antisymm i j }
+  le_antisymm := λ _ _ i j, full_subcategory.ext _ _ $ le_antisymm i j }
 
 instance (x : X) : lattice (open_nhds x) :=
 { inf := λ U V, ⟨U.1 ⊓ V.1, ⟨U.2, V.2⟩⟩,
@@ -92,7 +92,7 @@ lemma open_embedding {x : X} (U : open_nhds x) : open_embedding (U.1.inclusion)
 U.1.open_embedding
 
 def map (x : X) : open_nhds (f x) ⥤ open_nhds x :=
-{ obj := λ U, ⟨(opens.map f).obj U.1, by tidy⟩,
+{ obj := λ U, ⟨(opens.map f).obj U.1, U.2⟩,
   map := λ U V i, (opens.map f).map i }
 
 @[simp] lemma map_obj (x : X) (U) (q) : (map f x).obj ⟨U, q⟩ = ⟨(opens.map f).obj U, by tidy⟩ :=
diff --git a/src/topology/sheaves/sheaf_condition/opens_le_cover.lean b/src/topology/sheaves/sheaf_condition/opens_le_cover.lean
index 7af25b4afdc98..081f85a57a0bd 100644
--- a/src/topology/sheaves/sheaf_condition/opens_le_cover.lean
+++ b/src/topology/sheaves/sheaf_condition/opens_le_cover.lean
@@ -47,13 +47,12 @@ namespace sheaf_condition
 /--
 The category of open sets contained in some element of the cover.
 -/
-def opens_le_cover : Type v := { V : opens X // ∃ i, V ≤ U i }
+@[derive category]
+def opens_le_cover : Type v := full_subcategory (λ (V : opens X), ∃ i, V ≤ U i)
 
 instance [inhabited ι] : inhabited (opens_le_cover U) :=
 ⟨⟨⊥, default, bot_le⟩⟩
 
-instance : category (opens_le_cover U) := category_theory.full_subcategory _
-
 namespace opens_le_cover
 
 variables {U}
@@ -66,7 +65,7 @@ def index (V : opens_le_cover U) : ι := V.property.some
 /--
 The morphism from `V` to `U i` for some `i`.
 -/
-def hom_to_index (V : opens_le_cover U) : V.val ⟶ U (index V) :=
+def hom_to_index (V : opens_le_cover U) : V.obj ⟶ U (index V) :=
 (V.property.some_spec).hom
 
 end opens_le_cover
@@ -244,7 +243,7 @@ variables {Y : opens X} (hY : Y = supr U)
     in the sieve. This full subcategory is equivalent to `opens_le_cover U`, the (poset)
     category of opens contained in some `U i`. -/
 @[simps] def generate_equivalence_opens_le :
-  {f : over Y // (sieve.generate (presieve_of_covering_aux U Y)).arrows f.hom} ≌
+  full_subcategory (λ (f : over Y), (sieve.generate (presieve_of_covering_aux U Y)).arrows f.hom) ≌
   opens_le_cover U :=
 { functor :=
   { obj := λ f, ⟨f.1.left, let ⟨_,h,_,⟨i,hY⟩,_⟩ := f.2 in ⟨i, hY ▸ h.le⟩⟩,
diff --git a/src/topology/sheaves/sheafify.lean b/src/topology/sheaves/sheafify.lean
index 46368756c0bce..3c707fbc5aa5e 100644
--- a/src/topology/sheaves/sheafify.lean
+++ b/src/topology/sheaves/sheafify.lean
@@ -104,9 +104,9 @@ begin
   dsimp at e',
   use ⟨W ⊓ (U' ⊓ V'), ⟨mW, mU, mV⟩⟩,
   refine ⟨_, _, _⟩,
-  { change W ⊓ (U' ⊓ V') ⟶ U.val,
+  { change W ⊓ (U' ⊓ V') ⟶ U.obj,
     exact (opens.inf_le_right _ _) ≫ (opens.inf_le_left _ _) ≫ iU, },
-  { change W ⊓ (U' ⊓ V') ⟶ V.val,
+  { change W ⊓ (U' ⊓ V') ⟶ V.obj,
     exact (opens.inf_le_right _ _) ≫ (opens.inf_le_right _ _) ≫ iV, },
   { intro w,
     dsimp,
diff --git a/src/topology/sheaves/stalks.lean b/src/topology/sheaves/stalks.lean
index 5ff3e104a9df6..90f4f1ce8cb0c 100644
--- a/src/topology/sheaves/stalks.lean
+++ b/src/topology/sheaves/stalks.lean
@@ -155,7 +155,7 @@ begin
   dsimp [stalk_pushforward, stalk_functor],
   ext1,
   tactic.op_induction',
-  cases j, cases j_val,
+  rcases j with ⟨⟨_, _⟩, _⟩,
   rw [colimit.ι_map_assoc, colimit.ι_map, colimit.ι_pre, whisker_left_app, whisker_right_app,
        pushforward.id_hom_app, eq_to_hom_map, eq_to_hom_refl],
   dsimp,
@@ -172,8 +172,7 @@ begin
   dsimp [stalk_pushforward, stalk_functor],
   ext U,
   induction U using opposite.rec,
-  cases U,
-  cases U_val,
+  rcases U with ⟨⟨_, _⟩, _⟩,
   simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc,
              whisker_right_app, category.assoc],
   dsimp,