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