Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: a functor from a small category to a filtered category factors through a small filtered category #6212

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat: a functor from a small category to a filtered category factors through a small filtered category #6212

wants to merge 21 commits into from

Commits on Jul 27, 2023

  1. Don't think I'll be able to save this

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    3c4da37 View commit details
    Browse the repository at this point in the history

  2. Sorry-free

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    b180633 View commit details
    Browse the repository at this point in the history

  3. Start cleaning up

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    9bcd36c View commit details
    Browse the repository at this point in the history

  4. First draft, needs to be dualized

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    77310a0 View commit details
    Browse the repository at this point in the history

  5. Remove useless linarith import

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    c8ea177 View commit details
    Browse the repository at this point in the history

  6. Try to follow naming convention

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    5255830 View commit details
    Browse the repository at this point in the history

  7. Weird apostrophe

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    607595c View commit details
    Browse the repository at this point in the history

  8. Remove instance names

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    104591a View commit details
    Browse the repository at this point in the history

  9. Remove unnecessary _root_

    @TwoFX
    TwoFX committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    a9ab4b3 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2023

  1. Rename hypothesis

    @TwoFX
    TwoFX committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    8c774ae View commit details
    Browse the repository at this point in the history

  2. Cleanup + dualize

    @TwoFX
    TwoFX committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    ae0cc0d View commit details
    Browse the repository at this point in the history

  3. Minor

    @TwoFX
    TwoFX committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    78f319d View commit details
    Browse the repository at this point in the history

  4. Generalize universes

    @TwoFX
    TwoFX committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    61160ed View commit details
    Browse the repository at this point in the history

  5. Empty line after starting a section

    @TwoFX
    TwoFX committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    18f7cfe View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2023

  1. Merge remote-tracking branch 'origin/master' into small-filtered-2

    @TwoFX
    TwoFX committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    a1819fc View commit details
    Browse the repository at this point in the history

  2. Filtered.lean -> Filtered/Basic.lean

    @TwoFX
    TwoFX committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    603e553 View commit details
    Browse the repository at this point in the history

Commits on Aug 20, 2023

  1. Add categories and sheaves to references

    @TwoFX
    TwoFX committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    d60631f View commit details
    Browse the repository at this point in the history

  2. Move, namespaces

    @TwoFX
    TwoFX committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    5265be0 View commit details
    Browse the repository at this point in the history

  3. Fixes

    @TwoFX
    TwoFX committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    727fca8 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into small-filtered-2

    @TwoFX
    TwoFX committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    ac67bef View commit details
    Browse the repository at this point in the history

  5. Fix after bumping past autoimplicits

    @TwoFX
    TwoFX committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    dea748b View commit details
    Browse the repository at this point in the history