mailman.iro.umontreal.ca
Sign In
Sign Up
Manage this list
Sign In
Sign Up
×
Keyboard Shortcuts
Thread View
j
: Next unread message
k
: Previous unread message
j a
: Jump to all threads
j l
: Jump to MailingList overview
Typer
Thread
Start a new thread
Download
Threads by
month
----- 2026 -----
June
May
April
March
February
January
----- 2025 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2024 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2023 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2022 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2021 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2020 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2019 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2018 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2017 -----
December
November
October
September
August
July
June
May
April
March
February
January
----- 2016 -----
December
November
October
September
August
July
June
May
April
March
February
typer@iro.umontreal.ca
April 2024
1 participants
1 discussions
Propositional truncation
by Stefan Monnier
25 Apr '24
25 Apr '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
Results per page:
10
25
50
100
200