Indexed type theories

DOI10.1017/S0960129520000092zbMath1494.18018arXiv1806.08038MaRDI QIDQ5156767

Valery Isaev

Publication date: 11 October 2021

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

category theoryhomotopy type theory

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (1)

A formal logic for formal category theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Univalence in locally Cartesian closed categories
• On localization and stabilization for factorization systems
• Internal languages of finitely complete \((\infty , 1)\)-categories
• Idempotents in intensional type theory
• Invariance de laK-Théorie par équivalences dérivées
• A type theory for synthetic $\infty$-categories
• Adjoint functor theorems for ∞‐categories
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Fibred Fibration Categories
• Modalities in homotopy type theory
• Fibrations of $\infty$-categories
• Generalizations of Hedberg’s Theorem
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• Homotopy limits in type theory

This page was built for publication: Indexed type theories