If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev

hyperhello an hour ago | parent | next [-]

If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.

▲

lioeters an hour ago | parent | prev [-]

Oh how interesting, they're using a fork of Agda called Mikan, not Lean as I imagined before visiting the link. https://1lab.dev/Mikan.html

	▲	solomonb 42 minutes ago \| parent [-]
		Yup, Mikan is a fork of Agda that focuses specifically on Cubical Type Theory. Lean's CIC is only one approach to dependent type based formal verification. Cubical gives you a computational approach to Homotopy Type Theory. The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free." All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.