HoTT
From MaRDI portal
Software:27040
swMATH15147MaRDI QIDQ27040FDOQ27040
Author name not available (Why is that?)
Source code repository: https://github.com/HoTT/HoTT
Cited In (20)
- Categoricity results and large model constructions for second-order ZF in dependent type theory
- Synthetic topology in Homotopy Type Theory for probabilistic programming
- Formalizing abstract computability: Turing categories in Coq
- Extensional constructive real analysis via locators
- A formalized general theory of syntax with bindings: extended version
- Semantics of higher inductive types
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Category Theory in Coq 8.5
- Idempotents in intensional type theory
- Title not available (Why is that?)
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Homotopy type theory in Lean
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Quotienting the delay monad by weak bisimilarity
- The Marriage of Univalence and Parametricity
- Foundations of dependent interoperability
- An introduction to univalent foundations for mathematicians
- Internal languages of finitely complete \((\infty , 1)\)-categories
This page was built for software: HoTT
