Zulip Chat Archive

Stream: condensed mathematics

Topic: identity functor is additive


view this post on Zulip Johan Commelin (Mar 19 2021 at 14:39):

@Scott Morrison thanks for library_search!! It auto-generated

instance id.additive : (𝟭 C).additive :=
{ map_zero' := id (λ (X Y : C), eq.refl ((𝟭 C).map 0)),
  map_add' := id (λ (X Y : C) (f g : X  Y), eq.refl ((𝟭 C).map (f + g))) }

view this post on Zulip Eric Wieser (Mar 19 2021 at 14:45):

Does that work with rfl in place of eq.refl _?

view this post on Zulip Johan Commelin (Mar 19 2021 at 14:49):

yeah, it can be golfed into oblivion (-;


Last updated: May 09 2021 at 22:13 UTC