<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    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. <br>
    <br>
    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?<br>
    <br>
    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).<br>
    <br>
    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<br>
    <a class="moz-txt-link-freetext" href="https://agda.github.io/agda-categories/Categories.Category.Core.html">https://agda.github.io/agda-categories/Categories.Category.Core.html</a><br>
    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?<br>
    <br>
    Nicolai<br>
    <br>
    <br>
    <div class="moz-cite-prefix">On 16/12/2020 16:20, Peter LeFanu
      Lumsdaine wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAAkwb-khw8jR-zUzG+kKeLt4uZZDW3=8A-vJenALRam8E=4Nrg@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div dir="ltr">On Wed, Dec 16, 2020 at 1:40 PM Thorsten
          Altenkirch <<a
            href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"
            moz-do-not-send="true">Thorsten.Altenkirch@nottingham.ac.uk</a>>
          wrote:<br>
          ><br>
          > But this is not the arrow category it is something else.<br>
          <br>
          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.
          <div><br>
            <div>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.
              <div><br>
              </div>
              <div>I gave the main details of this in my talk at the
                memorial conference for Erik Palmgren.<br>
                Slides: <a
href="http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf"
                  moz-do-not-send="true">http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf</a><br>
                Video: <a href="https://youtu.be/glC8tC7xdBY"
                  moz-do-not-send="true">https://youtu.be/glC8tC7xdBY</a>
                <div><br>
                </div>
                <div>
                  <div style="color:rgb(0,0,0)">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).</div>
                  <div style="color:rgb(0,0,0)"><br>
                  </div>
                  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”.</div>
                <div><br>
                </div>
                <div>–Peter.</div>
                <div><br>
                </div>
                <div><br>
                </div>
              </div>
            </div>
          </div>
        </div>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>