Marco Maggesi

Search for another author

Author Description

Ask a Question About This Mathematician

All published works (36)

Universal algebra in UniMath

2024-12-09

Gianluca Amato , Matteo Calosci , Marco Maggesi +1 more

We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof … We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof assistant. By constituting a formal system for isolating the invariants of the theory we are interested in -- that is, general algebraic structures modulo isomorphism -- Univalent Mathematics seems to provide a suitable environment to carry on our endeavour.

Chat View PDF

Variable binding and substitution for (nameless) dummies

2024-03-01

André Hirschowitz , Tom Hirschowitz , Ambroise Lafont +1 more

By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a … By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

Chat View PDF

Mechanising Gödel-Löb provability logic in HOL Light

2022-01-01

Marco Maggesi , Cosimo Perini Brogi

We introduce our implementation in HOL Light of the metatheory for G\"odel-L\"ob provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem … We introduce our implementation in HOL Light of the metatheory for G\"odel-L\"ob provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation -- according to the formal language and tools at hand -- of the proof given in George Boolos' 1995 monograph. Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness and the design of our proof search algorithm. Furthermore, we propose some examples of the latter's interactive and automated use.

Chat View PDF

Variable binding and substitution for (nameless) dummies

2022-01-01

André Hirschowitz , Tom Hirschowitz , Ambroise Lafont +1 more

Chat View PDF

Bicategories in univalent foundations

2021-11-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Chat View PDF

A formal proof of modal completeness for provability logic.

2021-02-11

Marco Maggesi , Cosimo Perini Brogi

This work presents a formalized proof of modal completeness for Godel-Lob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details … This work presents a formalized proof of modal completeness for Godel-Lob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices in structuring proofs which make essential use of the tools of HOL Light and which differ in part from the standard strategies found in main textbooks covering the topic in an informal setting. Moreover, we propose a reflection on our own experience in using this specific theorem prover for this formalization task, with an analysis of pros and cons of reasoning within and about the formal system for GL we implemented in our code.

Chat View PDF

Universal Algebra in UniMath

2021-01-01

Gianluca Amato , Marco Maggesi , Cosimo Perini Brogi

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 … 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.

Chat View PDF

A formal proof of modal completeness for provability logic

2021-01-01

Marco Maggesi , Cosimo Perini Brogi

This work presents a formalized proof of modal completeness for G\"odel-L\"ob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details … This work presents a formalized proof of modal completeness for G\"odel-L\"ob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices in structuring proofs which make essential use of the tools of HOL Light and which differ in part from the standard strategies found in main textbooks covering the topic in an informal setting. Moreover, we propose a reflection on our own experience in using this specific theorem prover for this formalization task, with an analysis of pros and cons of reasoning within and about the formal system for GL we implemented in our code.

Chat View PDF

Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System.

2020-07-09

Marco Maggesi , Massimo Nocentini

We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mechanism … We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mechanism for enabling the logic programming style for reasoning and computing in a theorem prover, and a framework for writing logic programs that produce solutions endowed with a formal proof of correctness.

Chat View PDF

Extension and tangential CRF conditions in quaternionic analysis

2020-03-16

Marco Maggesi , Donato Pertici , Giuseppe Tomassini

Chat View PDF

Universal Algebra in UniMath

2020-01-01

Gianluca Amato , Marco Maggesi , Maurizio Parton +1 more

Chat View PDF

Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System

2020-01-01

Marco Maggesi , Massimo Nocentini

Chat View PDF

Reduction monads and their signatures

2019-12-20

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

In this work, we study reduction monads , which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects … In this work, we study reduction monads , which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, the lambda calculus is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented multigraph whose vertices are terms and whose edges witness the reductions between two terms. We study presentations of reduction monads. To this end, we propose a notion of reduction signature . As usual, such a signature plays the role of a virtual presentation, and specifies arities for generating operations—possibly subject to equations—together with arities for generating reduction rules. For each such signature, we define a category of models; any model is, in particular, a reduction monad. If the initial object of this category of models exists, we call it the reduction monad presented (or specified) by the given reduction signature . Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. We show in the examples that our approach covers several standard variants of the lambda calculus.

