cubicaltt

swMATH22723MaRDI QIDQ34514FDOQ34514

Author name not available (Why is that?)

Source code repository: https://github.com/mortberg/cubicaltt

Cited In (56)

• Eliminating dependent pattern matching without K
• Canonicity for cubical type theory
• Guarded Dependent Type Theory with Coinductive Types
• 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
• Title not available (Why is that?)
• A type theory for synthetic $\infty$-categories
• 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
• Models of Type Theory Based on Moore Paths
• Title not available (Why is that?)
• Modelling and computing homotopy types: I
• Guarded cubical type theory
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Naive cubical type theory
• Varieties of Cubical Sets
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Title not available (Why is that?)
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Title not available (Why is that?)
• Title not available (Why is that?)
• The univalence axiom in cubical sets
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The construction of set-truncated higher inductive types
• Some Wellfounded Trees in UniMath
• Combinatorial topology and constructive mathematics
• Cubical methods in homotopy type theory and univalent foundations
• A meaning explanation for HoTT
• Simplicial sets inside cubical sets
• A cubical model of homotopy 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
• Modal dependent type theory and dependent right adjoints
• Constructive sheaf models of type theory
• Title not available (Why is that?)
• Towards a Cubical Type Theory without an Interval
• Ornaments for Proof Reuse in Coq
• Syntax and models of Cartesian cubical type theory
• 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
• A rewriting coherence theorem with applications in homotopy type theory
• Arrow categories of monoidal model categories
• Induced model structures for higher categories
• Title not available (Why is that?)

This page was built for software: cubicaltt