feat: Replace Coq by Rocq

cf. hmemcpy/milewski-ctfp-pdf#398

Author: ktgw0316

english/part1/ch09.md

@@ -344,9 +344,9 @@ newtype Void = Void Void
 \noindent
 As always, the type `Void` is tricky. This definition makes it impossible to construct a value because in order to construct one, you would need to provide one. Therefore, the function `absurd` can never be called.
 
-These are all interesting examples, but is there a practical side to Curry-Howard isomorphism? Probably not in everyday programming. But there are programming languages like Agda or Coq, which take advantage of the Curry-Howard isomorphism to prove theorems.
+These are all interesting examples, but is there a practical side to Curry-Howard isomorphism? Probably not in everyday programming. But there are programming languages like Agda or Rocq^[Formerly known as Coq], which take advantage of the Curry-Howard isomorphism to prove theorems.
 
-Computers are not only helping mathematicians do their work — they are revolutionizing the very foundations of mathematics. The latest hot research topic in that area is called Homotopy Type Theory, and is an outgrowth of type theory. It's full of Booleans, integers, products and coproducts, function types, and so on. And, as if to dispel any doubts, the theory is being formulated in Coq and Agda. Computers are revolutionizing the world in more than one way.
+Computers are not only helping mathematicians do their work — they are revolutionizing the very foundations of mathematics. The latest hot research topic in that area is called Homotopy Type Theory, and is an outgrowth of type theory. It's full of Booleans, integers, products and coproducts, function types, and so on. And, as if to dispel any doubts, the theory is being formulated in Rocq and Agda. Computers are revolutionizing the world in more than one way.
 
 ## Bibliography
 

english/part2/ch04.md

@@ -4,7 +4,7 @@ It's about time we had a little talk about sets. Mathematicians have a love/hate
 
 A set is the closest thing to a featureless blob you can get outside of categorical objects. A set has elements, but you can't say much about these elements. If you have a finite set, you can count the elements. You can kind of count the elements of an infinite set using cardinal numbers. The set of natural numbers, for instance, is smaller than the set of real numbers, even though both are infinite. But, maybe surprisingly, a set of rational numbers is the same size as the set of natural numbers.
 
-Other than that, all the information about sets can be encoded in functions between them --- especially the invertible ones called isomorphisms. For all intents and purposes isomorphic sets are identical. Before I summon the wrath of foundational mathematicians, let me explain that the distinction between equality and isomorphism is of fundamental importance. In fact it is one of the main concerns of the latest branch of mathematics, the Homotopy Type Theory (HoTT). I'm mentioning HoTT because it's a pure mathematical theory that takes inspiration from computation, and one of its main proponents, Vladimir Voevodsky, had a major epiphany while studying the Coq theorem prover. The interaction between mathematics and programming goes both ways.
+Other than that, all the information about sets can be encoded in functions between them --- especially the invertible ones called isomorphisms. For all intents and purposes isomorphic sets are identical. Before I summon the wrath of foundational mathematicians, let me explain that the distinction between equality and isomorphism is of fundamental importance. In fact it is one of the main concerns of the latest branch of mathematics, the Homotopy Type Theory (HoTT). I'm mentioning HoTT because it's a pure mathematical theory that takes inspiration from computation, and one of its main proponents, Vladimir Voevodsky, had a major epiphany while studying the Rocq theorem prover. The interaction between mathematics and programming goes both ways.
 
 The important lesson about sets is that it's okay to compare sets of unlike elements. For instance, we can say that a given set of natural transformations is isomorphic to some set of morphisms, because a set is just a set. Isomorphism in this case just means that for every natural transformation from one set there is a unique morphism from the other set and vice versa. They can be paired against each other. You can't compare apples with oranges, if they are objects from different categories, but you can compare sets of apples against sets of oranges. Often transforming a categorical problem into a set-theoretical problem gives us the necessary insight or even lets us prove valuable theorems.
 

japanese/part1/ch09.md

@@ -363,9 +363,9 @@ newtype Void = Void Void
 \noindent
 いつものように、型`Void`はトリッキーだ。この定義により、値を構成するには値を提供する必要があるため、値を構成できない^[訳注：ここで構成しようとしている値も提供されるべき値もともにVoid型である。]。したがって、この関数`absurd`は決して呼び出せない。
 