Chat View PDF

Recent developments in quaternionic analysis

2019-09-27

Marco Maggesi , Donato Pertici , Giuseppe Tomassini

We prove some extension theorems for quaternionic holomorphic functions in the sense of Fueter. We prove some extension theorems for quaternionic holomorphic functions in the sense of Fueter.

Chat View PDF

Bicategories in Univalent Foundations

2019-03-04

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories, we develop the notion of `displayed bicategories', an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-category is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Chat View PDF

Modular specification of monads through higher-order presentations

2019-01-01

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of … In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair. In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating (`higher-order') operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to $\beta$- and $\eta$-equalities. Such a 2-signature is hence a pair $(\Sigma,E)$ of a binding signature $\Sigma$ and a family $E$ of equations for $\Sigma$. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature $(\Sigma,E)$, a category of `models of $(\Sigma,E)$; and we say that a 2-signature is `effective' if this category has an initial object; the monad underlying this (essentially unique) object is the `monad specified by the 2-signature'. Not every 2-signature is effective; we identify a class of 2-signatures, which we call `algebraic', that are effective. Importantly, our 2-signatures together with their models enjoy `modularity': when we glue (algebraic) 2-signatures together, their initial models are glued accordingly. We provide a computer formalization for our main results.

Chat View PDF

Extension and tangential CRF conditions in quaternionic analysis

2019-01-01

Marco Maggesi , Donato Pertici , Giuseppe Tomassini

We prove some extension theorems for quaternionic holomorphic functions in the sense of Fueter. Starting from the existence theorem for the nonhomogeneous Cauchy-Riemann-Fueter Problem, we prove that an $\mathbb{H}$-valued function … We prove some extension theorems for quaternionic holomorphic functions in the sense of Fueter. Starting from the existence theorem for the nonhomogeneous Cauchy-Riemann-Fueter Problem, we prove that an $\mathbb{H}$-valued function $f$ on a smooth hypersurface, satisfying suitable tangential conditions, is locally a jump of two $\mathbb{H}$-holomorphic functions. From this, we obtain, in particular, the existence of the solution for the Dirichlet Problem with smooth data. We extend these results to the continous case. In the final part, we discuss the octonian case.

Chat View PDF

High-level signatures and initial semantics

2018-09-04

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

Chat View PDF

High-level signatures and initial semantics

2018-05-09

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of signature for specifying syntactic constructions. In … We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of signature for specifying syntactic constructions. In the spirit of Initial Semantics, we define the syntax generated by a signature to be the initial object---if it exists---in a suitable category of models. In our framework, the existence of an associated syntax to a signature is not automatically guaranteed. We identify, via the notion of presentation of a signature, a large class of signatures that do generate a syntax. Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions. One key feature of our notions of signature, syntax, and presentation is that they are highly compositional, in the sense that complex examples can be obtained by assembling simpler ones. Moreover, through the Initial Semantics approach, our framework provides, beyond the desired algebra of terms, a well-behaved substitution and the induction and recursion principles associated to the syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.

Chat View PDF

Presentable signatures and initial semantics

2018-05-09

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

We present a device for specifying and reasoning about for datatypes, programming languages, and logic calculi. More precisely, we study a notion of for specifying syntactic constructions. In the spirit … We present a device for specifying and reasoning about for datatypes, programming languages, and logic calculi. More precisely, we study a notion of for specifying syntactic constructions. In the spirit of Initial Semantics, we define the syntax generated by a to be the initial object -- if it exists -- in a suitable category of models. In our framework, the existence of an associated to a signature is not automatically guaranteed. We identify, via the notion of presentation of a signature, a large class of signatures that do generate a syntax. Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions. One key feature of our notions of signature, syntax, and presentation is that they are highly compositional, in the sense that complex examples can be obtained by gluing simpler ones. Moreover, through the Initial Semantics approach, our framework provides, beyond the desired algebra of terms, a well-behaved substitution and the induction and recursion principles associated to the syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.

Presentable signatures and initial semantics

