[Agda] Tips for working around proof relevance

[Nicolai Kraus]

Peter, thanks a lot for explaining this [again]! It's a really 
interesting observation that setoid-categories are a "maximally 
unsaturated" version of 1-categories.

What is unfortunate is that such unsaturated notions are very 
representation-dependent. Different choices of representation, which 
would lead to equivalent saturated definitions, give non-equivalent 
unsaturated definitions. Do you have intuition for which choices lead to 
well-behaved structures? Or is this just a matter of trying it out?

My impression is that, in order to get well-behaved structures, we 
either want no redundancy at all *or* as much redundancy, and thus 
"leeway", as possible. Here, I mean "redundancy" in the sense of 
"missing conditions on which components should be identified". 
Intuition: If we do a construction and all the input is perfect, then we 
hopefully can expect the result to be perfect, so the construction 
works. Or, if the input doesn't satisfy any conditions, but we also 
don't require the output to satisfy any conditions, then the 
construction also works. But if the input is "partially ok" and the 
output is required to be "partially ok", then the risk is that the wrong 
part of the output will be "partially ok". This is similar to what you 
said about saturation (and probably something similar can be said about 
strictness).

Univalent categories have no redundancy, and the agda-categories library 
includes a lot of redundancy. What if we remove some redundancy from 
agda-categories? If, for example, we remove `sym-assoc` in
https://agda.github.io/agda-categories/Categories.Category.Core.html
and replace all occurrences by what we get from `assoc` and the witness 
of `IsEquivalence (_≈_)`? This would cause more work in some places 
(judging by the comment on why `sym-assoc` was included), but could all 
constructions still be fixed? I would expect they can, but I don't think 
it's a priori clear. Jacques, did you find that some redundancy is 
really required rather than just convenient in the implementation?

Nicolai


On 16/12/2020 16:20, Peter LeFanu Lumsdaine wrote:
> On Wed, Dec 16, 2020 at 1:40 PM Thorsten Altenkirch 
> <Thorsten.Altenkirch at nottingham.ac.uk 
> <mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:
> >
> > But this is not the arrow category it is something else.
>
> No, that construction really is the arrow category (when one is taking 
> “category” = “category with hom-setoids”), and behaves in all the ways 
> you expect the construction to behave!  It’s not “forgetting” the 
> setoid-equalities on arrows — those are still there, just as 
> isomorphisms in the category — so it doesn’t mean you need to make 
> objects a setoid as well, or anything like that.
>
> Following the HoTT/univalent analysis of category theory, one can see 
> that setoid-based categories fit very naturally into the hierarchy of 
> notions of “(n-)category” with varying levels of “saturation”.  Just 
> like “precategories” (e.g. categories in classical foundations) don’t 
> assume saturation/univalence at the object level, if you relax 
> saturation at the levels of arrows/equalities as well, then you get 
> categories with hom-setoids.
>
> I gave the main details of this in my talk at the memorial conference 
> for Erik Palmgren.
> Slides: 
> http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf
> Video: https://youtu.be/glC8tC7xdBY
>
> Category theory seems to develop well as long as your saturation 
> assumption is of the form “saturated in levels ≥n” for some n. 
>  “Univalent categories” = “saturated in levels ≥0”; “precategories“ = 
> “saturated in levels ≥1”; “setoid-categories” = “not saturated at all” 
> — all of these give a good development of category theory.  “Wild 
> categories” are badly behaved exactly because when you view them in 
> this analysis, they assume “saturation of arrows” (1-saturation) but 
> NOT “saturation of 2-cells” (2-saturation, which turns out to be the 
> condition that equality on arrows is propositional).
>
> There are certainly reasons (theoretical and practical) to prefer the 
> non-setoid versions for many purposes — just as there are purposes for 
> which the setoid versions are good — and also just like how there are 
> advantages and disadvantages to always requiring saturation at the 
> object level.  But these are all natural parts of the same 
> mathematical picture — it certainly isn’t a matter of “the right 
> mathematical way” vs “nasty hacks” or “assembly language”.
>
> –Peter.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201219/559ac193/attachment.html>