HoTT
From MaRDI portal
Cited in
(33)- Roosterize
- PCM library
- Homotopy type theory in Lean
- A formalized general theory of syntax with bindings: extended version
- Categoricity results and large model constructions for second-order ZF in dependent type theory
- Formalizing abstract computability: Turing categories in Coq
- Internal languages of finitely complete ( , 1)-categories
- Mtac
- UniMath
- Idempotents in intensional type theory
- Globular
- CertiKOS
- cubicaltt
- RedPRL
- MathOverflow
- SerAPI
- Quotienting the delay monad by weak bisimilarity
- Foundations of dependent interoperability
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- cart-cube
- An introduction to univalent foundations for mathematicians
- Semantics of higher inductive types
- scientific article; zbMATH DE number 7474655 (Why is no real title available?)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Synthetic topology in Homotopy Type Theory for probabilistic programming
- The Marriage of Univalence and Parametricity
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Extensional constructive real analysis via locators
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
- UALib
- JSNice
- Category theory in Coq 8.5
This page was built for software: HoTT
