Right adjoint to Functor.Slice.Free

agda / agda-categories

A new Categories library for Agda

https://agda.github.io/agda-categories

MIT License

359 stars 67 forks source link

Right adjoint to Functor.Slice.Free #408

Open Taneb opened 6 months ago

Taneb commented 6 months ago

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 commented 6 months ago

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 commented 5 months ago

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 commented 2 months ago

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

JacquesCarette commented 2 months ago

Anything I could do to help?

Taneb commented 2 months ago

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?