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.Preserves.Shapes.Pullbacks #2571

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks #2571

wants to merge 12 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Mar 2, 2023 •
edited by github-actions bot

@mattrobball
feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks
4ae5a00
@mattrobball
Initial file copy from mathport
041a449
@mattrobball
automated fixes
4508cbd 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mattrobball
Squashed commit of the following:
da04b77 
commit fdfb90aa706c177622b3007234ee19bb0ea5e4da
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 28 07:13:40 2023 -0500

    fix import file again

commit afbef870a0c63af2b90361c17e656623515a643d
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 28 06:55:04 2023 -0500

    fix long line

commit aead3fc10697c49ed592a62ec47448a747ce51a3
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 28 06:52:32 2023 -0500

    fix import file

commit 9b884074bdfb2dee2615f5499a1cefa61c76c5ad
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 23:59:36 2023 -0500

    lint for names

commit 50d99037c616c011a3083ed0e511a8852626950d
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 23:41:34 2023 -0500

    lint for linters

commit f10cc5f24aed69a735bfce76b7a12ad47a8f6496
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 23:20:54 2023 -0500

    lint for long lines

commit 43770398685f1b0e733b8068fa93c663638ebe63
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 23:08:46 2023 -0500

    fix last errors

commit efb9e6e9cf5c93a8b6acf4d19b57af0cb6be1a97
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 10:33:11 2023 -0500

    attempt to get aesop working

commit 47985048e7fd763876f0e124bcf05790392acf88
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 23:38:49 2023 -0500

    fix more errors

    reasonably small now

commit 15e4a31af8b05b83da2cc68866b0caef51a15780
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 18:02:23 2023 -0500

    fix errors quick pass

commit 2bacc4cce0faac47ced1fa8b83af5d73f68cd2f0
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 17:37:06 2023 -0500

    add updated dependency

commit d68f5038eaaf93147734326be4c7e11c072226a8
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 17:27:03 2023 -0500

    add dependency

