The Royal Swedish Academy of Sciences(17)

Theequalizerofarrowsx:A s:Bandx:A t:Bisconstructedasfollows:

x:AEqB(s,t)π1AstB

Provingthatthearrowπ1equalizessandtamountstoprovingthat

v:x:AEqB(s,t) s{π1(v)/x}=t{π1(v)/x}.

Thisfollowsfromtheextensionalityofequalitysinceπ2(v)isatermoftype

EqB(s{π1(v)/x},t{π1(v)/x}).

Supposez:C h:Aequalizessandt:

z:C s{h/x}=t{h/x}:B

Thenwecanformthetermwitnessingtheequality

z:C r(s{h/x}):EqB(s{h/x},t{h/x})

13

搜索“diyifanwen.net”或“第一范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，第一范文网，提供最新人文社科The Royal Swedish Academy of Sciences(17)全文阅读和word下载服务。