Propositional truncation
25 Avr
2024
25 Avr
'24
14:38
Pour transformer une proposition en une "mere proposition", et que tu ne veux/peux pas utiliser `conv_erase`, au lieu de |P| = Erased P tu peux utiliser la double négation |P| = (P → ?A) → ?A maintenant qu'on a la "functional extensionality". Stefan
Afficher les réponses par date
778
Âge (en jours)
778
Dernière activité (en jours)
0 commentaires
1 participants
participants (1)
-
Stefan Monnier