3 citations · 4 across the 3 of their papers we have counts for
5 papers
Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
Matteo Spadetto
We prove a conservativity result for extensional type theories over propositional ones, i.e. dependent type theories with propositional computation rules, or computation axioms, us…
Dialectica Principles via Gödel Doctrines
Davide Trotta, Matteo Spadetto, Valeria de Paiva
Gödel'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…
Dialectica Logical Principles
Davide Trotta, Matteo Spadetto, Valeria de Paiva
Gödel'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 o…
The Gödel Fibration
Davide Trotta, Matteo Spadetto, Valeria de Paiva
We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principle of traditional Skolemization (we can exchange the order of qua…
Quantifier completions, choice principles and applications
Davide Trotta, Matteo Spadetto
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 th…