Jean Abou Samra (new account) on Nostr: nprofile1q…3adwt Do we even have a proof of subject reduction, confluence, ...
nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzs6fpmv0n0jgacjmy8k7ynuy808xwawg9p7mn8pa8w5uj3j0kmgzr3adwt (nprofile…adwt) Do we even have a proof of subject reduction, confluence, normalization and decidability of type checking for book HoTT?!?!