Skip to content
New issue

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

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.Terminal #2459

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.Terminal #2459

wants to merge 15 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Feb 23, 2023 •
edited by github-actions bot

@mattrobball
feat: port CategoryTheory.Limits.Shapes.Terminal
f41f8c4
@mattrobball
Initial file copy from mathport
86755fb
@mattrobball
automated fixes
73d983e 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mattrobball
Squashed commit of the following:
f5ba002 
commit d0a99d9
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 21 23:16:12 2023 -0500

    move names to new convention

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

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

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

    add updated files

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

    fix case error

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

    remove script

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

    fix import line typo

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

    fix import file

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

    align names in comments

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

    lint for CI

commit 73f99ea
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 20b586b
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:26:14 2023 -0500

    fix final error

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

    fix all but one decl

commit f1ba8d3
Merge: 40cb047 69d5e24
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 40cb047
Merge: 5eddc98 f580834
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 5eddc98
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 1021550
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Limits.HasLimits

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

    lint

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

    fix errors

    warning: hacky

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

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

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

    lint

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

    fix errors

commit 3459090
Merge: 88d6a64 e1a7f98
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 88d6a64
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 0644127
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 17 19:20:57 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Limits.IsLimit

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

    lint

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

    fix errors

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

    fix some more

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

    fix some errors

commit 0185da3
Merge: 1fa3691 7f41cf3
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 1fa3691
Merge: ab990e7 24c70cb
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 ab990e7
Merge: 1c31831 37804c7
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 1c31831
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 8beaf77
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 22:59:12 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Limits.Cones

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

    fix last errors; lint

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

    Merge branch 'master' into port/CategoryTheory.Yoneda

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

    fix errors; lint; shorten filename

commit 5d6e14e
Merge: f103536 936a011
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 f103536
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 1fe7733
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 21:51:28 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Functor.ReflectsIsomorphisms

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

    fix errors; lint

commit 0552b42
Merge: 2bf91be 084cffd
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 2bf91be
Merge: a8492d2 e296a22
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 a8492d2
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 1aaf063
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:54:23 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Functor.EpiMono

commit ea56ec5
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 084cffd
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 e296a22
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:43:39 2023 -0500

    fix errors; lint

commit db380ce
Merge: 43628fb 0e07734
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 43628fb
Merge: f80301f 6a1bbf0
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 f80301f
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 fc177c8
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:28:27 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.LiftingProperties.Adjunction

commit 24c70cb
Merge: 38a89b8 18f8822
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 38a89b8
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:20:24 2023 -0500

    lint some more

commit 18f8822
Merge: eb14644 68e722a
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 eb14644
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:14:21 2023 -0500

    lint

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

    Update Mathlib.lean

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

    fix errors; lint

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

    get file to build

commit cbc27d7
Merge: d9d7366 6a1bbf0
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 d9d7366
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 1979ee1
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 18:54:09 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Limits.Shapes.StrongEpi

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

    fix errors; lint

commit c6ecc99
Merge: bd1174b 332636e
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 bd1174b
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 e49ab39
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 18:25:51 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.LiftingProperties.Basic

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

    remove spurious edit

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

    fix lint

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

    names and removing restate_axiom

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

    first pass

commit 8e67aa7
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 b108a9d
Author: Moritz Firsching <firsching@google.com>
Date:   Thu Feb 16 20:42:37 2023 +0100

    Initial file copy from mathport

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

    feat: port CategoryTheory.CommSq

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

    restore lost import line

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

    add missing aligns for fields; lint

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

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

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

    Fix

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

    Rename file

commit 5d9a97b
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 02606a1
Author: Yury G. Kudryashov <urkud@urkud.name>
Date:   Thu Feb 16 00:17:51 2023 -0600

    Initial file copy from mathport

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

    feat: port CategoryTheory.Category.Ulift

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

    fix most linter issues

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

    Merge branch 'master' into port/CategoryTheory.Yoneda

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

    fill in some docstrings

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

    fix all but four

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

    minor fixes

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

    fix some errors

commit 70bf280
Merge: 155f173 278e110
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 155f173
Merge: 3a22ebf 92feef6
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 3a22ebf
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 5a1eb5b
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Feb 15 00:40:41 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Yoneda

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

    fix last errors

commit 2203485
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 10bf4bb
Author: adamtopaz <github@adamtopaz.com>
Date:   Tue Feb 14 22:06:54 2023 -0700

    Initial file copy from mathport

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

    feat: port CategoryTheory.DiscreteCategory

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

    fix all but one decl

commit f147507
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 2b3c437
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 14 22:56:08 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Functor.Currying

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

    fix error

commit 4891412
Merge: b163ac1 2b370d2
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 b163ac1
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 d5ec61a
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 14 22:41:16 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Functor.Hom

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

    fix errors; lint; add porting note

