scientific article; zbMATH DE number 7003197

DOI10.23638/LMCS-15(1:2)2019MaRDI QIDQ4611383

Ian Orton, Andrew M. Pitts

Publication date: 18 January 2019

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

toposhomotopy theorydependent type theoryMoore path

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Uses Software

• cubicaltt
• GitHub
• cart-cube

Cites Work

• Sheaves in geometry and logic: a first introduction to topos theory
• Wellfounded trees in categories
• Topological and Simplicial Models of Identity Types
• The Local Universes Model
• Natural models of homotopy type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Globalizing fibrations by schedules
• On a Topological Topos
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Path Categories and Propositional Identity Types
• Internal type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item