From f7a004057d3e5c43a5f83f354c47f53774e87a42 Mon Sep 17 00:00:00 2001
From: s-taiga <neverbefore351@gmail.com>
Date: Sun, 25 Aug 2024 14:50:57 +0900
Subject: [PATCH] =?UTF-8?q?=E3=82=BB=E3=83=AB=E3=83=95=E3=83=AC=E3=83=93?=
 =?UTF-8?q?=E3=83=A5=E3=83=BC?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 functional-programming-lean/src/SUMMARY.md         |  2 +-
 .../indices-parameters-universes.md                | 14 ++++----------
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md
index 3aacd52d..24672165 100644
--- a/functional-programming-lean/src/SUMMARY.md
+++ b/functional-programming-lean/src/SUMMARY.md
@@ -56,7 +56,7 @@
   - [添字族](dependent-types/indexed-families.md)
   - [ユニバースによるデザインパターン](dependent-types/universe-pattern.md)
   - [使用事例：型付きクエリ](dependent-types/typed-queries.md)
-  - [Indices, Parameters, and Universe Levels](dependent-types/indices-parameters-universes.md)
+  - [添字・パラメータ・宇宙レベル](dependent-types/indices-parameters-universes.md)
   - [Pitfalls of Programming with Dependent Types](dependent-types/pitfalls.md)
   - [Summary](./dependent-types/summary.md)
 - [Interlude: Tactics, Induction, and Proofs](./tactics-induction-proofs.md)
diff --git a/functional-programming-lean/src/dependent-types/indices-parameters-universes.md b/functional-programming-lean/src/dependent-types/indices-parameters-universes.md
index 1dbede4a..71a9f723 100644
--- a/functional-programming-lean/src/dependent-types/indices-parameters-universes.md
+++ b/functional-programming-lean/src/dependent-types/indices-parameters-universes.md
@@ -2,7 +2,7 @@
 # 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.
@@ -161,19 +161,13 @@ The rules of parameters and indices are as follows:
 
  <!--
  1. Parameters must be used identically in each constructor's type.
- -->
- 1. パラメータは各コンストラクタの型で同じものを使用しなければなりません。
- <!--
  2. All parameters must come before all indices.
- -->
- 2. すべてのパラメータはすべての添字より前に来なければなりません。
- <!--
  3. The universe level of the datatype being defined must be at least as large as the largest parameter, and strictly larger than the largest index.
- -->
- 3. 定義されるデータ型の宇宙レベルは最も低くても最大のパラメータのものと同じ大きさでなければならず、最大の添字より大きくなければなりません。
- <!--
  4. Named arguments written before the colon are always parameters, while arguments after the colon are typically indices. Lean may determine that the usage of arguments after the colon makes them into parameters if they are used consistently in all constructors and don't come after any indices.
  -->
+ 1. パラメータは各コンストラクタの型で同じものを使用しなければなりません。
+ 2. すべてのパラメータはすべての添字より前に来なければなりません。
+ 3. 定義されるデータ型の宇宙レベルは最も低くても最大のパラメータのものと同じ大きさでなければならず、最大の添字より大きくなければなりません。
  4. コロンの前に書かれた名前付きの引数は常にパラメータであり、コロンの後ろに書かれた引数は通常は添字です。コロンの後ろにある引数が一貫して使われ、かつ添字より後ろに来ないように使われている場合、それらをパラメータに変更するよう判断できます。
 
 <!--