2018-01-01

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In … We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object -- if it exists -- in a suitable category of models. In our framework, the existence of an associated syntax to a signature is not automatically guaranteed. We identify, via the notion of presentation of a signature, a large class of signatures that do generate a syntax. Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions. One key feature of our notions of signature, syntax, and presentation is that they are highly compositional, in the sense that complex examples can be obtained by gluing simpler ones. Moreover, through the Initial Semantics approach, our framework provides, beyond the desired algebra of terms, a well-behaved substitution and the induction and recursion principles associated to the syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.

Chat View PDF

Formalizing Basic Quaternionic Analysis

2017-01-01

Andrea Gabrielli , Marco Maggesi

Some elementary remarks on lci algebraic cycles

2016-01-01

Marco Maggesi , Gabriele Vezzosi

In this short note, we simply collect some known results about representing algebraic cycles by various kind of "nice" (e.g. smooth, local complete intersection, products of local complete intersection) algebraic … In this short note, we simply collect some known results about representing algebraic cycles by various kind of "nice" (e.g. smooth, local complete intersection, products of local complete intersection) algebraic cycles, up to rational equivalence. We also add a few elementary and easy observations on these representation problems that we were not able to locate in the literature.

Chat View PDF

Initial Semantics for Strengthened Signatures

2012-02-14

André Hirschowitz , Marco Maggesi

We give a new general definition of arity, yielding the companion notions of signature and associated syntax. This setting is modular in the sense requested by Ghani and Uustalu: merging … We give a new general definition of arity, yielding the companion notions of signature and associated syntax. This setting is modular in the sense requested by Ghani and Uustalu: merging two extensions of syntax corresponds to building an amalgamated sum. These signatures are too general in the sense that we are not able to prove the existence of an associated syntax in this general context. So we have to select arities and signatures for which there exists the desired initial monad. For this, we follow a track opened by Matthes and Uustalu: we introduce a notion of strengthened arity and prove that the corresponding signatures have initial semantics (i.e. associated syntax). Our strengthened arities admit colimits, which allows the treatment of the \lambda-calculus with explicit substitution.

Chat View PDF

A Certified Proof of the Cartan Fixed Point Theorems

2010-08-18

Gianni Ciolli , Graziano Gentili , Marco Maggesi

Modules over Monads and Linearity

2007-01-01

André Hirschowitz , Marco Maggesi

Chat View PDF

Higher-order theories

2007-01-01

André Hirschowitz , Marco Maggesi

We extend our approach to abstract syntax (with binding constructions) through modules and linearity. First we give a new general definition of arity, yielding the companion notion of signature. Then … We extend our approach to abstract syntax (with binding constructions) through modules and linearity. First we give a new general definition of arity, yielding the companion notion of signature. Then we obtain a modularity result as requested by Ghani and Uustalu (2003): in our setting, merging two extensions of syntax corresponds to building an amalgamated sum. Finally we define a natural notion of equation concerning a signature and prove the existence of an initial semantics for a so-called representable signature equipped with a set of equations.

Chat View PDF

Modules over monads and the structure of untyped lambda-calculi

2006-08-11

André Hirschowitz , Marco Maggesi

Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of … Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of left modules (Linear natural transformations) captures an important property of compatibility with substitution, in the heterogeneous case where terms and variables therein could be of different types as well as in the homogeneous case. In this paper, we present basic constructions of modules and we show examples concerning in particular abstract syntax and lambda-calculus.

Chat View PDF

Modules over Monads and Linearity

2006-01-01

André Hirschowitz , Marco Maggesi

Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of … Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of left modules ("Linear" natural transformations) captures an important property of compatibility with substitution, in the heterogeneous case where "terms" and variables therein could be of different types as well as in the homogeneous case. In this paper, we present basic constructions of modules and we show examples concerning in particular abstract syntax and lambda-calculus.

Chat View PDF

Verifica automatica del ragionamento matematico

2006-01-01

Marco Maggesi , Carlos Simpson

On the Quantum Cohomology of Some Fano Threefolds

2005-01-01

Vincenzo Ancona , Marco Maggesi

