# Agda Template

Remix or try out this notebook to get started with Agda, check the notes below about interaction limitations. The first cell of an Agda Runtime *must* start with a module declaration (optionally preceded by pragmas with options) and this will be subject to Agda module naming conventions when imported in other runtimes.

`module HelloAgda where`

`import Relation.Binary.PropositionalEquality as Eq`

`open Eq using (_≡_)`

`open Eq.≡-Reasoning using (begin_;_≡⟨⟩_;_∎)`

`data ℕ : Set where`

` zero : ℕ`

` suc : ℕ → ℕ`

`_+_ : ℕ → ℕ → ℕ`

`0 + n = n`

`suc n + m = suc (n + m)`

`_ : 1 + 1 ≡ 2`

`_ = begin `

` (suc 0) + 1`

` ≡⟨⟩`

` suc (0 + 1)`

` ≡⟨⟩`

` suc 1`

` ≡⟨⟩`

` 2`

` ∎`

And if you feel you're in that HoTT mood, give Cubical a try:

`module CubiTest {ℓ} where`

`open import Cubical.Core.Primitives`

` hiding (_≡_)`

`postulate`

` ℐ : I → Set ℓ`

` a₀ : (ℐ i0)`

` a₁ : (ℐ i1)`

`-- PathP : (ℐ : I → Set ℓ) → (ℐ i0) → (ℐ i1) → Set ℓ`

`-- intro and elim`

`PathP⁺ : (f : (i : I) → (ℐ i)) → PathP ℐ (f i0) (f i1)`

`PathP⁺ f = λ i → f i`

`PathP⁻ : (p : PathP ℐ a₀ a₁) → (r : I) → (ℐ r)`

`PathP⁻ p r = p r`

`_≡_ : {A : Set ℓ} → A → A → Set ℓ`

`_≡_ {A} = PathP (λ _ → A)`

`funExt : {A : Set ℓ} → {B : A → Set ℓ} →`

` {f g : (x : A) → B x} →`

` (p : (x : A) → f x ≡ g x) → f ≡ g`

`funExt p i = λ x → (p x) i`

follow the environment links to see how they're built.

## Interactive Theorem Proving in Nextjournal

Since our runtimes are powered by an Agda Jupyter Kernel, we can support only a limited subset of Emacs Agda mode and interaction.

With `Tab`

and `Shift-Tab`

(in a running Agda runtime) you can get assistance in providing terms of the correct type, placing the cursor next to a `?`

or a hole `{! !}`

. In the following example you can hit `Tab`

at the end of the code to obtain a list of suggestions

`data Vec (A : Set) : ℕ → Set where`

` [] : Vec A zero`

` _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)`

`hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A`

`hd x = ?`

Choosing the *hole* expression `{! !}`

you can further refine your goal, or ask Agda to split your definition on a variable for *pattern matching* by typing it inside the hole:

`hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A`

`hd x = {! x !}`

now hitting `Tab`

again with the cursor on the right of the hole should suggest to replace the above with a constructor expression, like so

`hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A`

`hd (x :: x₁) = ?`

now pressing `Tab`

again after `?`

we'll be suggested to replace an `x`

for `?`

and this will already type check fine. We can also go further and ask Agda to split on the variable `x₁`

instead, by inserting it into the hole, i.e. turn

`hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A`

`hd (x :: x₁) = {! x₁ !}`

into

`hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A`

`hd (x :: []) = ?`

`hd (x :: (x₁ :: x₂)) = ?`

and so on.

With `Shift+Tab`

while the cursor is next to `?`

or a hole, you'll get a summary of the current goals and their types. Code execution and completions is handled by (our fork of) Agda Jupyter Kernel. Unicode input method is triggered via typing a first `\`

and follows emacs agda mode translations.