Update c3_universes_types_terms.md

タイポを修正

src/c3_universes_types_terms.md

@@ -57,7 +57,7 @@ $\pi$ が要素を持つべき理由はありません．これは数学の基
 
 数学におけるコロンの標準的な使い方があります．―― 関数を書くための記法です．`X` と `Y` が集合
 （あなたが集合論を使っている場合）または型（型理論を使っている場合）であるとき，
-`X` から `Y` への関数を `f : X → Y` と書きます．これは実は Lean におけるコロンの使い方と一致sています，
+`X` から `Y` への関数を `f : X → Y` と書きます．これは実は Lean におけるコロンの使い方と一致しています．
 `X` から `Y` への関数の集まり $\mathrm{Hom}(X,Y)$ に対する Lean の表記法は `X → Y` であり，
 これは型です．（つまり `X → Y : Type` です．これは集合論で
 $\mathrm{Hom}(X,Y)$ を集合と考えることに対応しています）`f : X → Y` は `f` が `X → Y`
@@ -68,4 +68,4 @@ $\mathrm{Hom}(X,Y)$ を集合と考えることに対応しています）`f : X
 
 （これは試験に出ません）厳密に言えば，宇宙は型であり，型は項ですが，これは用語の問題です．
 多くの場合，ひとが型について語るとき，それは宇宙ではない型を意味し，ひとが項について語るとき，
-それは型ではない項を意味します．しかし常にそうとは限りません．私が初心者の頃は，これで混乱しました．
+それは型ではない項を意味します．しかし常にそうとは限りません．私が初心者の頃は，これで混乱しました．