Andreas Lynge

The HoTT library relies on Coq version >= 8.10. So at least issue https://github.com/MetaCoq/metacoq/issues/138 is standing in the way of making metacoq compatible with HoTT.

I do not understand why we use module types instead records and classes. Considering the inflexibility with universes in module types, I would try using records and classes before module...

The following two branches allows one to play with ssreflect in HoTT: - https://github.com/andreaslyn/HoTT/tree/SSR-THIS-ONE - https://github.com/andreaslyn/coq/tree/SSR-FOR-HoTT Maybe someone will be interested in continuing this.

@gares I made those changes to the Coq sources to make ssreflect work in HoTT. Maybe some of those things have been fixed already in Coq, so I am not...

I agree that the inductive `FinSeq` is often more convenient. Note that induction on `n` is not the only option for `Fin n -> A`. We can use induction on...

Hi @spitters. I have looked a bit into porting Equations to HoTT, https://github.com/mattam82/Coq-Equations/compare/8.8+alpha...andreaslyn:hott-port?expand=1. I am currently working on building Equations with HoTT, which is challenging. Equations depends on tactics from...

Fixing congruence seems to be the next step in porting Equations to HoTT. I can take a look at it, but I am not sure how tricky it is, and...

Sounds good. Thank you for the input.

Hi @mattam82. I have some problems with porting Equations to HoTT related to universes. I hope you can find some time to help with this. I have created a script...

Thanks a lot. I can make more progress now.