feat: Structured model #170
Conversation
|
|
||
| variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) | ||
|
|
||
| structure PartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C) where |
There was a problem hiding this comment.
Could we have a docstring?
| open Lake DSL | ||
|
|
||
| require Poly from git "https://github.com/sinhp/Poly" @ "master" | ||
| require Poly from git "https://github.com/Jlh18/Poly.git" @ "master" |
There was a problem hiding this comment.
Looks like your fork has diverged from Sina's (both bumped mathlib at one point). Is Sina's more recent version too recent?
There was a problem hiding this comment.
I wasn't aware that Poly was getting updated. It should be ok to go to the new version of Poly. I was mainly trying to get a newer version of mathlib.
There was a problem hiding this comment.
Oh jeez. They changed the defintion of morphisms in Cat. This will be a big refactor
There was a problem hiding this comment.
Maybe let's merge with the current version and leave the refactor for later? Unless you prefer to do it now.
There was a problem hiding this comment.
I think we should just get the refactor done with some (reasonable) sorrys. I am halfway through
There was a problem hiding this comment.
Update: fixing the breakages in the groupoid pi types file will be a decent amount of work, since the API for the new definitions in the Cat library is not very complete. I will make a new branch for the TYPES2026 submission and leave this PR open for now. That way we don't have the time pressure to get this mathlib update done.
| @@ -0,0 +1,1340 @@ | |||
| import HoTTLean.ForMathlib.CategoryTheory.Clan | |||
|
|
|||
There was a problem hiding this comment.
What's the plan with this file? It's redoing a lot of Poly at the generality of morphism properties, right? Is this going into mathlib (instead of Poly)?
There was a problem hiding this comment.
@Jlh18 Is there a plan to push this development to the Poly repo? Also, curious if have you proved some theorems for generalized polynomials which we already did not have for the standard polynomials?
I also think we need a different terminology other than "Polynomial" for these "generalized polynomials".
Before pushing into mathlib, we need to discuss how LCCCs, Polys and their generalization can be synthesized. I recently have thought how we can do this, happy to chat about it.
(LCCCs are growing in mathlib: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory/LocallyCartesianClosed
This is about 1100 loc, and about 1000 loc in LCCC PRs under review.)
There was a problem hiding this comment.
I guess we need to have a meeting to discuss this. It certainly can refactor the Poly library, which if I understand correctly should end up being PRed to mathlib.
if have you proved some theorems for generalized polynomials which we already did not have for the standard polynomials?
I don't think I proved anything extra, only more general in the sense of 1. doing everything MvPoly first and 2. using partial exponentiability/pushforwards/clans
I also think we need a different terminology other than "Polynomial" for these "generalized polynomials".
Why? Aren't they just polynomials, but more general?
happy to chat about it.
same - let me know when is good for you!
I have half an eye on your LCC PRs, glad to see that! I feel like there is a lot to do before polynomials can be PRed.
|
|
||
| /-- A natural model with support for dependent types (and nothing more). | ||
| The data is a natural transformation with representable fibers, | ||
| stored as a choice of representative for each fiber. -/ |
There was a problem hiding this comment.
Brief explanation of what this adds to the unstructured universe? Right now they have the same doc.
I have moved some of the code from
clans1branch here, now that it is more or less stable. It should be ready for merging with master, though note that it uses my version of Poly, which is a more recent version of mathlib