**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

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.

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))}$

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

Last revised on December 27, 2022 at 17:10:10. See the history of this page for a list of all contributions to it.