Abstract Fano threefolds which are IP 1 -bundles on smooth projective surfaces have been classified by Szurek and Wiśniewski in [17]. The aim of the present paper is to describe … Abstract Fano threefolds which are IP 1 -bundles on smooth projective surfaces have been classified by Szurek and Wiśniewski in [17]. The aim of the present paper is to describe the quantum cohomology ring in these explicit cases.

Minimal resolution of general stable rank-2 vector bundles on $\mathbb{P}^2$

2003-01-01

Carla Dionisi , Marco Maggesi

On the quantum cohomology of Fano bundles over projective spaces and the conjecture of Batyrev

2000-12-07

Vincenzo Ancona , Marco Maggesi

In their paper Quantum cohomology of projective bundles over P^n (Trans. Am. Math. Soc. (1998) 350:9 3615-3638) Z.Qin and Y.Ruan introduce interesting techniques for the computation of the quantum ring … In their paper Quantum cohomology of projective bundles over P^n (Trans. Am. Math. Soc. (1998) 350:9 3615-3638) Z.Qin and Y.Ruan introduce interesting techniques for the computation of the quantum ring of Fano manifolds which are projectivized bundles over projective spaces; in particular, in the case of splitting bundles they prove under some restrictions the conjecture of Batyrev about the quantum ring of toric manifolds. We give examples of splitting bundles whose associated projective bundle are Fano manifolds which do not satisfy the Batyrev conjecture.

Chat View PDF

On the quantum cohomology of Fano bundles over projective spaces

2000-01-01

Vincenzo Ancona , Marco Maggesi

In their paper "Quantum cohomology of projective bundles over $P^n$" (Trans. Am. Math. Soc. (1998)350:9 3615-3638) Z.Qin and Y.Ruan introduce interesting techniques for the computation of the quantum ring of … In their paper "Quantum cohomology of projective bundles over $P^n$" (Trans. Am. Math. Soc. (1998)350:9 3615-3638) Z.Qin and Y.Ruan introduce interesting techniques for the computation of the quantum ring of manifolds which are projectivized bundles over projective spaces; in particular, in the case of splitting bundles they prove under some restrictions the formula of Batyrev about the quantum ring of toric manifolds. Here we prove the formula of Batyrev on the quantum Chern-Leray equation for a large class of splitting bundles.

Chat View PDF

Minimal resolution of general stable vector bundles on $\PP^2$

2000-01-01

Carla Dionisi , Marco Maggesi

We study the general elements of the moduli spaces (\MM_{\PP^2} (r, c_1, c_2) ) of stable holomorphic vector bundle on $\PP^2$ and their minimal free resolution. Incidentally, a quite easy … We study the general elements of the moduli spaces (\MM_{\PP^2} (r, c_1, c_2) ) of stable holomorphic vector bundle on $\PP^2$ and their minimal free resolution. Incidentally, a quite easy proof of the irreducibility of (\MM_{\PP^2} (r, c_1, c_2)) is shown.

Chat View PDF

On the quantum cohomology of blow-ups of projective spaces along linear subspaces

1998-01-01

Marco Maggesi

We give an explicit presentation with generators and relations of the quantum cohomology ring of the blow-up of a projective space along a linear subspace. We give an explicit presentation with generators and relations of the quantum cohomology ring of the blow-up of a projective space along a linear subspace.

Chat View PDF

Common Coauthors

Coauthor	Papers Together
André Hirschowitz	13
Ambroise Lafont	8
Benedikt Ahrens	8
Cosimo Perini Brogi	6
Donato Pertici	3
Giuseppe Tomassini	3
Vincenzo Ancona	3
Gianluca Amato	2
Niccolò Veltri	2
Tom Hirschowitz	2
Niels van der Weide	2
Dan Frumin	2
Carla Dionisi	2
Massimo Nocentini	2
Matteo Calosci	1
Gianluca Amato	1
Gianni Ciolli	1
Carlos Simpson	1
Gabriele Vezzosi	1
Graziano Gentili	1
Maurizio Parton	1
Andrea Gabrielli	1

Commonly Cited References

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

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 … 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.

Chat View PDF

