On: The Origins and Motivations of Univalent Foundatio...

[cphoward]

I am rather interested in this line of work for both mathematicians and computer scientists. What is the best way to get started? What's the quickest way to get up to speed in this field?

[smokel → cphoward]

I am a cluebie in this field, but I guess working your way through some Lean tutorials [1], and/or reading the introduction to the HoTT book [1] might either scare you off, or get you enthused enough to continue.

[1] https://leanprover.github.io/theorem_proving_in_lean4/

[2] https://homotopytypetheory.org/book/