search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Implementation of Lax Slice bicategory #337

Closed maxsnew closed 2 years ago

maxsnew commented 2 years ago

The lax slice bicategory is like the slice category, but rather than a commuting triangle you get a 2-cell.

This is my first time using Agda in earnest so I am not very adept at using the module system, so some code review would help here for sure. I'm not really sure if I got the naming conventions right. I based most of the naming on the slice 1-category.

Some caveats

  1. I still have two spots of yellow in Emacs when I type check on Line 310. I'm not sure how to debug this.
  2. Type checking at least while it was incomplete became very slow. When I was working on the unitors I had to comment out the associator proofs to speed things up. Not sure what the best practice is for mitigating this. Should I break it up into multiple files? Maybe move the SliceHom module into a different file.
  3. The proofs sometimes had several lines in a row of associativity, is there a simpler way to do this? A reflective free category solver maybe?
  4. One proof (inverse of the right unitor) is a copy-paste-rename of the proof for the inverse of the left unitor. This should probably be a lemma instead.
maxsnew commented 2 years ago

Ok I think it's much better now. I did the following:

  1. Moved all the imports to the top
  2. Used explicit using for the top-level opens
  3. Lifted a lot of local functions to definitions and got rid of all the lets instead using wheres
  4. Used push/pull/center etc for the associativity arguments, which made the proofs much shorter.
  5. Made the naming of arguments consistent.
maxsnew commented 2 years ago

Sorry for all the commits, I intended to squash them when the review was done

JacquesCarette commented 2 years ago

Actually, I kind of like fine-grained commits.