Concrete category class redesign

Stream: mathlib4

[Anne Baanen]

I have been running some experiments in redesigning the ConcreteCategory class so we don't have a mismatch between docs#ConcreteCategory.instFunLike based on the forgetful functor and the FunLike instance for the morphisms of a particular category, e.g. RingHom.instFunLike. Essentially, what I would like to do is to split off having a faithful forgetful functor forget C : C --> Type from being a category where the homomorphisms are concretely implemented by FunLikes. (Previous mention here.)

I started attempting this in the branch#redesign-ConcreteCategory. The basic idea is to rename ConcreteCategory to HasForget and to introduce a new ConcreteCategory class parametrized by three things:

• FC : C -> C -> Type* maps the categorical type of Homs, for example RingCat.Hom to the concrete type of maps, for example RingHom,
• CC : C -> Type* maps objects of C to the concrete carriers,
• and an instance ∀ X Y, FunLike (FC X Y) (CC X) (CC Y).
  Then we'd have fields asserting the coercion from Homs to functions, via FC, preserves the identity and composition.

class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) (CC : outParam <| C → Type w)
    [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (hom_id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (hom_comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

Previously I tried doing this slightly differently, parametrizing ConcreteCategory over instances of CoeSort C (Type w) and CoeFun (X ⟶ Y) (X -> Y). This did not work as well, since those coercions will be unfolded to e.g. Bundled.ɑ if we work with e.g. RingCat, but if the instances are free variables they can't be unfolded and we see CoeSort.coe. Having the carrier as a free variable will fix this (at the expense of making the discrimination tree less keyed).

Note that ConcreteCategory and HasForget as defined here are logically equivalent: the difference lies in their elaboration properties.

Everything seems to go somewhat smoothly, albeit tediously, until we need to put this ConcreteCategory structure on Type: giving a CC and FC are no problem, but there is no FunLike instance on plain functions! We want the coercion of f : X -> Y to X -> Y to be f itself, not FunLike.toFun f. So probably in this setup it doesn't make sense to talk about Type as a concrete category. Since we have no such problem with HasForget, that's still logically okay: we can prove things for HasForget and then manually transfer them to Type like we currently have to do for each concrete category.

Where it gets a bit more tricky is when we want to work with presheaves that can be valued in Type or in other concrete categories, but the natural way to phrase properties involves the full ConcreteCategory structure with its coercions. For example docs#CategoryTheory.Presheaf.IsLocallyInjective is defined to be about (forget D).obj (F₁.obj X), which would become CC (F₁.obj X) in the refactored version. But the concrete category D here is commonly also Type, so with this design we'll need to keep the HasForget version and set up aliases to use lemmas seamlessly for both Type and general ConcreteCategory.

[Anne Baanen]

I think this is definitely a path worth pursuing, although I would like to make sure I'm not missing something that would make it possible to incorporate Type with the other concrete categories.

Thoughts?

[Anne Baanen]

Tagging @Adam Topaz @Joël Riou @Christian Merten who have authored a lot of concrete categories recently. @Yury G. Kudryashov might also be interested?

[Christian Merten]

Previously I tried doing this slightly differently, parametrizing ConcreteCategory over instances of CoeSort C (Type w) and CoeFun (X ⟶ Y) (X -> Y). This did not work as well, since those coercions will be unfolded to e.g. Bundled.ɑ if we work with e.g. RingCat, but if the instances are free variables they can't be unfolded and we see CoeSort.coe. Having the carrier as a free variable will fix this (at the expense of making the discrimination tree less keyed).

A naive thought: what about keeping the CC argument and replacing the FunLike by CoeFun (X ⟶ Y) (CC X -> CC Y)?

[Edward van de Meent]

i suspect that then you get the same issue? from my understanding, FunLike is basically CoeFun with the added condition that the coercion is injective...

[Joël Riou]

probably in this setup it doesn't make sense to talk about Type as a concrete category.

I think it would be very problematic if Type was no longer a concrete category.

[Christian Merten]

No, CoeFun.coe is inlined as I learned recently. My point is that a CoeFun (X -> Y) (fun _ => X -> Y) should not have the issue that Anne describes here:

but there is no FunLike instance on plain functions! We want the coercion of f : X -> Y to X -> Y to be f itself, not FunLike.toFun f

Making Type a ConcreteCategory again. And with CCinstead of CoeSort there will be no CoeSort.coe.

[Christian Merten]

Of course in the general setup, the CoeFun can't be unfolded so it will behave like FunLike.

[Christian Merten]

Alternatively one could keep both CC and FC and just replace FunLike (FC X Y) (CC X) (CC Y) by CoeFun (FC X Y) (fun _ => CC X -> CC Y).

[Yury G. Kudryashov]

Are there any simp lemmas about concrete categories? If you use coercions that expand at elaboration time, then simp lemmas will no longer match.

[Christian Merten]

Yes there are and I think it is even worse, they don't even apply with rw. So indeed, my suggestion does not work. CoeFun does not seem to be the right tool for this type of abstraction.

[Yury G. Kudryashov]

CoeFun unfolds too.

[Christian Merten]

That's why I say it does not seem to be the right tool here. Am I misunderstanding you?

[Yury G. Kudryashov]

Sorry, I've missed "not" in your message.

[Yury G. Kudryashov]

:man_facepalming:

[Christian Merten]

If we make morphisms in Type u one field structures, which we might want to do anyways, it would fit Anne's redesigned concrete categories again by setting FC X Y = Hom X Y and defining FunLike (Hom X Y) X Y.

[Anne Baanen]

I can check how much pain we cause by changing the Type category to use the Hom structures. I suppose an alternative is to make X -> Y a local FunLike instance in the way that we currently have a local ConcreteCategory.instFunLike to open.

[Anne Baanen]

Answer to the first question: a lot of pain, and it doesn't help to try and combine this with the ConcreteCategory class. I'll try the no-op FunLike now.

[Anne Baanen]

This also runs into difficulties, unfortunately: to apply results about docs#CategoryTheory.Functor.id to forget Type we want these two to be with_reducible rfl, and if we want to define the forgetful functor using a ConcreteCategory instance, then we only get a with_reducible_and_instances rfl.

[Anne Baanen]

Unless of course we use forgetful inheritance between HasForget and ConcreteCategory...

[Anne Baanen]

Nope, not going to work either, because that would break the defeq (forget C).obj X = carrier X, meaning we can't even state that (forget C).map f = hom f unless we insert a bunch of casts...

[Anne Baanen]

I have been playing around with a few options, seeing if maybe we can get the reducible defeq between ConcreteCategory.hasForget.forget, HasForget.types.forget and Functor.id Type to work by brute force anyway.

Option 1: make ConcreteCategory.hom and DFunLike.coe reducible:

import Mathlib.CategoryTheory.EpiMono
import Mathlib.CategoryTheory.Functor.FullyFaithful
import Mathlib.Data.Set.Operations
import Mathlib.Tactic.PPWithUniv

set_option autoImplicit false

namespace CategoryTheory

universe w w' v v' v'' u u' u''

/- The `@[to_additive]` attribute is just a hint that expressions involving this instance can
  still be additivized. -/
@[to_additive existing CategoryTheory.types]
instance types : LargeCategory (Type u) where
  Hom a b := a → b
  id _ := id
  comp f g := g ∘ f

theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
  rfl

-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10688): this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
-- because of its "if all else fails, apply all `ext` lemmas" policy,
-- which apparently we want to move away from.
@[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g := by
  funext x
  exact h x

/-- Class for categories `C` with a fixed faithful functor `forget : C ⥤ Type`.

This forgetful functor should not be used to cast objects or morphisms to
types or functions respectively: see `ConcreteCategory` for that.

Note that `HasForget` potentially depends on three independent universe levels,
* the universe level `w` appearing in `forget : C ⥤ Type w`
* the universe level `v` of the morphisms (i.e. we have a `Category.{v} C`)
* the universe level `u` of the objects (i.e `C : Type u`)
They are specified that order, to avoid unnecessary universe annotations.
-/
class HasForget (C : Type u) [Category.{v} C] where
  /-- We have a functor to Type -/
  protected forget : C ⥤ Type w
  /-- That functor is faithful -/
  [forget_faithful : forget.Faithful]

attribute [inline, reducible] HasForget.forget
attribute [instance] HasForget.forget_faithful

/-- The forgetful functor from a concrete category to `Type u`. -/
abbrev forget (C : Type u) [Category.{v} C] [HasForget.{w} C] : C ⥤ Type w :=
  HasForget.forget

-- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _`
@[instance] abbrev HasForget.types : HasForget.{u, u, u+1} (Type u) where
  forget := 𝟭 _

class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) (CC : outParam <| C → Type w)
    [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

export ConcreteCategory (id_apply comp_apply)

section

variable {C : Type u} [Category.{v} C] {F : C → C → Type*} {CC : C → Type w}
variable [∀ X Y, FunLike (F X Y) (CC X) (CC Y)]
variable [ConcreteCategory C F CC]

namespace ConcreteCategory

attribute [simp] id_apply comp_apply

/-- We can apply morphisms of concrete categories by first casting them down
to the base functions.
-/
instance {X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ CC X → CC Y) where
  coe f := hom f

lemma hom_injective {X Y : C} : Function.Injective (hom : (X ⟶ Y) → F X Y) :=
  Function.LeftInverse.injective ofHom_hom

@[ext] lemma hom_ext {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g :=
  hom_injective h

abbrev toHasForget : HasForget C where
  forget.obj := CC
  forget.map f := ⇑(hom f)
  forget_faithful.map_injective h := hom_injective (DFunLike.coe_injective h)

end ConcreteCategory

section

variable (C)

/-- Build a coercion to functions out of `HasForget`.

The intended usecase is to provide a `FunLike` instance in `HasForget.toConcreteCategory`.
See that definition for the considerations in making this an instance.
-/
abbrev HasForget.toFunLike [HasForget C] (X Y : C) :
    FunLike (X ⟶ Y) ((forget C).obj X) ((forget C).obj Y) where
  coe := (forget C).map
  coe_injective' _ _ h := Functor.Faithful.map_injective h

attribute [local instance] HasForget.toFunLike
/-- Build a concrete category out of `HasForget`.

The intended usecase is to prove theorems referencing only `(forget C)`
and not `(forget C).obj X` nor `(forget C).map f`: those should be written
as `CC X` and `ConcreteCategory.hom f` respectively.
-/
abbrev HasForget.toConcreteCategory [HasForget C] :
    ConcreteCategory C (· ⟶ ·) _ where
  hom f := f
  ofHom f := f
  id_apply := congr_fun ((forget C).map_id _)
  comp_apply _ _ := congr_fun ((forget C).map_comp _ _)

attribute [local instance] HasForget.toConcreteCategory

/-- Check that the new `ConcreteCategory` has the same forgetful functor as we started with. -/
example [inst : HasForget C] :
    @forget C _ ((HasForget.toConcreteCategory _).toHasForget) = @forget C _ inst := by
  with_reducible_and_instances rfl

/-- In particular, this should work for the category of types. -/
example :
    @forget Type _ ((HasForget.toConcreteCategory _).toHasForget) = @forget Type _ HasForget.types := by
  with_reducible_and_instances rfl -- Fails at `with_reducible`

/-- In addition, `forget Type` should be the identity functor. -/
example :
    @forget Type _ ((HasForget.toConcreteCategory _).toHasForget) = Functor.id _ := by
  with_reducible_and_instances rfl -- Fails at `with_reducible`

set_option allowUnsafeReducibility true
attribute [reducible] ConcreteCategory.hom DFunLike.coe

/-- In particular, this should work for the category of types. -/
example :
    @forget Type _ ((HasForget.toConcreteCategory _).toHasForget) = @forget Type _ HasForget.types := by
  with_reducible rfl

/-- In addition, `forget Type` should be the identity functor. -/
example :
    @forget Type _ ((HasForget.toConcreteCategory _).toHasForget) = Functor.id _ := by
  with_reducible rfl

end

[Anne Baanen]

Option 2 is to make a one-field structure Types.Hom that wraps plain functions, and then try to put a ConcreteCategory instance on that. But the outcome is even worse:

import Mathlib.CategoryTheory.EpiMono
import Mathlib.CategoryTheory.Functor.FullyFaithful
import Mathlib.Data.Set.Operations
import Mathlib.Tactic.PPWithUniv

set_option autoImplicit false

namespace CategoryTheory

universe w w' v v' v'' u u' u''

@[ext]
structure Types.Hom (X Y : Type u) : Type u where private mk ::
  hom : X → Y

/- The `@[to_additive]` attribute is just a hint that expressions involving this instance can
  still be additivized. -/
@[to_additive existing CategoryTheory.types]
instance types : LargeCategory (Type u) where
  Hom a b := Types.Hom a b
  id _ := ⟨id⟩
  comp f g := ⟨g.hom ∘ f.hom⟩

abbrev types.ofHom {X Y : Type u} (f : X → Y) : X ⟶ Y := ⟨f⟩

-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10688): this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
-- because of its "if all else fails, apply all `ext` lemmas" policy,
-- which apparently we want to move away from.
@[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f.hom a = g.hom a) : f = g := by
  apply Types.Hom.ext
  funext x
  exact h x

/-- Class for categories `C` with a fixed faithful functor `forget : C ⥤ Type`.

This forgetful functor should not be used to cast objects or morphisms to
types or functions respectively: see `ConcreteCategory` for that.

Note that `HasForget` potentially depends on three independent universe levels,
* the universe level `w` appearing in `forget : C ⥤ Type w`
* the universe level `v` of the morphisms (i.e. we have a `Category.{v} C`)
* the universe level `u` of the objects (i.e `C : Type u`)
They are specified that order, to avoid unnecessary universe annotations.
-/
class HasForget (C : Type u) [Category.{v} C] where
  /-- We have a functor to Type -/
  protected forget : C ⥤ Type w
  /-- That functor is faithful -/
  [forget_faithful : forget.Faithful]

attribute [inline, reducible] HasForget.forget
attribute [instance] HasForget.forget_faithful

/-- The forgetful functor from a concrete category to `Type u`. -/
abbrev forget (C : Type u) [Category.{v} C] [HasForget.{w} C] : C ⥤ Type w :=
  HasForget.forget

-- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _`
@[instance] abbrev HasForget.types : HasForget.{u, u, u+1} (Type u) where
  forget := 𝟭 _

class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) (CC : outParam <| C → Type w)
    [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

export ConcreteCategory (id_apply comp_apply)

section

variable {C : Type u} [Category.{v} C] {F : C → C → Type*} {CC : C → Type w}
variable [∀ X Y, FunLike (F X Y) (CC X) (CC Y)]
variable [ConcreteCategory C F CC]

namespace ConcreteCategory

attribute [simp] id_apply comp_apply

/-- We can apply morphisms of concrete categories by first casting them down
to the base functions.
-/
instance {X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ CC X → CC Y) where
  coe f := hom f

lemma hom_injective {X Y : C} : Function.Injective (hom : (X ⟶ Y) → F X Y) :=
  Function.LeftInverse.injective ofHom_hom

@[ext] lemma hom_ext {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g :=
  hom_injective h

lemma coe_ext_iff {X Y : C} {f g : X ⟶ Y} : f = g ↔ ⇑(hom f) = ⇑(hom g) :=
  ConcreteCategory.hom_ext_iff.trans DFunLike.coe_injective.eq_iff.symm

instance types.instFunLike {X Y : Type u} : FunLike (Types.Hom X Y) X Y where
  coe f := f.hom
  coe_injective' _ _ h := Types.Hom.ext h

/-- The category of types as a concrete category. -/
instance : ConcreteCategory (Type u) Types.Hom (fun X => X) where
  hom f := f
  ofHom f := f

@[simp] lemma hom_types_ofHom {α β : Type u} (f : α → β) :
    hom (types.ofHom f) = types.ofHom f := rfl

abbrev toHasForget : HasForget C where
  forget.obj := CC
  forget.map f := types.ofHom (hom f)
  forget_faithful.map_injective h := hom_injective <| by simpa using congr_arg hom h

end ConcreteCategory

section

open ConcreteCategory

variable (C)

/-- Build a coercion to functions out of `HasForget`.

The intended usecase is to provide a `FunLike` instance in `HasForget.toConcreteCategory`.
See that definition for the considerations in making this an instance.
-/
abbrev HasForget.toFunLike [HasForget C] (X Y : C) :
    FunLike (X ⟶ Y) ((forget C).obj X) ((forget C).obj Y) where
  coe f := (forget C).map f
  coe_injective' _ _ h := forget_faithful.map_injective (hom_ext (DFunLike.coe_injective h))

attribute [local instance] HasForget.toFunLike
/-- Build a concrete category out of `HasForget`.

The intended usecase is to prove theorems referencing only `(forget C)`
and not `(forget C).obj X` nor `(forget C).map f`: those should be written
as `CC X` and `ConcreteCategory.hom f` respectively.
-/
abbrev HasForget.toConcreteCategory [HasForget C] :
    ConcreteCategory C (· ⟶ ·) _ where
  hom f := f
  ofHom f := f
  id_apply := DFunLike.congr_fun ((forget C).map_id _)
  comp_apply _ _ := DFunLike.congr_fun ((forget C).map_comp _ _)

attribute [local instance] HasForget.toConcreteCategory

/-- Check that the new `ConcreteCategory` has the same forgetful functor as we started with. -/
example [inst : HasForget C] :
    @forget C _ ((HasForget.toConcreteCategory _).toHasForget) = @forget C _ inst := by
  with_reducible_and_instances rfl

/-- In particular, this should work for the category of types. -/
example :
    @forget Type _ ((HasForget.toConcreteCategory _).toHasForget) = @forget Type _ HasForget.types := by
  with_reducible_and_instances rfl -- Fails at `with_reducible`

/-- In addition, `forget Type` should be the identity functor. -/
example :
    @forget Type _ ((HasForget.toConcreteCategory _).toHasForget) = Functor.id _ := by
  with_reducible_and_instances rfl -- Fails at `with_reducible`

set_option allowUnsafeReducibility true
attribute [reducible] Quiver.Hom

-- But making `Quiver.Hom` reducible blows up everything, in particular instance synth.
example (X Y : Type) : FunLike (X ⟶ Y) ((forget Type).obj X) ((forget Type).obj Y) := by
  fail_if_success infer_instance
  exact types.instFunLike

end

[Anne Baanen]

Option 3 is to try replacing HasForget.toConcreteCategory with an instance specialized for Type. This has essentially the same issues as option 1 but additionally breaks the equality between forget and Functor.id.

import Mathlib.CategoryTheory.EpiMono
import Mathlib.CategoryTheory.Functor.FullyFaithful
import Mathlib.Data.Set.Operations
import Mathlib.Tactic.PPWithUniv

set_option autoImplicit false

namespace CategoryTheory

universe w w' v v' v'' u u' u''

/- The `@[to_additive]` attribute is just a hint that expressions involving this instance can
  still be additivized. -/
@[to_additive existing CategoryTheory.types]
instance types : LargeCategory (Type u) where
  Hom a b := a → b
  id _ := id
  comp f g := g ∘ f

theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
  rfl

-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10688): this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
-- because of its "if all else fails, apply all `ext` lemmas" policy,
-- which apparently we want to move away from.
@[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g := by
  funext x
  exact h x

/-- Class for categories `C` with a fixed faithful functor `forget : C ⥤ Type`.

This forgetful functor should not be used to cast objects or morphisms to
types or functions respectively: see `ConcreteCategory` for that.

Note that `HasForget` potentially depends on three independent universe levels,
* the universe level `w` appearing in `forget : C ⥤ Type w`
* the universe level `v` of the morphisms (i.e. we have a `Category.{v} C`)
* the universe level `u` of the objects (i.e `C : Type u`)
They are specified that order, to avoid unnecessary universe annotations.
-/
class HasForget (C : Type u) [Category.{v} C] where
  /-- We have a functor to Type -/
  protected forget : C ⥤ Type w
  /-- That functor is faithful -/
  [forget_faithful : forget.Faithful]

attribute [inline, reducible] HasForget.forget
attribute [instance] HasForget.forget_faithful

/-- The forgetful functor from a concrete category to `Type u`. -/
abbrev forget (C : Type u) [Category.{v} C] [HasForget.{w} C] : C ⥤ Type w :=
  HasForget.forget

-- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _`
@[instance] abbrev HasForget.types : HasForget.{u, u, u+1} (Type u) where
  forget := 𝟭 _

class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) (CC : outParam <| C → Type w)
    [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

export ConcreteCategory (id_apply comp_apply)

section

variable {C : Type u} [Category.{v} C] {F : C → C → Type*} {CC : C → Type w}
variable [∀ X Y, FunLike (F X Y) (CC X) (CC Y)]
variable [ConcreteCategory C F CC]

namespace ConcreteCategory

attribute [simp] id_apply comp_apply

/-- We can apply morphisms of concrete categories by first casting them down
to the base functions.
-/
instance {X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ CC X → CC Y) where
  coe f := hom f

lemma hom_injective {X Y : C} : Function.Injective (hom : (X ⟶ Y) → F X Y) :=
  Function.LeftInverse.injective ofHom_hom

@[ext] lemma hom_ext {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g :=
  hom_injective h

abbrev toHasForget : HasForget C where
  forget.obj := CC
  forget.map f := ⇑(hom f)
  forget_faithful.map_injective h := hom_injective (DFunLike.coe_injective h)

end ConcreteCategory

section

variable (C)

/-- Put a do-nothing `FunLike` structure on plain functions.

The intended usecase is to provide a `FunLike` instance in `types.toConcreteCategory`.
See that definition for the considerations in making this an instance.
-/
abbrev types.instFunLike (X Y : Type u) :
    FunLike (X → Y) X Y where
  coe f := f
  coe_injective' _ _ h := h

attribute [local instance] types.instFunLike

/-- A `ConcreteCategory` instance for the category of types.

This unfortunately causes defeq issues, since it puts a new `HasForget` instance on `Type`;
the `forget` functor should be reducibly defeq to that of `HasForget.types` but also both of these
should be reducibly defeq to the identity functor on `Type`; we have not figured out how to achieve
all conditions simultaneously.
-/
abbrev types.instConcreteCategory :
    ConcreteCategory (Type u) (· → ·) _ where
  hom f := f
  ofHom f := f
  id_apply _ := rfl
  comp_apply _ _ _ := rfl

attribute [local instance] types.instConcreteCategory

/-- The two ways to get a forgetful functor should be equal. -/
example :
    @forget Type _ types.instConcreteCategory.toHasForget = @forget Type _ HasForget.types := by
  rfl -- Even fails at `with_reducible_and_instances`.

/-- The concrete category should have the identity functor as the forgetful functor. -/
example :
    @forget Type _ types.instConcreteCategory.toHasForget = Functor.id _ := by
  rfl -- Even fails at `with_reducible_and_instances`.

/-- The `HasForget` instance should have the identity functor as the forgetful functor. -/
example : @forget Type _ HasForget.types = Functor.id _ := by
  with_reducible rfl

-- In addition to option 1, we also need `Functor.id` to be reducible.
set_option allowUnsafeReducibility true
attribute [reducible] DFunLike.coe ConcreteCategory.hom Functor.id

/-- The two ways to get a forgetful functor should be equal. -/
example :
    @forget Type _ types.instConcreteCategory.toHasForget = @forget Type _ HasForget.types := by
  with_reducible rfl

/-- The concrete category should have the identity functor as the forgetful functor. -/
example :
    @forget Type _ types.instConcreteCategory.toHasForget = Functor.id _ := by
  with_reducible rfl

/-- The `HasForget` instance should have the identity functor as the forgetful functor. -/
example : @forget Type _ HasForget.types = Functor.id _ := by
  with_reducible rfl

end

[Anne Baanen]

And finally my least favourite Option 4, we bundle HasForget into ConcreteCategory and get heterogeneous equalities everywhere.

import Mathlib.CategoryTheory.EpiMono
import Mathlib.CategoryTheory.Functor.FullyFaithful
import Mathlib.Data.Set.Operations
import Mathlib.Tactic.PPWithUniv

set_option autoImplicit false

namespace CategoryTheory

universe w w' v v' v'' u u' u''

/- The `@[to_additive]` attribute is just a hint that expressions involving this instance can
  still be additivized. -/
@[to_additive existing CategoryTheory.types]
instance types : LargeCategory (Type u) where
  Hom a b := a → b
  id _ := id
  comp f g := g ∘ f

theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
  rfl

-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10688): this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
-- because of its "if all else fails, apply all `ext` lemmas" policy,
-- which apparently we want to move away from.
@[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g := by
  funext x
  exact h x

/-- Class for categories `C` with a fixed faithful functor `forget : C ⥤ Type`.

This forgetful functor should not be used to cast objects or morphisms to
types or functions respectively: see `ConcreteCategory` for that.

Note that `HasForget` potentially depends on three independent universe levels,
* the universe level `w` appearing in `forget : C ⥤ Type w`
* the universe level `v` of the morphisms (i.e. we have a `Category.{v} C`)
* the universe level `u` of the objects (i.e `C : Type u`)
They are specified that order, to avoid unnecessary universe annotations.
-/
class HasForget (C : Type u) [Category.{v} C] where
  /-- We have a functor to Type -/
  protected forget : C ⥤ Type w
  /-- That functor is faithful -/
  [forget_faithful : forget.Faithful]

attribute [inline, reducible] HasForget.forget
attribute [instance] HasForget.forget_faithful

/-- The forgetful functor from a concrete category to `Type u`. -/
abbrev forget (C : Type u) [Category.{v} C] [HasForget.{w} C] : C ⥤ Type w :=
  HasForget.forget

-- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _`
@[instance] abbrev HasForget.types : HasForget.{u, u, u+1} (Type u) where
  forget := 𝟭 _

class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) (CC : outParam <| C → Type w)
    [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)
  (toHasForget : HasForget C) -- This could be an autoparam, but I don't want to bother with that.
  (forget_obj (X) : (toHasForget.forget).obj X = CC X)
  (forget_map {X Y} (f : X ⟶ Y) : HEq ((toHasForget.forget).map f) ⇑(hom f))

[Anne Baanen]

Those are all the options I could come up with. None of them look particularly appealing. Assuming there is no other option, I believe we should continue with what I had before yesterday. That is: manually enable HasForget.toConcreteCategory whenever we really need to treat Type as a concrete category (instead of a HasForget). Since the equalities still hold on the with_reducible_and_instances level, most tactics won't break, and the main breakage from adding this instance locally is that some instance searches will fail due to looking for the wrong forget.

[Matthew Ballard]

Can we enumerate precise goals for this project?

[Anne Baanen]

The issue I want to solve is that the current ConcreteCategory setup has two incompatible ways to talk about elements of a concrete category and mapping them. Namely, in the general way we have ConcreteCategory.hasCoeToSort and ConcreteCategory.instFunLike, while for a specific category such as CommRingCat we have CommRingCat.carrier and CommRingCat.Hom.hom.

For a very concrete example, how can we make the following compile?

import Mathlib.Algebra.Category.Ring.Basic
import Mathlib.CategoryTheory.Elementwise

lemma CommRingCat.inv_hom_apply {R S : CommRingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r := by
  simp only [CategoryTheory.Iso.hom_inv_id_apply]

[Matthew Ballard]

simprocs?

[Anne Baanen]

That could work, but then rw wouldn't. Although rw might be made to work using unification hints...

[Matthew Ballard]

Do we have precedent for simp only being ok while rw being not ok elsewhere?

[Christian Merten]

If we can't figure out a good principled solution, we could also write some meta program generating the specialized lemmas for RingCat, ModuleCat, etc.

[Anne Baanen]

(Sorry, mixed up hom_inv_id and inv_hom_id while copying files. Now the example above fails for the right reason.)

[Anne Baanen]

Another example, that I haven't been able to minimize, is that docs#TopCat.Presheaf.restrictOpenCommRingCat requires a type hint (C := CommRingCat) in its definition, since unification can't figure this out from the problem (forget ?C).obj X =?= CommRingCat.carrier X. (Again something that we might solve using unification hints.)

[Anne Baanen]

Unification hints seems to be able to solve the last example! #20075

[Anne Baanen]

Here’s an update on concrete categories. I am now confident that we can redesign the implementation so that the defeq issues with simp failing, and rws needing to be erws, can be drastically reduced. The branch#redesign-ConcreteCategory has seen quite a few experiments and I’ve settled on something we can implement.

My expertise in the end lies much more in the elaboration side of things than the categorical side of things. I tried to be as thorough as possible before committing to this. Still I probably have overlooked some difficulties. Feedback is always welcome!

The issues this redesign is trying to solve

Let's try and sum up what I want to do here. Concrete categories have the issue that we have several different ways to spell the same notion. Let R S : CommRingCat and f : R ⟶ S. Then we can write DFunLike.coe f.hom : R -> S using the FunLike machinery (and this will give us access to RingHomClass with map_mul, etc.), or we can write (forget CommRingCat).map f : R → S and plug into the categorical mechanisms. These are definitionally equal, but not reducibly so. The same holds for converting objects to types: Bundled.ɑ R versus (forget CommRingCat).obj R. Having non-reducibly defeq different ways to write the same thing means we end up with lots of erw in the library. And often if Lean sees DFunLike.coe f =?= (forget ?).map ? it can’t figure out which category we’re supposed to be working in.

We can’t fix this by changing the way we define the coercion from concrete categories to types: CoeFun and CoeSort instances can be inlined, but not if those instances are free variables. For example if we write variables [Category C] [ConcreteCategory C] (X : C), then the cast X : Type will not get unfolded.

What we can do instead is unbundle the carrier and FunLike from the concrete category, and that’s what the refactor does.

Declaring concrete categories

The new ConcreteCategory class will look like this:

class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) {CC : outParam <| C → Type w}
    [outParam <| ∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  /-- Convert a morphism of `C` to a bundled function. -/
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  /-- Convert a bundled function to a morphism of `C`. -/
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

This looks rather intimidating, but on the other hand, you should not need to interact with this complication in practical uses.

Declaring a ConcreteCategory instance needs changes, but nothing as complicated as the above. E.g. the minimal change for CommRingCat is to go from

instance : ConcreteCategory.{u} CommRingCat where
  forget :=
    { obj := fun R => R
      map := fun f => f.hom }
  forget_faithful := ⟨fun h => by ext x; simpa using congrFun h x⟩

to

instance : ConcreteCategory.{u} CommRingCat (fun (R S : CommRingCat) => R →+* S) where
  hom := Hom.hom
  ofHom := ofHom

As you can see, we now explicitly mention the type of bundled functions in ConcreteCategory. The carrier type can be unified from the FunLike instance. This should be enough to upgrade everything with minimal breakage.

To really make use of the generalisation brought by concrete categories, we need one step extra: make ConcreteCategory.hom and ConcreteCategory.ofHom the primary ways of converting between the bundled functions and the category morphisms. For CommRingCat, this means that Hom.hom and ofHom are declared as aliases for the ConcreteCategory declarations:

variable {R} in
/-- The type of morphisms in `CommRingCat`. -/
@[ext]
structure Hom (R S : CommRingCat) where
  private mk ::
  /-- The underlying ring hom. The preferred spelling is `f.hom`. -/
  hom' : R →+* S

instance : Category CommRingCat where
  Hom R S := Hom R S
  id R := ⟨RingHom.id R⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

instance : ConcreteCategory.{u} CommRingCat (fun R S => R →+* S) where
  hom := Hom.hom'
  ofHom f := ⟨f⟩

/-- The underlying ring hom. -/
abbrev Hom.hom {R S : CommRingCat.{u}} (f : Hom R S) :=
  ConcreteCategory.hom (C := CommRingCat) f

/-- Typecheck a `RingHom` as a morphism in `CommRingCat`. -/
abbrev ofHom {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : of R ⟶ of S :=
  ConcreteCategory.ofHom (C := CommRingCat) f

Now all the elementwise lemmas will apply automatically:

lemma inv_hom_apply {R S : CommRingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r := by simp

lemma hom_inv_apply {R S : CommRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s := by simp

Parametrizing over concrete categories

Taking a ConcreteCategory as a parameter is a bit more verbose now. You get variables lines like:

variable {C : Type u} [Category.{v} C] {FC : C → C → Type*} {CC : C → Type w}
variable [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
variable [ConcreteCategory C FC]

I tried looking for a way for variables? or similar metaprograms to generate this automatically, but it seems this is going to be a bit too complicated to make happen soon.

Once you have gotten through the variables lines, working with concrete categories should be a lot nicer. The carrier type of an object X is written ToType X, and the bundled function underlying a morphism f is called hom f (and we have a CoeFun instance so that f x gets turned into DFunLike.coe (hom f) x automatically). In exchange for those more complicated variable lines, you don’t need to add ConcreteCategory.instFunLike and ConcreteCategory.hasCoeToSort as local instances. And of course you don’t need to worry about casting back and forth across (forget _).map = DFunLike.coe _. You can still write forget C for the forgetful functor.

/-- The equivalence `ToType (∏ᶜ F) ≃ ∀ j, ToType F j` if `F : J → C` is a family of objects
in a concrete category `C`. -/
noncomputable def productEquiv : ToType (∏ᶜ F) ≃ ∀ j, ToType (F j) :=
  ((PreservesProduct.iso (forget C) F) ≪≫ (Types.productIso.{w, v}
    (fun j => ToType (F j)))).toEquiv

Forgetful functors

In order to reduce the impact of the change (and so we won’t have to make one PR fixing about a thousand files all at once), I want to keep around the current definition of ConcreteCategory. This will be renamed HasForget, to match the already existing HasForget₂. Then we can move over each ConcreteCategory instance one by one, and finally we can start replacing usage of HasForget in lemmas with ConcreteCategory. In the long term, we might still want to keep the HasForget class for cases that really do not fit the concrete category redesign. Such as Type (see below!)

While HasForget is around, there should be a new design rule: a result should be parametrized over HasForget if it only refers to forget itself, and use ConcreteCategory if it refers to (forget _).map (which should therefore be replaced with function coercion, using hom) or (forget _).obj (which should be replaced with ToType).

Type as concrete category

One issue is with the category of types: the objects and morphisms of Type are in fact already types and functions! So here we have to add a FunLike instance on functions themselves. This seems to have no structural issues, but right now a lot breaks locally. Namely: forget Type is assumed to be reducibly defeq to the identity map, and with the redesign of ConcreteCategory, this assumption needs to be fixed everywhere. We’ll have to keep the FunLike and ConcreteCategory instances on Type as local instances for now and fix this gradually.

In the meantime, while the identification forget Type = id remains true, we can work with Type as a ConcreteCategory by adding the instance locally. The errors caused by missing local instances are harder to understand compared to those by making forget Type = id non-reducible, so making Type a concrete category everywhere should be a longer term goal for the project.

BundledHom

The BundledHom class resembles the new ConcreteCategory quite closely. The main difference is that BundledHom is only for types bundled with a single typeclass argument, and ConcreteCategory uses FunLike, so it does not care so much about typeclasses. I had some trouble integrating the two. Since they are quite similar to decide how to transfer gracefully between the two. In the end the identification between the two costs quite a lot of headaches. So for now we can keep them living in their own separate worlds. Perhaps we can get away with removing BundledHom entirely later on.

Elementwise

I have a version of the @[elementwise] attribute that works with the new concrete category design. It works on all examples I encountered so far, but I might need some metaprogramming assistance to make it more robust.

Overall plan

This is how I see the refactor progressing:

• Make a PR renaming the existing ConcreteCategory to HasForget.
• Make a PR adding the new ConcreteCategory class.
• Implement @[elementwise] for the new ConcreteCategory.
• Upgrade HasForget instances to ConcreteCategory. Can be done alongside the Hom structure refactor.*
• Upgrade HasForget uses to ConcreteCategory.*
• Clean up forget Type = id issues.*
• Bugfixing and cleanup downstream.*

After the first few steps, the remainder marked with * can be done in parallel.

[Anne Baanen]

I am confident that this redesign can be made to work, and that this can be made to work without requiring so much effort that it's not worth it. But it can surely be optimized. So I would be very happy if you could check out branch#redesign-ConcreteCategory and play around with it, see what I missed! :)

[Matthew Ballard]

I think this is very well considered. Thanks for the hard work @Anne Baanen !

I don’t remember off the top of my head but does bare Type have a category instance?

[Anne Baanen]

Matthew Ballard said:

I don’t remember off the top of my head but does bare Type have a category instance?

It does: docs#CategoryTheory.types (with plain functions as the morphisms.)

[Matthew Ballard]

I would argue one shouldn’t do that to begin with

[Anne Baanen]

I did try a few alternatives. There should be no technical issue with hiding types and functions behind one-field structures, only refactoring a good chunk of the library which assumes them to be reducibly equal to the plain things.

[Matthew Ballard]

IRL, I don’t think Category when I see Type. I have to think “Type as a category”. So I don’t think we should ask Lean to do so either

[Yaël Dillies]

Does it really matter what the objects of the category of types are? I would think only the morphisms are relevant for defeq purposes

[Joël Riou]

We obviously need the category of sets (whether on Type u, or with a different name, like Sets.{u}). I think that a good test case about design decisions is the bunch of results we have about limits in common concrete categories (e.g. the fact that the forget functor to types commute with all limits).

[Anne Baanen]

I just finished going through and getting every Limits and Colimits file for concrete categories building. Some fixes were needed, but everything was very local. Lots of confusion between MonoidHom X Y and X --> Y, so we should probably do the Hom structure change for MonCat, Grp, etc. simultaneously with adding the new ConcreteCategory instance. Also a few proofs that used to be complicated and can be replaced with simp or aesop. Only docs#ModuleCat.restrictScalars is still very fragile and caused actual trouble.

[Kim Morrison]

Anne Baanen said:

Also a few proofs that used to be complicated and can be replaced with simp or aesop.

:tada:

[Anne Baanen]

I think it's time to get the first few PRs out!

• #20809 is the preparation PR renaming HasForget to ConcreteCategory

[Matthew Ballard]

Will merge soon unless there are objections.

[Anne Baanen]

• #20810 defines the new ConcreteCategory class

[Anne Baanen]

• #20811 adapts elementwise to generate the right form of lemmas when ConcreteCategory is in scope

This is only the first bit of adaptation we need for elementwise: later on when the amount of ConcreteCategory instances justifies it, it should add a ConcreteCategory instance to the context when none is found. (It currently adds a HasForget instance.)

[Anne Baanen]

And #20815 gives us a nontrivial ConcreteCategory instance!

I am having trouble with a timeout in docs#AlgebraicGeometry.SpecMapRestrictBasicOpenIso: the show statements are much slower than before. I could get rid of one, but don't know how to start with the other.

[Christian Merten]

rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra] gets rid of the show, but the timeout still happens.

[Jireh Loreaux]

@Anne Baanen I'm obviously late to the party, but let me ask what is a potentially very stupid question. ConcreteCategory now takes the type of bundled morphisms as an argument. Why does this same consideration not apply to the isomorphisms in the category? Should that type also be passed along with some fields dictating how they behave?

Obviously, this would mean that working with generic concrete categories gets even more verbose. I'd be happy to understand a reason why I'm and idiot and it's obviously not necessary.

[Anne Baanen]

It's a good question! I never really thought about it until you asked, in fact, since it didn't really come up. The reason we can get away with not considering Isos is that to apply an Iso, let's say e, we write e.hom or e.inv to first convert it to a morphism: it doesn't have its own FunLike instance, unlike the morphisms themselves.

[Anne Baanen]

I can see a place for something that could wrap all the Iso.toFooEquiv/FooEquiv.toIso conversion, which might be an upgraded ConcreteCategory class along the lines you're thinking of.

[Yury G. Kudryashov]

If you want to allow custom Isos, you need to include Isos into the signature of a Category instead of defining them as a pair of inverse Homs.

[Johan Commelin]

Agreed. But I also think we should not do that.

[Yury G. Kudryashov]

I don't use Mathlib category theory, so I have no opinion on whether we should do that.

[Anne Baanen]

I have now made PRs for RingCat, AlgebraCat and ModuleCat:

[Anne Baanen]

• #20815 implements a new ConcreteCategory instance for rings. A few fixes, typically old workarounds that got in the way. One timeout fixed by rewriting the proof.

[Anne Baanen]

• #21121 implements ConcreteCategory for AlgebraCat. No fixes at all needed, everything just works!

[Anne Baanen]

• #21125 implements ConcreteCategory for ModuleCat. It seems that docs#ModuleCat.restrictScalars and docs#PresheafOfModules do not like changes to the elaboration/defeq, so I had to come up with ugly workarounds. Anyone have ideas how to make a more principled fix?

[Anne Baanen]

#21192 refactors categories of groups: redo the objects as a custom structure, add a Hom structure, implement ConcreteCategory and rework the @[simp] set. (Still needs to be linted and benchmarked.)

[Anne Baanen]

Next up should be Mon (already got halfway before I realized that it would be easier to do Grp first, due to parent projections) and SemiGrp, then I want to try looking at some topological categories.

[Anne Baanen]

Fixed all the regressions in the MonCat refactor: #21222 should be ready to review!

[Anne Baanen]

Got topological spaces compiling just before the weekend: #21302. After a bit of struggle in the basic files, there were lots of places where it was very easy to find cleanup opportunities: 34 porting notes and 11 erws deleted. :octopus:

[Kim Morrison]

That's what we were hoping for!!

[Anne Baanen]

Quick refactor of MagmaCat and Semigrp while waiting for the TopCat benchmark results to come in: #21368

[Anne Baanen]

I'm happy with the topological spaces PR: #21302

[Anne Baanen]

Categories of orders: #21409

[Anne Baanen]

Depends on the previous one: a minimal cleanup of CompleteLattice, #21410

[Anne Baanen]

I think I am done with all the HasForget instances we have in the library! Lots of little PRs ready for review: https://github.com/leanprover-community/mathlib4/pulls?q=is%3Aopen+is%3Apr+author%3AVierkantor+label%3At-category-theory

[Andrew Yang]

I’ve been using mathlib with the new design and it is a lot smoother compared to what we had before. It’s great!
A feature request is that my infoview is now filled with ConcreteCategory.hom that made it less readable than before. Is there a good way to use some pretty printer magic to hide this?

[Yury G. Kudryashov]

Does it make sense to make it a coe?

[Kim Morrison]

Anne Baanen said:

I think I am done with all the HasForget instances we have in the library! Lots of little PRs ready for review: https://github.com/leanprover-community/mathlib4/pulls?q=is%3Aopen+is%3Apr+author%3AVierkantor+label%3At-category-theory

I've sent the ones without merge conflicts or awaiting-author to bors.

[Anne Baanen]

Andrew Yang said:

I’ve been using mathlib with the new design and it is a lot smoother compared to what we had before. It’s great!
A feature request is that my infoview is now filled with ConcreteCategory.hom that made it less readable than before. Is there a good way to use some pretty printer magic to hide this?

I'm very glad to hear it's working for you! I was expecting that the transition period would be more suffering because we now have even more ways that things would be mismatched :)

Making .hom a @[coe] sounds like a good idea, thanks for the suggestion!

[Anne Baanen]

I finished upgrading HasForget to ConcreteCategory for sheaves: #21575.

[Anne Baanen]

For the order instances PR: #21409, anything else I can do?

[Andrew Yang]

What’s the preferred way to apply results about concrete category to Type now?

[Anne Baanen]

Currently: if you get errors about a missing instance ConcreteCategory (Type _) _, then the magic line is:

attribute [local instance] Types.instFunLike Types.instConcreteCategory in
...

[Anne Baanen]

In the future I would like to promote these local instances to global instances but that took quite some fixes when I tested it before.

[Anne Baanen]

In particular, you might run into missing instances on the functor forget Type: this was previously reducibly defeq to the identity functor, so properties of the identity functor would apply to forget for free. Enabling Types.instConcreteCategory turns that into a reducible-with-instances defeq, and then they can't be found as easily.

The solution is to copy the id instance to forget, see e.g. the start of Limits.ConcreteCategory.Basic.

[Anne Baanen]

By the way, could I ask for a meta expert on #21729 to figure out if there isn't a better way to write this bit?