Avviso Seminario
Dipartimento di Matematica e Applicazioni “Renato Caccioppoli”
Università degli Studi di Napoli “Federico II”
Mercoledì 10 gennaio 2024 Aula D, h. 11:00

Cipriano Junior Cioffo

Università degli studi di Padova

“An introduction to Fibrations in Logic and Type Theory”

The notion of fibration was introduced by A. Grothendieck in a purely geometric context [1],
providing a fundamental tool in category theory that is pervasive in many areas of mathematics. In
this talk, we will explore some applications of fibrations to logic and type theory [2]. To achieve this,
we will begin by analyzing the classical example of indexed families of sets and then discuss the
general definition and the main properties of fibrations. Time permitting, we will present some current
applications to foundations of constructive mathematics based on the Minimalist Foundation of
Maietti and Sambin [3,4].
[1] A. Grothendieck. Technique de descente et théorèmes d’existenceen géométrie algébrique. I.
Généralités. Descente par morphismesfidélement plats. In Séminaire Bourbaki, no. 5, Séminaire
Bourbaki:années 1958/59 -1959/60, exposés 169-204, Talk no. 190, 29 p.,1960. Erratum in
[Gro62].
[2] B. Jacobs. Categorical Logic and Type Theory, volume 141 of Studiesin Logic and the
foundations of mathematics. North Holland, 1999.
[3] M. E. Maietti and G. Sambin. “Toward a minimalist foundation for constructive mathematics”.
In: From sets and types to topology and analysis. Vol. 48. OxfordLogic Guides. Oxford Univ. Press,
Oxford, 2005, pp. 91–114.
[4] M. E. Maietti. “A minimalist two-level foundation for constructive mathematics”. In: Ann. Pure
Appl. Logic 160.3 (2009), pp. 319–354.
La Proponente
Giuseppina Terzo