All Questions

HoTT provides a foundation of math that remains mysterious for many mathematicians including me. Hence this question. There are several implementations of math based on ZFC, an example being MetaMath. ...

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...

The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...