Package Displayed_Cats

Authors: Benedikt Ahrens, Peter LeFanu Lumsdaine

Contents

The files of this package provide:

• Auxiliary.v
  • Some background material
• Core.v
  • Definition of displayed categories
  • Definition of total categories
  • Displayed functors
  • Displayed natural transformations
• Fibrations.v
  • Definitions of isofibrations, (op)fibrations, discrete fibrations
  • Clovenness of any univalent fibration
• Constructions.v
  • Direct product of displayed categories
  • Sigmas of displayed categories
  • Displayed functor categories
  • Fiber categories
• Equivalences.v
  • Displayed adjunctions
  • Displayed equivalences
  • Transfer of displayed equivalences to fibers
• Examples.v
  • Displayed arrow category
• SIP.v
  • Proof of the Structure Identity Principle (HoTT book, chapter 9.8)