Comment by lioeters
2 days ago
I'd never heard of Cubical Type Theory, how interesting. Aside from that, and Mikan - why they forked, their development/contribution policy (which I happen to agree with more or less); and the notion of equality and equivalence (you didn't use this word but I read an article¹ with a glimpse into these concepts).. "Equalities are paths" - I'm going to be thinking about that for a while. Anyway the link to 1lab and the comments in this thread gave me various ideas to chew on, there's lot of substance there.
On the 1lab site, I started with simply-typed lambda calculus, an all-time classic that I've always wanted to understand more fully. How the site is designed, I love the syntax-highlighted math/code and the interface where every single concept can be clicked and hovered over to show additional information with usually a link to its own page. It led me to a kind of branching, graph-like manner of learning, where I open pages on categories, products, morphisms, uniqueness, equality - filling holes in my understanding as needed, then going back to more specific ideas built from those general foundational concepts.
An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression, to support an autodidactic and exploratory style of learning. It relates to topics raised elsewhere in this thread, like a "proper IDE for math" (integrated development environment for mathematics) and a language-agnostic "standard library" of data structures, algorithms, definitions, theorems, etc., where programming languages can import from a shared corpus of mathematically rigorous primitives.
> how to use dependent types to explore, teach, and formalize mathematics in a pro-human way
I find it meaningful how you phrased this - at this point in history with the state of technology that can overwhelm and devalue human intelligence, it's more important than ever to focus on how we teach, learn, communicate and cultivate understanding.
On a tangent, one of my interests is the book _Reflective Programs in Tree Calculus_² by Barry Jay, its proofs in Rocq, his more recent article "Typed Program Analysis without Encodings"³, and the work of his main collaborator⁴. I lack the relevant academic background to fully grasp it yet, so I've been chipping away at learning the necessary basics. So the link to 1lab is appreciated, it's a resource I'll be digging into over time.
---
¹ With Category Theory, Mathematics Escapes From Equality https://www.quantamagazine.org/with-category-theory-mathemat...
² https://github.com/barry-jay-personal/tree-calculus/blob/mas... (PDF)
³ https://github.com/barry-jay-personal/typed_tree_calculus/bl... (PDF)
What a wonderful response :)
> I'm going to be thinking about that for a while.
This is a deep and fascinating world to get into. Enjoy!
> It led me to a kind of branching, graph-like manner of learning...
Yes! I love this experience. It takes a little owrk but you can even import the 1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.
The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.
If you wanted a place to get started I would highly recommend PLFA: https://plfa.github.io/
> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression
I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.