nLab
fiber type
Redirected from "fiber types".
Contents
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 → B f:A \to B over a term b : B b:B is defined to be the type
fiber A , B ( f , b ) ≔ ∑ a : A ( f ( a ) = b )
\mathrm{fiber}_{A, B}(f, b)
\;\coloneqq\;
\sum_{a : A}
\big(
f(a) = b
\big)
hence the dependent sum over A A of the identity type on B B with f ( a ) f(a) and b 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:
Γ ⊢ A type Γ ⊢ B type Γ , f : A → B , y : B , x : A ⊢ f ( x ) = B y type Γ , f : A → B , y : B ⊢ fiber A , B ( f , y ) type \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:
Γ ⊢ A type Γ ⊢ B type Γ , f : A → B , y : B , x : A ⊢ b ( x ) : f ( x ) = B y Γ ⊢ a : A Γ , f : A → B , y : B ⊢ p : f [ a / x ] = B y Γ , f : A → B , y : B ⊢ ( a , b ) : fiber A , B ( f , y ) \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:
Γ , f : A → B , y : B ⊢ z : fiber A , B ( f , y ) Γ ⊢ π 1 ( z ) : A Γ , f : A → B , y : B ⊢ z : fiber A , B ( f , y ) Γ , f : A → B , y : B ⊢ π 2 ( z ) : f ( π 1 ( z ) ) = B y \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:
Γ , f : A → B , y : B , x : A ⊢ b ( x ) : f ( x ) = B b Γ ⊢ a : A Γ ⊢ β fiber A , B 1 : π 1 ( a , b ) = A a Γ , f : A → B , y : B , x : A ⊢ b ( x ) : f ( x ) = B y Γ ⊢ a : A Γ , f : A → B , y : B ⊢ β fiber A , B 2 : π 2 ( a , b ) = f ( π 1 ( a , b ) ) = B y b \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:
Γ , f : A → B , y : B ⊢ z : fiber A , B ( f , y ) Γ , f : A → B , y : B ⊢ η fiber A , B : z = fiber A , B ( f , y ) ( π 1 ( z ) , π 2 ( z ) ) \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
References
The notion of fiber types (and with it the modern notion of equivalence in homotopy type theory ) originates around:
Textbook account:
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.