← Back to context

Comment by westurner

1 year ago

Homotopy type theory (HoTT) > HoTT in CoQ: Coq-HoTT: https://github.com/leanprover/lean2/tree/master/hott

Lean4:

"Theorem Proving in Lean 4" https://lean-lang.org/theorem_proving_in_lean4/

Learnxinimutes > Lean 4: https://learnxinyminutes.com/lean4/

/? Hott in lean4 https://www.google.com/search?q=hott+in+lean4

> What is the relation between Coq-HoTT & Homotopy Type Theory and Set Theory with e.g. ZFC?