A characterisation of elementary fibrations

Jacopo Emmenegger, Fabio Pasquali, Giuseppe Rosolini

Research output: Contribution to journalArticlepeer-review

5 Downloads (Pure)

Abstract

In the categorical approach to logic proposed by Lawvere, which systematically uses adjoints to describe the logical operations, equality is presented in the form of a left adjoint to reindexing along diagonal arrows in the base. Taking advantage of the modular perspective provided by category theory, one can look at those Grothendieck fibrations which sustain just the structure of equality, the so-called elementary fibrations, aka fibrations with equality.

The present paper provides a characterisation of elementary fibrations which is a substantial generalisation of the one already available for faithful fibrations. The characterisation is based on a particular structure in the fibres which may be understood as proof-relevant equality predicates equipped with a principle of indiscernibility of identicals à la Leibniz. We exemplify this structure for several classes of fibrations, in particular, for fibrations used in the semantics of the identity type of Martin-Löf type theory. We close the paper discussing some fibrations related to Hofmann and Streicher's groupoid model of the identity type and showing that one of them is elementary.
Original languageEnglish
Article number103103
JournalAnnals of Pure and Applied Logic
Volume173
Issue number6
Early online date16 Feb 2022
DOIs
Publication statusPublished - 1 Jun 2022

Keywords

  • Elementary fibration
  • Equality predicate
  • Weak factorisation system
  • Identity type

Fingerprint

Dive into the research topics of 'A characterisation of elementary fibrations'. Together they form a unique fingerprint.

Cite this