Conversation
Taneb
force-pushed
the
MoreBaseChanges
branch
from
182cc4e to
56f4a35
Compare
|
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 |
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
It's looking really good. Tiny tweaks to do in one spot, otherwise, it's just comments.
| Free⊣Coforgetful = record | ||
| { unit = ntHelper record | ||
| { η = λ X → p.universal (sliceobj π₁) (λ-unique₂′ (unit-pb X)) | ||
| ; commute = λ {S} {T} f → p.unique-diagram (sliceobj π₁) !-unique₂ $ begin |
There was a problem hiding this comment.
For these longer proofs, best to put them either in where or named in a private block. Purely for efficiency.
| λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ (sliceobj π₁) ⟩ | ||
| λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ λg swap ≈⟨ subst ⟩ | ||
| λg (((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ first (λg swap)) ≈⟨ λ-cong (pullʳ β′) ⟩ | ||
| λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap) ≈⟨ λ-cong (pull-last swap∘swap) ⟩ |
src/Categories/Functor/Slice.agda
Outdated
| open Terminal terminal | ||
| open BinaryProducts products | ||
|
|
||
| -- Needs better name! |
There was a problem hiding this comment.
Yes, it does. Ask on the category theory Zulip? It feels like it ought to have a name. (Does the 1lab have this yet?)
There was a problem hiding this comment.
1lab calls this functor exponentiable→product, and what we call Free they call constant-family. I can't see a counterpart to our Forgetful but I've asked in their Discord.
I would like to, following Polynomial Functors and Polynomial Monads (the paper I'm slowly working towards formalize here), call Forgetful Σ, Free Δ, and Coforgetful Π, but those names are even less indicative of their function than what we currently have. Aspects of Topoi uses the same names for Forgetful and Coforgetful, but calls Free ×.
There was a problem hiding this comment.
Yes, those single-letter names are even worse. The 1lab's names don't seem so bad?
I could try to summon @TOTBWF to see if he has opinions.
There was a problem hiding this comment.
I have been SUMMONED ✨🧊 🧙✨
To get a good idea for names, it's good to understand exactly what is going on with slices. The intuition here is that a slice f : X -> I is how we can encode an I-indexed family of objects X_i without any sort of classifying object like Type. In places like Set, we can move between the two by taking the fibres of f and by forming the total space π₁ : Σ[ i ∈ I ] (P i) → I, but in a general category we cannot do this, so slices it is.
As such, base change pullback-functorial should really be thought of as a functor on slices C/B -> C/A for a morphism A -> B: from the perspective of families, this restricts a family f : X -> B to a new family P -> A along f potentially duplicating or deleting fibres. In other words, we take the fibre product: IE, the pullback. By composing with the projection out of the slice, we've essentially "forgotten" the indexing, and are just looking at the total space of the reindexed family.
From this perspective, Free isn't really the free slice, but rather the constant family on I: each fibre over is a copy of X. Furthermore, Forgetful doesn't really "forget" a slice: it returns the total space of a family by discarding the indexing.
Coforgetful is the trickiest: the bottom leg of the pullback is an obfuscation of the identity morphism, and the right leg is more or less postcomposition by the projection out of the family X -> I. Therefore, this pullback consists of sections of the family X -> I internalized as a exponential objects.
With all that background out of the way, here are my suggestions:
- Make
pullback-functoriala functor on slices, and rename it toBase-changeorReindex FreebecomesConstant-familyForgtefulbecomesTotal-spaceorTotalCoforgetfulbecomesInternal-sectionsorSections
PS: this is some really great work!
There was a problem hiding this comment.
I like these names a lot! Thanks for the explanation.
While switching to them, I noticed that pullback-functorial (after @TOTBWF's suggestion to make it less forgetful) looks a lot like Categories.Functor.Slice.BaseChange.BaseChange*. I haven't quite been able to convince myself that they are the same thing, because there's a lot of redirection and it's a little confusing to get my head around, but if they are, I'd like to remove pullback-functorial entirely.
EDIT: I was able to write a NaturalIsomorphism between the two where almost everything was trivial (one use of universal-resp-≈ was necessary for commute), so I went ahead and deleted what was once pullback-functorial
I also fiddled with pbarr a bit to make its equality argument abstract
It was pretty much exactly the same as Functor.Slice.BaseChange.BaseChange*
|
Looks like I've broken |
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
This is looking really nice!
|
I'd like to finish this off... but I've gotten lost with what was going on with it :( |
|
Anything I could do to help? |
|
Remaining considerations:
|
|
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 |
3 participants
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
agdarepo rather than my own fork so it's easier for other contributors to make commits.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.