表現微修正

MIL/C07_Hierarchies/S02_Morphisms.lean

@@ -68,7 +68,7 @@ is really a function that happens to be continuous. This is one reason why Mathl
 
 OMIT. -/
 /- TEXT:
-より根本的な問題として，上記のように述語を使うか（ ``def`` か ``structure`` のどちらでも），それとも関数と述語を束ねた構造を使うのかということです．これは気持ちの問題でもあります．射ではないモノイド間の関数を考えることは非常にまれです．「モノイドの射」は普通の関数につけられる形容詞ではなく，名詞なのです．一方で位相空間の間の連続関数は，考えていた対象の関数がたまたま連続だったと主張することもできます．これがMathlibに ``Continuous`` という述語がある理由です．例えば次のように書くことができます:
+より根本的な問題として，上記のように述語を使うか（ ``def`` か ``structure`` のどちらでも），それとも関数と述語を束ねた構造体を使うのかということです．これは気持ちの問題でもあります．射ではないモノイド間の関数を考えることは非常にまれです．「モノイドの射」は普通の関数につけられる形容詞ではなく，名詞なのです．一方で位相空間の間の連続関数は，考えていた対象の関数がたまたま連続だったと主張することもできます．これがMathlibに ``Continuous`` という述語がある理由です．例えば次のように書くことができます:
 BOTH: -/
 -- QUOTE:
 example : Continuous (id : ℝ → ℝ) := continuous_id
@@ -205,7 +205,7 @@ replace ``def badInst`` with ``instance``, and look for random failures in this
 
 OMIT. -/
 /- TEXT:
-このようなインスタンスの作成はよくありません． ``f`` が関数の型ではない場合に ``f x`` という式に遭遇した時，Leanは ``f`` を関数に変換するために ``CoeFun`` インスタンスを探そうとします．上記の関数の型は ``{M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N)`` となり，したがってこれを適用しようとすると，未知の型 ``M`` と ``N`` ， ``F`` がどの順番で推論されるべきかLeanにとっては先験的に明らかではありません．これは前節で見た悪いインスタンスの種類とはまた少し違うものですが，同じ問題に帰着します． ``M`` のインスタンスがわからないと，Leanは未知の型のモノイドインスタンスを探さなければならず，データベース内の *すべての* モノイドインスタンスを試すことになります．このようなインスタンスの効果を見たい場合は，上記の宣言の上に ``set_option synthInstance.checkSynthOrder false in`` と入力し， ``def badInst`` を ``instance`` に置き換えると，このファイル中であちこち失敗することを確認できるでしょう．
+このようなインスタンスの作成はよくありません． ``f`` が関数の型ではない場合に ``f x`` という式に遭遇した時，Leanは ``f`` を関数に変換するために ``CoeFun`` インスタンスを探そうとします．上記の関数の型は ``{M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N)`` となり，したがってこれを適用しようとすると，未知の型 ``M`` と ``N`` ， ``F`` がどの順番で推論されるべきかLeanにとっては先験的に明らかではありません．これは前節で見た悪いインスタンスの種類とはまた少し違うものですが，同じ問題に帰着します． ``M`` のインスタンスがわからないと，Leanは未知の型のモノイドインスタンスを探さなければならず，データベース内の **すべての** モノイドインスタンスを試すことになります．このようなインスタンスの効果を見たい場合は，上記の宣言の上に ``set_option synthInstance.checkSynthOrder false in`` と入力し， ``def badInst`` を ``instance`` に置き換えると，このファイル中であちこち失敗することを確認できるでしょう．
 
 TEXT. -/
 /- OMIT: