Jean Abou Samra (new account) on Nostr: nprofile1q…8nauq nprofile1q…d6kk0 Yes, “hprop” (homotopy proposition) and ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjy9a8k5prc8wn4jven7agerdchhyaweggg03xj0tz29xyzr9020s08nauq (nprofile…nauq) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) Yes, “hprop” (homotopy proposition) and “mere proposition” are synonyms. (But what do you mean by “Prop is the (-1)-truncation of Type”?)