🚀 go-pugleaf

$B>>K\!w?t3X2J$/$:$l$G$9!#(B

In article <SATOSHI.93Feb22191139@whale.math.ryukoku.ac.jp> satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) writes:
 |$B$H$3$m$G!">e$NOC$GLLGr$$$H;W$&$N$O!"(BLeibniz equality $B$H(B extensional
 |equality $B$rHf$Y$?;~!"A0<T$N$[$&$,$:$C$HD61[E*$JDj5A$K$J$C$F$$$k(B($BA0<T$O(B 
 |impredicative $B$JM}O@$G9M$($k$b$N$@$,!"8e<T$O(B predicative $B$JDj5A$G!"$=(B
 |$B$b$=$b(B1$B3,$NM}O@$G$bDj5A$G$-$k(B)$B$K$b4X$o$i$:!"(Bequality $B$NH=Dj$OA0<T$N$[(B
 |$B$&$,4JC1$G$"$k$3$H$G$9!#(B...

 $B$I$&$b!"Aa$H$A$j$G!"(Ball$B$,B+G{(B$B$7$F$$$kJQ?t$N0c$$$rL5;k$7$F$*$j$^$7$?!#(B
 $B$7$+$7!"(BP$B$rB+G{$9$k(BLeibniz equality$B$NJ}$,H=Dj$7$d$9$$$H$O0U(B$B30$G$7$?!#(B

 |                    ...  $B$I$&$b(B fj.ai $B$G$N5DO@$r8+$F$$$k$H!"(BLeibniz
 |equality $B$r!VDj5A(B$B$K=>$C$F!WH=Dj(B($B$"$k$$$OG'<1(B)$B$9$k(B($B$D$^$j!"A4$F$N(B P $B$K(B
 |$B$D$$$F(B P(x) <-> P(y) $B$+$I$&$+$r8+$k(B)$B$N$OET9g$,(B$B0-$$!"$_$?$$$JOC$K$J$C$F(B
 |$B$$$k$h$&$G$9$1$I!"2?$bDj5ADL$j$K$d$kI,MW$O$J$$$o$1$G$9!#>e$N$h$&$K!"<B(B
 |$B:](B$B$K$O$b$C$HC1=c$KH=Dj$G$-$F$7$^$&$+$bCN$l$J$$$o$1$G$9!#(B... 

  $B$J$k$[$I!#(Bequality$B$r(BLeibniz equality$B$H$7(B$B$FDj5A$9$k$N$H!"$=$l$r$I$N$h$&(B
$B$KH=Dj$9$k$+$OJL$NLdBj$H$$$&$o$1$G$9$M!#$&$`!#(B

$B!t$I$&$b!VA4$F$N=R8l(B P$B$K$D$$$F!W$J$I$H$$$&$N$r$_$k$H(B
$B!t$D$$7Y2|?4$,$*$3$k$b$N$G(B(^^;)

 |$B$3$&$$$&;v$+$i9M$($F$b!"!VF1$8!W$H$$(B$B$&35G0$NDj5A$=$N$b$N$H!"$=$NG'<1$N(B
 |$B;EJ}$H$O!"$O$C$-$jJ,$1$F9M$($J$1$l$P$J$i$J$$$H;W$$$^$9!#(B

  $BMWE@(B$B$H$7$F$O!"$^$5$K$=$3$N$H$3$m$r$$$$$?$+$C$?$o$1$J$s$G$9$,!#(B
  $B$d$O$j!"J,$1$F9M$($k$H$3$m$,IT==J,$@$C$?(B$B$h$&$G$9!#(B
  ($BLZ2<$5$s$+$i$b!"$3$NA0$NH=Dj$K4X$9$k5-;v$G!"F1MM$N;XE&$r$$$?$@$-$^$7$?!#(B)

$B!]!]!]!]!]!](B$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B
$B!!!!!!!!!!E4E4E4E4!!!!!!>>K\??8c(B (Shingo Matumoto)$B!!!!!!!!!!!!!!!!!!!!!!!!!!!!(B
$B!!!!!!!!!!E4!!!!!!E4!!!!(Bshingo@ipc02.rtri.or.jp$B!!!!!!!!!!(B$B!!!!(B $B!!!!!!!!!!!!!!!!(B
$B!!!!!!!!!!E4!!E4E4!!!!!!")#1#8#5!!El5~ET9qJ,;{;T8wD.#2!]#8!]#3#8!!!!!!!!!!!!!!(B
$B!!E4!!!!!!E4!!!!E4!!!!!!E4F;Am9g5;=Q8&5f=j!!M"Aw%7%9%F%`I>2A8&5f<<!!!!!!!!!!!!(B
$B!!!!E4E4E4!!!!!!!!E4!!(B$B!!#0#4#2#5!]#7#3!]#7#3#0#6!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!(B
$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B