mathlib3
feat(category_theory/equivalence): make definition of adjointify_η easier to elaborate
#1045
Merged
Overview
Commits
1
Changes
View On GitHub

feat(category_theory/equivalence): make definition of adjointify_η easier to elaborate #1045

mergify merged 1 commit into master from adjointify
fpvandoorn
fpvandoorn feat(adjointify): make definition easier for elaborator
42dd0385
fpvandoorn fpvandoorn requested a review 6 years ago
fpvandoorn fpvandoorn changed the title feat(adjointify): make definition easier for elaborator feat(category_theory/equivalence): make definition of adjointify_η easier to elaborate 6 years ago
digama0
digama0 approved these changes on 2019-05-17
jcommelin
jcommelin approved these changes on 2019-05-17
jcommelin jcommelin added ready-to-merge
mergify mergify merged 5e5298b9 into master 6 years ago
mergify mergify deleted the adjointify branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum