indexed categories and hyperdoctrines

Stream: Is there code for X?

[Chris Henson]

Are there any formalizations of indexed categories and hyperdoctrines? I don't see anything in mathlib, but maybe there are some other projects that use them.

[Johan Commelin]

I'm not aware of a formalization of hyperdoctrines, but it would be fun to have them (-;

[Chris Henson]

@Johan Commelin I am curious to hear your thoughts on how you would define/work with indexed categories here. I tried two approaches. One is to treat the indexed category as a functor, like this

import Mathlib
open CategoryTheory Limits

class Hyperdoctrine [Category C] (P : C ⥤ Cat) where
  limits (A : C) : Limits.HasFiniteProducts (P.obj A)
  ccc (A : C) : CartesianClosed (P.obj A)
  sigma (f : A ⟶  B): P.obj B ⟶  P.obj A
  sigma_adjoint (f : A ⟶  B) : sigma f ⊣ P.map f
  sigmaBeckChevalley (g : X ⟶  Z) (f : Y ⟶  Z) [Limits.HasPullback f g] (pb := pullback.cone f g) :
    sigma pb.fst ⋙  P.map pb.snd = P.map f ⋙  sigma g
  Pi (f : A ⟶  B): P.obj B ⟶  P.obj A
  pi_adjoint (f : A ⟶  B) : P.map f ⊣ Pi f
  piBeckChevalley (g : X ⟶  Z) (f : Y ⟶  Z) [Limits.HasPullback f g] (pb := pullback.cone f g) :
    Pi pb.fst ⋙  P.map pb.snd = P.map f ⋙  Pi g

I've had a bit of trouble previously with something like this, because sometimes being a functor is a bit restrictive. The other approach in mind is to define something like this

import Mathlib
open CategoryTheory Limits

class IndexedCategory (C : Type) [Category C] where
  index : C → Type
  instCategory (A : C) : Category (index A)
  istar {A B : C} (f : A ⟶  B) : index B ⥤ index A
  id : istar (𝟙 A) = 𝟭 (index A)
  comp (f : X ⟶  Y) (g : Y ⟶  Z) : istar (f ≫ g) = istar g ⋙  istar f

attribute [instance] IndexedCategory.instCategory

with pretty much the same definitions for hyperdoctrines. Very open to suggestions, I'm relatively new to using the category theory library.

[Joël Riou]

I do not know much about this area, but it seems the better language would be to use pseudofunctors from the 2-categoryLocallyDiscrete Cto the 2-category Cat, with some additional data/assumptions about the adjoints. @Yuma Mizuno and @Calle Sönne who have been working on 2-categories, pseudofunctors (and fibered categories) may have more detailed suggestions.

[Yuma Mizuno]

I'm not familiar with the concept of hyperdoctrine, but formalizing it seems a nice project! Lean usually prefers natural transformations (or natural isomorphisms) over equalities between functors, and pseudofunctors (or possibly fibered categories) are suitable for that purpose.

[Chris Henson]

@Yuma Mizuno @Joël Riou Thanks for the suggestions! My motivation for hyperdoctrines is as a semantics to the polymorphic lambda calculus, so I think I will run into some trickiness around equality versus isomorphism at some point. I might cross that bridge later and see for instance if I can prove the correspondence between hyperdoctrines and LCCCs as a first step.