Univalent polymorphism

DOI10.1016/j.apal.2020.102793zbMath1440.18048arXiv1803.10113OpenAlexW4205371208MaRDI QIDQ1987219

Benno van den Berg

Publication date: 14 April 2020

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1803.10113

zbMATH Keywords

realizabilityhomotopy type theorycategorical semanticsimpredicative type theory

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Categorical semantics of formal languages (18C50) Metamathematics of constructive systems (03F50) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items

On Church’s thesis in cubical assemblies ⋮ Categories of partial equivalence relations as localizations

Uses Software

• Coq
• Lean

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The category of equilogical spaces and the effective topos as homotopical quotients
• Realizability. An introduction to its categorical side
• A small complete category
• Constructivism in mathematics. An introduction. Volume II
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Higher Homotopies in a Hierarchy of Univalent Universes
• A homotopy-theoretic model of function extensionality in the effective topos
• Colimit completions and the effective topos
• The Discrete Objects in the Effective Topos
• Path Categories and Propositional Identity Types
• Internal type theory
• On Church’s thesis in cubical assemblies
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Abstract homotopy theory and generalized sheaf cohomology
• A notion of homotopy for the effective topos