I got Agda code export to work for my blog

Now, I will be able to present syntax highlighted, type checked, hyperlinked proofs.

module blog.Agda where
open import Terra.Data.Nat
open import Terra.Data.Nat.Functions using (_+_)
open import Terra.Data.Equality

id-right : (x : Nat) -> x + 0 ≡ x
id-right zero = refl
id-right (suc x) = cong suc (id-right x)

suc-bubble : (x y : Nat) -> x + suc y ≡ suc (x + y)
suc-bubble zero y = refl
suc-bubble (suc x) y = cong suc (suc-bubble x y)

+-comm : (x y : Nat) -> x + y ≡ y + x
+-comm zero y = sym (id-right y)
+-comm (suc x) y = sym (suc-bubble y x →← cong suc (+-comm y x))