Fibred Fibration Categories
Category Theory
2017-09-25 v5
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.
Keywords
Cite
@article{arxiv.1602.08206,
title = {Fibred Fibration Categories},
author = {Taichi Uemura},
journal= {arXiv preprint arXiv:1602.08206},
year = {2017}
}