Playground

This page runs Agda 2.8.0 itself. Not a recording, not a server, and not a simulation: the checker is a real Agda compiled to WebAssembly, it runs in your tab, and what it says about your proof is what it would say on a terminal.

Nothing is downloaded until you ask.

Fill the hole

Two Boolean values, a negation defined by the only two equations it can have, and a claim: negating twice gets you back where you started. The ? is a hole. Your job is to replace it.

module Main where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

not : Bool → Bool
not true  = false
not false = true

not-involutive : (b : Bool) → not (not b) ≡ b
not-involutive b = ?

Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 49 KB for this exercise, which covers 4 compiled modules. Nothing is downloaded until you ask, and nothing you type leaves this tab.

Three hints, in order

What is b, really? It is not a value you can inspect at run time. It is one of exactly two constructors, and Agda knows that.

Agda will not compute not (not b) until it knows which b it has. So refl on its own cannot work: there is nothing yet to reduce.

Write one line per constructor. Replace the last line with two, giving the proof for true and the proof for false separately.

The wrong answers teach more than the right one, and each of these is worth trying before you finish:

What you write	What Agda says
not-involutive b = refl	not (not b) != b of type Bool. Pattern matching is what makes it compute.
not-involutive b = not-involutive b	a termination error. Agda will not accept a proof that assumes itself.
not-involutive true = refl, alone	Missing cases: not-involutive false. It names the case you forgot.

Five from a benchmark

The exercise above is a toy in one respect: it defines its own not over Agda's builtin Bool, so it needs no library at all. The five below are obligations from the benchmark behind the research on proof automation, stated over the standard library and importing this project's own reflection prelude, which is what a machine-generated attempt is checked against.

They share one download, the standard-library modules all five need, fetched once for whichever you open first. Two things differ from the benchmark's files. Each module is called Main, because that is the file this page checks. And the three that use equality import _≡_ and refl from Relation.Binary.PropositionalEquality.Core, where those are defined, rather than from the module that re-exports them beside the rest of the equality library. The proofs are the same either way, and that one import is most of what the download would otherwise cost.

The same lemma, over the standard library

If you finished the first exercise, you have already written the answer to this one.

module Main where

open import AgdaDojang.Debug

open import Data.Bool.Base using ( Bool ; true ; false ; not )
open import Relation.Binary.PropositionalEquality.Core using ( _≡_ ; refl )

not-involutive : ∀ (b : Bool) → not (not b) ≡ b
not-involutive b = {!!}

Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 1.4 MB for library files this exercise shares with the four after it, which cover 45 compiled modules. Once one of them is loaded, the others download nothing more. Nothing is downloaded until you ask, and nothing you type leaves this tab.

Left and right are not the same

Addition on the natural numbers is defined by recursion on its first argument: zero + n = n and suc m + n = suc (m + n). So Agda can compute 0 + n, and it cannot compute n + 0 until it knows what n is. Try refl on both.

module Main where

open import AgdaDojang.Debug

open import Data.Nat.Base   using ( ℕ ; zero ; suc ; _+_ )
open import Relation.Binary.PropositionalEquality.Core using ( _≡_ ; refl )

+-identityˡ : ∀ (n : ℕ) → 0 + n ≡ n
+-identityˡ n = {!!}

Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 1.4 MB for library files it shares with four other exercises on this page, which cover 45 compiled modules. Once one of them is loaded, the others download nothing more. Nothing is downloaded until you ask, and nothing you type leaves this tab.

module Main where

open import AgdaDojang.Debug

open import Data.Nat.Base using ( ℕ ; zero ; suc ; _+_ )
open import Relation.Binary.PropositionalEquality.Core using ( _≡_ ; refl ; cong )

+-identityʳ : ∀ (n : ℕ) → n + 0 ≡ n
+-identityʳ n = {!!}

Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 1.4 MB for library files it shares with four other exercises on this page, which cover 45 compiled modules. Once one of them is loaded, the others download nothing more. Nothing is downloaded until you ask, and nothing you type leaves this tab.

A hint for the second

Split on n, as the first exercise split on b. The suc n case needs the proof for n underneath a suc, and cong suc puts it there.

A proof is a value

_<_ is not a test that answers true or false. m < n is defined as suc m ≤ n, and _≤_ is a data type with two constructors: z≤n, zero is at most anything, and s≤s, which turns m ≤ n into suc m ≤ suc n. A proof of an inequality is a value built from them.

module Main where

open import AgdaDojang.Debug

open import Data.Nat.Base using ( ℕ ; zero ; suc ; _<_ ; _≤_ ; z≤n ; s≤s )

