2016/02/29 by Taichi Uemura · 1 citation
Mathematics · #Advanced Topics in Algebra #Algebra over a field #Algebraic structures and combinatorial models #Categorical variable #Combinatorics #Concatenation (mathematics) #Discrete mathematics #Fibered knot #Fibration #Homotopy #Homotopy and Cohomology in Algebraic Topology #Mathematics #Pure mathematics #Type (biology) #Type theory #math.CT
paper · pdf · doi:10.1109/lics.2017.8005084
arxiv created 2017/04/20 · openalex publication_date 2017/06/01 · arxiv updated 2017/09/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Lö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.