search

maxsnew / cubical-categorical-logic

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

Adjoints #18

Closed maxsnew closed 5 months ago

maxsnew commented 1 year ago

Once https://github.com/maxsnew/multi-poly-cats/issues/7 is done, there are several applications to adjunctions that are more or less immediate:

  1. In Cubical.Categories.Adjoint They give two definitions of adjoint functors (unit/counit and hom-bijection) and construct functions back and forth between them (no proof of Iso). The hom-bijection one should be fairly easy to show is Iso to a formulation using profunctors because it essentially is in terms of profunctors.
  2. Then we can define the "universal element" definitions of left and right adjoints (i.e., given one functor F a right adjoint a functor representing Hom(F-,=). And it should follow by stuff we already have that this is Iso to the hom-bijection definition.
  3. I think actually proving the iso between unit/counit and hom-bijection doesn't directly follow from what we've done so far but we should be able to reuse most of the functions we have right? Maybe there's a variant of the Yoneda lemma we can extract that is the kernel of the argument?
maxsnew commented 1 year ago

But we probably shouldn't bother with (3) before the pr. I've already done (2) so (1) is all that's left

GenericMonkey commented 1 year ago

Regarding 1 -- when you say "is Iso to a formulation using profunctors" -- is this the definition in Categories/Adjoint/UniversalElements.agda? I also found this definition on nlab -- is this a good place to wrap my head around the definition there?

Sorry, missed your comment until I refreshed the page. Looks like whats left is an Iso between the definition you provided and the one in Adjoints.agda?

Also, were you looking at this issue or is this something I can pick up? I was between doing this and taking a look at the Grothendieck construction.

maxsnew commented 8 months ago

Removing this from the milestone as we don't really need it for anything, we just use the formulation of adjoints in terms of representables