<div dir="ltr">Hi Nicolai, Jacques,<div><br></div><div>Thanks for the pointers! I have indeed already had to assume function extensionality. </div><div><br></div><div>So just to make sure I understand correctly, the reason that associativity is impossible to prove in the "wild categories" setting is that you not only need associativity in the original category, but also a sort of "second level" notion of associativity in the composition of the commutative diagrams? And the reason it goes through when you assume that hom-sets are sets is that any two commutative diagrams, as long as their components are the same, are now assumed to be identical. Is that right?</div><div><br></div><div>Then, is it possible to add this higher-dimensional coherence rather than removing higher-dimensional structure completely?</div><div><br></div><div>I think I'll try out the setoid approach Jacques suggested, it does seem like it could make things easier. Are there any major downsides to this approach which would be useful to know. I've heard of talk of "setoid hell" before where you build up a ton of extra proof obligations. Should I be worried about that in this case?</div><div><br></div><div>Lastly, how would you recommend defining hom/represented functors? Currently, I've used a universe category parametrized by some level 'c' whose objects are 'Set c'. Will I run into similar issues with "wildness" if I don't enforce that the objects in the category are sets?</div><div><br></div><div>Thanks again for the help.</div><div><br></div><div>Best,</div><div>Daniel</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Dec 14, 2020 at 7:22 PM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com">nicolai.kraus@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  
    
  
  <div>
    Hi Daniel,<br>
    <br>
    nice Agda project! But using the winter break to learn category
    theory, topology, HoTT, AND to formalise things in Agda sounds
    pretty ambitious to me ;-)<br>
    <br>
    The short answer to your question is "no". There's no nice way to do
    this without the assumption that hom-sets are sets (or another
    assumption). Actually, there is just no way at all, not even an ugly
    one. It's not just involved and tedious and hard to read, it's not
    provable. The comma category construction does not work for the
    notion of categories that you use.<br>
    <br>
    To see why, look at your Agda code:<br>
    When you define the objects of the comma category, you need to use
    objects + morphisms of the original categories.<br>
    When you define the morphisms of the comma category, you  need to
    use morphisms + composition of the original categories.<br>
    When you define composition in the comma category, you need
    composition + associativity of the original categories.<br>
    Do you see where this is going? You always need "one level more" of
    the original categories than you currently define in the comma
    category.<br>
    Thus, when you want to prove associativity for the comma category,
    you should expect that you need more than only associativity of the
    original categories: you also need the first coherence condition for
    associativity, known as "MacLane's pentagon". MacLane's pentagon
    doesn't show up explicitly for standard categories (where it is
    automatic), but it shows up when you study e.g. bicategories.
    Something similar happens for the identity laws.<br>
    <br>
    The notion of categories that you currently consider is badly
    behaved. We call them "wild categories" (or "naive" or "incoherent"
    or "approximate"). They are higher-dimensional categories, but with
    almost all coherence structure removed. To understand why this is
    bad, think about categories where you don't require composition to
    be associative: you can probably imagine that all sorts of
    constructions from standard category theory will break.<br>
    <br>
    Your approach to require hom-sets to be sets is the standard
    approach. It ensures that the categories behave like standard
    1-categories. It implies MacLane's pentagon coherence and all other
    coherences. Thus, it's a really strong assumption, but it's the
    right assumption if you want to do 1-category theory in this style.
    This is also how it's done in the HoTT book. I think this is
    equivalent to Jacques' approach with setoids, but I haven't checked
    this in detail. ("Equivalent" in the sense that the two approaches
    should make the same constructions possible, not equivalent in terms
    of how tedious things can become.)<br>
    <br>
    "--with-K" would, of course, imply that hom-sets are sets. But it
    also would mean that the type of objects (and everything else) is a
    set. This is quite restrictive. For example, your development
    wouldn't capture univalent categories. I don't know whether the
    added convenience would make up for the loss of generality.<br>
    <br>
    The issue that you found here is a pretty deep one. This issue,
    together with things that are very much related, causes the problem
    and motivates the constructions in this paper:<br>
    <a href="https://arxiv.org/abs/2009.01883" target="_blank">https://arxiv.org/abs/2009.01883</a><br>
    See also Section 3.2, "Deficiency of Wild/Incoherent Structure", for
    a discussion. Especially Example 9, which uses a slice category
    (special case of the comma category, where one can already see the
    issues).<br>
    <br>
    Best,<br>
    Nicolai<br>
    <br>
    <br>
    <div>On 15/12/2020 01:40, Daniel Lee wrote:<br>
    </div>
    <blockquote type="cite">
      
      <div dir="ltr">Hi everyone,
        <div><br>
        </div>
        <div>I'm an undergraduate in CS, trying to use this winter break
          to learn category theory via Categories in Context (and
          hopefully topology and HoTT). I thought it would be cool to
          formalize in Agda at the same time. </div>
        <div><br>
        </div>
        <div>
          <div><font face="arial, sans-serif">Here's the link to the
              Agda development for reference: </font><a href="https://github.com/dan-iel-lee/categories-in-agda" target="_blank">https://github.com/dan-iel-lee/categories-in-agda</a>
            . Relevant files are probably "Core" and "Examples/Comma".</div>
        </div>
        <div><br>
        </div>
        <div><br>
        </div>
        <div>I've run into a roadblock, specifically with proving that
          the comma category is a category, but which I imagine could be
          an issue in the future as well.</div>
        <div><br>
        </div>
        <div>I've defined the arrows in the category as:</div>
        <div><font face="monospace">Σ[ (h , k) ∈ d ⟶ᴰ d' × e ⟶ᴱ e' ] f'
            ∘ (ℱ h) ≡ (𝒢 k) ∘ f</font></div>
        <div><font face="monospace"><br>
          </font></div>
        <div><font face="arial, sans-serif">Where h and k are the
            component arrows, and the body of the Sigma is the
            commutativity condition. Defining composition and identity
            are relatively straightforward, but proving the left/right
            unit and associativity properties become difficult
            because it requires proving that the identities are
            identified. And because there are a lot of steps,
            compositions,... involved, the Goal is super hard to read
            and I don't know where to start in trying to prove it. I
            managed to work around it by enforcing that all the hom-sets
            are sets (in the sense that their identification types are
            all identical). Is there a nice way to prove this without
            using proof irrelevance though?</font></div>
        <div><font face="arial, sans-serif"><br>
          </font></div>
        <div><font face="arial, sans-serif">All help is very very
            appreciated. Thanks :)))</font></div>
        <div><font face="arial, sans-serif"><br>
          </font></div>
        <div><font face="arial, sans-serif">Best,</font></div>
        <div><font face="arial, sans-serif">Daniel</font></div>
      </div>
      <br>
      <fieldset></fieldset>
      <pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </div>

</blockquote></div>