Max S. New ⚜️ on Nostr: Is the principle of unique choice provable in any flavor of Observational type ...
Is the principle of unique choice provable in any flavor of Observational type theory? I saw in nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq9q3q6p8cfsc52e8thrsdhmy8hyqmnwxja4f5zq7s7elj3e75fk4qq8fcvf (nprofile…fcvf) 's paper (https://hal.science/hal-03857705v2/) that it is not provable in that version