Our great sponsors
-
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
Is Lean a Category?
(like much debated: is Hask(ell) a Category)
"In this section we set up the theory so that Lean's types and functions between them can be viewed as a `LargeCategory` in our framework."
So it seems to be proven that there is a Category Lean!
https://github.com/leanprover-community/mathlib4/blob/master...
Me too, I want to follow
https://github.com/blanchette/logical_verification_2023
The hitchhiker's guide
Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps.
https://github.com/leanprover-community/mathlib
Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the community have had great success with that kind of project; one million lines of mathlib was translated from Lean 3 to Lean 4 using a combination of automation and human work)