0<1+n : ∀ {n : ℕ} → 0 < suc n
0<1+n = {!!}

Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 1.4 MB for library files it shares with four other exercises on this page, which cover 45 compiled modules. Once one of them is loaded, the others download nothing more. Nothing is downloaded until you ask, and nothing you type leaves this tab.

Passing a decision on

The hardest of the five. A Dec A is either yes with a proof of A, or no with a proof that A is impossible, which is a function from A to the empty type. Given maps both ways between A and B, turn a decision about A into one about B.

module Main where

open import AgdaDojang.Debug

open import Relation.Nullary using ( Dec ; yes ; no )

map′ : {A B : Set} → (A → B) → (B → A) → Dec A → Dec B
map′ A→B B→A d = {!!}

Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 1.4 MB for library files it shares with four other exercises on this page, which cover 45 compiled modules. Once one of them is loaded, the others download nothing more. Nothing is downloaded until you ask, and nothing you type leaves this tab.

A hint

Split on d. The yes case is one application. In the no case you hold a function from A to the empty type and need one from B: write it as a λ.

What is actually running

The binary is agda, built for wasm32-wasi, unmodified. It declares 24 imports and they are all wasi_snapshot_preview1: no JavaScript bridge, no threads, no shared memory. So the only thing standing between it and a browser is a filesystem, and this page brings one, about four hundred lines of JavaScript holding a tree of files in memory for the length of one check.

Each exercise mounts a filesystem image: a tar of exactly the sources and compiled interface files its imports need, which several exercises can share. Building those interfaces ahead of time is what makes the checks fast; without them every benchmark exercise would type-check dozens of standard-library modules from scratch on every attempt. The image also carries the exact command line its interfaces were built under, and the page runs that and nothing else, because an interface compiled under different options is silently ignored rather than rejected.

Typing Agda needs Agda's input method, which is here in miniature: a backslash, a name and a space, so \to becomes an arrow and \== becomes the equality sign. The row of characters under the editor does the same thing for a reader who would rather click, and names the sequence for each. It is about a hundred and fifty of agda-input's several thousand bindings, chosen for what this site's Agda actually writes. The editor colors what you type by the rules that color every Agda block on this site, and when Agda names a place in your text, the place is marked where it is.

What this page does not have is interaction. A hole here reports its position; it does not show you the goal's type or its context, and there is no refine and no case split. The checker running here can answer those questions too, but a page built around them is a larger thing to ship, and it belongs where the library being explored already lives. For the full experience, against a whole book's worth of Agda, go to plfa.isotopy.xyz.

Three consequences worth stating plainly:

• Nothing you type leaves your browser. There is no server to send it to. Each check builds a fresh filesystem, runs the checker over it, and throws it away; nothing is stored between checks or between visits.
• Nothing is fetched until you press a button, and the button says how many bytes it is about to spend.
• With JavaScript off this page is still a page: the lemma, the hints and the table of wrong answers are all here, and there is no broken widget where the checker would be.

What it costs, measured

Measured in headless Chromium 153 on 2026-09-25, driving this page's own build: each exercise opened in turn, then its solution checked ten times. Sizes are what crosses the wire.

	Fill the hole	The five benchmark exercises
the checker, once per visit	9.3 MB	shared
the filesystem image	49 KB	1.4 MB, once for all five
compiled interfaces shipped	4	45
opening another on a loaded image		nothing fetched
a check, steady state	150 to 231 ms	606 to 798 ms
peak WebAssembly memory	21.9 MiB	31.3 to 34.8 MiB

On the same machine, the previous version of this page, whose one benchmark exercise imported the whole equality module and shipped 73 interfaces, took 2.2 to 2.4 s a check.

Credits

• The WebAssembly Agda is agda-web/agda-wasm-dist, MIT, Copyright 2024 Agda Web, shipped unmodified. The browser-side approach follows agda-web/als-demo, MIT, Copyright 2026 Andy Pan, from which no code is taken: the WASI host and the page code are this site's own.
• The editor's colors come from a port of the Agda rules of Pygments, BSD 2-Clause, the highlighter behind every code block on this site, so an exercise looks the same before and after the checker arrives.
• Agda 2.8.0 and the Agda standard library 2.3, both MIT-licensed, and the benchmark exercises' AgdaDojang modules from agda-native-air, Apache-2.0. Every notice the downloads require is published beside them, in the notices file.
• The measurements this page was built against were taken against plfa.isotopy.xyz, a deployment of the same checker with a full editor and interactive goals, built from plfa-playground, MIT, Copyright 2026 Andy Pan, which grew out of als-demo. Its interface pipeline, which lets several chapters share one archive of compiled interfaces, is the model for the shared images here. Nothing from it is included, and it is the place to go for the interactive experience this page does not attempt.