Skip to content

Show that polynomial functors preserve pullbacks #57

Closed
sinhp/Poly
#31
Closed
Show that polynomial functors preserve pullbacks#57
sinhp/Poly
#31
Assignees
awodey
Labels
C-modelComponent: abstract model (natural or unstructured)D-lowDifficulty: lowI-critImpact: criticalO-polyOther: improvements to Poly

Description

@Vtec234
Vtec234
opened on Feb 19, 2025

This should be easy given forgetCreatesConnectedLimits.

We need this to lift Pi formation from universe-monomorphic to universe-polymorphic as described here.

Activity

  1. Vtec234
    added
    C-modelComponent: abstract model (natural or unstructured)
    D-lowDifficulty: low
    I-critImpact: critical
    O-polyOther: improvements to Poly
    on Feb 19, 2025
  2. Vtec234
    self-assigned this
    on Feb 19, 2025
  3. Vtec234
    removed their assignment
    on Apr 28, 2025
  4. Vtec234
    added a parent issue on May 1, 2025
  5. awodey
    self-assigned this
    on Jun 25, 2025
  6. Vtec234
    closed this as completedin Poly#31on Aug 19, 2025

  7. Vtec234 commented on Aug 19, 2025

    @Vtec234
    Vtec234
    on Aug 19, 2025
    CollaboratorAuthor

    Note: we also have this for all connected limits here, but assuming that C has all such limits. Once leanprover-community/mathlib4#28131 is merged, we'll be able to drop this assumption.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

C-modelComponent: abstract model (natural or unstructured)D-lowDifficulty: lowI-critImpact: criticalO-polyOther: improvements to Poly

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions