Our great sponsors

HoTT is somewhat independent of the choice of proof assistant.
Coq: https://github.com/HoTT/HoTT
Lean: https://github.com/gebner/hott3
idk what you mean by "blue screened", or results being on the way. afaict most of the nonfoundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.

HoTT is somewhat independent of the choice of proof assistant.
Coq: https://github.com/HoTT/HoTT
Lean: https://github.com/gebner/hott3
idk what you mean by "blue screened", or results being on the way. afaict most of the nonfoundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.

OPS
OPS  Build and Run Open Source Unikernels. Quickly and easily build and deploy open source unikernels in tens of seconds. Deploy in any language to any cloud.
