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(CategoryTheory): Relation between the Grothendieck construction and AsSmall #19539

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(CategoryTheory): Relation between the Grothendieck construction and AsSmall #19539

wants to merge 13 commits into from
+108 −8

Commits on Nov 27, 2024

  1. asSmall

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    8ea919c View commit details
    Browse the repository at this point in the history

  2. eqToHom_down

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    014a5d2 View commit details
    Browse the repository at this point in the history

  3. asSmallEquiv

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    e845fe1 View commit details
    Browse the repository at this point in the history

  4. progress on mapWhiskerRightAsSmall

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    3e4eff2 View commit details
    Browse the repository at this point in the history

  5. finish mapWhiskerRightAsSmall

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    4cd2699 View commit details
    Browse the repository at this point in the history

  6. fix universes

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    ff64623 View commit details
    Browse the repository at this point in the history

  7. doc

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    8f2c069 View commit details
    Browse the repository at this point in the history

  8. move down_comp

    @javra
    javra committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    2530dd0 View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2024

  1. address @joelriou's suggestions

    @javra
    javra committed Nov 28, 2024
    Configuration menu
    Copy the full SHA
    7540b74 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2024

  1. address @joelriou's suggestions 

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
    @javra @joelriou
    javra and joelriou authored Nov 29, 2024
    Configuration menu
    Copy the full SHA
    22aab94 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2024

  1. address @joelriou's suggestions

    @javra
    javra committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    5864d34 View commit details
    Browse the repository at this point in the history

  2. address @joelriou's suggestions

    @javra
    javra committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    0834358 View commit details
    Browse the repository at this point in the history

  3. more renamings

    @javra
    javra committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    7efc4bc View commit details
    Browse the repository at this point in the history