HoTT/Univalent foundations?

Stream: new members

[Elliot Evans]

Hi all, I am new here and I am interested in understanding the broader context that the lean theorem proving community operates within. Does this community use HoTT/Univalent foundations? If not, is there a write-up about the holistic strategy behind ensuring that this library of proofs will be able to scale and grow? Please excuse me if I have asked this in an incorrect or innapropriate manner, I am just trying to jump in :)