cubicaltt

swMATH22723MaRDI QIDQ34514FDOQ34514

Author name not available (Why is that?)

Official website: https://github.com/mortberg/cubicaltt

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

Cited In (75)

• Arrow categories of monoidal model categories
• Models of Type Theory Based on Moore Paths
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically
• Induced model structures for higher categories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Eliminating dependent pattern matching without K
• Canonicity for cubical type theory
• 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
• Modelling and computing homotopy types: I
• Guarded cubical type theory
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• 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
• Title not available (Why is that?)
• Constructing higher inductive types as groupoid quotients
• Title not available (Why is that?)
• The construction of set-truncated higher inductive types
• APS-1
• Kenzo
• Models of type theory based on Moore paths
• Agda
• Epigram
• Irdis
• HoTT
• UniMath
• Some Wellfounded Trees in UniMath
• Combinatorial topology and constructive mathematics
• CoqMTU
• Ghostbuster
• Idris
• Celf
• RedPRL
• HoTTSQL
• Equations
• MiniML
• ProofPeer
• cart-cube
• 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
• 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
• Smooth_Manifolds
• Modal dependent type theory and dependent right adjoints
• Internal parametricity for cubical type theory
• Guarded dependent type theory with coinductive types
• Constructive sheaf models of type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• A type theory for synthetic \(\infty\)-categories
• The Cayley-Dickson construction in homotopy type theory
• Internal universes in models of homotopy type theory
• Ornaments for Proof Reuse in Coq
• Syntax and models of Cartesian cubical type theory
• An introduction to univalent foundations for mathematicians
• Cubical Agda
• 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

This page was built for software: cubicaltt