nLab fiber type

Definition

In a dependent type theory with function types, dependent sum types, and identity types, the fiber (or “fiber type”) of a function $f:A \to B$ over a term $b:B$ is defined to be the type

$$\mathrm{fiber}_{A, B}(f, b) \;\coloneqq\; \sum_{a : A} \big( f(a) = b \big)$$

hence the dependent sum over $A$ of the identity type on $B$ with $f(a)$ and $b$ substituted.

Rules for fiber types

If the dependent type theory does not have dependent sum types, it is still possible to define fiber types by adding the formation, introduction, elimination, computation, and uniqueness rules for fiber types

Formation rules for fiber types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B, x:A \vdash f(x) =_B y \; \mathrm{type}}{\Gamma, f:A \to B, y:B \vdash \mathrm{fiber}_{A, B}(f, y) \; \mathrm{type}}$$

Introduction rules for fiber types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B y \quad \Gamma \vdash a:A \quad \Gamma, f:A \to B, y:B \vdash p:f[a/x] =_B y}{\Gamma, f:A \to B, y:B \vdash (a, b):\mathrm{fiber}_{A, B}(f, y)}$$

Elimination rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma, f:A \to B, y:B \vdash \pi_2(z):f(\pi_1(z)) =_B y}$$

Computation rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B b \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\mathrm{fiber}_{A, B} 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B y \quad \Gamma \vdash a:A}{\Gamma, f:A \to B, y:B \vdash \beta_{\mathrm{fiber}_{A, B} 2}:\pi_2(a, b) =_{f(\pi_1(a, b)) =_B y} b}$$

Uniqueness rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma, f:A \to B, y:B \vdash \eta_{\mathrm{fiber}_{A, B}}:z =_{\mathrm{fiber}_{A, B}(f, y)} (\pi_1(z), \pi_2(z))}$$

See also

• equivalence of types

• fiber

• homotopy fiber

• cofiber type

References

The notion of fiber types (and with it the modern notion of equivalence in homotopy type theory) originates around:

• Vladimir Voevodsky, p. 8, 10 of: Univalent Foundations Project (2010) [pdf, pdf]

Textbook account:

• Univalent Foundations Project, Def. 4.2.4 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

For the corresponding Coq code see

• Vladimir Voevodsky, Foundations/Generalities/uuo.v