The development of category theory in univalent foundations and the formalization thereof is an active field of research. Categories in that setting are often assumed to be univalent which means that identities and isomorphisms of objects coincide. One consequence hereof is that equivalences and identities coincide for univalent categories and that structure on univalent categories transfers along equivalences. However, constructions such as the Kleisli category, the Karoubi envelope, and the tripos-to-topos construction, do not necessarily give univalent categories. To deal with that problem, one uses the Rezk completion, which completes a category into a univalent one. However, to use the Rezk completion when considering categories with structure, one also needs to show that the Rezk completion inherits the structure from the original category. In this work, we present a modular framework for lifting the Rezk completion from categories to categories with structure. We demonstrate the modularity of our framework by lifting the Rezk completion from categories to elementary topoi in manageable steps.
Type theories with multi-clocked guarded recursion provide a flexible framework for programming with coinductive types encoding productivity in types. Combining this with solutions to general guarded domain equations one can also construct relatively simple denotational models of programming languages with advanced features. These constructions have previously been explored in the setting of extensional type theory through a presheaf model, which proves correctness of encodings of W-types. That model has been adapted to presheaves of cubical sets (functors into the category of cubical sets), where the model verifies correctness of encodings also of coinductive types whose definitions involve quotient inductive types such as finite powersets or finite distributions. Likewise the cubical model also verifies correctness of coinductive predicates defined using existential quantification and allows the results to be related to the global world of cubical sets. This paper looks at how to extend the extensional presheaf model of multi-clocked guarded recursion to higher ordinals, so that correctness of encodings of coinductive types can be extended from W-types to those involving finite powersets and finite distributions, as well as coinductive predicates involving existential quantification. This extension will allow results previously proved in Clocked Cubical Type Theory to be interpreted in a model based on set-theory, proving the correctness of these results as understood in their usual set theoretic interpretation.
There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, which can be used to specify the type of binders. The resulting syntax representation (nominal data types) makes alpha-equivalent terms equal, and features a name-invariant induction principle. It is known that name abstraction types can be presented either as existential or universal quantification on names. On the one hand, nominal frameworks use the existential presentation for practical reasoning since the user is allowed to match on a name-term pattern where the name is bound in the term. However inference rules for existential name abstraction are cumbersome to specify/implement because they must keep track of information about free and bound names at the type level. On the other hand, universal name abstractions are easier to specify since they are treated not as pairs, but as functions consuming fresh names. Yet the ability to pattern match on such functions is seemingly lost. In this work we show that this ability and others are recovered in a type theory consisting of (1) nullary (0-ary) internally parametric type theory (nullary PTT) (2) a type of names and a novel name induction principle (3) nominal data types. This extension of nullary PTT can act as a legitimate nominal framework. Indeed it has universal name abstractions, nominal pattern matching, a freshness type former, name swapping and local-scope operations and (non primitive) existential name abstractions. We illustrate how term-relevant nullary parametricity is used to recover nominal pattern matching. Our main example involves synthetic Kripke parametricity.
Sorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on the underlying set of elements. As mathematical functions, they are functions on lists that perform combinatorial operations on the representation of the input list. In this paper, we study sorting algorithms conceptually as abstract sorting functions. There is a canonical surjection from the free monoid on a set (lists of elements) to the free commutative monoid on the same set (multisets of elements). We show that sorting functions determine a section (right inverse) to this surjection satisfying two axioms, that do not presuppose a total order on the underlying set. Then, we establish an equivalence between (decidable) total orders on the underlying set and correct sorting functions. The first part of the paper develops concepts from universal algebra from the point of view of functorial signatures, and gives constructions of free monoids and free commutative monoids in (univalent) type theory. Using these constructions, the second part of the paper develops the axiomatisation of sorting functions. The paper uses informal mathematical language, and comes with an accompanying formalisation in Cubical Agda.
The operations to be performed by a quantum computer are almost invariably given in the form of a quantum circuit. In the final stage of compilation, a quantum circuit must be translated into the input signals accepted by the quantum hardware itself. For a quantum computer based on superconducting qubits, this will be a sequence of microwave control pulses to be sent to the various input channels. A pulse schedule gives a full specification for which pulse should be applied to which channel at what time. There is as yet no language for these pulse schedules that is very amenable to formal semantics. In this paper, we propose such a language called GRAMPUS (GRAded Modal type theory for PUlse Schedules). It is a graded modal type theory, where the grades represent timing information: a variable x :^50 Q_1 will represent a state of qubit Q_1 that will exist 50 nanoseconds in the future, and a variable y :^-75 Q_2 will represent a state of qubit Q_2 that existed 75 nanoseconds in the past. We give the syntax for two type theories, one with grades (the annotated language) and one without (the plain language). We prove some metatheoretic properties, and describe the semantics in terms of category theory. We show that the input signals to a quantum chip forms a model of the annotated language. We also give a syntatic model, prove that it is initial, and hence prove soundness and completeness theorems.
In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20
We propose weaker but constructively provable variants of the contrapositive of Konig ' s lemma. We derive those from a generalization of the FAN theorem for inductive bars to inductive covers, for which we give a concise proof. We compare the positive, negative and sequential characterizations of covers and bars in classical and constructive contexts, giving precise accounts of the role played by the axioms of excluded middle and dependent choice. As an application, we discuss some examples where the use of Konig's lemma can be replaced by one of our weaker variants to obtain fully constructive accounts of results or proofs that could otherwise appear as inherently classical. 2012 ACM Subject Classification Theory of computation -> Type theory; Theory of computation -> Constructive mathematics
We report on an experimental implementation in Haskell of a dependent type theory featuring an observational equality type, based on Pujet et al.' s CCobs. We use normalisation by evaluation to produce an efficient normalisation function, which is used to implement a bidirectional type checker. To allow for greater expressivity, we extend the core CCobs calculus with quotient types and inductive types. To make the system usable, we explore various proof-assistant features, notably a rudimentary version of a "hole" system similar to Agda ' s. While rather crude, this experience should inform other, more substantial implementation efforts of observational equality. 2012 ACM Subject Classification Software and its engineering -> Functional languages; Theory of computation -> Type theory; Theory of computation -> Denotational semantics
We provide a comprehensive classification of the cofibration entailment problem, COFENT, for the cofibration logics of various cubical type theories in use today. The problem COFENT arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an n-dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of COFENT are coNP-complete. 2012 ACM Subject Classification Theory of computation -> Type theory
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids. Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.2012 ACM Subject Classification Theory of computation -> Type theory; Theory of computation -> Categorical semantics
Intersection type systems, as adequate models of the.-calculus, induce an equational theory on terms, that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system. We prove a folklore result: weak head type equivalence coincides with Sangiorgi ' s normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence. The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing shape typings that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term. 2012 ACM Subject Classification Theory of computation -> Lambda calculus
