Skip to content

[Merged by Bors] - feat: Port CategoryTheory.Monad.Adjunction#3528

Closed
adamtopaz wants to merge 21 commits intomasterfrom
port/CategoryTheory.Monad.Adjunction
Closed

[Merged by Bors] - feat: Port CategoryTheory.Monad.Adjunction#3528
adamtopaz wants to merge 21 commits intomasterfrom
port/CategoryTheory.Monad.Adjunction

Conversation

@adamtopaz
Copy link
Copy Markdown
Contributor

@adamtopaz adamtopaz commented Apr 19, 2023 •
edited
Loading

This is still WIP. There may be a change to reassoc that would make this nicer, see zulip

Open in Gitpod

@adamtopaz
feat: port CategoryTheory.Monad.Adjunction
37f1b97
@adamtopaz
Initial file copy from mathport
d61ea4d
@adamtopaz
automated fixes
32b2ad4 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@adamtopaz
wip
29c1c9b
@adamtopaz adamtopaz added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 19, 2023
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 20, 2023
@adamtopaz adamtopaz mentioned this pull request Apr 20, 2023
Closed
1 task
@Parcly-Taxel Parcly-Taxel added awaiting-review WIP Work in progress and removed WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review labels Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

This PR/issue depends on:

@adamtopaz adamtopaz added awaiting-review and removed WIP Work in progress labels Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 20, 2023
bors bot pushed a commit that referenced this pull request Apr 20, 2023
@adamtopaz
feat: Port CategoryTheory.Monad.Adjunction (#3528)
184ec5c 
~~This is still WIP.~~ There may be a change to `reassoc` that would make this nicer, see [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20reassoc.3F/near/351111877)
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Port CategoryTheory.Monad.Adjunction [Merged by Bors] - feat: Port CategoryTheory.Monad.Adjunction Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the port/CategoryTheory.Monad.Adjunction branch April 20, 2023 15:35
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@adamtopaz @kbuzzard
feat: Port CategoryTheory.Monad.Adjunction (#3528)
adca24f 
~~This is still WIP.~~ There may be a change to `reassoc` that would make this nicer, see [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20reassoc.3F/near/351111877)
kim-em pushed a commit that referenced this pull request May 10, 2023
@adamtopaz
feat: Port CategoryTheory.Monad.Adjunction (#3528)
fe54b92 
~~This is still WIP.~~ There may be a change to `reassoc` that would make this nicer, see [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20reassoc.3F/near/351111877)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

3 participants

@adamtopaz @kim-em @Parcly-Taxel