search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
26 stars 5 forks source link

Collect recent things in a PR to Cubical #16

Closed maxsnew closed 9 months ago

maxsnew commented 1 year ago

We should submit a PR to cubical soon to upstream some of our recent stuff. I talked to the cubical maintainers and they said it's probably best to add to this existing PR (https://github.com/agda/cubical/pull/988) and I'll do a code review with them at the end of this month.

  1. Category & Functor solvers and their corresponding free category/functor theorems
  2. Stuff from (https://github.com/maxsnew/multi-poly-cats/issues/8)
  3. Stuff from (https://github.com/maxsnew/multi-poly-cats/issues/7)
  4. And potentially we could flesh out the stuff in Cubical.Categories.Limits to prove some Isos/equivalences between the representability definition and the "elementary" definition.

Any other thoughts on what to include?

stschaef commented 1 year ago

1, 2, 3 are merged into main as of #19. These could be a reasonable chunk to PR into cubical, but I like the idea of expanding Limits to show the power of this via some concrete examples

Opening a new branch to handle the 4th point. Aiming for

  1. Equivalence of your CONE and Cubical's Cone. Likewise with the competing limit definitions.
  2. Then we show that if you have all limits (i.e. a param univ elt for the new definition of limit) you can extract a representing functor
  3. Instantiate 2 with some concrete examples like product/etc

I started on this today, and it feels like we did a lot of heavy lifting in Profunctor so I'm hoping by Monday I'll have all of the 4th bullet point. In case this proves problematic, would you rather PR the first few points into Cubical or block and wait for the limit examples?

maxsnew commented 1 year ago

Take a look at Cubical.Categories.Limits.BinProduct.More as the starting point for the product stuff. It should be straightforward to adapt to an Iso. I did it for BinProducts (plural) but we should probably do it for BinProduct (singular) as well. Since limits are all an example of adjoints you can use the RightAdjointAt for singluar and RightAdjoint for plural from Cubical.Categories.Adjoint.UniversalElements. See Cubical.Categories.Exponentials for an example.

maxsnew commented 1 year ago

Ok I did it for BinProduct (singular) and BinProduct with a fixed object. and just pushed.

maxsnew commented 1 year ago

We should revisit this after https://github.com/maxsnew/multi-poly-cats/issues/36 is implemented.