-
Notifications
You must be signed in to change notification settings - Fork 11
Open
3 / 53 of 5 issues completedLabels
C-grpdComponent: groupoid modelComponent: groupoid modelC-modelComponent: abstract model (natural or unstructured)Component: abstract model (natural or unstructured)C-syntaxComponent: typing rules, interpretation functionComponent: typing rules, interpretation functionD-highDifficulty: highDifficulty: highI-critImpact: criticalImpact: criticalO-polyOther: improvements to PolyOther: improvements to Poly
Description
In the branch clans1, PR #164.
Here is a roadmap for (natural) model semantics in the setting of a pi-clan, if we settle on doing things this way:
Polynomials:
- use a different version of mathlib (currently in a PR) to generalize some pullback results so that we can define pullback functors without all pullbacks existing on the category
- refactor the UvPoly results in this pi-clan setting. I will try to write out enough definitions and
sorrys for us to continue the rest of the development => Pi-clan polynomials #148
General semantics:
- define semantics in the setting of pi-clans, starting with a universe in the pi-clan. (done for pis and sigmas) pi-clan refactor general semantics #149
- refactor the interpretation used in
SynthLeanto target Ctx with a pi-clan instead of Psh(Ctx)? (should be very easy, and is totally optional)
Groupoids:
- Define the class of isofibrations in
Grpdand show that it is a pi-clan (that it is closed under pushforwards is a fairly involved but self-contained theorem) => Groupoid isofibrations are closed under pushforwards. #147 - Make the previous constructions instantiate the new semantics => FunctorOperation.Sigma --> GroupoidModel.Universe.Sigma #150
Reactions are currently unavailable
Sub-issues
Metadata
Metadata
Assignees
Labels
C-grpdComponent: groupoid modelComponent: groupoid modelC-modelComponent: abstract model (natural or unstructured)Component: abstract model (natural or unstructured)C-syntaxComponent: typing rules, interpretation functionComponent: typing rules, interpretation functionD-highDifficulty: highDifficulty: highI-critImpact: criticalImpact: criticalO-polyOther: improvements to PolyOther: improvements to Poly