Zulip Chat Archive

Stream: general

Topic: Typeclass not triggering


view this post on Zulip Adam Topaz (Mar 31 2021 at 02:28):

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 :)

view this post on Zulip Adam Topaz (Mar 31 2021 at 02:28):

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

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:17):

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

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:21):

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.

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:23):

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?

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:27):

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!

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:29):

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.

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:29):

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

view this post on Zulip Adam Topaz (Mar 31 2021 at 18:40):

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.


Last updated: May 07 2021 at 00:30 UTC