Codisplayed Category

A codisplayed category $\mathcal{C}$ should be the dual of a Displayed category: instead of describing the data of a functor into $\mathcal{C}$, we want to describe the data out of $\mathcal{C}$. Put another way, we are looking for a nice, non-evil description of $\mathcal{C}/\rm{Cat}$ instead of $\rm{Cat}/\mathcal{C}$.

One good source of inspiration comes from the theory of Model categories: in particular, a codisplayed category should be able to describe the cofibrations.

One possible idea came from a "The Language of a Model Category", which considered "extensions" of a theory. I played this this a bit, and wasn't too pleased. The final form it took was something like:

record Codisplayed
  {o ℓ}
  (B : Precategory o ℓ)
  (o' ℓ' : Level)
  : Type (o ⊔ ℓ ⊔ lsuc o' ⊔ lsuc ℓ') where
  field
  open Precategory B
  field
    Ob+ : Type o'
    Hom+ : Ob ⊎ Ob+ → Ob ⊎ Ob+ → Type ℓ'
    Hom+-set : ∀ x y → is-set (Hom+ x y)

    id⁺ : ∀ {x} → Hom+ x x
    _∘⁺_ : ∀ {x y z} → Hom+ y z → Hom+ x y → Hom+ x z
    idl+ : ∀ {x y} (f : Hom+ x y) → id⁺ ∘⁺ f ≡ f
    idr+ : ∀ {x y} (f : Hom+ x y) → f ∘⁺ id⁺ ≡ f
    assoc+ : ∀ {w x y z} (f : Hom+ y z) (g : Hom+ x y) (h : Hom+ w x) → f ∘⁺ (g ∘⁺ h) ≡ (f ∘⁺ g) ∘⁺ h

    ι⁺ : ∀ {x y} → Hom x y → Hom+ (inl x) (inl y)
    ι-id : ∀ {x} → ι⁺ (id {x}) ≡ id⁺
    ι-∘ : ∀ {x y z} (f : Hom y z) (g : Hom x y) → ι⁺ (f ∘ g) ≡ (ι⁺ f ∘⁺ ι⁺ g)

which is clunky at best. I now think that the best way to think about this is in terms of Partitions, in particular, "proof relevant" partititions; EG: something like

record Codisplayed
  {o ℓ}
  (B : Precategory o ℓ)
  : Type (o ⊔ ℓ ⊔ lsuc lzero) where
  field
  open Precategory B
  field
    Ob⁺ : Type
    Hom⁺ : Ob⁺ → Ob⁺ → Type

    C₀ : Ob → Ob⁺ → Type
    C₁ : ∀ {x y x⁺ y⁺} → Hom x y → C₀ x x⁺ → C₀ y y⁺ → Hom⁺ x⁺ y⁺ → Type

    id⁺ : ∀ {x} → Hom⁺ x x
    _∘⁺_ : ∀ {x y z} → Hom⁺ y z → Hom⁺ x y → Hom⁺ x z

    C₁-id
      : ∀ {x x⁺}
      → (c : C₀ x x⁺)
      → C₁ id c c id⁺
    C₁-∘
      : ∀ {x y z x⁺ y⁺ z⁺ f g f⁺ g⁺}
      → {cx : C₀ x x⁺} {cy : C₀ y y⁺} {cz : C₀ z z⁺}
      → C₁ f cy cz f⁺ → C₁ g cx cy g⁺
      → C₁ (f ∘ g) cx cz (f⁺ ∘⁺ g⁺)

Note that this is a sort of "partial partition"; we need an operation that assigns objects to their partitions. One possible way to do this is by picking out an isomorphism class, but this doesn't capture the desired strictness.

This feels very closely related to Anafunctors.

If we look at Codisplayed, it almost looks like a Displayed Category. Perhaps the move is to consider some sort of "exact sequence of categories"?