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(category_theory/limits): bicartesian squares #14375

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat(category_theory/limits): bicartesian squares #14375

wants to merge 25 commits into from

Commits on May 18, 2022

  1. feat(category_theory/limits): pullback squares

    @semorrison
    semorrison committed May 18, 2022
    Configuration menu
    Copy the full SHA
    1c65a3c View commit details
    Browse the repository at this point in the history

  2. lint

    @semorrison
    semorrison committed May 18, 2022
    Configuration menu
    Copy the full SHA
    b187a2a View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into semorrison/pullback… 

    …_square
    @semorrison
    semorrison committed May 18, 2022
    Configuration menu
    Copy the full SHA
    a77b9b7 View commit details
    Browse the repository at this point in the history

Commits on May 23, 2022

  1. Add comm_sq, and renames

    @semorrison
    semorrison committed May 23, 2022
    Configuration menu
    Copy the full SHA
    d33704a View commit details
    Browse the repository at this point in the history

  2. feat(category_theory/limits): products give pullback squares

    @semorrison
    semorrison committed May 23, 2022
    Configuration menu
    Copy the full SHA
    414918b View commit details
    Browse the repository at this point in the history

  3. merge

    @semorrison
    semorrison committed May 23, 2022
    Configuration menu
    Copy the full SHA
    9cf4475 View commit details
    Browse the repository at this point in the history

  4. fix merge

    @semorrison
    semorrison committed May 23, 2022
    Configuration menu
    Copy the full SHA
    809b26e View commit details
    Browse the repository at this point in the history

Commits on May 25, 2022

  1. .

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    daac4d4 View commit details
    Browse the repository at this point in the history

  2. oops, finish merge, and do the work

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    eee3f39 View commit details
    Browse the repository at this point in the history

  3. add file

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    27c0121 View commit details
    Browse the repository at this point in the history

  4. fix module doc

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    8d64155 View commit details
    Browse the repository at this point in the history

  5. merge

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    95e0f5a View commit details
    Browse the repository at this point in the history

  6. fix merge

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    e0cf284 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'semorrison/pullback_square2' into semorrison/bicartesian

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    c126928 View commit details
    Browse the repository at this point in the history

  8. refactor a bit

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    cf4f64b View commit details
    Browse the repository at this point in the history

  9. lint

    @semorrison
    semorrison committed May 25, 2022
    Configuration menu
    Copy the full SHA
    ea8d4ab View commit details
    Browse the repository at this point in the history

Commits on May 27, 2022

  1. merge

    @semorrison
    semorrison committed May 27, 2022
    Configuration menu
    Copy the full SHA
    37e7690 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2022

  1. Merge remote-tracking branch 'origin/master' into semorrison/bicartesian

    @semorrison
    semorrison committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    055ee60 View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2022

  1. fix and update comment

    @semorrison
    semorrison committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    c37ccad View commit details
    Browse the repository at this point in the history

  2. fix

    @semorrison
    semorrison committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    239f430 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2022

  1. Apply suggestions from code review 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @semorrison @jcommelin
    semorrison and jcommelin committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    59dfe46 View commit details
    Browse the repository at this point in the history

  2. merge

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    40f5919 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'semorrison/bicartesian' of github.com:leanprover-commun… 

    …ity/mathlib into semorrison/bicartesian
    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    c594459 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2022

  1. Merge remote-tracking branch 'origin/master' into semorrison/bicartesian

    @semorrison
    semorrison committed Oct 4, 2022
    Configuration menu
    Copy the full SHA
    6937b55 View commit details
    Browse the repository at this point in the history

  2. fix

    @semorrison
    semorrison committed Oct 4, 2022
    Configuration menu
    Copy the full SHA
    5f476ef View commit details
    Browse the repository at this point in the history