[Agda] Tips for working around proof relevance
Thorsten Altenkirch
Thorsten.Altenkirch at nottingham.ac.uk
Wed Dec 16 13:40:07 CET 2020
But this is not the arrow category it is something else.
If you want to implement category theory you need to work with a type theory with a reasonable notion of equality. Setoids are a bad idea because you never hide implementation details. You also want to be able to transport properties among equal elements.
The message is simple: don't program in assembly language.
Thorsten
On 16/12/2020, 12:35, "Agda on behalf of James Wood" <agda-bounces at lists.chalmers.se on behalf of james.wood.100 at strath.ac.uk> wrote:
On 16/12/2020 07:36, Thorsten Altenkirch wrote:
> But then how do you construct the arrow category?
The canonical answer to questions like this is to look in
agda-categories, and see what it does.
In this case
(https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Construction/Arrow.agda),
it looks like when we make the type of objects of the arrow category, we
just forget the equivalence relation on the hom-setoid. Objects of the
arrow category (A, B, f) and (A, B, f′) where f ≈ f′ are isomorphic,
which should be good enough because we never talk about equality on
objects. The answer to the original question about comma categories
should be very similar.
Best regards,
James
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
More information about the Agda
mailing list