ファイバー - pogi-log

ファイバー

ファイバー(fiber)

$ B がA上の型族(type family) ($ B \in A )であり、$ a:A が存在する場合、$ B[a/x] を$ B の$ a におけるファイバーと呼ぶ。

Definition 1.3.1 When B is a family of types over A in context Γ, and if we have a : A, then we also say that B[a/x] is the fiber of B at a. We will usually write B(a) for the fiber of B at a.

When b is a section of the family B over A in context Γ, we call the element b the value of b at a. Again, we will usually write b(a) for the value of b at a.

ref: 『Introduction to Homotopy Type Theory』 P8

↓

定義 1.3.1 文脈 Γ において、B が A 上の型族であり、a : A が存在する場合、B[a/x] を B の a におけるファイバーと呼ぶ。通常、B の a におけるファイバーを B(a) と表記する。

文脈 Γ において、b が A 上の族 B の断面(sectioin)であるとき、要素 b を a における b の値と呼ぶ。ここでも、a における b の値は通常 b(a) と表記する。

$ B[a/x] はBのaにおけるファイバー

xをaで置き換える

β-簡約？

確認用

Q. ファイバー

参考

『Introduction to Homotopy Type Theory』 P8

E. Rijke, “Introduction to Homotopy Type Theory”. Dec. 21, 2022, arXiv: arXiv:2212.11082. doi: 10.48550/arXiv.2212.11082.