PR !4#15055: feat: the category of pointed objects of a c...

Stream: triage

[Random Issue Bot]

Today I chose PR #15055 for discussion!

feat: the category of pointed objects of a concrete category
Created by @Sina Hazratpour (@sinhp) on 2024-07-23
Labels: awaiting-author, t-category-theory

Is this PR still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose PR #15055 for discussion!

feat: the category of pointed objects of a concrete category
Created by @Sina Hazratpour (@sinhp) on 2024-07-23
Labels: awaiting-author, merge-conflict, t-category-theory

Is this PR still relevant? Any recent updates? Anyone making progress?

[Sina Hazratpour]

@Anne Baanen You've been working on concrete categories after this PR was committed. I wonder what you think about this. Do you think the content of this PR is now covered elsewhere and not of use anymore, or do you think it would be worth ironing out the last bits of this PR for adding this to mathlib?

[Anne Baanen]

Hi! I only really worked on refactoring existing definitions in concrete categories and have not added any new work. So I am not very qualified for reviewing your PR. Maybe you can ask @Dagur Asgeirsson or @Christian Merten? Neither is subscribed to this channel, however, so I suppose you would have to send a direct message.