commit abef74a
Merge: b6d5b6e e1d3cf3
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 b6d5b6e
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 e252760
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 14 21:13:52 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Types

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

    fix errors; lint; add porting notes

commit 67a9548
Merge: 985720e 9b2cb68
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 985720e
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 7f42580
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 14 20:02:31 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.EpiMono

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

    lint

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

    fix errors

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

    initial pass

commit a1adaec
Merge: e2cfafa b49b6cc
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 e2cfafa
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 466cb9f
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 14 14:10:41 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Groupoid

commit b49b6cc
Merge: b0fba35 0f5ac2f
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 14 14:01:22 2023 -0500

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

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

    add porting note about proliferation of match

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

    add porting note for scary warning

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

    lint

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

    finally fixed

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

    more fixes

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

    some more fixes

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

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

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

    fix two simpNF lints

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

    fix comments

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

    delete linter command

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

    break long lines

commit df3b93e
Merge: 8136307 10bfe18
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 13 10:24:08 2023 -0500

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

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

    filled in last sorry

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

    fix some errors

commit a4ea90f
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 8414826
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 11 20:38:10 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Pi.Basic

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

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

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

    only one error left

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

    some progress

commit 3809ccc
Merge: e0de198 8306c5f
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 e0de198
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 5bde226
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Feb 9 13:49:57 2023 -0500

    Initial file copy from mathport

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

    feat: port CategoryTheory.Adjunction.Basic

commit 8306c5f
Merge: 68bcb25 6c1fbbf
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 68bcb25
Merge: e6ec924 bac7310
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 9 11:51:47 2023 -0500

    Merge branch 'master' into port/CategoryTheory.Equivalence

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

    update slice naming

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

    Merge branch 'slice' into port/CategoryTheory.Equivalence

commit ce383e4
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 80596f2
Author: thorimur <68410468+thorimur@users.noreply.github.com>
Date:   Wed Feb 8 14:58:19 2023 -0500

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

commit 2c56111
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 0c247c7
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Feb 8 14:19:58 2023 -0500

    fix final long line

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

    fix refl error and lint errors

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

    fix all but refl error

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

    Merge branch 'slice' into port/CategoryTheory.Equivalence

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

    fix test/slice.lean

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

    fix module docs

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

    Merge branch 'slice' into port/CategoryTheory.Equivalence

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

    minor changes

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

    add module documentation(?)

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

    modify documentation lines

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

    add slice to global import file

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

    move iteration tactics to core

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

    Merge branch 'master' into slice

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

    add documentation and clean up

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

    remove rewriteTarget'; change MonadExceptOf to MonadExcept

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

    remove equivalence.lean

commit afafdf0
Merge: c76b450 c16c0c4
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Feb 8 09:15:56 2023 -0500

    Merge branch 'master' into port/CategoryTheory.Equivalence

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

    test: create `slice.lean` test file

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

    add example and equivalence file for testing

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

    seems to work

commit c76b450
Merge: afd9aed 98c1295
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 afd9aed
Author: Henrik Böving <hargonix@gmail.com>
Date:   Mon Jan 2 13:21:50 2023 +0100

    push it as far as possible

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

    Mathbin -> Mathlib; add import to Mathlib.lean

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

    Initial file copy from mathport
@mattrobball
fix errors
09a2181
@mattrobball
lint; fix names
ea627ff
@mattrobball mattrobball added the mathlib-port This is a port of a theory file from mathlib. label Feb 23, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 23, 2023
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 24, 2023
@mattrobball mattrobball mentioned this pull request Feb 24, 2023
Closed
1 task
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 28, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@mattrobball 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 1, 2023
jcommelin
jcommelin reviewed Mar 1, 2023
View reviewed changes
Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean Outdated Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean Outdated Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean Outdated Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean Outdated
open Lean Elab Meta Tactic in
-- Porting note: trying a macro
/-- A local tactic replacing the use of discrete cases in Lean 3 -/
elab (name := discrete_empty_elim) "dee" : tactic => withMainContext do
Copy link
Member

Choose a reason for hiding this comment

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

What does dee stand for? Please add the explanation to the docstring.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I added this to the docstring.

Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 1, 2023
@mattrobball mattrobball added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 1, 2023
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 1, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 2, 2023
jcommelin
jcommelin approved these changes Mar 2, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 2, 2023
bors bot pushed a commit that referenced this pull request Mar 2, 2023
@mattrobball @jcommelin
feat: port CategoryTheory.Limits.Shapes.Terminal (#2459)
0451175 
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Mar 2, 2023

Pull request successfully merged into master.

Build succeeded:

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

@jcommelin jcommelin jcommelin approved these changes

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

Successfully merging this pull request may close these issues.

None yet
3 participants
@mattrobball @semorrison @jcommelin