10 citations · 19 across the 3 of their papers we have counts for
3 papers
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first…
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library bas…
Cubical Type Theory: a constructive interpretation of the univalence axiom
Cyril Cohen, Thierry Coquand, Simon Huber +1
This paper presents a type theory in which it is possible to directly manipulate -dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent…