## 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: Jan 29 2023 at 07:29 UTC