[Merged by Bors] - feat: port CategoryTheory.ConcreteCategory.Basic #2619
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 4, 2023
•
mattrobball
commented
- depends on: [Merged by Bors] - feat: port CategoryTheory.Limits.Constructions.EpiMono #2573
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
commit 5c006d53f6a4b6667d6ef886cf10abe32ae469d4
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 22:50:55 2023 -0500
fix import file again
commit 64deb9c843902381a73106cfd6c7263bb86d9279
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 22:49:50 2023 -0500
fix import file
commit c9f968ce8e44cc96c979f42c6cd1bebe169f2e4c
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 22:47:08 2023 -0500
fix errors; lint; fix names
commit 3e8335717f386af8348a8b71a4bf6ddbd6e1a8ab
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 21:16:05 2023 -0500
update dependency
commit 163469d199727e750fcaf6fa5fa58320c2e15101
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 21:10:28 2023 -0500
out damn spot
commit da04b77517d04a5ccf440624d6af3a0c0c8afcd7
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 21:10:18 2023 -0500
Squashed commit of the following:
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
commit 4508cbd049c8b5333c8b3bec463f5a8746def8d6
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 21:07:36 2023 -0500
automated fixes
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
commit 041a4496929f87766850757c7e673adab622ee7b
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 21:07:36 2023 -0500
Initial file copy from mathport
commit 4ae5a00366267dcee06f1c53a4f79977f8ba381c
Author: Matthew Ballard <matt@mrb.email>
Date: Wed Mar 1 21:07:36 2023 -0500
feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks
also fix an align back in Pullbacks
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
…port/CategoryTheory.ConcreteCategory.Basic
semorrison
added
the
blocked-by-other-PR
semorrison
added
merge-conflict
|
This PR/issue depends on: |
mattrobball
added
awaiting-review
mattrobball
added
the
awaiting-review
|
bors r+ |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.