mailman.iro.umontreal.ca
S'identifier
S'inscrire
Gérer cette liste
S'identifier
S'inscrire
×
Raccourcis clavier
Vue discussion
j
: Message non lu suivant
k
: Message non lu précédent
j a
: Aller à tous les fils
j l
: Accéder à l'aperçu de la liste de diffusion
Typer
Discussion
Start a new thread
Télécharger
Discussions par
mois
----- 2026 -----
juin
mai
avril
mars
février
janvier
----- 2025 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2024 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2023 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2022 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2021 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2020 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2019 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2018 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2017 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
janvier
----- 2016 -----
décembre
novembre
octobre
septembre
août
juillet
juin
mai
avril
mars
février
typer@iro.umontreal.ca
Avril 2024
1 participants
1 discussions
Propositional truncation
by Stefan Monnier
25 Avr '24
25 Avr '24
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
1
0
0
0
Résultats par page :
10
25
50
100
200