mjub/hott My own implementation of homotopy type theory in Coq. Documentation is available at https://mjub.github.io/hott/.