2つのラムダ抽象の同値関係の定義

2つの型付きラムダ式M, M': A\to Bについて、任意のN:AについてM(N)=_{\beta\eta}M'(N)が成り立つならばM=_{\beta\eta}M'が成り立つという性質

関数f,gについて

\forall x, f(x)=g(x)\Rightarrow f=gがなりたつこと

「外延性」という言葉がわかりにくすぎるな

内容自体はシンプルなのに無駄に難しそうに見える

参考

『圏論の歩き方』 p.62