I'm interested in your $HOBBYPROJECT. I'm hoping to develop some software similar to edukera.com, ie using proof assistants as educational tools for mathematics. Would love to swap some cool links and references. Thanks!
That a function is the same thing as a proof, with the theorem it proves being the type it constructs and its assumptions being the types it takes in. (Functions are proofs (which in this case, are things that take witnesses of their assumptions and produce witnesses of their theorem), values are witnesses that something is true, types are theorems, etc.)
I have an interest in topology, and want to understand HoTT, but my intuition around type theory wasn't up to par -- so I'm trying to tackle it in a constrained setting (ie, not proving theorems about mathematics as such, but a narrower problem space). Figured there was nothing to do besides get into the messy bits of it.
Can you tell me a bit more about what you're trying to do?
Do you have any suggestions for simple introductions to HoTT, especially for someone without the topology background?
It's then using that equivalence structure between the proofs to reason about constructing proofs, as you can reason about the constructions that are possible out of classes of proofs. And that's basically where I get lost, because I don't quite know enough type theory to understand the structure they're trying to build, so I can't quite get the specific motivations. (The obvious high-level one is better formal reasoning.)
I haven't been following HoTT super closely for a year or two, getting sidetracked into the background, but last I checked there wasn't a ton of simple material on it -- it was sort of read the book, read the Coq proofs/framework, and figure it out. (Though, this easily could have changed.)