agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard
verified publisher icon agda

Right adjoint to Functor.Slice.Free

Open Taneb opened this issue 2 years ago • 6 comments

Supercedes #370

I started over with a better understanding of the problem space, on top of the cleaned up version of the module. Also, I'm making this branch in the agda repo rather than my own fork so it's easier for other contributors to make commits.

  • [X] Functor
  • [x] Adjoint
  • [ ] Corresponding functor and adjoint for base changes

Even with what I have so far there's a lot of potential for simplifying the proofs.

An insight I've had is that the proof passed in to universal constructions (and other ways to construct a morphism or object from a proof) should generally be abstract. for compilation times. Other proofs don't matter nearly as much in this respect. This is because we generally have many many copies of the morphism term in other terms and types.

Taneb avatar Jan 10 '24 07:01 Taneb

This isn't complete but it's at a point where I'd like some other eyes on it if anyone wants to take a look

Taneb avatar Jan 10 '24 13:01 Taneb

Looks like I've broken Categories.Category.CartesianClosed.Locally.Properties, a module which I had honestly forgotten about, but I think I should be able to entirely replace that with Categories.Functor.Slice.BaseChange, with an actual proof of adjointness soon. It's making me wonder if there's a simpler implementation of InternalSections, though

Taneb avatar Jan 27 '24 20:01 Taneb

I'd like to finish this off... but I've gotten lost with what was going on with it :(

Taneb avatar May 15 '24 17:05 Taneb

Anything I could do to help?

JacquesCarette avatar May 15 '24 18:05 JacquesCarette

Remaining considerations:

  • Define the next base change functor (composition of slice⇒slice-slice and InternalSections)
  • Define the base change adunction
  • Can the proofs be simplified? They're huge and scary
  • Can the environment of InternalSections be simplified? We don't need all products
  • Is BaseChange⁎ in Categories.Category.CartesianClosed.Locally the same thing as what we're defining in this PR? Is it a viable way to simplify the definitions?

Taneb avatar May 15 '24 20:05 Taneb

I'm not happy with this and I don't think I'm going to become happy with this from where it is now. I'm going to try and take out some small nice stuff, get that merged, and then consider what I want to do for this

Taneb avatar Oct 24 '24 13:10 Taneb