Cited in
(75)- A rewriting coherence theorem with applications in homotopy type theory
- Canonicity for cubical type theory
- Eliminating dependent pattern matching without K
- A co-reflection of cubical sets into simplicial sets with applications to model structures
- From signatures to monads in \textsf{UniMath}
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- Model structure on the universe of all types in interval type theory
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Canonicity and homotopy canonicity for cubical type theory
- The Frobenius condition, right properness, and uniform fibrations
- Arrow categories of monoidal model categories
- Models of Type Theory Based on Moore Paths
- Modelling and computing homotopy types: I
- Guarded cubical type theory
- Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Naive cubical type theory
- Towards a cubical type theory without an interval
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- The univalence axiom in cubical sets
- scientific article; zbMATH DE number 7288622 (Why is no real title available?)
- Induced model structures for higher categories
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Constructing higher inductive types as groupoid quotients
- APS-1
- Kenzo
- Agda
- Epigram
- Irdis
- HoTT
- UniMath
- CoqMTU
- Ghostbuster
- Idris
- Celf
- RedPRL
- HoTTSQL
- Equations
- MiniML
- ProofPeer
- cart-cube
- scientific article; zbMATH DE number 7215286 (Why is no real title available?)
- The construction of set-truncated higher inductive types
- Models of type theory based on Moore paths
- scientific article; zbMATH DE number 7407785 (Why is no real title available?)
- Some Wellfounded Trees in UniMath
- Combinatorial topology and constructive mathematics
- Cubical methods in homotopy type theory and univalent foundations
- A meaning explanation for HoTT
- A cubical model of homotopy type theory
- Simplicial sets inside cubical sets
- Varieties of cubical sets
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- The clocks they are adjunctions. Denotational semantics for clocked type theory
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Denotational semantics for guarded dependent type theory
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Cubical Agda
- Guarded dependent type theory with coinductive types
- Modal dependent type theory and dependent right adjoints
- Internal parametricity for cubical type theory
- A type theory for synthetic \(\infty\)-categories
- The Cayley-Dickson construction in homotopy type theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- Constructive sheaf models of type theory
- scientific article; zbMATH DE number 7566056 (Why is no real title available?)
- Internal universes in models of homotopy type theory
- Syntax and models of Cartesian cubical type theory
- Ornaments for Proof Reuse in Coq
- An introduction to univalent foundations for mathematicians
- Canonicity and normalization for dependent type theory
- An implementation of effective homotopy of fibrations
- Univalent foundations as structuralist foundations
- Smooth_Manifolds
This page was built for software: cubicaltt
