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.
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
[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes/Biproducts #2710
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
mattrobball
commented
Mar 8, 2023
•
edited
edited
- depends on: [Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.Kernels #2636
- depends on: [Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.FiniteProducts #2688
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
commit ffdced4b0cab8f90361b0aa60f01f607d82f5400 Merge: 0b0ed018 b66eff51 Author: Matthew Ballard <matt@mrb.email> Date: Tue Mar 7 12:38:39 2023 -0500 Merge branch 'master' into port/CategoryTheory.Limits.Shapes.FiniteProducts commit 0b0ed018ea8f413d3e929b85bf2830f15f99acbc Author: Matthew Ballard <matt@mrb.email> Date: Tue Mar 7 00:47:41 2023 -0500 fix errors; lint; align names commit 754aa6f1861e028b08ba4be41a67239b72f0ebc9 Author: Matthew Ballard <matt@mrb.email> Date: Tue Mar 7 00:35:02 2023 -0500 Squashed commit of the following: commit 5ca68007957bc6e0fac226c035f92af7778516a6 Author: Matthew Ballard <matt@mrb.email> Date: Sun Mar 5 08:53:09 2023 -0500 lint; align names commit 2fa0269587ea3a9e7fa4001f5747c6ec30535ba9 Author: Matthew Ballard <matt@mrb.email> Date: Sun Mar 5 07:42:08 2023 -0500 fixed errors finally commit 0348e63995ac4c90fdc2c29c281c26d3444aaf97 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 21:35:48 2023 -0500 fix some errors commit 84084c3bf7393fadf03e54f5dc40ff3fae551962 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 13:13:59 2023 -0500 Squashed commit of the following: commit c55f4c91f090284d9145962ab949d99ca2a434ad Author: Matthew Ballard <matt@mrb.email> Date: Wed Mar 1 23:28:18 2023 -0500 fix names 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 afd9aed65…
commit 84b19c91d4747aab0e46d2b845533af4752211e2 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 13:04:37 2023 -0500 fix errors; lint; align names commit f4df0b76ef8f98a4ef7ad2624f14f6bc2b46feef Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 09:48:42 2023 -0500 fix first pass commit 17a3bf3dc541b0125f996b86d21e3a8e456cb37b Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 06:41:20 2023 -0500 Squashed commit of the following: commit 54dc6ce80313301e36c1ace156b8e02d6f8d4aa2 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 00:38:17 2023 -0500 fix errors; lint; align names commit 1113c9652e4fa4b19c4c7a39ada3e0f379d7c7db Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 00:19:26 2023 -0500 update mathlib.lean commit 21937f0aa38ec48d992d773b06ba88d1846a4661 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 00:18:36 2023 -0500 Squashed commit of the following: commit 3839e2c914940a86a1ef7143892abbec867341d7 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 00:10:14 2023 -0500 fix import file commit bdbfb083e06a15f9e40357249dc6384a0ce90302 Author: Matthew Ballard <matt@mrb.email> Date: Sat Mar 4 00:06:56 2023 -0500 fix errors; lint; align names commit 635c4838895eea9f63657afb6b0eb9695b574330 Author: Matthew Ballard <matt@mrb.email> Date: Fri Mar 3 21:21:15 2023 -0500 Squashed commit of the following: commit b68570ef16d874bfcf1dc27f052f0dff65a7ed06 Author: Matthew Ballard <matt@mrb.email> Date: Fri Mar 3 18:59:02 2023 -0500 fix names commit 2eb6574419cb9417f9de90eb68db0c1cebc3feb9 Author: Matthew Ballard <matt@mrb.email> Date: Fri Mar 3 18:46:40 2023 -0500 lint commit e568a0d14c17bd7a610d4c583f149068c807752d Author: Matthew Ballard <matt@mrb.email> Date: Fri Mar 3 15:20:42 2023 -0500 fix last errors commit 3adb0b6304d76e8be2cb2f9b3fc8c8abdd1f83dd Author: Matthew Ballard <matt@mrb.email> Date: Thu Mar 2 20:50:32 2023 -0500 fix some more commit e7166bc1e20949618c20fc5cdc4c157e8f5a3c1f Author: Matthew Ballard <matt@mrb.email> Date: Thu Mar 2 14:41:52 2023 -0500 fix a few errors quickly commit 0b639f8b8b175b79a3eb0c6c52ad250a8b3f7e69 Merge: 839a79b6 c55f4c91 Author: Matthew Ballard <matt@mrb.email> Date: Thu Mar 2 14:14:55 2023 -0500 Merge branch 'port/CategoryTheory.Limits.Shapes.Pullbacks' into port/CategoryTheory.Limits.Shapes.Images commit 839a79b6a604fc9a9e90ad7c1ae464bc92d19867 Author: Matthew Ballard <matt@mrb.email> Date: Thu Mar 2 14:12:52 2023 -0500 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit 122ca716273c0e07432213d920ea00d1d3d0fc2e Author: Matthew Ballard <matt@mrb.email> Date: Thu Mar 2 14:12:52 2023 -0500 Initial file copy from mathport commit 074f15a94a9a66754d9f0f94f3865a628d403eca Author: Matthew Ballard <matt@mrb.email> Date: Thu Mar 2 14:12:52 2023 -0500 feat: port CategoryTheory.Limits.Shapes.Images commit c55f4c91f090284d9145962ab949d99ca2a434ad Author: Matthew Ballard <matt@mrb.email> Date: Wed Mar 1 23:28:18 2023 -0500 fix names 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 …
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 8, 2023
This PR/issue depends on: |
mattrobball
added
awaiting-review
The author would like community review of the PR
and removed
merge-conflict
The PR has a merge conflict with master, and needs manual merging.
labels
Mar 8, 2023
1 task
jcommelin
approved these changes
Mar 8, 2023
There was a problem hiding this 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
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 8, 2023
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
feat: port CategoryTheory.Limits.Shapes/Biproducts
[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes/Biproducts
Mar 8, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
mathlib-port
This is a port of a theory file from mathlib.
ready-to-merge
This PR has been sent to bors.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.