Hi all; I am learning homotopy type theory.

If $X$ is a type and $Y : X \to hProp$ is a dependent type, let $a: X, t : Y a, s : Y a$. Do we have $(a, t) = (a,s)$ in the dependent sum type iff $t = s$ in $Y a$?

Are you sure the rhs is $(s,t)$?

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 $(a,s)$. Thank you, Theo.

With the types you give, you do have $(a, t) = (a, s) \iff t = s$ 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: Jan 29 2023 at 07:29 UTC