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: port CategoryTheory.Bicategory.CoherenceTactic #4610

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Bicategory.CoherenceTactic #4610

wants to merge 14 commits into from

Commits on Jun 2, 2023

  1. feat: port CategoryTheory.Bicategory.CoherenceTactic

    @joelriou
    joelriou committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    c4fe5d1 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joelriou
    joelriou committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    a6a8320 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    05f7ec2 View commit details
    Browse the repository at this point in the history

  4. ported the non tactic code

    @joelriou
    joelriou committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    0db1177 View commit details
    Browse the repository at this point in the history

  5. fixed long line

    @joelriou
    joelriou committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    0661e06 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2023

  1. commented out the unported meta code

    @joelriou
    joelriou committed Jun 3, 2023
    Configuration menu
    Copy the full SHA
    a7e16aa View commit details
    Browse the repository at this point in the history

Commits on Jun 5, 2023

  1. almost but not quite there

    @semorrison
    semorrison committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    64ddb7c View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2023

  1. import everything

    @semorrison
    semorrison committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    805deea View commit details
    Browse the repository at this point in the history

  2. working

    @semorrison
    semorrison committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    feeb635 View commit details
    Browse the repository at this point in the history

  3. fixes

    @semorrison
    semorrison committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    ad1012b View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into port/CategoryTheory… 

    ….Bicategory.CoherenceTactic
    Scott Morrison committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    4a04d12 View commit details
    Browse the repository at this point in the history

Commits on Jun 7, 2023

  1. open MonoidalCategory as needed, for notation

    Scott Morrison committed Jun 7, 2023
    Configuration menu
    Copy the full SHA
    60ba13e View commit details
    Browse the repository at this point in the history

  2. fix

    Scott Morrison committed Jun 7, 2023
    Configuration menu
    Copy the full SHA
    0d36a03 View commit details
    Browse the repository at this point in the history

  3. fix

    Scott Morrison committed Jun 7, 2023
    Configuration menu
    Copy the full SHA
    b07238c View commit details
    Browse the repository at this point in the history