Beta
Fancy bool #2: Bool as a higher inductive type (corrected)
7
Beta Status:Testing & feedback needed
Beta
Fancy bool #1: Bool as a higher inductive type
11
Beta Status:Testing & feedback needed
Beta
suc N = suc M implies N = M? Prove it about finite sets!
3
Beta Status:Testing & feedback needed
Beta
N + 1 = suc N? Prove it about h-sets!
7
Beta Status:Testing & feedback needed
Beta
Natural number is not path-equivalent to unit type
14
Beta Status:Ranking feedback needed
Beta
Unordered pair #3: you can (not) subtract
8
Beta Status:Testing & feedback needed
Beta
Unordered pair #2: just a commutative semigroup
9
Beta Status:Testing & feedback needed
Beta
Unordered pair #1: add two natural numbers
14
Beta Status:Ranking feedback needed
Beta
A map from a truncated set to a set
7
Beta Status:Testing & feedback needed
7 kyu
Kacarott's path factorization
18
8 kyu
Voile's question: ∀ (n : ℕ), 1 = 2 * n -> false
49
4 kyu
A+A=B+B so A=B? Prove it in Haskell!
50
Beta
Function extensionality and explicitness
17
Beta Status:Awaiting approval
Beta
A+B=B+A? Prove it in using DataKinds!
14
Beta Status:Testing & feedback needed
Beta
Join until impossible
7
Beta Status:Ranking feedback needed
Loading more items...