Modules over Monads and Linearity

2007-01-01

André Hirschowitz , Marco Maggesi

Chat View PDF

Second-Order Algebraic Theories

2010-01-01

Marcelo Fiore , Ola Mahmoud

Chat View PDF

Modules over relative monads for syntax and semantics

2014-12-05

Benedikt Ahrens

We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding. We introduce a notion of 2-signature: such a signature specifies not only … We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding. We introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature $S$ we associate a category of "models" of $S$. This category has an initial object, which integrates the terms freely generated by $S$, and which is equipped with reductions according to the inequations given in $S$. We call this initial object the language generated by $S$. Models of a 2--signature are built from relative monads and modules over such monads. Through the use of monads, the models---and in particular, the initial model---come equipped with a substitution operation that is compatible with reduction in a suitable sense. The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.

Chat View PDF

Modular specification of monads through higher-order presentations

2019-01-01

Benedikt Ahrens , André Hirschowitz , Ambroise Lafont +1 more

Chat View PDF

Quaternionic analysis

1979-03-01

A. Sudbery

The richness of the theory of functions over the complex field makes it natural to look for a similar theory for the only other non-trivial real associative division algebra, namely … The richness of the theory of functions over the complex field makes it natural to look for a similar theory for the only other non-trivial real associative division algebra, namely the quaternions. Such a theory exists and is quite far-reaching, yet it seems to be little known. It was not developed until nearly a century after Hamilton's discovery of quaternions. Hamilton himself (1) and his principal followers and expositors, Tait(2) and Joly(3), only developed the theory of functions of a quaternion variable as far as it could be taken by the general methods of the theory of functions of several real variables (the basic ideas of which appeared in their modern form for the first time in Hamilton's work on quaternions). They did not delimit a special class of regular functions among quaternion-valued functions of a quaternion variable, analogous to the regular functions of a complex variable.

HOMOTOPY THEORY OF COALGEBRAS

1986-06-30

Vladimir A. Smirnov

This paper makes a study of operads and of coalgebras over operads. Certain operads En and E are defined, constituting the algebraic analogues of the little n-cube operads; it is … This paper makes a study of operads and of coalgebras over operads. Certain operads En and E are defined, constituting the algebraic analogues of the little n-cube operads; it is then shown that the singular chain complex C*(X;R) of a topological space X is a coalgebra over the operad E, and that this structure completely determines the weak homotopy type of the space. Bibliography: 26 titles.

The biequivalence of locally cartesian closed categories and Martin-Löf type theories

2014-04-29

Pierre Clairambault , Peter Dybjer

Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category … Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L\"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L\"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.

Chat View PDF

Monads need not be endofunctors

2015-03-06

Thosten Altenkirch , James Chapman , Tarmo Uustalu

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We … We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Under reasonable assumptions, relative monads are monoids in the functor category concerned and extend to monads, giving rise to a coreflection between relative monads and monads. Arrows are also an instance of relative monads.

Chat View PDF

Analysis of Dirac Systems and Computational Algebra

2004-01-01

Fabrizio Colombo , Irene Sabadini , F. Sommen +1 more

* Preface * Background Material * Computational Algebraic Analysis for Systems of Linear Constant Coefficients Differential Equations * The Cauchy-Fueter Systems and its Variations * Special First Order Systems in … * Preface * Background Material * Computational Algebraic Analysis for Systems of Linear Constant Coefficients Differential Equations * The Cauchy-Fueter Systems and its Variations * Special First Order Systems in Clifford Analysis * Some First Order Linear Operators in Physics * Open Problems and Avenues for Further Research * References * Index

Initial Semantics for higher-order typed syntax in Coq

2010-01-01

