This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent cubical set model. enables new ways reason about identity types, for instance, function extensionality provable the system. Further, Voevodsky's univalence axiom this We also explain extension with some higher inductive types like circle and propositional truncation. Finally we provide semantics constructive meta-theory.

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of major implementations lack powerful extensionality principles reasoning about equality, such as function propositional extensionality. These are typically added axiomatically which disrupts constructive properties these systems. Cubical provides a solution by giving computational meaning to Homotopy Type Theory Univalent Foundations, in...

Cubical type theory provides a constructive justification to certain aspects of homotopy such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. paper describes semantics, expressed presheaf topos with suitable structure inspired by cubical sets, some higher inductive types. It also extends syntax for types spheres, torus, suspensions, truncations, pushouts. All these are justified...

This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent cubical set model. enables new ways reason about identity types, for instance, function extensionality provable the system. Further, Voevodsky's univalence axiom this We also explain extension with some higher inductive types like circle and propositional truncation. Finally we provide semantics constructive meta-theory.

Abstract Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of major implementations lack powerful extensionality principles reasoning about equality, such as function propositional extensionality. These are typically added axiomatically which disrupts constructive properties these systems. Cubical provides a solution by giving computational meaning to Homotopy Type Theory Univalent Foundations,...

In their usual form, representation independence metatheorems provide an external guarantee that two implementations of abstract interface are interchangeable when they related by operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal such invariance results within the itself, in order obtain correctness theorems for complex transferring them from simpler, implementations. Recent work proof assistants has shown Voevodsky's...

This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to in Smith normal form. The main results are the these support essential operations algebra, classification theorem finitely presented modules such and uniqueness form up multiplication by units. We present formally verified algorithms computing this on variety coefficient structures including Euclidean domains constructive principal ideal domains. also...

We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work models, ours depends neither diagonal cofibrations nor connections. This is made possible by weakening the notion fibration from cartesian set model, so that it not necessary to assume interval cofibration. have formally verified in Agda these fibrations are closed under formers and satisfies univalence axiom. By applying construction presence or connections reversals, we recover existing De...

Persistent homology is one of the most active branches computational algebraic topology with applications in several contexts such as optical character recognition or analysis point cloud data. In this article, we report on formal development certified programs to compute persistent Betti numbers , an instrumental tool homology, using C oq proof assistant together SSR eflect extension. To aim it has been necessary formalize underlying mathematical theory these algorithms. This another...

Homotopy type theory is an extension of that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations multiple classical results from However, many proofs are still surprisingly complicated formalize. One reason for this the axiomatic treatment univalence higher inductive types which complicates as intermediate steps, could hold simply by computation, require explicit arguments. Cubical offers a solution in form new with native support...

Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of classical result that fourth homotopy group 3-sphere is ℤ/2ℤ. The one most impressive pieces theory to date and uses a lot advanced algebraic topology rephrased synthetically. Furthermore, fully constructive main can be reduced question whether particular "Brunerie number" β normalized ±2. could formalized assistant, either by computing this number or formalizing pen-and-paper proof, has since...

In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of rings. These rings may be defined as direct sums groups together with a multiplication induced cup product, can in many cases characterized quotients multivariate polynomial To this end, we introduce appropriate definitions graded rings, which then use to define both Using this,...

This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well its computer formalisation. The objectives this are (1) to generalise previous work on integral HoTT by current authors and Brunerie (2022) with arbitrary coefficients (2) provide mathematical details of, extend, results underpinning formalisation rings Lamiaux (2023). With respect objective (1), we new direct definitions group operations cup product, which, just (Brunerie et al., 2022),...

When working in Homotopy Type Theory and Univalent Foundations, the traditional role of category sets, Set, is replaced by hSet homotopy sets (h-sets); types with h-propositional identity types. Many properties Set hold for ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, univalence axiom implies that Ob(hSet) not itself an h-set, but h-groupoid. This expected univalent foundations, it sometimes useful to also have a stricter universe example when constructing...

When working in a proof assistant, automation is key to discharging routine goals such as equations between algebraic expressions. Homotopy Type Theory allows the user reason about higher structures, topological spaces, using inductive types (HITs) and univalence. Cubical Agda an extension of with computational support for HITs A difficulty when dealing complex combinatorics infinite-dimensional generalisation equational reasoning. To solve these higher-dimensional consists constructing...

Abstract When working in homotopy type theory and univalent foundations, the traditional role of category sets, $\mathcal{Set}$ , is replaced by $\mathcal{hSet}$ sets (h-sets); types with h-propositional identity types. Many properties hold for ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, univalence axiom implies that $\mathsf{Ob}\,\mathcal{hSet}$ not itself an h-set, but h-groupoid. This expected it sometimes useful to also have a stricter universe...

In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from signature, mechanized the UniMath library based on Coq proof assistant. present work, describe what was necessary generalize that account for simply-typed languages. First, some definitions had be generalized natural appearance non-endofunctors case. As it turns out, many cases our results carried over without any code change. Second, an existing...