Dealing with multiple instances on a single type

Stream: mathlib4

[Robin Carlier]

Following a suggestion in one of my PR’s (#8013), I’m trying to play with categories freely generated by a Quiver. They are built in the file Mathlib/CategoryTheory/PathCategory.lean and as far as I understand, the idea is to change the Quiver instance on the type from the original one to the one defined by Quiver.Path, and using the composition of Paths there.

This results in a type having multiple Quiver instances at the same time, and looks like the elaborator really doesn’t like this. Here’s a short example

import Mathlib.CategoryTheory.PathCategory

namespace CategoryTheory

inductive foo : Type where
  | a
  | b
  | c

namespace foo

inductive Hom : foo → foo → Type where
  | f : Hom a b
  | g : Hom b c

instance Q: Quiver foo where
  Hom := Hom

def C := Paths foo
instance : SmallCategory C := Paths.categoryPaths foo

#check (@Quiver.Hom.toPath foo _ _ _ Hom.f)
#check (@Quiver.Hom.toPath foo _ _ _ Hom.f : (a : Paths foo) ⟶  (b : Paths foo)) -- Error
#check (@Quiver.Hom.toPath foo _ _ _ Hom.f) ≫ (@Quiver.Hom.toPath foo _ _ _ Hom.g) -- Error here

lemma bar :
    (@Quiver.Hom.toPath foo _ _ _ Hom.f) ≫  (@Quiver.Hom.toPath foo _ _ _ Hom.g) =
      Quiver.Path.cons (@Quiver.Hom.toPath foo _ _ _ Hom.f) Hom.g := by
  sorry

end foo

Ideally, I would like to be able to use the notations ⟶ and ≫ in a transparent way on stuff of the form _.toPath, but it looks like lean want me to give the explicit quiver structure at every step. Is it doomed?

[Kyle Miller]

@Robin Carlier It looks like the key part of the Paths API is docs#CategoryTheory.Paths.of, which you can use to convert objects to the Paths category and turn morphisms into length-1 paths. (Note that having multiple instances on the same type is fine if you use a type synonym like docs#CategoryTheory.Paths, since this is a non-@[reducible]/abbrev definition, so typeclass inference sees it as being a different type.)

Something that you need to make this convenient is a function to convert from your Hom to the -->. I added this as the abbrev Hom.toHom.

Also, something to be aware of is that there's a difference between Paths.of.map Hom.f.toHom and Hom.f.toHom.toPath. They might be defeq, but the first is syntactically a morphism in the path category, and the second is a Quiver.Path.

import Mathlib.CategoryTheory.PathCategory

namespace CategoryTheory

inductive foo : Type where
  | a
  | b
  | c

namespace foo

inductive Hom : foo → foo → Type where
  | f : Hom a b
  | g : Hom b c

instance Q : Quiver foo where
  Hom := Hom

abbrev Hom.toHom {x y : foo} (a : Hom x y) : x ⟶ y := a

#check Paths.of.map Hom.f.toHom
#check (Paths.of.map Hom.f.toHom : Paths.of.obj a ⟶ Paths.of.obj b)
#check Paths.of.map Hom.f.toHom ≫ Paths.of.map Hom.g.toHom

lemma bar :
    Paths.of.map Hom.f.toHom ≫ Paths.of.map Hom.g.toHom =
      Quiver.Path.cons Hom.f.toHom.toPath Hom.g.toHom := by
  rfl

end foo

[Kyle Miller]

The errors you were seeing mostly had to do with the elaborator not seeing things in the syntactic forms they're supposed to have to get different instances to be found. For example, (a : Paths foo) isn't enough to get a to be an object in Paths foo. All this does is have Lean check that a could be, but a remains having type foo. This is the purpose of using Paths.of.obj directly; it inserts the necessary retyping.

Also, just so you know, you don't need to create instances yourself. This pattern

def C := Paths foo
instance : SmallCategory C := Paths.categoryPaths foo

is for creating a new type without any instances and then copying over an instance (instance : SmallCategory C := inferInstanceAs <| SmallCategory (Paths foo) is the same but a bit nicer because it doesn't name the instance). If you did

abbrev C := Paths foo

then C would have all the instances on Paths foo.

[Robin Carlier]

Kyle Miller said:

Robin Carlier It looks like the key part of the Paths API is docs#CategoryTheory.Paths.of, which you can use to convert objects to the Paths category and turn morphisms into length-1 paths. (Note that having multiple instances on the same type is fine if you use a type synonym like docs#CategoryTheory.Paths, since this is a non-@[reducible]/abbrev definition, so typeclass inference sees it as being a different type.)

Something that you need to make this convenient is a function to convert from your Hom to the -->. I added this as the abbrev Hom.toHom.

Also, something to be aware of is that there's a difference between Paths.of.map Hom.f.toHom and Hom.f.toHom.toPath. They might be defeq, but the first is syntactically a morphism in the path category, and the second is a Quiver.Path.

import Mathlib.CategoryTheory.PathCategory

namespace CategoryTheory

inductive foo : Type where
  | a
  | b
  | c

namespace foo

inductive Hom : foo → foo → Type where
  | f : Hom a b
  | g : Hom b c

instance Q : Quiver foo where
  Hom := Hom

abbrev Hom.toHom {x y : foo} (a : Hom x y) : x ⟶ y := a

#check Paths.of.map Hom.f.toHom
#check (Paths.of.map Hom.f.toHom : Paths.of.obj a ⟶ Paths.of.obj b)
#check Paths.of.map Hom.f.toHom ≫ Paths.of.map Hom.g.toHom

lemma bar :
    Paths.of.map Hom.f.toHom ≫ Paths.of.map Hom.g.toHom =
      Quiver.Path.cons Hom.f.toHom.toPath Hom.g.toHom := by
  rfl

end foo

Thank you a lot for pointing out that Paths.of is a thing and for the detailed explanations of how things work, this is really instructive!