agda-categories
agda-categories copied to clipboard
agda
FinSetoids is Cartesian
This is a WIP because:
- [x] I want to implement Cocartesian also
- [ ] I want to look into doing something with ObjectRestriction to make this work a little more general
I wonder if there might be an opportunity for proving a theorem of the sort "if category X has property P, then sub-category Y of X (as witnesses by relation R) also has property P if P and R are related in way Z". As sort of "R preserves P".
Is this what you meant by part 2 of the TODO?
I wonder if there might be an opportunity for proving a theorem of the sort "if category X has property P, then sub-category Y of X (as witnesses by relation R) also has property P if P and R are related in way Z". As sort of "R preserves P".
Is this what you meant by part 2 of the TODO?
Yeah, that's exactly what I meant by part 2.
The main thing stopping me from working on this PR is that I don't know where to put the tools for constructing terminal objects and binary products and things like that for object restrictions of categories. Any suggestions? I was thinking something like Categories.Category.Construction.ObjectRestriction.Properties.Terminal etc but I'm not satisfied by that
Why not put them directly in Categories.Category.Construction.ObjectRestriction.Properties ? Only if that grows very large would it need to be split (probably as you propose).
It might well be that some of the actual constructions should go elsewhere, and then just 'assembled' in the above?
@Taneb It would be really nice to get this finished and merged in. What can I do to help?
@JacquesCarette thanks for reminding me that this PR exists! I need to take another look at it to refamiliarise myself, it's been a while