[Agda] Tips for working around proof relevance

James Wood james.wood.100 at strath.ac.uk
Wed Dec 16 13:34:53 CET 2020


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


More information about the Agda mailing list