翻訳開始

lean-ja · Aug 14, 2024 · 8fe60a8 · 8fe60a8
1 parent f66242f
commit 8fe60a8
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/functional-programming-lean/src/dependent-types/indices-parameters-universes.md b/functional-programming-lean/src/dependent-types/indices-parameters-universes.md
@@ -1,4 +1,6 @@
-# Indices, Parameters, and Universe Levels
+<!-- # Indices, Parameters, and Universe Levels -->
+
+# 添字、パラメータ、宇宙レベル
 
 The distinction between indices and parameters of an inductive type is more than just a way to describe arguments to the type that either vary or do not between the constructors.
 Whether an argument to an inductive type is a parameter or an index also matters when it comes time to determine the relationships between their universe levels.