Benedikt Ahrens , Julianna Zsidó

Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with … Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author's PhD thesis in 2010, and verified formally shortly afterwards. To a simply-typed binding signature S over a fixed set T of object types we associate a category called the category of representations of S. We show that this category has an initial object Sigma(S). From its construction it will be clear that the object Sigma(S) merits the name abstract syntax associated to S. Our theorem is implemented and proved correct in the proof assistant Coq through heavy use of dependent types. The approach through monads gives rise to an implementation of syntax where both terms and variables are intrinsically typed, i.e. where the object types are reflected in the meta-level types. This article is to be seen as a research article rather than about the formalization of a classical mathematical result. The nature of our theorem - involving lengthy, technical proofs and complicated algebraic structures - makes it particularly interesting for formal verification. Our goal is to promote the use of computer theorem provers as research tools, and, accordingly, a new way of publishing mathematical results: a parallel description of a theorem and its formalization should allow the verification of correct transcription of definitions and statements into the proof assistant, and straightforward but technical proofs should be well-hidden in a digital library. We argue that Coq's rich type theory, combined with its various features such as implicit arguments, allows a particularly readable formalization and is hence well-suited for communicating mathematics.

Chat View PDF

Introduction to bicategories

1967-01-01

Jean Bénabou

Natural models of homotopy type theory

2016-11-17

Steve Awodey

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly … The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id , as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.

Chat View PDF

Discrete Generalised Polynomial Functors

2012-01-01

Marcelo Fiore

Signatures and models for syntax and operational semantics in the presence of variable binding

2019-01-01

Ambroise Lafont

This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of signature for specifying objects of a … This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of signature for specifying objects of a given category as initial objects in a suitable category of models.This characterization, in the spirit of Initial Semantics, gives a justification of the recursion principle. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets specified through the classical algebraic signatures. The first extensions to syntaxes with equations that we consider are quotients of these algebraic signatures. They allow, for example, to specify a binary commutative operation. But some equations, such as associativity, seem to remain out of reach. We thus introduce the notion of 2-signature, consisting in two parts: a specification of operations through a usual signature as before, and a set of equations among them. We identify the class of algebraic 2-signatures for which the existence of the associated syntax is guaranteed. Finally, we takle the specification of the operational semantics of a programming language such as lambda calculus with beta-reduction. To this end, we introduce the notion of reduction monad and their signatures, then we generalize them to get the notion of operational monad.

Chat View PDF

Bar constructions for topological operads and the Goodwillie derivatives of the identity

2005-05-23

Michael Ching

