Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

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

Closed
wants to merge 161 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
161 commits
Select commit Hold shift + click to select a range
01c7d9e
Initial file copy from mathport
hargoniX Jan 1, 2023
bc9467d
Mathbin -> Mathlib; add import to Mathlib.lean
hargoniX Jan 1, 2023
afd9aed
push it as far as possible
hargoniX Jan 2, 2023
c76b450
Merge branch 'master' into port/CategoryTheory.Equivalence
Ruben-VandeVelde Jan 17, 2023
f0f6502
seems to work
mattrobball Feb 3, 2023
91f541a
add example and equivalence file for testing
mattrobball Feb 7, 2023
92e65be
test: create `slice.lean` test file
thorimur Feb 7, 2023
afafdf0
Merge branch 'master' into port/CategoryTheory.Equivalence
mattrobball Feb 8, 2023
eedfb61
remove equivalence.lean
mattrobball Feb 8, 2023
ef7ef69
remove rewriteTarget'; change MonadExceptOf to MonadExcept
mattrobball Feb 8, 2023
84ddfcb
add documentation and clean up
mattrobball Feb 8, 2023
adb9495
Merge branch 'master' into slice
mattrobball Feb 8, 2023
3c369ce
move iteration tactics to core
mattrobball Feb 8, 2023
69bbb93
add slice to global import file
mattrobball Feb 8, 2023
319fa30
modify documentation lines
mattrobball Feb 8, 2023
720d311
add module documentation(?)
mattrobball Feb 8, 2023
8256a85
minor changes
mattrobball Feb 8, 2023
88ac2d0
Merge branch 'slice' into port/CategoryTheory.Equivalence
mattrobball Feb 8, 2023
388aaa0
fix module docs
mattrobball Feb 8, 2023
6bae31a
fix test/slice.lean
mattrobball Feb 8, 2023
06c4b46
Merge branch 'slice' into port/CategoryTheory.Equivalence
mattrobball Feb 8, 2023
7140d1c
fix all but refl error
mattrobball Feb 8, 2023
2c8c8a7
fix refl error and lint errors
mattrobball Feb 8, 2023
0c247c7
fix final long line
mattrobball Feb 8, 2023
2c56111
use `Mathport` syntax
thorimur Feb 8, 2023
80596f2
test: add simple `rhs`/`lhs` tests
thorimur Feb 8, 2023
ce383e4
minor changes to `Tactic.Core`
thorimur Feb 8, 2023
cf945f0
Merge branch 'slice' into port/CategoryTheory.Equivalence
mattrobball Feb 8, 2023
e6ec924
update slice naming
mattrobball Feb 8, 2023
68bcb25
Merge branch 'master' into port/CategoryTheory.Equivalence
mattrobball Feb 9, 2023
8306c5f
Merge remote-tracking branch 'origin/master' into port/CategoryTheory…
hargoniX Feb 9, 2023
bcc402f
feat: port CategoryTheory.Adjunction.Basic
mpenciak Feb 9, 2023
5bde226
Initial file copy from mathport
mpenciak Feb 9, 2023
e0de198
automated fixes
mpenciak Feb 9, 2023
3809ccc
Merge remote-tracking branch 'origin/port/CategoryTheory.Equivalence'…
mpenciak Feb 9, 2023
cfe5dc1
some progress
mpenciak Feb 11, 2023
3278d7d
only one error left
mattrobball Feb 11, 2023
fc93825
Merge branch 'master' into port/CategoryTheory.Adjunction.Basic
jcommelin Feb 11, 2023
b3e68ca
feat: port CategoryTheory.Pi.Basic
mattrobball Feb 12, 2023
8414826
Initial file copy from mathport
mattrobball Feb 12, 2023
a4ea90f
automated fixes
mattrobball Feb 12, 2023
8136307
fix some errors
mattrobball Feb 12, 2023
1f56a41
filled in last sorry
mpenciak Feb 13, 2023
df3b93e
Merge branch 'master' into port/CategoryTheory.Pi.Basic
mattrobball Feb 13, 2023
0914b9d
break long lines
mpenciak Feb 13, 2023
671edf6
delete linter command
mpenciak Feb 13, 2023
0e48e0e
fix comments
mpenciak Feb 13, 2023
4d3bf86
fix two simpNF lints
jcommelin Feb 14, 2023
051b55e
Merge branch 'master' into port/CategoryTheory.Pi.Basic
mattrobball Feb 14, 2023
2001518
some more fixes
mattrobball Feb 14, 2023
2319358
more fixes
mattrobball Feb 14, 2023
ebdee62
finally fixed
mattrobball Feb 14, 2023
c189778
lint
mattrobball Feb 14, 2023
7cbd34d
add porting note for scary warning
mattrobball Feb 14, 2023
b0fba35
add porting note about proliferation of match
mattrobball Feb 14, 2023
b49b6cc
Merge branch 'master' into port/CategoryTheory.Pi.Basic
mattrobball Feb 14, 2023
5d61758
feat: port CategoryTheory.Groupoid
mattrobball Feb 14, 2023
466cb9f
Initial file copy from mathport
mattrobball Feb 14, 2023
e2cfafa
automated fixes
mattrobball Feb 14, 2023
a1adaec
Merge branch 'port/CategoryTheory.Pi.Basic' into port/CategoryTheory.…
mattrobball Feb 14, 2023
ee114ee
initial pass
mattrobball Feb 14, 2023
7598ce4
fix errors
mattrobball Feb 15, 2023
9b2cb68
lint
mattrobball Feb 15, 2023
e2aebba
feat: port CategoryTheory.EpiMono
mattrobball Feb 15, 2023
7f42580
Initial file copy from mathport
mattrobball Feb 15, 2023
985720e
automated fixes
mattrobball Feb 15, 2023
67a9548
Merge branch 'port/CategoryTheory.Groupoid' into port/CategoryTheory.…
mattrobball Feb 15, 2023
e1d3cf3
fix errors; lint; add porting notes
mattrobball Feb 15, 2023
8c3a9c0
feat: port CategoryTheory.Types
mattrobball Feb 15, 2023
e252760
Initial file copy from mathport
mattrobball Feb 15, 2023
b6d5b6e
automated fixes
mattrobball Feb 15, 2023
abef74a
Merge branch 'port/CategoryTheory.EpiMono' into port/CategoryTheory.T…
mattrobball Feb 15, 2023
2b370d2
fix errors; lint; add porting note
mattrobball Feb 15, 2023
7fe5c64
feat: port CategoryTheory.Functor.Hom
mattrobball Feb 15, 2023
d5ec61a
Initial file copy from mathport
mattrobball Feb 15, 2023
b163ac1
automated fixes
mattrobball Feb 15, 2023
4891412
Merge branch 'port/CategoryTheory.Types' into port/CategoryTheory.Fun…
mattrobball Feb 15, 2023
278e110
fix error
mattrobball Feb 15, 2023
2e8b88f
feat: port CategoryTheory.Functor.Currying
mattrobball Feb 15, 2023
2b3c437
Initial file copy from mathport
mattrobball Feb 15, 2023
f147507
automated fixes
mattrobball Feb 15, 2023
d492619
fix all but one decl
mattrobball Feb 15, 2023
82e2512
feat: port CategoryTheory.DiscreteCategory
adamtopaz Feb 15, 2023
10bf4bb
Initial file copy from mathport
adamtopaz Feb 15, 2023
2203485
automated fixes
adamtopaz Feb 15, 2023
92feef6
fix last errors
mattrobball Feb 15, 2023
26291ab
feat: port CategoryTheory.Yoneda
mattrobball Feb 15, 2023
5a1eb5b
Initial file copy from mathport
mattrobball Feb 15, 2023
3a22ebf
automated fixes
mattrobball Feb 15, 2023
155f173
Merge branch 'port/CategoryTheory.Functor.Currying' into port/Categor…
mattrobball Feb 15, 2023
70bf280
Merge branch 'port/CategoryTheory.Functor.Hom' into port/CategoryTheo…
mattrobball Feb 15, 2023
8a683dd
fix some errors
mattrobball Feb 15, 2023
dadd6da
minor fixes
mattrobball Feb 15, 2023
8981ee1
fix all but four
mattrobball Feb 15, 2023
5b11f3d
fill in some docstrings
mpenciak Feb 15, 2023
3f4e459
Merge branch 'master' into port/CategoryTheory.Yoneda
mattrobball Feb 15, 2023
ccb1de5
fix most linter issues
mpenciak Feb 15, 2023
cda62dd
Merge branch 'master' into port/CategoryTheory.Adjunction.Basic
mattrobball Feb 16, 2023
3603497
add missing aligns for fields; lint
mattrobball Feb 16, 2023
0e07734
restore lost import line
mattrobball Feb 16, 2023
5fedaef
feat: port CategoryTheory.CommSq
mo271 Feb 16, 2023
b108a9d
Initial file copy from mathport
mo271 Feb 16, 2023
8e67aa7
automated fixes
mo271 Feb 16, 2023
ca10bfb
first pass
mo271 Feb 16, 2023
2e1beb7
names and removing restate_axiom
mo271 Feb 16, 2023
45532e0
fix lint
mo271 Feb 16, 2023
332636e
remove spurious edit
mo271 Feb 16, 2023
4968e19
feat: port CategoryTheory.LiftingProperties.Basic
mattrobball Feb 16, 2023
e49ab39
Initial file copy from mathport
mattrobball Feb 16, 2023
bd1174b
automated fixes
mattrobball Feb 16, 2023
c6ecc99
Merge branch 'port/CategoryTheory.CommSq' into port/CategoryTheory.Li…
mattrobball Feb 16, 2023
6a1bbf0
fix errors; lint
mattrobball Feb 16, 2023
4ebb6e1
feat: port CategoryTheory.Limits.Shapes.StrongEpi
mattrobball Feb 16, 2023
1979ee1
Initial file copy from mathport
mattrobball Feb 16, 2023
d9d7366
automated fixes
mattrobball Feb 16, 2023
cbc27d7
Merge branch 'port/CategoryTheory.LiftingProperties.Basic' into port/…
mattrobball Feb 16, 2023
8860e0d
get file to build
adamtopaz Feb 17, 2023
118d7ed
fix errors; lint
mattrobball Feb 17, 2023
5e558ae
Update Mathlib.lean
mattrobball Feb 17, 2023
eb14644
lint
mattrobball Feb 17, 2023
18f8822
Merge branch 'master' into port/CategoryTheory.DiscreteCategory
mattrobball Feb 17, 2023
38a89b8
lint some more
mattrobball Feb 17, 2023
24c70cb
Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory…
mattrobball Feb 17, 2023
12c4a61
feat: port CategoryTheory.LiftingProperties.Adjunction
mattrobball Feb 17, 2023
fc177c8
Initial file copy from mathport
mattrobball Feb 17, 2023
f80301f
automated fixes
mattrobball Feb 17, 2023
43628fb
Merge branch 'port/CategoryTheory.LiftingProperties.Basic' into port/…
mattrobball Feb 17, 2023
db380ce
Merge branch 'port/CategoryTheory.Adjunction.Basic' into port/Categor…
mattrobball Feb 17, 2023
e296a22
fix errors; lint
mattrobball Feb 17, 2023
084cffd
Delete start_port-macos.sh
mattrobball Feb 17, 2023
ea56ec5
Delete start_port-macos.sh
mattrobball Feb 17, 2023
b71ba2c
feat: port CategoryTheory.Functor.EpiMono
mattrobball Feb 17, 2023
1aaf063
Initial file copy from mathport
mattrobball Feb 17, 2023
a8492d2
automated fixes
mattrobball Feb 17, 2023
2bf91be
Merge branch 'port/CategoryTheory.LiftingProperties.Adjunction' into …
mattrobball Feb 17, 2023
0552b42
Merge branch 'port/CategoryTheory.Limits.Shapes.StrongEpi' into port/…
mattrobball Feb 17, 2023
936a011
fix errors; lint
mattrobball Feb 17, 2023
e91cd26
feat: port CategoryTheory.Functor.ReflectsIsomorphisms
mattrobball Feb 17, 2023
1fe7733
Initial file copy from mathport
mattrobball Feb 17, 2023
f103536
automated fixes
mattrobball Feb 17, 2023
5d6e14e
Merge branch 'port/CategoryTheory.Functor.EpiMono' into port/Category…
mattrobball Feb 17, 2023
7f41cf3
fix errors; lint; shorten filename
mattrobball Feb 17, 2023
cbe8924
Merge branch 'master' into port/CategoryTheory.Yoneda
mattrobball Feb 17, 2023
37804c7
fix last errors; lint
mattrobball Feb 17, 2023
9e93b3f
feat: port CategoryTheory.Limits.Cones
mattrobball Feb 17, 2023
8beaf77
Initial file copy from mathport
mattrobball Feb 17, 2023
1c31831
automated fixes
mattrobball Feb 17, 2023
ab990e7
Merge branch 'port/CategoryTheory.Yoneda' into port/CategoryTheory.Li…
mattrobball Feb 17, 2023
1fa3691
Merge branch 'port/CategoryTheory.DiscreteCategory' into port/Categor…
mattrobball Feb 17, 2023
0185da3
Merge branch 'port/CategoryTheory.Functor.ReflectsIsomorphisms' into …
mattrobball Feb 17, 2023
86f2d01
fix some errors
mattrobball Feb 17, 2023
ea4b275
fix some more
mattrobball Feb 17, 2023
8d19aa9
fix errors
mattrobball Feb 17, 2023
e1a7f98
lint
mattrobball Feb 18, 2023
bd0f2cf
add updated files
mattrobball Feb 24, 2023
039e15f
Merge branch 'master' into port/CategoryTheory.Limits.Cones
mattrobball Feb 24, 2023
64d878d
replace X with pt for cone field
mattrobball Feb 24, 2023
0ae8a12
fix import file
mattrobball Feb 24, 2023
7abe319
remove script
mattrobball Feb 24, 2023
cf0ddc2
fix one error
mattrobball Feb 24, 2023
a46ad8b
move comment
mattrobball Feb 24, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -269,6 +269,7 @@ import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.IsomorphismClasses
import Mathlib.CategoryTheory.LiftingProperties.Adjunction
import Mathlib.CategoryTheory.LiftingProperties.Basic
import Mathlib.CategoryTheory.Limits.Cones
import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
import Mathlib.CategoryTheory.Monoidal.Category
import Mathlib.CategoryTheory.Monoidal.Functor
Expand Down