nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq9q3q6p8cfsc52e8thrsdhmy8hyqmnwxja4f5zq7s7elj3e75fk4qq8fcvf (nprofile…fcvf)
yea looks like a simpler version of cubical to me: sacrifice definitional proof irrelevance and transport refl is identity to get extensionality principles