[ refactor ] make `contradiction` and friends entirely definitionally proof-irrelevant - #2802

Closed

jamesmckinna wants to merge 21 commits into

agda:masterfrom

jamesmckinna:v3.0-contradiction

Commits on Aug 4, 2025

[ refactor ] make `contradiction` and friends entirely proof-irrelevant
jamesmckinna
committed
0db4874
fix: whitespace
jamesmckinna
committed
1c7b74e
add: eta law for ¬¬ monad
jamesmckinna
committed
c4cb90f
fix: more eta-expansion needed
jamesmckinna
committed
00c0354
fix: more eta-expansion needed
jamesmckinna
committed
863d63c
fix: `_-uno` bad fit for irrelevant arguments
jamesmckinna
committed
757f28a
fix: more eta-expansion needed
jamesmckinna
committed
9ce9d09
fix: more eta-expansion needed
jamesmckinna
committed
3fbf7ec
fix: remove named telescopes
jamesmckinna
committed
680839b

Commits on Aug 5, 2025

Merge branch 'master' into v3.0-contradiction
jamesmckinna
authored
4d6f4f7
fix: `CHANGELOG`
jamesmckinna
committed
9e2ee23
Merge branch 'master' into v3.0-contradiction
jamesmckinna
authored
280492b

Commits on Oct 29, 2025

reset: `CHANGELOG`
jamesmckinna
committed
21c909b
Merge branch 'master' into v3.0-contradiction
jamesmckinna
authored
8da38e6
fix: merge conflict
jamesmckinna
committed
8d0a6b9
fix: merge conflict
jamesmckinna
committed
eb74536
fix: merge conflict
jamesmckinna
committed
6285f2c
fix: simplify
jamesmckinna
committed
00c9cc6
fix: simplify
jamesmckinna
committed
c625e32
fix: simplify
jamesmckinna
committed
1ea83fc
fix: simplify
jamesmckinna
committed
f80af54