The compatibility of the minimalist foundation with homotopy type theory

DOI10.1016/j.tcs.2024.114421arXiv2207.03802OpenAlexW4392066353MaRDI QIDQ6122600

Michele Contente, Maria Emilia Maietti

Publication date: 1 March 2024

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

homotopy type theorydependent type theorymany-sorted logicfoundations for constructive mathematicstwo-level foundations

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quotient completion for the foundation of constructive mathematics
• A minimalist two-level foundation for constructive mathematics
• The calculus of constructions
• Independence of the induction principle and the axiom of choice in the pure calculus of constructions
• Wellfounded trees in categories
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• Setoid type theory -- a syntactic translation
• Intuitionistic fixed point logic
• Higher Inductive Types as Homotopy-Initial Algebras
• Elementary quotient completion
• On Choice Rules in Dependent Type Theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Extensional Constructs in Intensional Type Theory
• Internal type theory
• Conservativity of equality reflection over intensional type theory
• Canonicity and homotopy canonicity for cubical type theory
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• On Higher Inductive Types in Cubical Type Theory
• A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
• Relating Quotient Completions via Categorical Logic
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Theorem Proving in Higher Order Logics
• Sets in homotopy type theory

This page was built for publication: The compatibility of the minimalist foundation with homotopy type theory