commit 970e5a07941718e547e6a116b6b5c743258f379e
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 17:24:11 2023 -0500

    Squashed commit of the following:

    commit 4de54ba44d632696bec86a1c17ca0a2afbc69aae
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sun Feb 26 17:02:34 2023 -0500

        lint for names

    commit 724546e1e0808312e525d577d0cbb6b02724b6ac
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sun Feb 26 16:50:23 2023 -0500

        lint

    commit 3edb4dee4346ee353dd3c2f93bebecf50ca478e5
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sun Feb 26 16:24:32 2023 -0500

        fix last errors

    commit 4c715ddaef7a902e4a099f6f2539b175c3e7167e
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sat Feb 25 22:14:41 2023 -0500

        fix on first pass

    commit e0ca1c095fa2ad3748192f5d55f2d84d00a9139a
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sat Feb 25 20:05:08 2023 -0500

        Squashed commit of the following:

        commit 1aaa9e6950c98a56a22aafb66c498fc15c45090d
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Sat Feb 25 10:38:19 2023 -0500

            fix names in comments

        commit e77700c8b2ba0d73f53037329fd50b09c185a4db
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Sat Feb 25 10:31:33 2023 -0500

            lint

        commit d997da4eaf5d0d569a581085a96441679cd17515
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Sat Feb 25 10:18:23 2023 -0500

            fix remaining errors

        commit 2f59f85661fd708f6385184ce3fc957292a96173
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 22:04:57 2023 -0500

            perform basic pass

        commit cbf04a8a5a1af46bb391c5bc92fe4cab8cd872dc
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 21:52:19 2023 -0500

            fix one more

        commit de6138f54fb6c6a58864ecab253055362735661f
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 21:50:42 2023 -0500

            update X to pt

        commit 63366ed3d0559148417befcaddec6b3a8d2e5f3b
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 21:12:45 2023 -0500

            Squashed commit of the following:

            commit b27bf68dc04e7e68600a96dfe7a8c00d9ae5c019
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Fri Feb 24 16:00:22 2023 -0500

                expand comment

                weird behavior from simpNF

            commit 36b91d370a2089ba954ea2dca5e8d3eeaf6f0da0
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Fri Feb 24 15:58:05 2023 -0500

                lint

            commit 9188b8ed09b7a996514c3db00504c677d26976d5
            Author: adamtopaz <github@adamtopaz.com>
            Date:   Fri Feb 24 11:02:44 2023 -0700

                clean up more proofs

            commit 24728b02640ff3be43a113e25d255d1f860b4448
            Author: adamtopaz <github@adamtopaz.com>
            Date:   Fri Feb 24 10:58:00 2023 -0700

                more cleanup

            commit 279d9ea58734f8514e6327b78ce69171932e9d5a
            Author: adamtopaz <github@adamtopaz.com>
            Date:   Fri Feb 24 10:56:03 2023 -0700

                cleanup

            commit 05aed830d891040ebd197b24fb559f91a7ba2657
            Author: adamtopaz <github@adamtopaz.com>
            Date:   Fri Feb 24 10:39:16 2023 -0700

                kill all sorries

            commit 6c29220487fd7f0a9444bdc5bee0a9a4b2167816
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Fri Feb 24 10:55:30 2023 -0500

                fix most errors; get intro crazy state

            commit c741d30ca6900213f55be575e6fa5b2a0e9e78ba
            Merge: 9478bf23 bae55acd
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Thu Feb 23 19:17:37 2023 -0500

                Merge branch 'port/CategoryTheory.Limits.Shapes.Terminal' into port/CategoryTheory.StructuredArrow

            commit 9478bf2324686ef6f608d5cddcee506ca64470ad
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Thu Feb 23 19:17:01 2023 -0500

                automated fixes

                Mathbin -> Mathlib

                fix certain import statements

                move "by" to end of line

                add import to Mathlib.lean

            commit 648591e4af5dc579c2820404b893ca4e1ab2face
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Thu Feb 23 19:17:01 2023 -0500

                Initial file copy from mathport

            commit 387de5183870a70f33ec08545c4b5f74f0f009e1
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Thu Feb 23 19:17:01 2023 -0500

                feat: port CategoryTheory.StructuredArrow

            commit bae55acd4ae60c37b4a75746ccc0fba627a48582
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 23:27:33 2023 -0500

                fix imports

            commit ea627ff707030f5aa6293a59b07b40a1c5a4d986
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 23:10:46 2023 -0500

                lint; fix names

            commit 09a2181e2afdb67c31dd4154454f1d670a2f8733
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 23:00:13 2023 -0500

                fix errors

            commit f5ba00238c536c7c8ceb330dbdfbff6e182d58d6
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 18:52:22 2023 -0500

                Squashed commit of the following:

                commit d0a99d9548ceab22a6a38d44faeca635ca2b75fa
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 21 23:16:12 2023 -0500

                    move names to new convention

                commit dba0c31778cf86fcf01764b4e8ca6b38a8e88277
                Merge: 8350d86a f89a71d4
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 21 23:03:58 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.Limits.HasLimits

                commit 8350d86ad846997e4d5947d77c4dd74032a8083e
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 21 23:02:58 2023 -0500

                    add updated files

                commit 0d6760d2b59a2d0ef2b9e21759b7f95ef3445608
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sun Feb 19 19:19:52 2023 -0500

                    fix case error

                commit 79cfc312fb624fa1f6a00505cdf5cf5361b84df5
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sun Feb 19 09:09:05 2023 -0500

                    remove script

                commit 5d7be116cffbca1a21c9b19eea7838ee6921d8d4
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sun Feb 19 00:02:32 2023 -0500

                    fix import line typo

                commit 0814483e24f12520c0130f10fff907ce59e3b8da
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 23:52:06 2023 -0500

                    fix import file

                commit 1483f34940f8662726ade55e0fbf637cb7744f9d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 23:51:22 2023 -0500

                    align names in comments

                commit b596e2ef8d9045e252708db72fc8d224f5573c6b
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 23:38:31 2023 -0500

                    lint for CI

                commit 73f99ead9d6eb03843a05e2167fe8a354b2be079
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 23:28:31 2023 -0500

                    try fix-comments.py

                    only fixed a single issue for the second time now

                commit 20b586bf36dc200874e43918aaeec5d3792a04c1
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 23:26:14 2023 -0500

                    fix final error

                commit 615b8b38c0a0dfe8bbf9f848e206b53a65213fcd
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 23:22:54 2023 -0500

                    fix all but one decl

                commit f1ba8d3af00c51c66649bdd53230d9a02ed2065b
                Merge: 40cb0473 69d5e246
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 21:21:58 2023 -0500

                    Merge branch 'port/CategoryTheory.Category.Ulift' into port/CategoryTheory.Limits.HasLimits

                commit 40cb0473a05dc70f09db799ceca9f7b94e410424
                Merge: 5eddc98d f580834a
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 21:21:11 2023 -0500

                    Merge branch 'port/CategoryTheory.Limits.IsLimit' into port/CategoryTheory.Limits.HasLimits

                commit 5eddc98d0ebb5eb10a12505a35d58d3a910c4ec9
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 21:19:06 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 102155013addcae4cdb7d346a6ef3368aa2bea8f
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 21:19:06 2023 -0500

                    Initial file copy from mathport

                commit 2c2749ca573ce102440e5d3c60d1f262503a9afb
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 21:19:06 2023 -0500

                    feat: port CategoryTheory.Limits.HasLimits

                commit 69d5e246e8949f91971811cd5211bbf71de8b743
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 17:20:51 2023 -0500

                    lint

                commit 7509f249c55386d4a02b0996aa5c9f2c3e4a10f7
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 15:36:05 2023 -0500

                    fix errors

                    warning: hacky

                commit 1730c0d062af4381d8fc4cb04fa0910b2fc3cdbc
                Merge: c32ab52a c22f5070
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 18 08:51:21 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.Category.Ulift

                commit f580834ac1c004d4516ed2437e4808c153694fac
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 22:31:54 2023 -0500

                    lint

                commit 950fce510e45e380b579177460dcd7b56e8a0f40
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 22:08:21 2023 -0500

                    fix errors

                commit 345909017e093d875fe3cc383d5ea33071d8a8a5
                Merge: 88d6a645 e1a7f989
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 19:22:29 2023 -0500

                    Merge branch 'port/CategoryTheory.Limits.Cones' into port/CategoryTheory.Limits.IsLimit

                commit 88d6a64570665207979536195931660a23b636a0
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 19:20:57 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 0644127943eb77947b6ba62a3bbc734ac9accee2
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 19:20:57 2023 -0500

                    Initial file copy from mathport

                commit 1b09be99a4c87386cb46c762f9d8b024d630826d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 19:20:57 2023 -0500

                    feat: port CategoryTheory.Limits.IsLimit

                commit e1a7f9895bd2c4846fba5383c5e4f9d5463bb60c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 19:10:12 2023 -0500

                    lint

                commit 8d19aa905c08e582695bf3de8de828ce99a42339
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 16:29:22 2023 -0500

                    fix errors

                commit ea4b2759f6e3615c49edffe607d361cddf8850b6
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 17 09:09:06 2023 -0500

                    fix some more

                commit 86f2d01767ca9a03c5513cde111ef02d6914d971
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 23:47:10 2023 -0500

                    fix some errors

                commit 0185da3b3bb330be908826a98ba8553974d0581e
                Merge: 1fa3691c 7f41cf3e
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 23:01:59 2023 -0500

                    Merge branch 'port/CategoryTheory.Functor.ReflectsIsomorphisms' into port/CategoryTheory.Limits.Cones

                commit 1fa3691c0d8891d803e69de8f816deec03a219d3
                Merge: ab990e73 24c70cbb
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 23:00:56 2023 -0500

                    Merge branch 'port/CategoryTheory.DiscreteCategory' into port/CategoryTheory.Limits.Cones

                commit ab990e73ee4b7ad6f89553e01d0a59ed25074717
                Merge: 1c318313 37804c73
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 23:00:36 2023 -0500

                    Merge branch 'port/CategoryTheory.Yoneda' into port/CategoryTheory.Limits.Cones

                commit 1c31831334ebc9719047d6959ed54f8f27088d44
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 22:59:12 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 8beaf77097eabe84bffb0d26a9c99ed176a75411
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 22:59:12 2023 -0500

                    Initial file copy from mathport

                commit 9e93b3f3c49ec2c492c1c5f4d06cf179e5e08aef
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 22:59:11 2023 -0500

                    feat: port CategoryTheory.Limits.Cones

                commit 37804c731698bd81deec996e09179b50799ed7ce
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 22:48:37 2023 -0500

                    fix last errors; lint

                commit cbe8924b05c4cd7aad47770f33fe8dfdedd3ada8
                Merge: ea56ec58 68e722a8
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 22:07:55 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.Yoneda

                commit 7f41cf3e83e6504ef6a51c98a584bfeddb7e8e6d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 21:56:57 2023 -0500

                    fix errors; lint; shorten filename

                commit 5d6e14e26fdc1f553b6a5b647715bd5e358cb01d
                Merge: f1035364 936a0113
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 21:51:58 2023 -0500

                    Merge branch 'port/CategoryTheory.Functor.EpiMono' into port/CategoryTheory.Functor.ReflectsIsomorphisms

                commit f10353648b41fda6604f9f113a28f0cf4a98d9fa
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 21:51:28 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 1fe7733c0208090554e299b8064bd0c91dbe4d6c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 21:51:28 2023 -0500

                    Initial file copy from mathport

                commit e91cd26b896609fca086d8063f34df1e7c0bc8b3
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 21:51:28 2023 -0500

                    feat: port CategoryTheory.Functor.ReflectsIsomorphisms

                commit 936a01130bd821e2f77c219d863452cfe2442e32
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 21:45:18 2023 -0500

                    fix errors; lint

                commit 0552b426c7e2677435b39ce196eda3bfb4d006c0
                Merge: 2bf91beb 084cffd3
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:57:23 2023 -0500

                    Merge branch 'port/CategoryTheory.Limits.Shapes.StrongEpi' into port/CategoryTheory.Functor.EpiMono

                commit 2bf91beb8945490cdfc2ae17dff523b10df4483f
                Merge: a8492d25 e296a228
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:57:02 2023 -0500

                    Merge branch 'port/CategoryTheory.LiftingProperties.Adjunction' into port/CategoryTheory.Functor.EpiMono

                commit a8492d25b2be69fff94027f95d2a88610afafaaa
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:54:23 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 1aaf0634f5ef32b714115b0b9269e372c33b4c71
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:54:23 2023 -0500

                    Initial file copy from mathport

                commit b71ba2c67dc73e042653f5323707acf7f97fc40c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:54:23 2023 -0500

                    feat: port CategoryTheory.Functor.EpiMono

                commit ea56ec586f895b600d33d1af80a55e08296a696f
                Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
                Date:   Thu Feb 16 20:53:18 2023 -0500

                    Delete start_port-macos.sh

                commit 084cffd36c2ebc0cef803306cb46853280ba0668
                Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
                Date:   Thu Feb 16 20:52:10 2023 -0500

                    Delete start_port-macos.sh

                commit e296a228228bacf1f27d6f9ac7a9c0478a05bea2
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:43:39 2023 -0500

                    fix errors; lint

                commit db380ce3dce26cb3b0a6b22fdbaccffedbffc6ba
                Merge: 43628fba 0e077343
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:31:17 2023 -0500

                    Merge branch 'port/CategoryTheory.Adjunction.Basic' into port/CategoryTheory.LiftingProperties.Adjunction

                commit 43628fbaaf39b332fb60e876b2e4b9e0ac2a1cf7
                Merge: f80301f4 6a1bbf0b
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:30:56 2023 -0500

                    Merge branch 'port/CategoryTheory.LiftingProperties.Basic' into port/CategoryTheory.LiftingProperties.Adjunction

                commit f80301f4b52e3561d9cd011a37214151d164fb17
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:28:27 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit fc177c8bfcfb00763f829f6c32ccdac3ae6121c3
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:28:27 2023 -0500

                    Initial file copy from mathport

                commit 12c4a61f8b1e0a74354e0e36a022320f822b915c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:28:27 2023 -0500

                    feat: port CategoryTheory.LiftingProperties.Adjunction

                commit 24c70cbb23f140fc451716c7d346ac4c19888da6
                Merge: 38a89b87 18f8822c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:20:59 2023 -0500

                    Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.DiscreteCategory' into port/CategoryTheory.DiscreteCategory

                commit 38a89b87e6655d9e89c6b89032e22096d94d24b5
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:20:24 2023 -0500

                    lint some more

                commit 18f8822c79724d281f17886fd67d55461d5a867e
                Merge: eb146446 68e722a8
                Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
                Date:   Thu Feb 16 20:16:53 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.DiscreteCategory

                commit eb1464469358a6a9502a0b8ddaba399068e45293
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 20:14:21 2023 -0500

                    lint

                commit 5e558ae23775522c1c7774bada74f2a2477c7e4d
                Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
                Date:   Thu Feb 16 20:14:04 2023 -0500

                    Update Mathlib.lean

                commit 118d7ed86fd869f52d3f1a07923a4ebcf2242be8
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 19:57:39 2023 -0500

                    fix errors; lint

                commit 8860e0dbee2c5b58a3e890ba3447af0443052316
                Author: adamtopaz <github@adamtopaz.com>
                Date:   Thu Feb 16 17:33:00 2023 -0700

                    get file to build

                commit cbc27d710ea28f74eded3d77da143f5aca33dfb1
                Merge: d9d73661 6a1bbf0b
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:55:18 2023 -0500

                    Merge branch 'port/CategoryTheory.LiftingProperties.Basic' into port/CategoryTheory.Limits.Shapes.StrongEpi

                commit d9d7366134998e4fac6df9bb9c98113d454ac39d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:54:09 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 1979ee1cc3e427404bba9a46653d436f51ee2960
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:54:09 2023 -0500

                    Initial file copy from mathport

                commit 4ebb6e167f419bf5ae0ae3dd1428b6a307bb4500
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:54:09 2023 -0500

                    feat: port CategoryTheory.Limits.Shapes.StrongEpi

                commit 6a1bbf0b253e18332c2458143174db9bb204d636
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:44:09 2023 -0500

                    fix errors; lint

                commit c6ecc99ef7bb12c518e4e46a5fbeaf569f3c0b83
                Merge: bd1174bf 332636e7
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:34:28 2023 -0500

                    Merge branch 'port/CategoryTheory.CommSq' into port/CategoryTheory.LiftingProperties.Basic

                commit bd1174bfeac59e971bdd020bc8d5bada65d5c45b
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:25:51 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit e49ab39736ed2ab5eb8f0932df657b9f172be70a
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:25:51 2023 -0500

                    Initial file copy from mathport

                commit 4968e1930ea358a28f15e5c91ee3893641e13f84
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 18:25:50 2023 -0500

                    feat: port CategoryTheory.LiftingProperties.Basic

                commit 332636e77bb683528ae78319fde579f5161ea414
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 21:43:02 2023 +0100

                    remove spurious edit

                commit 45532e0e360404240de1f7548aa8f17cd8043765
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 21:38:40 2023 +0100

                    fix lint

                commit 2e1beb73c300a888ee6875801c111562ff2a543a
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 21:20:51 2023 +0100

                    names and removing restate_axiom

                commit ca10bfb783814ba6eae8969b2efac1f518f912d7
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 21:02:54 2023 +0100

                    first pass

                commit 8e67aa7ef360a9dfb3d0b148287069f625b5eff0
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 20:42:37 2023 +0100

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit b108a9db4790757011118df697a33081815cfb64
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 20:42:37 2023 +0100

                    Initial file copy from mathport

                commit 5fedaef75b579d43b6c673749ca5a6ad605172e8
                Author: Moritz Firsching <firsching@google.com>
                Date:   Thu Feb 16 20:42:37 2023 +0100

                    feat: port CategoryTheory.CommSq

                commit 0e077343138b6fee647400c24e7070429f8f3577
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 14:38:55 2023 -0500

                    restore lost import line

                commit 3603497c98fe27899475c05bedd76d299af605b4
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 14:25:11 2023 -0500

                    add missing aligns for fields; lint

                commit cda62ddb04c2afb8dae55cce4676d1967252af07
                Merge: ccb1de54 6fa803ed
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 16 14:07:03 2023 -0500

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

                commit c32ab52aa5d5b08659d981201046142b7e611fb7
                Author: Yury G. Kudryashov <urkud@urkud.name>
                Date:   Thu Feb 16 00:51:38 2023 -0600

                    Fix

                commit bd29faa4ca19421dccd2b0124344c6a74ba21f75
                Author: Yury G. Kudryashov <urkud@urkud.name>
                Date:   Thu Feb 16 00:18:36 2023 -0600

                    Rename file

                commit 5d9a97b37d4447dc62499aa3fd50b299138cc792
                Author: Yury G. Kudryashov <urkud@urkud.name>
                Date:   Thu Feb 16 00:17:51 2023 -0600

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 02606a14da9b726ec04ddc00fb84e0d81f251bda
                Author: Yury G. Kudryashov <urkud@urkud.name>
                Date:   Thu Feb 16 00:17:51 2023 -0600

                    Initial file copy from mathport

                commit 72de17f4c749507f92b0cfbe8699f13044386adb
                Author: Yury G. Kudryashov <urkud@urkud.name>
                Date:   Thu Feb 16 00:17:51 2023 -0600

                    feat: port CategoryTheory.Category.Ulift

                commit ccb1de541ebe73e857f02ff9b674fe4509be6ffd
                Author: mpenciak <matej.penciak@gmail.com>
                Date:   Wed Feb 15 17:26:37 2023 -0500

                    fix most linter issues

                commit 3f4e45919f4e564f48577f349569d7694748ae99
                Merge: 8981ee1d dfb03545
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 14:45:27 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.Yoneda

                commit 5b11f3d9912b56e6f758fc83ca9cfa78f48770f3
                Author: mpenciak <matej.penciak@gmail.com>
                Date:   Wed Feb 15 14:29:42 2023 -0500

                    fill in some docstrings

                commit 8981ee1d62f837168758c37b572af2f5d04fe6f2
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 12:29:50 2023 -0500

                    fix all but four

                commit dadd6da033ff3197bceb38937a855f7aff064df6
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 09:40:49 2023 -0500

                    minor fixes

                commit 8a683dd0861f9755b384525d3707a3e9af5278b9
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 01:13:21 2023 -0500

                    fix some errors

                commit 70bf280adaf71683cb9fe368e9c9ce3e6db2585e
                Merge: 155f1737 278e1103
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 00:43:16 2023 -0500

                    Merge branch 'port/CategoryTheory.Functor.Hom' into port/CategoryTheory.Yoneda

                commit 155f1737a1d36f227f35f6012da296ca0d7bbade
                Merge: 3a22ebfc 92feef62
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 00:41:22 2023 -0500

                    Merge branch 'port/CategoryTheory.Functor.Currying' into port/CategoryTheory.Yoneda

                commit 3a22ebfc6b3d40a01f30fded3482451ee5dd93f6
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 00:40:41 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 5a1eb5b7785c20cddeb69e8262ce57740cd40546
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 00:40:41 2023 -0500

                    Initial file copy from mathport

                commit 26291ab73ffbe15322093e80cbaccf07be7002d1
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 00:40:41 2023 -0500

                    feat: port CategoryTheory.Yoneda

                commit 92feef62cbf017eefc2d5fad5646e5bd62463437
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 15 00:36:52 2023 -0500

                    fix last errors

                commit 22034856ebc97b161fcc7b9d476049ebeeb8daca
                Author: adamtopaz <github@adamtopaz.com>
                Date:   Tue Feb 14 22:06:54 2023 -0700

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 10bf4bb690318c385e5fa84948e4d987ad115bd9
                Author: adamtopaz <github@adamtopaz.com>
                Date:   Tue Feb 14 22:06:54 2023 -0700

                    Initial file copy from mathport

                commit 82e25124b8f38e2494e781bf4c1fd0ab432effc0
                Author: adamtopaz <github@adamtopaz.com>
                Date:   Tue Feb 14 22:06:54 2023 -0700

                    feat: port CategoryTheory.DiscreteCategory

                commit d4926192e3d1dff291e56f2e1ba3d3127b62e77e
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 23:34:11 2023 -0500

                    fix all but one decl

                commit f147507b8876443f930b7e9de0fed695e3980e69
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:56:08 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 2b3c437f0d93d63e52c27c162919ed29b4e0767a
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:56:08 2023 -0500

                    Initial file copy from mathport

                commit 2e8b88faa086edb0f3b26c1ca2e0c7e7c32d3856
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:56:08 2023 -0500

                    feat: port CategoryTheory.Functor.Currying

                commit 278e1103f53fa6da1a06fa9333c0092ed95618f1
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:50:46 2023 -0500

                    fix error

                commit 4891412b30bb0b9836e423991c224c05e085b153
                Merge: b163ac1b 2b370d2a
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:41:32 2023 -0500

                    Merge branch 'port/CategoryTheory.Types' into port/CategoryTheory.Functor.Hom

                commit b163ac1b57aeb7a2e3ca7ae1b18160e5d1adb736
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:41:16 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit d5ec61a73bba5f5e0180c17b677153d734f48b7f
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:41:16 2023 -0500

                    Initial file copy from mathport

                commit 7fe5c64ff3e38f6ac33c4a2577f5e45946be5413
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:41:16 2023 -0500

                    feat: port CategoryTheory.Functor.Hom

                commit 2b370d2ab4d5b6d9da8cb7eb43203e3acc8f1601
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 22:32:42 2023 -0500

                    fix errors; lint; add porting note

                commit abef74aed56a7beba54f2cba778ca76457b57210
                Merge: b6d5b6ed e1d3cf34
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 21:14:12 2023 -0500

                    Merge branch 'port/CategoryTheory.EpiMono' into port/CategoryTheory.Types

                commit b6d5b6ed4538f6b81b1a24460e3d045d6998c7f4
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 21:13:52 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit e25276059ba4479b7ff463e5a3db3da6a803e2ed
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 21:13:52 2023 -0500

                    Initial file copy from mathport

                commit 8c3a9c0724b27236fa3bdb41b132ac246195f16e
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 21:13:52 2023 -0500

                    feat: port CategoryTheory.Types

                commit e1d3cf34b386125ca57fbc8a6a939f5a51b4c3e5
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 20:57:45 2023 -0500

                    fix errors; lint; add porting notes

                commit 67a95480335866d012eabc186821ded5b060de2c
                Merge: 985720e0 9b2cb68a
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 20:03:43 2023 -0500

                    Merge branch 'port/CategoryTheory.Groupoid' into port/CategoryTheory.EpiMono

                commit 985720e0a47244e6a348049f8583ebc479cf58c0
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 20:02:31 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 7f4258066570dbb31d80a289e302c5359055b327
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 20:02:31 2023 -0500

                    Initial file copy from mathport

                commit e2aebba7aad66d6feb4b27767e682faadaf7834d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 20:02:31 2023 -0500

                    feat: port CategoryTheory.EpiMono

                commit 9b2cb68ad3aad071c74083893ff77406d07b53ce
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 19:46:46 2023 -0500

                    lint

                commit 7598ce4d98b3d216174eb82b967c5ca242edece0
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 19:35:41 2023 -0500

                    fix errors

                commit ee114ee578264c457aeacbf16885addedb398722
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 14:39:58 2023 -0500

                    initial pass

                commit a1adaec4028006d73fa485c866bc285f835fc502
                Merge: e2cfafa2 b49b6cc2
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 14:11:58 2023 -0500

                    Merge branch 'port/CategoryTheory.Pi.Basic' into port/CategoryTheory.Groupoid

                commit e2cfafa230c27afef0986c8b42a131c46ce1a1c3
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 14:10:41 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 466cb9fa0a505cd7c33e616a612acdfc51b18746
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 14:10:41 2023 -0500

                    Initial file copy from mathport

                commit 5d61758e863afe09236dc99758cfb32a5912ca0e
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 14:10:41 2023 -0500

                    feat: port CategoryTheory.Groupoid

                commit b49b6cc2954b12aa020e15edc836a4a8a4ee710d
                Merge: b0fba355 0f5ac2f7
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 14:01:22 2023 -0500

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

                commit b0fba3552d171b19772d83849291ef8100853706
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 13:57:46 2023 -0500

                    add porting note about proliferation of match

                commit 7cbd34da5d3af38cdf96b25c863e22158f4acc99
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 13:55:57 2023 -0500

                    add porting note for scary warning

                commit c1897788f9f7e0db3e9e597eceba0c9b9dcb33ad
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 13:50:07 2023 -0500

                    lint

                commit ebdee62603ecb810215bf8efb9c21fce4d702269
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 13:39:09 2023 -0500

                    finally fixed

                commit 23193580c24720bcbb06941b3ec1ceb2cdb3e3f8
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 10:07:44 2023 -0500

                    more fixes

                commit 200151823064ee08abfe63067eaadad8cd4f4875
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 07:30:31 2023 -0500

                    some more fixes

                commit 051b55e70988fdafa20f912097779667b0edb535
                Merge: df3b93ee 364f4696
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 14 06:34:29 2023 -0500

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

                commit 4d3bf86b12c08c68db4784ed37f47b96aceef3ee
                Author: Johan Commelin <johan@commelin.net>
                Date:   Tue Feb 14 07:42:47 2023 +0100

                    fix two simpNF lints

                commit 0e48e0e5e009a59784fe9f418ec5d0bb502c6c93
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Mon Feb 13 12:30:08 2023 -0500

                    fix comments

                commit 671edf63e9b9de977d878dcc2bd4481dd330aba4
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Mon Feb 13 11:32:00 2023 -0500

                    delete linter command

                commit 0914b9d0a55cc46a3204805ae989da5192f9bbbb
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Mon Feb 13 11:31:31 2023 -0500

                    break long lines

                commit df3b93eea099b92ba7c58d235d1b9e9f0449df62
                Merge: 81363073 10bfe189
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Mon Feb 13 10:24:08 2023 -0500

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

                commit 1f56a41b344cb16296a6c6fc4260aa26fdd0f809
                Author: mpenciak <matej.penciak@gmail.com>
                Date:   Mon Feb 13 01:14:36 2023 -0500

                    filled in last sorry

                commit 813630737bce52dc18e8f0ca4ce2e52838d44b10
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 11 22:25:59 2023 -0500

                    fix some errors

                commit a4ea90f81f619c7cba6abb7545982d69a5d7ada4
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 11 20:38:11 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 8414826065094327362452132ae9b8020f89df88
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 11 20:38:10 2023 -0500

                    Initial file copy from mathport

                commit b3e68ca52a36b1639c2e24c8b03664f55658d05f
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 11 20:38:10 2023 -0500

                    feat: port CategoryTheory.Pi.Basic

                commit fc93825bf7c5d5d772835cfa2d58f7c04939e7cb
                Merge: 3278d7df a4297454
                Author: Johan Commelin <johan@commelin.net>
                Date:   Sat Feb 11 17:21:51 2023 +0100

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

                commit 3278d7dfbbe23ee4a65f304d478c30b1733ab5ae
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Sat Feb 11 06:49:21 2023 -0500

                    only one error left

                commit cfe5dc1f7ceede7309c956343bdca17cbe0de5c7
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Fri Feb 10 20:43:41 2023 -0500

                    some progress

                commit 3809ccc0b0ee4a43f39dc0d9da06299fd64fe6e3
                Merge: e0de1980 8306c5ff
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Thu Feb 9 13:50:33 2023 -0500

                    Merge remote-tracking branch 'origin/port/CategoryTheory.Equivalence' into port/CategoryTheory.Adjunction.Basic

                commit e0de19809e25a0da91f9b856757b72ef74403e29
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Thu Feb 9 13:49:59 2023 -0500

                    automated fixes

                    Mathbin -> Mathlib

                    fix certain import statements

                    move "by" to end of line

                    add import to Mathlib.lean

                commit 5bde22616c0eb101abbbb494ca351efbaa58e2a1
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Thu Feb 9 13:49:57 2023 -0500

                    Initial file copy from mathport

                commit bcc402f2fcb6d43de80c6eaac7fcfc1f038186b7
                Author: Matej Penciak <matej.penciak@gmail.com>
                Date:   Thu Feb 9 13:49:56 2023 -0500

                    feat: port CategoryTheory.Adjunction.Basic

                commit 8306c5ff6cf09e66a02e6822d1678665db32e20c
                Merge: 68bcb258 6c1fbbf5
                Author: Henrik Böving <hargonix@gmail.com>
                Date:   Thu Feb 9 18:41:54 2023 +0100

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

                commit 68bcb25836d05802bd01597aea7c554a927cc3f7
                Merge: e6ec9246 bac7310c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Thu Feb 9 11:51:47 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.Equivalence

                commit e6ec92461ccdb71348ed8a5cc8970ccdd0bd3fe7
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 15:26:24 2023 -0500

                    update slice naming

                commit cf945f0fd56fff6aaa43ac7f7e78742b56625e7b
                Merge: 0c247c70 ce383e4b
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 15:25:02 2023 -0500

                    Merge branch 'slice' into port/CategoryTheory.Equivalence

                commit ce383e4b8827543f5159043d7336daf84397233f
                Author: thorimur <68410468+thorimur@users.noreply.github.com>
                Date:   Wed Feb 8 15:14:47 2023 -0500

                    minor changes to `Tactic.Core`
                    * use `m` instead of `TacticM` now that we use `MonadExcept`
                    * simplify code for `iterateRange`
                    * minor docs tweaks

                commit 80596f2643b17886668466a6c58802db2692817c
                Author: thorimur <68410468+thorimur@users.noreply.github.com>
                Date:   Wed Feb 8 14:58:19 2023 -0500

                    test: add simple `rhs`/`lhs` tests

                commit 2c56111eafac3bdc6298b3b4bfec8bc209fc8c92
                Author: thorimur <68410468+thorimur@users.noreply.github.com>
                Date:   Wed Feb 8 14:57:53 2023 -0500

                    use `Mathport` syntax
                    * use existing docs
                    * fix docs typos

                commit 0c247c701c0a6f511f9483a88d9c38e7966af99a
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 14:19:58 2023 -0500

                    fix final long line

                commit 2c8c8a74a92cf0e19914fe47d679e40adde0564d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 14:15:47 2023 -0500

                    fix refl error and lint errors

                commit 7140d1c4c844f59c3f16ba2e2a3681cec306643c
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 12:48:18 2023 -0500

                    fix all but refl error

                commit 06c4b46a9f84cfe531b1b717b18934bb10622385
                Merge: 88ac2d09 6bae31a1
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 12:23:47 2023 -0500

                    Merge branch 'slice' into port/CategoryTheory.Equivalence

                commit 6bae31a152336995e8aa9bc953fc9aa7ae266df0
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 12:05:58 2023 -0500

                    fix test/slice.lean

                commit 388aaa03c4b09f991b25b230ffa4086bb9ffafc1
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:51:12 2023 -0500

                    fix module docs

                commit 88ac2d092283f14cb556320e9eb71ca0eccee8f4
                Merge: 8256a85b 720d3112
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:33:05 2023 -0500

                    Merge branch 'slice' into port/CategoryTheory.Equivalence

                commit 8256a85b5a1300254f6311e8dc6520d7be89787d
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:32:20 2023 -0500

                    minor changes

                commit 720d3112e3d6761c8520455cad9a208bf4f14380
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:30:40 2023 -0500

                    add module documentation(?)

                commit 319fa30f96cbc9d4bdaeb654f12da65ee34c1c29
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:11:35 2023 -0500

                    modify documentation lines

                commit 69bbb9346f7e9bad98ef050eac82c1a63d55dcdc
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:08:38 2023 -0500

                    add slice to global import file

                commit 3c369ce1bb7ec4a6689730f20ab566dc48c28129
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:05:43 2023 -0500

                    move iteration tactics to core

                commit adb9495093314e4df79c094197e8646d395d0de4
                Merge: 84ddfcb9 c16c0c41
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:01:49 2023 -0500

                    Merge branch 'master' into slice

                commit 84ddfcb900a73c679d770e47eebe2fdb7770e579
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 10:00:38 2023 -0500

                    add documentation and clean up

                commit ef7ef69d790cee30f8d56ffdce215e9451058ae7
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 09:37:50 2023 -0500

                    remove rewriteTarget'; change MonadExceptOf to MonadExcept

                commit eedfb6167e983bd14ec76e3cbead7978121cc103
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 09:36:08 2023 -0500

                    remove equivalence.lean

                commit afafdf07856bc3dc0cf1d12594ddd95af69fef1a
                Merge: c76b450c c16c0c41
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Wed Feb 8 09:15:56 2023 -0500

                    Merge branch 'master' into port/CategoryTheory.Equivalence

                commit 92e65beac07e193b862f7f15a68bdb38af99da6f
                Author: thorimur <68410468+thorimur@users.noreply.github.com>
                Date:   Tue Feb 7 16:09:09 2023 -0500

                    test: create `slice.lean` test file

                commit 91f541a86962d4423416dd7573883a95bbb71934
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Tue Feb 7 14:00:33 2023 -0500

                    add example and equivalence file for testing

                commit f0f65020500fe71f52cca6477686ec43400ee9a2
                Author: Matthew Ballard <matt@mrb.email>
                Date:   Fri Feb 3 17:00:44 2023 -0500

                    seems to work

                commit c76b450c682b2e03c93f9f4c5251a0bd37af0a55
                Merge: afd9aed6 98c12958
                Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
                Date:   Tue Jan 17 14:29:14 2023 +0100

                    Merge branch 'master' into port/CategoryTheory.Equivalence

                commit afd9aed6550ed5f7bc5eb86cc41ba21af45bfa20
                Author: Henrik Böving <hargonix@gmail.com>
                Date:   Mon Jan 2 13:21:50 2023 +0100

                    push it as far as possible

                commit bc9467dcbd72b32db46289f388ecfe931d10aeca
                Author: Henrik Böving <hargonix@gmail.com>
                Date:   Sun Jan 1 17:57:13 2023 +0100

                    Mathbin -> Mathlib; add import to Mathlib.lean

                commit 01c7d9eb2cc39f51491c395482a7bf80340eb3bf
                Author: Henrik Böving <hargonix@gmail.com>
                Date:   Sun Jan 1 17:57:13 2023 +0100

                    Initial file copy from mathport

            commit 73d983ec91f35ab2f38aa651f22fdd984541c300
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 18:47:46 2023 -0500

                automated fixes

                Mathbin -> Mathlib

                fix certain import statements

                move "by" to end of line

                add import to Mathlib.lean

            commit 86755fbbf956a882fa2951150c1e734609576b4d
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 18:47:46 2023 -0500

                Initial file copy from mathport

            commit f41f8c48994b8b71cf9f21d37d03389b90706071
            Author: Matthew Ballard <matt@mrb.email>
            Date:   Wed Feb 22 18:47:46 2023 -0500

                feat: port CategoryTheory.Limits.Shapes.Terminal

        commit 7aa918360b25faa78c85e328bbe53221351dd315
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 21:10:09 2023 -0500

            automated fixes

            Mathbin -> Mathlib

            fix certain import statements

            move "by" to end of line

            add import to Mathlib.lean

        commit c71f6119d0b1e0ce12af5ff452d2ea4089e23116
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 21:10:09 2023 -0500

            Initial file copy from mathport

        commit c2f50a6b1d77cc58af4079f23723024bd2702b86
        Author: Matthew Ballard <matt@mrb.email>
        Date:   Fri Feb 24 21:10:09 2023 -0500

            feat: port CategoryTheory.Over

    commit 6fced213166c0283529be17ac8e77a4547cdb99a
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sat Feb 25 20:04:01 2023 -0500

        automated fixes

        Mathbin -> Mathlib

        fix certain import statements

        move "by" to end of line

        add import to Mathlib.lean

    commit dad96813dbb0bda3147d6067ab1b8c221d9ae467
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sat Feb 25 20:04:01 2023 -0500

        Initial file copy from mathport

    commit f6d96cc9ae4f9804dfda1146e3166f6ea97e6494
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Sat Feb 25 20:04:01 2023 -0500

        feat: port CategoryTheory.Limits.Shapes.BinaryProducts

