Stream: Miscellaneous

Topic: dependent sum types in HoTT


view this post on Zulip Patrick Nicodemus (Nov 08 2021 at 20:30):

Hi all; I am learning homotopy type theory.
If XX is a type and Y:XhProp Y : X \to hProp is a dependent type, let a:X,t:Ya,s:Yaa: X, t : Y a, s : Y a. Do we have (a,t)=(a,s)(a, t) = (a,s) in the dependent sum type iff t=st = s in YaY a?

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 20:34):

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

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Nov 08 2021 at 20:40):

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

view this post on Zulip Kenji Maillard (Nov 08 2021 at 20:40):

With the types you give, you do have (a,t)=(a,s)    t=s(a, t) = (a, s) \iff t = s but that's only a bi-implication not an equivalence between types

view this post on Zulip Patrick Nicodemus (Nov 08 2021 at 20:41):

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

view this post on Zulip 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

view this post on Zulip 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: Aug 19 2022 at 19:03 UTC