arXiv subjects

Matteo Spadetto

Publications and source records attributed to Matteo Spadetto.

7 recordsLinked to original sources

arXiv2025

A 2-categorical approach to the semantics of dependent type theory with computation axioms

Axiomatic type theory is a dependent type theory without computation rules. The term equality judgements that usually characterise these rules are replaced by computation axioms, i.e., additional term judgements that are typed by identity types. This paper is devoted to providing an effective description of its semantics, from a higher categorical perspective: given the challenge of encoding intensional type formers into 1-dimensional categorical terms and properties, a challenge that persists even for axiomatic type formers, we adopt Richard Garner's approach in the 2-dimensional study of dependent types. We prove that the type formers of axiomatic theories can be encoded into natural 2-dimensional category theoretic data, obtaining a presentation of the semantics of axiomatic type theory via 2-categorical models called display map 2-categories. In the axiomatic case, the 2-categorical requirements identified by Garner for interpreting intensional type formers are relaxed. Therefore, we obtain a presentation of the semantics of the axiomatic theory that generalises Garner's one for the intensional case. Our main result states that the interpretation of axiomatic theories within display map 2-categories is well-defined and enjoys the soundness property. We use this fact to provide a semantic proof that the computation rule of intensional identity types is not admissible in axiomatic type theory. This is achieved via a revisitation of Hofmann and Streicher's groupoid model that believes axiomatic identity types but does not believe intensional ones.

math.LO↗

arXiv2025

The biequivalence of path categories and axiomatic Martin-L\"of type theories

The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categories, while adding Pi-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 1- and Sigma-types are biequivalent to certain path categories, while adding axiomatic Pi-types yields dependent homotopy exponents. This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 1-, Sigma-, and Pi-types.

math.LO↗

arXiv2023

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms

We prove a conservativity result for extensional type theories over propositional ones, i.e. dependent type theories with propositional computation rules, or computation axioms, using insights from homotopy type theory. The argument exploits a notion of canonical homotopy equivalence between contexts, and uses the notion of a category with attributes to phrase the semantics of theories of dependent types. Informally, our main result asserts that, for judgements essentially concerning h-sets, reasoning with extensional or propositional type theories is equivalent.

math.LO↗

arXiv2022

Dialectica Principles via G\"odel Doctrines

G\"odel's Dialectica interpretation was conceived as a tool to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic in the 40s. In recent years, several proof-theoretic transformations, based on G\"odel's Dialectica interpretation, have been used systematically to extract new content from classical proofs, following a suggestion of Kreisel. Thus, the interpretation has found new relevant applications in several areas of mathematics and computer science. Several authors have explained the Dialectica interpretation in categorical terms. In our previous work, we introduced an intrinsic categorical presentation of the Dialectica construction via a generalisation of Hofstra's work, using the notion of G\"odel fibration and its proof-irrelevant version, a G\"odel doctrine. The key idea is that G\"odel fibrations can be thought of as fibrations generated by some basic elements playing the role of quantifier-free elements. This categorification of quantifier-free elements is crucial not only to show that our notion of G\"odel fibration is equivalent to Hofstra's Dialectica fibration in the appropriate way, but also to show how G\"odel doctrines embody the main logical features of the Dialectica Interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded by Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely Markov Principle and the Independence of Premise principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight correspondence between the logical system and the categorical framework. Finally, to complete our analysis, we characterise categories obtained as results of the tripos-to-topos of Hyland, Johnstone and Pitts applied to G\"odel doctrines.

math.CT↗

arXiv2021

Dialectica Logical Principles

G\"odel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are based on G\"odel's Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on G\"odel fibrations, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markov's Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.

math.CT↗

arXiv2021

The G\"odel Fibration

We introduce the notion of a G\"odel fibration, which is a fibration categorically embodying both the logical principle of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the existence of a prenex normal form presentation for every logical formula. Building up from Hofstra's earlier fibrational characterization of the de Paiva's categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a G\"odel fibration. This result establishes an internal presentation of the dialectica construction. Then we provide a deep structural analysis of the Dialectica construction producing a full description of which categorical structure behaves well with respect to this construction, focusing on (weak) finite products and coproducts. We conclude describing the applications we envisage for this generalized fibrational version of the Dialectica construction.

math.CT↗

arXiv2021

Quantifier completions, choice principles and applications

We contribute to the knowledge of the quantifier completions and their applications by using the language of doctrines. This algebraic presentation allows us to properly analyse the behaviour of the existential and universal quantifiers. We wish to convey the following points: the first is that these completions preserve the lattice structure and the distributive lattice structure of the fibres under opportune hypotheses which turn out to be preserved as well; the second regards the applications, in particular to the dialectica construction; the third is that these free constructions carry on some relevant choice principles.

math.CT↗