色々足りてないから酷い

data Nat : Set0
  where
    zero : Nat
    succ : Nat -> Nat

leibnizEq : Nat -> Nat -> Set1
leibnizEq x1 y1 = (P1 : Nat -> Set0) -> P1 x1 -> P1 y1

g : (P2 : Nat -> Set0) -> Nat -> Nat -> Set0
g P3 x2 z2 = (P3 z2 -> P3 x2)

h : (P4 : Nat -> Set0) -> (x3 : Nat) -> P4 x3 -> P4 x3
h P5 x4 px1 = px1

i : (P10 : Nat -> Set0) -> (f3 : Nat -> Nat) -> Nat -> Set0
i P11 f4 z3 = P11 (f4 z3)

sym : (x4 : Nat) -> (y2 : Nat) -> leibnizEq x4 y2 -> leibnizEq y2 x4
sym x5 y3 xy1 P6 py = xy1 (g P6 x5) (h P6 x5) py

refl : (n1 : Nat) -> leibnizEq n1 n1
refl n2 P7 px2 = px2

trans : (x6 : Nat) -> (y4 : Nat) -> (z1 : Nat) -> leibnizEq x6 y4 -> leibnizEq y4 z1 -> leibnizEq x6 z1
trans x7 y5 z2 xy2 yz1 P8 px3 = yz1 P8 (xy2 P8 px3)

mapEq : (x7 : Nat) -> (y5 : Nat) -> (f1 : Nat -> Nat) -> leibnizEq x7 y5 -> leibnizEq (f1 x7) (f1 y5)
mapEq x8 y6 f2 xy3 P9 = xy3 (i P9 f2)

add : Nat -> Nat -> Nat
add x0 y0 with x0
... | zero = y0
... | succ z0 = succ (add z0 y0)

lemma1 : (n2 : Nat) -> (m1 : Nat) -> leibnizEq (add (succ n2) m1) (succ (add n2 m1))
lemma1 n3 m2 = refl (add (succ n3) m2)

lemma2 : (x9 : Nat) -> leibnizEq (add zero x9) (add x9 zero)
lemma2 x10 with x10
... | zero = refl zero
... | succ z3 = mapEq z3 (add z3 zero) succ (lemma2 z3)

lemma3 : (n4 : Nat) -> (m3 : Nat) -> leibnizEq (add n4 (succ m3)) (succ (add n4 m3))
lemma3 n5 m4 with n5
... | zero = refl (succ m4)
... | succ z4 = mapEq (add z4 (succ m4)) (succ (add z4 m4)) succ (lemma3 z4 m4)

theorem : (n6 : Nat) -> (m5 : Nat) -> leibnizEq (add n6 m5) (add m5 n6)
theorem n7 m6 with n7
... | zero = lemma2 m6
... | succ z5 = trans (add (succ z5) m6) (succ (add m6 z5)) (add m6 (succ z5))
　　　　　　　　(mapEq (add z5 m6) (add m6 z5) succ (theorem z5 m6))
　　　　　　　　(sym (add m6 (succ z5)) (succ (add m6 z5)) (lemma3 m6 z5))

λ式と、whereが無いし、手動変数名衝突避けを行ってるのでカス過ぎる。

それとImplicit Parametersは欲しいよなぁ・・・。

Leibniz Equalityを使ってるのは、先日書いたように、Idを使うそれだとImplicit Parametersかdot patternがいるとかそういう事が起こるからですね！！