Zulip Chat Archive

Stream: general

Topic: implicit argument agony


Scott Morrison (Apr 01 2019 at 08:41):

I would like to write

@[simp] lemma map_id (F : (C × D) ⥤ E) (X : C) (Y : D) :
  F.map (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y)) :=
F.map_id (X, Y)

(complete context here), but I get an error message

type mismatch at application
  prod.mk (𝟙 X)
term
  𝟙 X
has type
  X ⟶ X
but is expected to have type
  ?m_1.fst ⟶ ?m_1.fstLean

and so have to write the rather unpleasant

@[simp] lemma map_id (F : (C × D) ⥤ E) (X : C) (Y : D) :
  @category_theory.functor.map _ _ _ _ F (X, Y) (X, Y) (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y)) :=
F.map_id (X, Y)

Anyone have ideas to help the elaborator along, here?

Kenny Lau (Apr 01 2019 at 08:43):

(term : type)

Scott Morrison (Apr 01 2019 at 08:50):

I've tried that, but can't get anything to work. Did you have a specific suggestion?

Kenny Lau (Apr 01 2019 at 08:53):

no, sorry

Chris Hughes (Apr 01 2019 at 09:21):

@[simp] lemma map_id (F : (C × D)  E) (X : C) (Y : D) :
  F.map ((𝟙 X, 𝟙 Y) : (X, Y)  (X, Y)) = 𝟙 (F.obj (X, Y)) :=
F.map_id (X, Y)

Scott Morrison (Apr 01 2019 at 09:59):

Thank you. :-) I should have managed that one...


Last updated: Dec 20 2023 at 11:08 UTC