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