Fibred fibration categories
From MaRDI portal
Type theory (03B38) Foundations, relations to logic and deductive systems (18A15) Homotopical algebra, Quillen model categories, derivators (18N40) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Abstract and axiomatic homotopy theory in algebraic topology (55U35)
Abstract: We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L"{o}f type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.
Recommendations
Cited in
(11)- PL fibrations are fibrations in the PL category
- Categorical notions of fibration
- Internal languages of finitely complete ( , 1)-categories
- scientific article; zbMATH DE number 3873561 (Why is no real title available?)
- Bundles Along the Fiber in the PL Category
- scientific article; zbMATH DE number 4101436 (Why is no real title available?)
- scientific article; zbMATH DE number 6152757 (Why is no real title available?)
- A cubical language for Bishop sets
- Indexed type theories
- Homotopy type theory as a language for diagrams of -logoses
- Strict universes for Grothendieck topoi
This page was built for publication: Fibred fibration categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5144630)
