We present our library for universal algebra in the UniMath framework dealing with multi-sorted signatures, their algebras and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.

This article constructs the moduli stack of torsion-free $G$-jet-structures in homotopy type theory with one monadic modality. This yields a construction of this moduli stack for any $\infty$-topos equipped with any stable factorization systems.

In the intended applications of this theory, the factorization systems are given by the deRham-Stack construction. Homotopy type theory allows a formulation of this abstract theory with surprisingly low complexity. This is witnessed by the accompanying formalization of large parts of this work.

This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, that is, generating covers are given by localization maps for finitely many elements $f_1,\dots, f_n$ that generate the ideal $(1)=A\subseteq A$. We use homotopy-type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types – in the homotopical sense – to define and reason about cohomology. Actually computing cohomology groups seems to need a principle along the lines of our “Zariski local choice” axiom, which we justify as well as the other axioms using a cubical model of homotopy-type theory.

When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$, is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of $\mathcal{Set}$ hold for $\mathcal{hSet}$ ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that $\mathsf{Ob}\,\mathcal{hSet}$ is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example, when constructing internal models of type theory. In this work, we equip the type of iterative sets $\mathsf{V}^0$, due to Gylterud ((2018). The Journal of Symbolic Logic 83 (3) 1132–1146) as a refinement of the pioneering work of Aczel ((1978). Logic Colloquium’77, Studies in Logic and the Foundations of Mathematics, vol. 96, Elsevier, 55–66.) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize $\mathsf{V}^0$ into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of $\mathsf{V}^0$ and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from $\mathsf{V}^0$ into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in $\texttt{Agda}$ using the $\texttt{agda}$-$\texttt{unimath}$ library of univalent mathematics.

We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry non-trivial (non-discrete) homotopical structure. In the spirit of realizability, this is intended to formalize a homotopical BHK interpretation, whereby evidence for an identification is a path. Specifically, we study partitioned groupoidal assemblies. Categories of such are parameterized by “realizer categories” (instead of the usual partial combinatory algebras) that come equipped with an interval qua internal cogroupoid. The interval furnishes a notion of homotopy as well as a fundamental groupoid construction. Objects in a base groupoid are realized by points in the fundamental groupoid of some object from the realizer category; isomorphisms in the base groupoid are realized by paths in said fundamental groupoid. The main result is that, under mild conditions on the realizer category, the ensuing category of partitioned groupoidal assemblies models intensional (1-truncated) type theory without function extensionality. Moreover, when the underlying realizer category is “untyped,” there exists an impredicative universe of 1-types (the modest fibrations). This is a groupoidal analog of the traditional situation.

In this paper, we study the approximate minimization problem of weighted finite automata (WFAs): to compute the best possible approximation of a WFA given a bound on the number of states. By reformulating the problem in terms of Hankel matrices, we leverage classical results on the approximation of Hankel operators, namely the celebrated Adamyan-Arov-Krein (AAK) theory. We solve the optimal spectral-norm approximate minimization problem for irredundant WFAs with real weights, defined over a one-letter alphabet. We present a theoretical analysis based on AAK theory and bounds on the quality of the approximation in the spectral norm and $\ell ^2$ norm. Moreover, we provide a closed-form solution, and an algorithm, to compute the optimal approximation of a given size in polynomial time.

This paper explain how the geometric notions of local contractibility and properness are related to the $\Sigma$-types and $\Pi$-types constructors of dependent type theory. We shall see how every Grothendieck fibration comes canonically with such a pair of notions—called smooth and proper maps—and how this recovers the previous examples and many more. This paper uses category theory to reveal a common structure between geometry and logic, with the hope that the parallel will be beneficial to both fields. The style is mostly expository, and the main results are proved in external references.

In homotopy type theory, few constructions have proved as troublesome as the smash product. While its definition is just as direct as in classical mathematics, one quickly realises that in order to define and reason about functions over iterations of it, one has to verify an exponentially growing number of coherences. This has led to crucial results concerning smash products remaining open. One particularly important such result is the fact that the smash product forms a (1-coherent) symmetric monoidal product on the universe of pointed types. This fact was used, without a complete proof, by, for example, Brunerie ((2016) PhD thesis, Université Nice Sophia Antipolis) to construct the cup product on integral cohomology and is, more generally, a fundamental result in traditional algebraic topology. In this paper, we salvage the situation by introducing a simple informal heuristic for reasoning about functions defined over iterated smash products. We then use the heuristic to verify, for example, the hexagon and pentagon identities, thereby obtaining a proof of symmetric monoidality. We also provide a formal statement of the heuristic in terms of an induction principle concerning the construction of homotopies of functions defined over iterated smash products. The key results presented here have been formalised in the proof assistant Cubical Agda.

We give a simple, direct, and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of automatic differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show how this code transformation provides us with correct forward- and reverse-mode AD.

The starting point is to interpret a functional programming language as a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD code transformation and the basic $\boldsymbol{\omega } \mathbf{Cpo}$-semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument.

The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $\omega$-cpos.

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion () order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix. We studied these logics extensively in Gomes et al. ((2022). Electronic Proceedings in Theoretical Computer Science 357 56–76.) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and order-preserving and $\top$-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil’s “symmetric modal logic.” For the order-preserving Set-Set logic, in particular, we obtain a Set-Set axiomatization that is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.

We discuss the complexity of completions of partial combinatory algebras, in particular, of Kleene’s first model. Various completions of this model exist in the literature, but all of them have high complexity. We show that although there are no computable completions, there exist completions of low Turing degree. We use this construction to relate completions of Kleene’s first model to complete extensions of $\mathrm{PA}$. We also discuss the complexity of pcas defined from nonstandard models of $\mathrm{PA}$.

One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in $\textrm{PA}+\bigcup _{\beta \prec \alpha } \textrm{TI}({\prec_{\beta}})$, the extension of Peano arithmetic by transfinite induction up to the ordinals below $\alpha$. Roughly speaking, we identify the functions as the ones that are computable by a sequence of $\textrm{PV}$-provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below $\alpha$, decreasing by the modifications. In the second part, and choosing $l \leq k$, we use similar technique to capture the functions with bounded definitions in the theory $T^k_2$ (resp. $S^k_2$) as the functions computable by exponentially (resp. polynomially) long sequence of $\textrm{PV}_{k-l +1}$-provable reductions between $l$-turn games starting with an explicit $\textrm{PV}_{k-l +1}$-provable winning strategy for the first game.

We take another look at the construction by Hofmann and Streicher of a universe $(U,{\mathcal{E}l})$ for the interpretation of Martin-Löf type theory in a presheaf category $[{{{\mathbb{C}}}^{\textrm{op}}},\textsf{Set}]$. It turns out that $(U,{\mathcal{E}l})$ can be described as the nerve of the classifier $\dot{{\textsf{Set}}}^{\textsf{op}} \rightarrow{{\textsf{Set}}}^{\textsf{op}}$ for discrete fibrations in $\textsf{Cat}$, where the nerve functor is right adjoint to the so-called “Grothendieck construction” taking a presheaf $P :{{{\mathbb{C}}}^{\textrm{op}}}\rightarrow{\textsf{Set}}$ to its category of elements $\int _{\mathbb{C}} P$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.

Generalized Algebraic Data Types (GADTs) are a syntactic generalization of the usual algebraic data types (ADTs), such as lists, trees, etc. ADTs’ standard initial algebra semantics (IAS) in the category $\mathit{Set}$ of sets justify critical syntactic constructs – such as recursion, pattern matching, and fold – for programming with them. In this paper, we show that semantics for GADTs that specialize to the IAS for ADTs are necessarily unsatisfactory. First, we show that the functorial nature of such semantics for GADTs in $\mathit{Set}$ introduces ghost elements, i.e., elements not writable in syntax. Next, we show how such ghost elements break parametricity. We observe that the situation for GADTs contrasts dramatically with that for ADTs, whose IAS coincides with the parametric model constructed via their Church encodings in System F. Our analysis reveals that the fundamental obstacle to giving a functorial IAS for GADTs is the inherently partial nature of their map functions. We show that this obstacle cannot be overcome by replacing $\mathit{Set}$ with other categories that account for this partiality.

Computability on uncountable sets has no standard formalization, unlike that on countable sets, which is given by Turing machines. Some of the approaches to define computability in these sets rely on order-theoretic structures to translate such notions from Turing machines to uncountable spaces. Since these machines are used as a baseline for computability in these approaches, countability restrictions on the ordered structures are fundamental. Here, we show several relations between the usual countability restrictions in order-theoretic theories of computability and some more common order-theoretic countability constraints, like order density properties and functional characterizations of the order structure in terms of multi-utilities. As a result, we show how computability can be introduced in some order structures via countability order density and multi-utility constraints.

We present an adapted construction of algebraic circuits over the reals introduced by Cucker and Meer to arbitrary infinite integral domains and generalize the $\mathrm{AC}_{\mathbb{R}}$ and $\mathrm{NC}_{\mathbb{R}}^{}$ classes for this setting. We give a theorem in the style of Immerman’s theorem which shows that for these adapted formalisms, sets decided by circuits of constant depth and polynomial size are the same as sets definable by a suitable adaptation of first-order logic. Additionally, we discuss a generalization of the guarded predicative logic by Durand, Haak and Vollmer, and we show characterizations for the $\mathrm{AC}_{R}$ and $\mathrm{NC}_R^{}$ hierarchy. Those generalizations apply to the Boolean $\mathrm{AC}$ and $\mathrm{NC}$ hierarchies as well. Furthermore, we introduce a formalism to be able to compare some of the aforementioned complexity classes with different underlying integral domains.

In this paper, we present a constructive and proof-relevant development of graph theory, including the notion of maps, their faces and maps of graphs embedded in the sphere, in homotopy type theory (HoTT). This allows us to provide an elementary characterisation of planarity for locally directed finite and connected multigraphs that takes inspiration from topological graph theory, particularly from combinatorial embeddings of graphs into surfaces. A graph is planar if it has a map and an outer face with which any walk in the embedded graph is walk-homotopic to another. A result is that this type of planar maps forms a homotopy set for a graph. As a way to construct examples of planar graphs inductively, extensions of planar maps are introduced. We formalise the essential parts of this work in the proof assistant Agda with support for HoTT.

It is known that without synchronization via a global clock one cannot obtain common knowledge by communication. Moreover, it is folklore that without communicating higher-level information one cannot obtain arbitrary higher-order shared knowledge. Here, we make this result precise in the setting of gossip where agents make one-to-one telephone calls to share secrets: we prove that “everyone knows that everyone knows that everyone knows all secrets” is unsatisfiable in a logic of knowledge for gossiping. We also prove that, given n agents, $2n-3$ calls are optimal to reach “someone knows that everyone knows all secrets” and that $n - 2 + \binom{n}{2}$ calls are optimal to reach “everyone knows that everyone knows all secrets.”

Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by imposing a soundness condition on derivations. The most common such condition is the global trace condition (GTC), a condition on the infinite paths through the derivation graph. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: first, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing a Ramsey-style trace condition. Furthermore, we connect our notion of trace to automata theory and prove that verifying the GTC for abstract cyclic proofs with certain trace conditions is PSPACE-complete.

Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition calculus with contraction rules is refutationally complete. In particular, this paper presents a new decision procedure for solving word problems over strings and provides a new method of solving unification problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system with contraction rules.