Simpler delooping constructions for presented groups in HoTT using 2-polygraphs, Cayley graphs, and complexes, formalized in cubical Agda.
Classifying Types
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
abstract
The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.
verdicts
UNVERDICTED 2representative citing papers
Decalf equips types with an intrinsic preorder so that cost bounds for effectful programs become ordinary programs, extending Calf to probabilistic choice and other effects, with a model in augmented simplicial sets.
citing papers explorer
-
Delooping presented groups in homotopy type theory
Simpler delooping constructions for presented groups in HoTT using 2-polygraphs, Cayley graphs, and complexes, formalized in cubical Agda.
-
Decalf: A Directed, Effectful Cost-Aware Logical Framework
Decalf equips types with an intrinsic preorder so that cost bounds for effectful programs become ordinary programs, extending Calf to probabilistic choice and other effects, with a model in augmented simplicial sets.