commit 766e8f699c3e845ece0bb1ea5d066ddf0e362f3d
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 17:23:35 2023 -0500

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit c7f02a1fab5197d274b133bf88dea24f5e6fb1e5
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 17:23:35 2023 -0500

    Initial file copy from mathport

commit 7aff00b424427a3cef1e087da66a84de42e99039
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 26 17:23:35 2023 -0500

    feat: port CategoryTheory.Limits.Shapes.Pullbacks
@mattrobball
out damn spot
163469d
@mattrobball
update dependency
3e83357
@mattrobball
fix errors; lint; fix names
c9f968c
@mattrobball mattrobball added the mathlib-port This is a port of a theory file from mathlib. label Mar 2, 2023
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR which is still in the queue. merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Mar 2, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@mattrobball mattrobball added the awaiting-review The author would like community review of the PR label Mar 7, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 7, 2023
@mattrobball mattrobball mentioned this pull request Mar 7, 2023
Closed
1 task
jcommelin
jcommelin reviewed Mar 7, 2023
View reviewed changes
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean Outdated
/-- The property of preserving pullbacks expressed in terms of binary fans. -/
def isLimitPullbackConeMapOfIsLimit [PreservesLimit (cospan f g) G]
(l : IsLimit (PullbackCone.mk h k comm)) :
-- Porting note: help figure out the hole
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please make this note a bit more explicit. I don't understand it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh. This one probably doesn't rise to the level of a porting note. I had to fill in h and k similarly for the others.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, in that case, please remove the note (-;

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean Outdated

/-- The property of reflecting pullbacks expressed in terms of binary fans. -/
def isLimitOfIsLimitPullbackConeMap [ReflectsLimit (cospan f g) G]
-- Porting note: more typeclass help
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In what sense?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean Outdated
/-- If `G` preserves pullbacks and `C` has them, then the pullback cone constructed of the mapped
morphisms of the pullback cone is a limit. -/
def isLimitOfHasPullbackOfPreservesLimit [i : HasPullback f g] :
-- Porting note: more typeclass help
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Idem.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed

jcommelin
jcommelin approved these changes Mar 7, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 7, 2023
bors bot pushed a commit that referenced this pull request Mar 7, 2023
@mattrobball
feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks (#2571)
b96f777
@bors
Copy link

bors bot commented Mar 7, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks [Merged by Bors] - feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks Mar 7, 2023
@bors bors bot closed this Mar 7, 2023
@bors bors bot deleted the port/CategoryTheory.Limits.Preserves.Shapes.Pullbacks branch March 7, 2023 15:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@mattrobball @semorrison @jcommelin