Skip to content

Establish naturality of type/term formers #49

Closed
Closed
Establish naturality of type/term formers#49
Labels
C-modelComponent: abstract model (natural or unstructured)D-unkDifficulty: unknownI-critImpact: critical

Description

@Vtec234
Vtec234
opened on Feb 11, 2025

Prove assorted sorrys, most of which have to do with naturality of various constructions, or follow from their universal properties. See here for a Zulip discussion of a (possibly too slow in terms of Lean typechecking time) approach to proving some of these with less code.

Activity

  1. Vtec234
    added
    C-modelComponent: abstract model (natural or unstructured)
    D-unkDifficulty: unknown
    I-critImpact: critical
    on Feb 11, 2025
  2. Vtec234
    added a parent issue on May 1, 2025
  3. Vtec234
    changed the title [-]Establish naturality of Pi constructions[/-] [+]Establish naturality of type/term formers[/+] on May 1, 2025
  4. Vtec234
    closed this as completedon Sep 2, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    C-modelComponent: abstract model (natural or unstructured)D-unkDifficulty: unknownI-critImpact: critical

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions