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.Limits.Cones #2337

Closed
wants to merge 161 commits into from
Closed

[Merged by Bors] - feat: port/CategoryTheory.Limits.Cones #2337

wants to merge 161 commits into from

Commits on Jan 1, 2023

  1. Initial file copy from mathport

    @hargoniX
    hargoniX committed Jan 1, 2023
    Configuration menu
    Copy the full SHA
    01c7d9e View commit details
    Browse the repository at this point in the history

  2. Mathbin -> Mathlib; add import to Mathlib.lean

    @hargoniX
    hargoniX committed Jan 1, 2023
    Configuration menu
    Copy the full SHA
    bc9467d View commit details
    Browse the repository at this point in the history

Commits on Jan 2, 2023

  1. push it as far as possible

    @hargoniX
    hargoniX committed Jan 2, 2023
    Configuration menu
    Copy the full SHA
    afd9aed View commit details
    Browse the repository at this point in the history

Commits on Jan 17, 2023

  1. Merge branch 'master' into port/CategoryTheory.Equivalence

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    c76b450 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2023

  1. seems to work

    @mattrobball
    mattrobball committed Feb 3, 2023
    Configuration menu
    Copy the full SHA
    f0f6502 View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2023

  1. add example and equivalence file for testing

    @mattrobball
    mattrobball committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    91f541a View commit details
    Browse the repository at this point in the history

  2. test: create slice.lean test file

    @thorimur
    thorimur committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    92e65be View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2023

  1. Merge branch 'master' into port/CategoryTheory.Equivalence

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    afafdf0 View commit details
    Browse the repository at this point in the history

  2. remove equivalence.lean

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    eedfb61 View commit details
    Browse the repository at this point in the history

  3. remove rewriteTarget'; change MonadExceptOf to MonadExcept

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    ef7ef69 View commit details
    Browse the repository at this point in the history

  4. add documentation and clean up

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    84ddfcb View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into slice

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    adb9495 View commit details
    Browse the repository at this point in the history

  6. move iteration tactics to core

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    3c369ce View commit details
    Browse the repository at this point in the history

  7. add slice to global import file

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    69bbb93 View commit details
    Browse the repository at this point in the history

  8. modify documentation lines

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    319fa30 View commit details
    Browse the repository at this point in the history

  9. add module documentation(?)

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    720d311 View commit details
    Browse the repository at this point in the history

  10. minor changes

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    8256a85 View commit details
    Browse the repository at this point in the history

  11. Merge branch 'slice' into port/CategoryTheory.Equivalence

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    88ac2d0 View commit details
    Browse the repository at this point in the history

  12. fix module docs

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    388aaa0 View commit details
    Browse the repository at this point in the history

  13. fix test/slice.lean

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    6bae31a View commit details
    Browse the repository at this point in the history

  14. Merge branch 'slice' into port/CategoryTheory.Equivalence

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    06c4b46 View commit details
    Browse the repository at this point in the history

  15. fix all but refl error

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    7140d1c View commit details
    Browse the repository at this point in the history

  16. fix refl error and lint errors

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    2c8c8a7 View commit details
    Browse the repository at this point in the history

  17. fix final long line

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    0c247c7 View commit details
    Browse the repository at this point in the history

  18. use Mathport syntax 

    * use existing docs
* fix docs typos
    @thorimur
    thorimur committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    2c56111 View commit details
    Browse the repository at this point in the history

  19. test: add simple rhs/lhs tests

    @thorimur
    thorimur committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    80596f2 View commit details
    Browse the repository at this point in the history

  20. minor changes to Tactic.Core 

    * use `m` instead of `TacticM` now that we use `MonadExcept`
* simplify code for `iterateRange`
* minor docs tweaks
    @thorimur
    thorimur committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    ce383e4 View commit details
    Browse the repository at this point in the history

  21. Merge branch 'slice' into port/CategoryTheory.Equivalence

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    cf945f0 View commit details
    Browse the repository at this point in the history

  22. update slice naming

    @mattrobball
    mattrobball committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    e6ec924 View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2023

  1. Merge branch 'master' into port/CategoryTheory.Equivalence

    @mattrobball
    mattrobball committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    68bcb25 View commit details
    Browse the repository at this point in the history

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

    ….Equivalence
    @hargoniX
    hargoniX committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    8306c5f View commit details
    Browse the repository at this point in the history

  3. feat: port CategoryTheory.Adjunction.Basic

    @mpenciak
    mpenciak committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    bcc402f View commit details
    Browse the repository at this point in the history

  4. Initial file copy from mathport

    @mpenciak
    mpenciak committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    5bde226 View commit details
    Browse the repository at this point in the history

  5. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mpenciak
    mpenciak committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    e0de198 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/port/CategoryTheory.Equivalence'… 

    … into port/CategoryTheory.Adjunction.Basic
    @mpenciak
    mpenciak committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    3809ccc View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2023

  1. some progress

    @mpenciak
    mpenciak committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    cfe5dc1 View commit details
    Browse the repository at this point in the history

  2. only one error left

    @mattrobball
    mattrobball committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    3278d7d View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into port/CategoryTheory.Adjunction.Basic

    @jcommelin
    jcommelin committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    fc93825 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2023

  1. feat: port CategoryTheory.Pi.Basic

    @mattrobball
    mattrobball committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    b3e68ca View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    8414826 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
    @mattrobball
    mattrobball committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    a4ea90f View commit details
    Browse the repository at this point in the history

  4. fix some errors

    @mattrobball
    mattrobball committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    8136307 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2023

  1. filled in last sorry

    @mpenciak
    mpenciak committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    1f56a41 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into port/CategoryTheory.Pi.Basic

    @mattrobball
    mattrobball committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    df3b93e View commit details
    Browse the repository at this point in the history

  3. break long lines

    @mpenciak
    mpenciak committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    0914b9d View commit details
    Browse the repository at this point in the history

  4. delete linter command

    @mpenciak
    mpenciak committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    671edf6 View commit details
    Browse the repository at this point in the history

  5. fix comments

    @mpenciak
    mpenciak committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    0e48e0e View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2023

  1. fix two simpNF lints

    @jcommelin
    jcommelin committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    4d3bf86 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into port/CategoryTheory.Pi.Basic

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    051b55e View commit details
    Browse the repository at this point in the history

  3. some more fixes

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    2001518 View commit details
    Browse the repository at this point in the history

  4. more fixes

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    2319358 View commit details
    Browse the repository at this point in the history

  5. finally fixed

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    ebdee62 View commit details
    Browse the repository at this point in the history

  6. lint

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    c189778 View commit details
    Browse the repository at this point in the history

  7. add porting note for scary warning

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    7cbd34d View commit details
    Browse the repository at this point in the history

  8. add porting note about proliferation of match

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    b0fba35 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' into port/CategoryTheory.Pi.Basic

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    b49b6cc View commit details
    Browse the repository at this point in the history

  10. feat: port CategoryTheory.Groupoid

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    5d61758 View commit details
    Browse the repository at this point in the history

  11. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    466cb9f View commit details
    Browse the repository at this point in the history

  12. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    e2cfafa View commit details
    Browse the repository at this point in the history

  13. Merge branch 'port/CategoryTheory.Pi.Basic' into port/CategoryTheory.… 

    …Groupoid
    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    a1adaec View commit details
    Browse the repository at this point in the history

  14. initial pass

    @mattrobball
    mattrobball committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    ee114ee View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2023

  1. fix errors

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    7598ce4 View commit details
    Browse the repository at this point in the history

  2. lint

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    9b2cb68 View commit details
    Browse the repository at this point in the history

  3. feat: port CategoryTheory.EpiMono

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    e2aebba View commit details
    Browse the repository at this point in the history

  4. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    7f42580 View commit details
    Browse the repository at this point in the history

  5. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    985720e View commit details
    Browse the repository at this point in the history

  6. Merge branch 'port/CategoryTheory.Groupoid' into port/CategoryTheory.… 

    …EpiMono
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    67a9548 View commit details
    Browse the repository at this point in the history

  7. fix errors; lint; add porting notes

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    e1d3cf3 View commit details
    Browse the repository at this point in the history

  8. feat: port CategoryTheory.Types

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    8c3a9c0 View commit details
    Browse the repository at this point in the history

  9. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    e252760 View commit details
    Browse the repository at this point in the history

  10. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    b6d5b6e View commit details
    Browse the repository at this point in the history

  11. Merge branch 'port/CategoryTheory.EpiMono' into port/CategoryTheory.T… 

    …ypes
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    abef74a View commit details
    Browse the repository at this point in the history

  12. fix errors; lint; add porting note

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    2b370d2 View commit details
    Browse the repository at this point in the history

  13. feat: port CategoryTheory.Functor.Hom

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    7fe5c64 View commit details
    Browse the repository at this point in the history

  14. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    d5ec61a View commit details
    Browse the repository at this point in the history

  15. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    b163ac1 View commit details
    Browse the repository at this point in the history

  16. Merge branch 'port/CategoryTheory.Types' into port/CategoryTheory.Fun… 

    …ctor.Hom
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    4891412 View commit details
    Browse the repository at this point in the history

  17. fix error

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    278e110 View commit details
    Browse the repository at this point in the history

  18. feat: port CategoryTheory.Functor.Currying

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    2e8b88f View commit details
    Browse the repository at this point in the history

  19. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    2b3c437 View commit details
    Browse the repository at this point in the history

  20. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    f147507 View commit details
    Browse the repository at this point in the history

  21. fix all but one decl

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    d492619 View commit details
    Browse the repository at this point in the history

  22. feat: port CategoryTheory.DiscreteCategory

    @adamtopaz
    adamtopaz committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    82e2512 View commit details
    Browse the repository at this point in the history

  23. Initial file copy from mathport

    @adamtopaz
    adamtopaz committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    10bf4bb View commit details
    Browse the repository at this point in the history

  24. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @adamtopaz
    adamtopaz committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    2203485 View commit details
    Browse the repository at this point in the history

  25. fix last errors

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    92feef6 View commit details
    Browse the repository at this point in the history

  26. feat: port CategoryTheory.Yoneda

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    26291ab View commit details
    Browse the repository at this point in the history

  27. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    5a1eb5b View commit details
    Browse the repository at this point in the history

  28. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    3a22ebf View commit details
    Browse the repository at this point in the history

  29. Merge branch 'port/CategoryTheory.Functor.Currying' into port/Categor… 

    …yTheory.Yoneda
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    155f173 View commit details
    Browse the repository at this point in the history

  30. Merge branch 'port/CategoryTheory.Functor.Hom' into port/CategoryTheo… 

    …ry.Yoneda
    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    70bf280 View commit details
    Browse the repository at this point in the history

  31. fix some errors

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    8a683dd View commit details
    Browse the repository at this point in the history

  32. minor fixes

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    dadd6da View commit details
    Browse the repository at this point in the history

  33. fix all but four

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    8981ee1 View commit details
    Browse the repository at this point in the history

  34. fill in some docstrings

    @mpenciak
    mpenciak committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    5b11f3d View commit details
    Browse the repository at this point in the history

  35. Merge branch 'master' into port/CategoryTheory.Yoneda

    @mattrobball
    mattrobball committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    3f4e459 View commit details
    Browse the repository at this point in the history

  36. fix most linter issues

    @mpenciak
    mpenciak committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    ccb1de5 View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2023

  1. Merge branch 'master' into port/CategoryTheory.Adjunction.Basic

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    cda62dd View commit details
    Browse the repository at this point in the history

  2. add missing aligns for fields; lint

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    3603497 View commit details
    Browse the repository at this point in the history

  3. restore lost import line

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    0e07734 View commit details
    Browse the repository at this point in the history

  4. feat: port CategoryTheory.CommSq

    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    5fedaef View commit details
    Browse the repository at this point in the history

  5. Initial file copy from mathport

    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    b108a9d View commit details
    Browse the repository at this point in the history

  6. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    8e67aa7 View commit details
    Browse the repository at this point in the history

  7. first pass

    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    ca10bfb View commit details
    Browse the repository at this point in the history

  8. names and removing restate_axiom

    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    2e1beb7 View commit details
    Browse the repository at this point in the history

  9. fix lint

    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    45532e0 View commit details
    Browse the repository at this point in the history

  10. remove spurious edit

    @mo271
    mo271 committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    332636e View commit details
    Browse the repository at this point in the history

  11. feat: port CategoryTheory.LiftingProperties.Basic

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    4968e19 View commit details
    Browse the repository at this point in the history

  12. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    e49ab39 View commit details
    Browse the repository at this point in the history

  13. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    bd1174b View commit details
    Browse the repository at this point in the history

  14. Merge branch 'port/CategoryTheory.CommSq' into port/CategoryTheory.Li… 

    …ftingProperties.Basic
    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    c6ecc99 View commit details
    Browse the repository at this point in the history

  15. fix errors; lint

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    6a1bbf0 View commit details
    Browse the repository at this point in the history

  16. feat: port CategoryTheory.Limits.Shapes.StrongEpi

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    4ebb6e1 View commit details
    Browse the repository at this point in the history

  17. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    1979ee1 View commit details
    Browse the repository at this point in the history

  18. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    d9d7366 View commit details
    Browse the repository at this point in the history

  19. Merge branch 'port/CategoryTheory.LiftingProperties.Basic' into port/… 

    …CategoryTheory.Limits.Shapes.StrongEpi
    @mattrobball
    mattrobball committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    cbc27d7 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2023

  1. get file to build

    @adamtopaz
    adamtopaz committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    8860e0d View commit details
    Browse the repository at this point in the history

  2. fix errors; lint

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    118d7ed View commit details
    Browse the repository at this point in the history

  3. Update Mathlib.lean

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    5e558ae View commit details
    Browse the repository at this point in the history

  4. lint

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    eb14644 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into port/CategoryTheory.DiscreteCategory

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    18f8822 View commit details
    Browse the repository at this point in the history

  6. lint some more

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    38a89b8 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory… 

    ….DiscreteCategory' into port/CategoryTheory.DiscreteCategory
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    24c70cb View commit details
    Browse the repository at this point in the history

  8. feat: port CategoryTheory.LiftingProperties.Adjunction

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    12c4a61 View commit details
    Browse the repository at this point in the history

  9. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    fc177c8 View commit details
    Browse the repository at this point in the history

  10. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    f80301f View commit details
    Browse the repository at this point in the history

  11. Merge branch 'port/CategoryTheory.LiftingProperties.Basic' into port/… 

    …CategoryTheory.LiftingProperties.Adjunction
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    43628fb View commit details
    Browse the repository at this point in the history

  12. Merge branch 'port/CategoryTheory.Adjunction.Basic' into port/Categor… 

    …yTheory.LiftingProperties.Adjunction
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    db380ce View commit details
    Browse the repository at this point in the history

  13. fix errors; lint

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    e296a22 View commit details
    Browse the repository at this point in the history

  14. Delete start_port-macos.sh

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    084cffd View commit details
    Browse the repository at this point in the history

  15. Delete start_port-macos.sh

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    ea56ec5 View commit details
    Browse the repository at this point in the history

  16. feat: port CategoryTheory.Functor.EpiMono

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    b71ba2c View commit details
    Browse the repository at this point in the history

  17. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    1aaf063 View commit details
    Browse the repository at this point in the history

  18. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    a8492d2 View commit details
    Browse the repository at this point in the history

  19. Merge branch 'port/CategoryTheory.LiftingProperties.Adjunction' into … 

    …port/CategoryTheory.Functor.EpiMono
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    2bf91be View commit details
    Browse the repository at this point in the history

  20. Merge branch 'port/CategoryTheory.Limits.Shapes.StrongEpi' into port/… 

    …CategoryTheory.Functor.EpiMono
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    0552b42 View commit details
    Browse the repository at this point in the history

  21. fix errors; lint

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    936a011 View commit details
    Browse the repository at this point in the history

  22. feat: port CategoryTheory.Functor.ReflectsIsomorphisms

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    e91cd26 View commit details
    Browse the repository at this point in the history

  23. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    1fe7733 View commit details
    Browse the repository at this point in the history

  24. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    f103536 View commit details
    Browse the repository at this point in the history

  25. Merge branch 'port/CategoryTheory.Functor.EpiMono' into port/Category… 

    …Theory.Functor.ReflectsIsomorphisms
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    5d6e14e View commit details
    Browse the repository at this point in the history

  26. fix errors; lint; shorten filename

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    7f41cf3 View commit details
    Browse the repository at this point in the history

  27. Merge branch 'master' into port/CategoryTheory.Yoneda

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    cbe8924 View commit details
    Browse the repository at this point in the history

  28. fix last errors; lint

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    37804c7 View commit details
    Browse the repository at this point in the history

  29. feat: port CategoryTheory.Limits.Cones

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    9e93b3f View commit details
    Browse the repository at this point in the history

  30. Initial file copy from mathport

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    8beaf77 View commit details
    Browse the repository at this point in the history

  31. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    1c31831 View commit details
    Browse the repository at this point in the history

  32. Merge branch 'port/CategoryTheory.Yoneda' into port/CategoryTheory.Li… 

    …mits.Cones
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    ab990e7 View commit details
    Browse the repository at this point in the history

  33. Merge branch 'port/CategoryTheory.DiscreteCategory' into port/Categor… 

    …yTheory.Limits.Cones
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    1fa3691 View commit details
    Browse the repository at this point in the history

  34. Merge branch 'port/CategoryTheory.Functor.ReflectsIsomorphisms' into … 

    …port/CategoryTheory.Limits.Cones
    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    0185da3 View commit details
    Browse the repository at this point in the history

  35. fix some errors

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    86f2d01 View commit details
    Browse the repository at this point in the history

  36. fix some more

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    ea4b275 View commit details
    Browse the repository at this point in the history

  37. fix errors

    @mattrobball
    mattrobball committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    8d19aa9 View commit details
    Browse the repository at this point in the history

Commits on Feb 18, 2023

  1. lint

    @mattrobball
    mattrobball committed Feb 18, 2023
    Configuration menu
    Copy the full SHA
    e1a7f98 View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2023

  1. add updated files

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    bd0f2cf View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into port/CategoryTheory.Limits.Cones

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    039e15f View commit details
    Browse the repository at this point in the history

  3. replace X with pt for cone field

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    64d878d View commit details
    Browse the repository at this point in the history

  4. fix import file

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    0ae8a12 View commit details
    Browse the repository at this point in the history

  5. remove script

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    7abe319 View commit details
    Browse the repository at this point in the history

  6. fix one error

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    cf0ddc2 View commit details
    Browse the repository at this point in the history

  7. move comment

    @mattrobball
    mattrobball committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    a46ad8b View commit details
    Browse the repository at this point in the history