Stream: Miscellaneous

Topic: dependent sum types in HoTT

Patrick Nicodemus (Nov 08 2021 at 20:30):

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$?

Théo Winterhalter (Nov 08 2021 at 20:34):

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

Karl Palmskog (Nov 08 2021 at 20:40):

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.

Patrick Nicodemus (Nov 08 2021 at 20:40):

sorry, meant $(a,s)$. Thank you, Theo.

Kenji Maillard (Nov 08 2021 at 20:40):

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

Patrick Nicodemus (Nov 08 2021 at 20:41):

Great, thanks, Kenji.
I will check out the HoTT Zulip chat.

Karl Palmskog (Nov 08 2021 at 20:47):

since the connection to Coq-HoTT (the Coq library) here is far from obvious, I'm going to have to move this to Miscellaneous

Notification Bot (Nov 08 2021 at 20:48):

This topic was moved here from #Coq users > dependent sum types in HoTT by Karl Palmskog

Last updated: May 31 2023 at 02:31 UTC