cubicaltt

swMATH22723MaRDI QIDQ34514

No author found.

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

Related Items (56)

Varieties of Cubical Sets ⋮ The construction of set-truncated higher inductive types ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ Simplicial sets inside cubical sets ⋮ Constructive sheaf models of type theory ⋮ Unnamed Item ⋮ Homotopy type theory in Lean ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Meaning explanations at higher dimension ⋮ Modelling and computing homotopy types: I ⋮ Canonicity and normalization for dependent type theory ⋮ An implementation of effective homotopy of fibrations ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Leibniz equality is isomorphic to Martin-Löf identity, parametrically ⋮ Univalent foundations as structuralist foundations ⋮ Eliminating dependent pattern matching without K ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ Unnamed Item ⋮ Denotational semantics for guarded dependent type theory ⋮ A type theory for synthetic $\infty$-categories ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Ornaments for Proof Reuse in Coq ⋮ Unnamed Item ⋮ The Frobenius condition, right properness, and uniform fibrations ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ Combinatorial topology and constructive mathematics ⋮ A cubical model of homotopy type theory ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Unnamed Item ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Modal dependent type theory and dependent right adjoints ⋮ A meaning explanation for HoTT ⋮ Some Wellfounded Trees in UniMath ⋮ The univalence axiom in cubical sets ⋮ Canonicity for cubical type theory ⋮ Guarded cubical type theory ⋮ From signatures to monads in \textsf{UniMath} ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Towards a Cubical Type Theory without an Interval ⋮ Arrow categories of monoidal model categories ⋮ Models of Type Theory Based on Moore Paths ⋮ A co-reflection of cubical sets into simplicial sets with applications to model structures ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Induced model structures for higher categories ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS ⋮ A rewriting coherence theorem with applications in homotopy type theory

This page was built for software: cubicaltt