相关论文: Formalizing of Category Theory in Agda

Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-L\"of type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of…

We introduce basic notions in category theory to type theorists, including comprehension categories, categories with attributes, contextual categories, type categories, and categories with families along with additional discussions that are…

An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which concerns the formalization of category theory…

The popular view according to which Category theory provides a support for Mathematical Structuralism is erroneous. Category-theoretic foundations of mathematics require a different philosophy of mathematics. While structural mathematics…

We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-L\"of type theory. Agda allows us to write mathematical definitions,…

The persisting gap between the formal and the informal mathematics is due to an inadequate notion of mathematical theory behind the current formalization techniques. I mean the (informal) notion of axiomatic theory according to which a…

The unprecedented pace of machine learning research has lead to incredible advances, but also poses hard challenges. At present, the field lacks strong theoretical underpinnings, and many important achievements stem from ad hoc design…

Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also…

Dependent types offer great versatility and power, but developing proofs with them can be tedious and requires considerable human guidance. We propose to integrate Satisfiability Modulo Theories (SMT)-based refinement types into the…

The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend…

Theorem provers are tools that help users to write machine readable proofs. Some of this tools are also interactive. The need of such softwares is increasing since they provide proofs that are more certified than the hand written ones. Agda…

The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new mathematical theories capable of…

We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas…

The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and…

System I is a recently introduced simply-typed lambda calculus with pairs where isomorphic types are considered equal. In this work we propose a variant of System I with the type Top, and present a complete formalization of this calculus in…

Despite the considerable interest in new dependent type theories, simple type theory (which dates from 1940) is sufficient to formalise serious topics in mathematics. This point is seen by examining formal proofs of a theorem about…

The development of mathematics has been characterized by the increasing interconnectivity of seemingly separate disciplines. Such interplay has been facilitated by a massive development in formalism; category theory has provided a common…

Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have…

Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata…

Questions of set-theoretic size play an essential role in category theory, especially the distinction between sets and proper classes (or small sets and large sets). There are many different ways to formalize this, and which choice is made…