We describe a cooperad structure on the simplicial bar construction on a reduced operad of based spaces or spectra and, dually, an operad structure on the cobar construction on a … We describe a cooperad structure on the simplicial bar construction on a reduced operad of based spaces or spectra and, dually, an operad structure on the cobar construction on a cooperad. We also show that if the homology of the original operad (respectively, cooperad) is Koszul, then the homology of the bar (respectively, cobar) construction is the Koszul dual. We use our results to construct an operad structure on the partition poset models for the Goodwillie derivatives of the identity functor on based spaces and show that this induces the `Lie' operad structure on the homology groups of these derivatives. We also extend the bar construction to modules over operads (and, dually, to comodules over cooperads) and show that a based space naturally gives rise to a left module over the operad formed by the derivatives of the identity.

Chat View PDF

Univalent higher categories via complete Semi-Segal types

2017-12-27

Paolo Capriotti , Nicolai Kraus

Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as … Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather higher categories. Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first ( n +3) levels of a semisimplicial type S , we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n -type . This is very similar to an earlier suggestion by Schreiber. The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a univalent n -category (more precisely, ( n ,1)-category) for n ∈ {0,1,2}, and we show that the type of complete semi-Segal n -types is equivalent to the type of univalent n -categories in these cases. Thus, we believe that the notion of a complete semi-Segal n -type can be taken as the definition of a univalent n -category. We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.

Chat View PDF

Categorical structures for type theory in univalent foundations

2017-01-01

Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps … In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

Chat View PDF

A Henkin-style completeness proof for the modal logic S5

2019-10-03

Bruno Bentzen

This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of … This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell [9], except that it is given for a system based on a different choice of axioms. Here the proof is based on a Hilbert-style presentation better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as rule of inference. The language has the false and implication as the only primitive logical connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.1.

Chat View PDF

Cartesian closed 2-categories and permutation equivalence in higher-order rewriting

2013-09-04

Tom Hirschowitz

We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete. We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete.

Chat View PDF

Octonion Analysis of Several Variables

2014-06-01

Haiyan Wang , Guangbin Ren

Chat View PDF

A new approach to Cullen-regular functions of a quaternionic variable

2006-04-18

Graziano Gentili , Daniele C. Struppa

Chat View PDF

Quantum cohomology of projective bundles over ℙⁿ

1998-01-01

Zhenbo Qin , Yongbin Ruan

In this paper we study the quantum cohomology ring of certain projective bundles over the complex projective space <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper P Superscript n"> <mml:semantics> <mml:msup> <mml:mrow … In this paper we study the quantum cohomology ring of certain projective bundles over the complex projective space <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper P Superscript n"> <mml:semantics> <mml:msup> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">P</mml:mi> </mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi>n</mml:mi> </mml:mrow> </mml:msup> <mml:annotation encoding="application/x-tex">\mathbb {P}^{n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. Using excessive intersection theory, we compute the leading coefficients in the relations among the generators of the quantum cohomology ring structure. In particular, Batyrev’s conjectural formula for quantum cohomology of projective bundles associated to direct sum of line bundles over <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper P Superscript n"> <mml:semantics> <mml:msup> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">P</mml:mi> </mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi>n</mml:mi> </mml:mrow> </mml:msup> <mml:annotation encoding="application/x-tex">\mathbb {P}^{n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is partially verified. Moreover, relations between the quantum cohomology ring structure and Mori’s theory of extremal rays are observed. The results could shed some light on the quantum cohomology for general projective bundles.

Chat View PDF

Categories for the Working Mathematician

1971-01-01

Saunders Mac Lane

Chat View PDF

Funzioni regolari nell'algebra di Cayley

1973-01-01

Paolo Dentoni , Michele Sce

An extension theorem for regular functions of two quaternionic variables

2019-10-08

Luca Baracco , Martino Fassina , Stefano Pinton

Chat View PDF

Internal type theory

1996-01-01

Peter Dybjer

Quaternionic contact Einstein structures and the quaternionic contact Yamabe problem

2006-01-01

Stefan Ivanov , Ivan Minchev , Dimiter Vassilev

A partial solution of the quaternionic contact Yamabe problem on the quaternionic sphere is given. It is shown that the torsion of the Biquard connection vanishes exactly when the trace-free … A partial solution of the quaternionic contact Yamabe problem on the quaternionic sphere is given. It is shown that the torsion of the Biquard connection vanishes exactly when the trace-free part of the horizontal Ricci tensor of the Biquard connection is zero and this occurs precisely on 3-Sasakian manifolods. All conformal deformations sending the standard flat torsion-free quaternionic contact structure on the quaternionic Heisenberg group to a quaternionic contact structure with vanishing torsion of the Biquard connection are explicitly described. A '3-Hamiltonian form' of infinitesimal conformal automorphisms of quaternionic contact structures is presented.

Chat View PDF

From left modules to algebras over an operad: application to combinatorial Hopf algebras

2010-01-01

Muriel Livernet

The purpose of this paper is two fold: we study the behaviour of the forgetful functor from 𝕊-modules to graded vector spaces in the context of algebras over an operad … The purpose of this paper is two fold: we study the behaviour of the forgetful functor from 𝕊-modules to graded vector spaces in the context of algebras over an operad and derive the construction of combinatorial Hopf algebras. As a byproduct we obtain freeness and cofreeness results for those Hopf algebras.

Chat View PDF

Finitary Higher Inductive Types in the Groupoid Model

2018-04-01

Peter Dybjer , Hugo Moeneclaey

A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces … A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.

Vector Bundles on Complex Projective Spaces

1980-01-01

Christian Okonek , Michael Schneider , Heinz Spindler

Die Funktionentheorie der Differentialgleichungen? u=0 und?? u=0 mit vier reellen Variablen

1934-12-01

Run Fueter

Analysis of the module determining the properties of regular functions of several quaternionic variables

2000-11-01

William W. Adams , Philippe Loustaunau

For a polynomial ring, R, in 4n variables over a field, we consider the submodule of R 4 corresponding to the 4 × 4n matrix made up of n groupings … For a polynomial ring, R, in 4n variables over a field, we consider the submodule of R 4 corresponding to the 4 × 4n matrix made up of n groupings of the linear representation of quarternions with variable entries (which corresponds to the Cauchy-Fueter operator in partial differential equations) and let M n be the corresponding quotient module.We compute many homological properties of M n including the degrees of all of its syzygies, as well as its Betti numbers, Hilbert function, and dimension.We give similar results for its leading term module with respect to the degree reverse lexicographical ordering.The basic tool in the paper is the theory of Gröbner bases.

Chat View PDF

Funzioni regolari di più variabili quaternioniche

1988-12-01

Donato Pertici

Chat View PDF

Linear Differential Operators with Constant Coefficients

1970-01-01

Victor Palamodov

Moduli of stable sheaves, II

1978-01-01

Masaki Maruyama

§ 1 . 5-equivalenceIn this section we shall introduce a n equivalence relation among semi-stable sheaves and then define a functor of (Sch/S) to (Sets).Lemma 1.1.L e t Y b … § 1 . 5-equivalenceIn this section we shall introduce a n equivalence relation among semi-stable sheaves and then define a functor of (Sch/S) to (Sets).Lemma 1.1.L e t Y b e a non-singular projectiv e v ariety w ith a v ery am ple inv ertible sheaf 6, (l ) an d let E , (o r, £ 2 ) be a stable (or, sem i-stable, resp.)sheaf ') The center of G L(V) acts trivially on P(V, r, W ) .Thus PGL(V)acts on P(V, r, W ) .Though the o(1) may not be PGL(V)-linearized, 0(m) carries a PGL(V)-linearization for some positive integer m.

Chat View PDF

A mathematical theory of quantum cohomology

1995-01-01

Yongbin Ruan , Gang Tian

Chat View PDF

Partial Differential Equations of Elliptic Type

1970-01-01

Carlo Miranda

A 2-Categories Companion

2009-09-16

Stephen Lack

This paper is a rather informal guide to some of the basic theory of 2-categories and bicategories, including notions of limit and colimit, 2-dimensional universal algebra, formal category theory, and … This paper is a rather informal guide to some of the basic theory of 2-categories and bicategories, including notions of limit and colimit, 2-dimensional universal algebra, formal category theory, and nerves of bicategories. As is the way of these things, the choice of topics is somewhat personal. No attempt is made at either rigour or completeness. Nor is it completely introductory: you will not find a definition of bicategory; but then nor will you really need one to read it. In keeping with the philosophy of category theory, the morphisms between bicategories play more of a role than the bicategories themselves.

Chat View PDF

Topological conditions for smoothing algebraic singularities

1974-09-01

Robin Hartshorne

Wellfounded Trees and Dependent Polynomial Functors

2004-01-01

Nicola Gambino , Martin Hyland

Chat View PDF

Holomorphic maps and invariant distances

1980-01-01

Tullio Franzoni , Edoardo Vesentini

Gromov-Witten invariants of blow-ups

1998-01-01

Andreas Gathmann

In the first part of the paper, we give an explicit algorithm to compute the (genus zero) Gromov-Witten invariants of blow-ups of an arbitrary convex projective variety in some points … In the first part of the paper, we give an explicit algorithm to compute the (genus zero) Gromov-Witten invariants of blow-ups of an arbitrary convex projective variety in some points if one knows the Gromov-Witten invariants of the original variety. In the second part, we specialize to blow-ups of P^r and show that many invariants of these blow-ups can be interpreted as numbers of rational curves on P^r having specified global multiplicities or tangent directions in the blown-up points. We give various numerical examples, including a new easy way to determine the famous multiplicity d^{-3} for d-fold coverings of rational curves on the quintic threefold, and, as an outlook, two examples of blow-ups along subvarieties, whose Gromov-Witten invariants lead to classical multisecant formulas.

Chat View PDF

Extension results for slice regular functions of a quaternionic variable

2009-07-16

Fabrizio Colombo , Graziano Gentili , Irene Sabadini +1 more

Chat View PDF