identity functor is additive

Stream: condensed mathematics

[Johan Commelin]

@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))) }

[Eric Wieser]

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

[Johan Commelin]

yeah, it can be golfed into oblivion (-;