Zulip Chat Archive
Stream: condensed mathematics
Topic: identity functor is additive
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))) }
Eric Wieser (Mar 19 2021 at 14:45):
Does that work with rfl
in place of eq.refl _
?
Johan Commelin (Mar 19 2021 at 14:49):
yeah, it can be golfed into oblivion (-;
Last updated: Dec 20 2023 at 11:08 UTC