-いずれも興味深い例だが、カリー・ハワード同型に実用面はあるのだろうか？　おそらく日々のプログラミングではないだろう。しかし、AgdaやCoqのようなプログラミング言語では、定理を証明するためにカリー・ハワード同型が利用されている。
+いずれも興味深い例だが、カリー・ハワード同型に実用面はあるのだろうか？　おそらく日々のプログラミングではないだろう。しかし、AgdaやRocq^[かつてはCoqとして知られていた。]のようなプログラミング言語では、定理を証明するためにカリー・ハワード同型が利用されている。
 
-コンピューターは数学者の仕事を助けている[^lean]だけでなく、数学の基礎そのものに革命をもたらしている。この分野の注目の最新のホットな研究テーマはホモトピー型理論 (Homotopy Type Theory, HoTT) と呼ばれ、型理論の派生物だ。ブーリアン、整数、積と余積、関数型などでいっぱいだ。そして、疑念を払拭するかのように、その理論はCoqとAgdaで定式化されようとしている。コンピューターは世界にさまざまな形で革命を起こしている。
+コンピューターは数学者の仕事を助けている[^lean]だけでなく、数学の基礎そのものに革命をもたらしている。この分野の注目の最新のホットな研究テーマはホモトピー型理論 (Homotopy Type Theory, HoTT) と呼ばれ、型理論の派生物だ。ブーリアン、整数、積と余積、関数型などでいっぱいだ。そして、疑念を払拭するかのように、その理論はRocqとAgdaで定式化されようとしている。コンピューターは世界にさまざまな形で革命を起こしている。
 
 [^lean]: 訳注：実際にこの種の言語のひとつであるLeanは、Scholze（フィールズ賞受賞者）が定理を確認するのに役立った。参考：
 

japanese/part2/ch04.md

@@ -4,7 +4,7 @@
 
 集合は、圏論における対象たちから取り出せる特徴のない塊、というのが最も近い。集合は要素を含むが、それらについて多くは語れない。有限集合なら要素数を数えられる。基数 (cardinal number) を使えば、無限集合の要素数をある意味で数えられる。たとえば、自然数の集合も実数の集合も無限集合だが、前者は後者よりも小さい。しかし、驚くかもしれないが、有理数の集合は自然数の集合と同じ大きさだ。
 
-それ以外には、集合に関するすべての情報は、集合間の関数――特に、同型と呼ばれる可逆関数――として表せる。どこからどう見ても同型集合は同一だ。数学基礎論の研究者の逆鱗に触れる前に、等しさと同型には根本的に重要な区別があることを説明しておこう。これは数学の最新分野であるホモトピー型理論 (Homotopy Type Theory, HoTT) の主要な関心事の1つだ。ここでHoTTについて触れる理由は、それが計算からインスピレーションを得た純粋な数学理論で、主唱者の1人であるVladimir Voevodskyによる大きな発見が定理証明器Coqを研究しているときに得られたものだからだ。数学とプログラミングの相互作用は双方向なのだ。
+それ以外には、集合に関するすべての情報は、集合間の関数――特に、同型と呼ばれる可逆関数――として表せる。どこからどう見ても同型集合は同一だ。数学基礎論の研究者の逆鱗に触れる前に、等しさと同型には根本的に重要な区別があることを説明しておこう。これは数学の最新分野であるホモトピー型理論 (Homotopy Type Theory, HoTT) の主要な関心事の1つだ。ここでHoTTについて触れる理由は、それが計算からインスピレーションを得た純粋な数学理論で、主唱者の1人であるVladimir Voevodskyによる大きな発見が定理証明器Rocqを研究しているときに得られたものだからだ。数学とプログラミングの相互作用は双方向なのだ。
 
 集合に関する重要な教訓は、別種の要素からなる集合同士を比較しても問題ないということだ。たとえば、任意の自然変換の集合は何らかの射の集合と同型である、などと主張できる。集合は集合にすぎないからだ。この場合の同型は単に、一方の集合に属するどの自然変換に対しても他方の集合に属する一意な射が存在し、その逆もまた成り立つことを意味する。それらは互いにペアにできる。リンゴとオレンジが異なる圏の対象なら比較できないが、リンゴの集合とオレンジの集合は比較できる。多くの場合、圏論の問題を集合論の問題に変換すれば、必要な洞察が得られ、有用な定理を証明することさえ可能になる。