--- a/paper/src/zero.agda.replaced	Mon Jan 27 20:46:38 2020 +0900
+++ b/paper/src/zero.agda.replaced	Wed Jan 29 22:36:17 2020 +0900
@@ -1,3 +1,3 @@
-+zero : { y : @$\mathbb{N}$@ } → y + zero  @$\equiv$@ y
++zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero  @$\equiv$@ y
 +zero {zero} = refl
-+zero {suc y} = cong ( @$\lambda$@ x → suc x ) ( +zero {y} )
++zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} )