Closed JacquesCarette closed 7 months ago
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
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.
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 Σ
do you or @HuStmpHrrr know where the names of
BaseChange!
andBaseChange*
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).
Sandro's answer is very much accurate.
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.
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.