Cleaning up Slice Functor and surrounding infrastructure

[JacquesCarette]

• split off the adjunction into Adjunction.Instance.BaseChange
• make the code less brute force, to hopefully be more revealing as to what is going on
• clean up imports

[Taneb]

I've been looking at this file again a bit. We can define BaseChange! in terms of Forgetful (in the Slice A category) and Categories.Category.Slice.Properties.slice⇒slice-slice, and we can define BaseChange* similarly in terms of Free and slice-slice≃slice. We can build the adjunction between them out of smaller pieces in this case. This even seems to load pretty quick.

It would need some rearrangement, though: because we're using Forgetful and Free in the Slice A category rather than in C they can't both live under the C module parameter

[JacquesCarette]

Thanks for looking. Think you can push this to the finish line? I'm unlikely to do so for the next 3 months - my term is crazy-busy.

[Taneb]

I can certainly give it a go. By the way, do you or @HuStmpHrrr know where the names of BaseChange! and BaseChange* come from? The papers I'm trying to translate to Agda (e.g. Polynomial Functors and Polynomial Monads call them ∆ and Σ

[sstucki]

do you or @HuStmpHrrr know where the names of BaseChange! and BaseChange* come from? The papers I'm trying to translate to Agda (e.g. Polynomial Functors and Polynomial Monads call them ∆ and Σ

I think ^* and _! are the standard symbols for denoting different base change functors. The name Σ for _! probably comes from the connection to disjoint unions or dependent sums in type theory: e.g. in a locally cartesian closed category, which is a model of dependent type theory, _! models such sum types. I think ∆ may be a reference to the "diagonal", since it gives you (projections out of) products A x B when you apply it to morphisms into the terminal object, but I'm not sure (type-theoretically, it corresponds to weakening substitution, IIRC).

[HuStmpHrrr]

Sandro's answer is very much accurate.

[Taneb]

I want to look closer at pullback-functorial. I don't understand where it comes from and how it relates to other functors. It can likely be improved.

I also want to rename Free, if I can find a satisfying name for it.

[JacquesCarette]

So I can't officially review, since strictly speaking, this PR is under my name - but @Taneb can review it. I'm actually happy with the PR as it is. The extra modifications above can be done in a subsequent PR.