You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jacques Carette (Jul 21 2023 at 13:36):I'm looking for formalization (i.e. inside proof assistants) of double categories. I want to contrast them to the one in agda-categories (which is idiosyncratic, but for good reasons). Googling around doesn't lead anywhere.
I am particularly very interested in highly universe polymorphic versions (which sadly seems to rule out the 'slick' definitions so dear to category theorists).
Max New (Jul 21 2023 at 17:34):I have a student that defined a "locally thin" version in cubical, i.e., where there is at most one square for any frame. The repo isn't public. It's maximally universe polymorphic, and looking at agda-categories it looks pretty much exactly the same modulo the thinness and we don't use setoids
Bryce Clarke (Jul 21 2023 at 19:01):I know that Nicolas Behr is looking to formalise double categories in Coq as part of CoREACT project he is leading.
Jacques Carette (Jul 21 2023 at 19:47):@Max New My main "innovation" there is to say "the heck with lists and natural numbers" and use types as indices, and then make explicit the necessary equivalence proofs (which are mighty obscure over List/Nat). I was wondering if I could indeed claim credit for that observation.
Jacques Carette (Jul 21 2023 at 19:48):Thanks for the pointer @Bryce Clarke but my feeling is that Coq people don't worry much about universe polymorphism.
Max New (Jul 21 2023 at 20:11):Where do Lists/Nats come in with double categories?
Jacques Carette (Jul 21 2023 at 20:34):D'oh!! I was mixing multi-categories with double categories!!!!
Jacques Carette (Jul 21 2023 at 20:35):With double categories, the issue is that the normal definition uses too much strictness, and we had to insert explicit coherences to make things match up.