Typeclass not triggering

Stream: general

[Adam Topaz]

I made a slight generalization to #6820 by assuming a slightly weaker condition on existence of (co)limits (this is so that we can define so-called "local" Kan extensions, as opposed to only global ones).

But there seem to be two places where typeclass inference doesn't work as expected. These are lines 195-197 and 217 in the following file:
https://github.com/leanprover-community/mathlib/blob/AT_kan_ext/src/category_theory/limits/kan_extension.lean

It's mostly an annoyance, but if anyone has any ideas on how to get these typeclasses to fire, that would be helpful.

Pinging: @Scott Morrison @Bhavik Mehta , since you've reviewed this PR :)

[Adam Topaz]

Somehow, the issue is only for Lan (which deals with colimits), whereas the case of Ran (which deals with limits) has no issues.

[Scott Morrison]

I'm not surprised it can't find the instances, because you've hidden things behind let (using change).

[Scott Morrison]

There's also the question of why you can't directly erw (as you do for Ran), without any let or change. I can't yet see what's going on, but I suspect it is some defeq abuse of either functor associativity, or costructured_arrow.map's 2-functoriality.

[Scott Morrison]

e.g. the fact you need a type annotation on line 179 is a bit of a warning flag. The fact you need a type annotation here is going to mean that sources and targets are not matching up (syntactically, even though they will defeq match), and this will break rw later. So perhaps we can work out an explicit isomorphism we can insert on line 179 instead of the type annotation?

[Scott Morrison]

Oh, maybe that type annotation is harmless. It is just coping with the fact that the S argument for costructured_arrow.map is implicit. That itself seems like a bad idea!

[Scott Morrison]

I would be typechecking by hand the right hand side:

colimit.ι (costructured_arrow.map (f ≫ g) ⋙ diagram ι F z) j ≫ colimit.pre (diagram ι F y) (costructured_arrow.map f) ≫ colimit.pre (diagram ι F z) (costructured_arrow.map g)

and seeing what has gone wrong there.

[Scott Morrison]

(Something is wrong, because erw [colimit.ι_pre_assoc], should work but doesn't...)

[Adam Topaz]

Okay, I understand what's happening now.
It's not an issue about the let ... in the proofs, but rather it's that these proofs "abuse" the fact that costructured_arrow.map f ⋙ diagram ι F x has the form diagram ι F y in the case where f : y ⟶ x.

I don't know how to work around this. I could add the following:

lemma has_colimit_diagram_map (F : S ⥤ D) (x y : L) (f : y ⟶ x) [has_colimit (diagram ι F y)] :
  has_colimit ((costructured_arrow.map f : costructured_arrow ι _ ⥤ _) ⋙ diagram ι F x) :=
by {change has_colimit (diagram ι F _), apply_instance}

lemma has_colimit_diagram_map_comp (F : S ⥤ D) (x y z : L) (f : y ⟶ x) (g : z ⟶ y)
  [has_colimit (diagram ι F z)] : has_colimit
  ((costructured_arrow.map g : costructured_arrow ι _ ⥤ _) ⋙
  costructured_arrow.map f ⋙ diagram ι F x) :=
by {change has_colimit (diagram ι F _), apply_instance}

lemma has_colimit_diagram_map_comp' (F : S ⥤ D) (x y z : L) (f : y ⟶ x) (g : z ⟶ y)
  [has_colimit (diagram ι F z)] : has_colimit
  (((costructured_arrow.map g : costructured_arrow ι _ ⥤ _) ⋙
  costructured_arrow.map f) ⋙ diagram ι F x) :=
by {change has_colimit (diagram ι F _), apply_instance}

local attribute [instance]
  has_colimit_diagram_map has_colimit_diagram_map_comp has_colimit_diagram_map_comp'

but this doesn't seem any better than just using haveI in the proofs themselves.