Experience Implementing a Performant Category-Theory Library in Coq: Complete List of References

For the Coq system, we propose to add the possibility to declare an inductive type as private to the module where it is defined. The effect is to preserve the possibility to compute with a restricted set of functions, but to disallow uses of the more powerful pattern-matching constructs. Such a private type has fruitful applications in homotopy type theory.

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of "category" for which equality and equivalence of categories agree. Such categories satisfy a version of the Univalence Axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them "saturated" or "univalent" categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

Keywords: Mathematics - Category Theory, Mathematics - Logic, 18A15

This article presents a development of Category Theory in Isabelle/HOL. A Category is defined using records and locales. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic. Extensive use is made of the HOLZF theory in both cases.

This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom. Finally, we present two applications of our proof techniques: a key lemma for characterising the discrete logarithm, and a matrix decomposition problem.

Keywords: Formalization of Algebra; Coercive subtyping; Type inference; Coq; SSReflect

Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. This is the first book on the subject and lays its foundations. Many examples are given throughout. There is also an introductory chapter motivating the subject for topologists.

A calculus for a fragment of category theory is presented. The types in the language denote categories and the expressions functors. The judgements of the calculus systematise categorical arguments such as: an expression is functorial in its free variables; two expressions are naturally isomorphic in their free variables. There are special binders for limits and more general ends. The rules for limits and ends support an algebraic manipulation of universal constructions as opposed to a more traditional diagrammatic approach. Duality within the calculus and applications in proving continuity are discussed with examples. The calculus gives a basis for mechanising a theory of categories in a generic theorem prover like Isabelle.

Herein we formalize a segment of category theory using the implementation of Calculus of Inductive Construction in Coq. Adopting the axiomatization proposed by Huet and Saibi we start by presenting basic concepts, examples and results of category theory in Coq. Next we define adjunction and cocartesian lifting and establish some results using the Coq proof assistant. Finally we remark that the axiomatization proposed by Huet and Saibi is not good when dealing with the equality for objects. 1...

Keywords: category-theory, formalization

Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of “universes”, each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure properties of type theories) and some practical (to achieve some of the advantages of a type of all types without sacrificing consistency.) The Generalized Calculus of Constructions (CC^ω) is a formal theory of types that includes such a hierarchy of universes. Although essential to the formalization of constructive mathematics, universes are tedious to use in practice, for one is required to make specific choices of universe levels and to ensure that all choices are consistent. In this paper we study several problems associated with type checking in the presence of universes in the context of CC^ω. First, we consider the basic type checking and well-typedness problems for this calculus. Second, we consider a formulation of Russell and Whitehead's “typical ambiguity” convention whereby universe levels may be elided, provided that some consistent assignment of levels leads to a correct derivation. Third, we consider the introduction of definitions to both the basic calculus and the calculus with typical ambiguity. This extension leads to a notion of “universe polymorphism” analogous to the type polymorphism of ML. Although our study is conducted for CC^ω, we expect that our methods will apply to other variants of the Calculus of Constructions and to type theories such as Constable's V3.