Hi all; I am learning homotopy type theory.
If is a type and is a dependent type, let . Do we have in the dependent sum type iff in ?
Are you sure the rhs is ?
unfortunately we don't have a suitable homotopy type theory stream here. If you don't get the help you want on HoTT here, consider trying the HoTT Zulip Chat, which explicitly covers HoTT in Coq.
sorry, meant . Thank you, Theo.
With the types you give, you do have but that's only a bi-implication not an equivalence between types
Great, thanks, Kenji.
I will check out the HoTT Zulip chat.
since the connection to Coq-HoTT (the Coq library) here is far from obvious, I'm going to have to move this to Miscellaneous
This topic was moved here from #Coq users > dependent sum types in HoTT by Karl Palmskog
Last updated: Aug 19 2022 at 19:03 UTC