Skip to content

Porting note: instance was not necessary (category theory) #10670

Closed
Closed
Porting note: instance was not necessary (category theory)#10670
Labels
porting-notesMathlib3 to Mathlib4 porting notes.t-category-theoryCategory theory
@pitmonticone

Description

@pitmonticone
pitmonticone
opened on Feb 17, 2024

This issue is specifically for cases of this in the category theory library.

Examples

mathlib4/Mathlib/Algebra/Category/GroupCat/Basic.lean

Lines 62 to 65 in 5e53cc1

-- porting note: this instance was not necessary in mathlib
@[to_additive]
instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
coe (f : X →* Y) := f

mathlib4/Mathlib/Algebra/Category/GroupCat/Preadditive.lean

Lines 21 to 23 in 5e53cc1

-- porting note: this instance was not necessary in mathlib
instance (P Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q) :=
(inferInstance : AddCommGroup (AddMonoidHom P Q))

mathlib4/Mathlib/Algebra/Category/MonCat/Basic.lean

Lines 83 to 86 in 5e53cc1

-- porting note: this instance was not necessary in mathlib
@[to_additive]
instance {X Y : MonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
coe (f : X →* Y) := f

Metadata

Metadata

Assignees

No one assigned

    Labels

    porting-notesMathlib3 to Mathlib4 porting notes.t-category-theoryCategory theory

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions