✳flâneur — a map of the web's best reading

1Lab - 1Lab

1lab.dev · 3,254 words · saved by 1 readers

This website is an experiment in discoverable formalisation: an extensive library of formalised mathematics, presented as an explorable reference resource. Our implementation of a mathematical library, using literate source code, has allowed us a dual approach to the explanation of mathematical concepts: the code and the prose are complementary, and everyone is presented with the opportunity to choose their own balance between the rigid formalisation and the intuitive explanations. Rather than yet another category theory library, the 1Lab aims to be an accessible introduction to structuralist mathematics, formalised in the setting of homotopy type theory, using a theorem prover to check and structure our work. As a result of using Agda, everything we mention knows its own definition, whether we are talking about a specific principle (like univalence), a big idea (like monoidal categories), or a punctual observation (like surjections are quotient maps). The code snippet above, a re-stat

Equations Inline Footnotes module index where 1Lab 🔗 This website is an experiment in discoverable formalisation : an extensive library of formalised mathematics in Mikan , presented as an explorable reference resource. Our implementation of a mathematical library, using literate source code , has allowed us a dual approach to the explanation of mathematical concepts: the code and the prose are complementary, and everyone is presented with the opportunity to choose their own balance between the rigid formalisation and the intuitive explanations. open import 1Lab.Univalence open import 1Lab.Eq

Explore this link on the map →

related reading