A Proof of Covariant Yoneda Lemma in the Lean3 Proof Assistant out of scratch not using Mathlib3. This proof was first constructed in my teaching Introduction to Proofs to upper Level undergraduates at Johns Hopkins University.
-
Notifications
You must be signed in to change notification settings - Fork 0
A Proof of Covariant Yoneda Lemma in the Lean3 Proof Assistant out of scratch not using Mathlib3.
License
sinhp/CovariantYonedaLean3
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
A Proof of Covariant Yoneda Lemma in the Lean3 Proof Assistant out of scratch not using Mathlib3.
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published