open import Cat.Bi.Base
open import Cat.Prelude

module Cat.LocallyGraded.Base where

private variable
  ob ℓb₁ ℓb₂ : Level

Locally graded categories🔗

There is a striking similarity between displayed categories, enriched categories, and actegories. All three of these concepts take the basic algebra of a category and replace the hom sets with some other notion of morphism graded by some base category $B\text{,}$ and then equip those morphisms with an action of $B\text{.}$

For a displayed category $\mathcal{E}\mathcal{B}\text{,}$ our $\mathcal{B}\text{-graded}$ morphisms are the displayed hom sets ${\mathcal{E}}_u(X^{\prime },Y^{\prime })$ over indexed over a $u:\mathcal{B}(X,Y)\text{.}$ The action of $\mathcal{B}$ is a bit hard to see initially, but becomes painfully clear once you’ve gotten your hands dirty: it is given by transport of hom families.

For an enriched category $\mathcal{C}\text{,}$ our $\mathcal{V}\text{-graded}$ morphisms are generalized elements $\mathcal{V}(\Gamma ,\mathcal{C}(X,Y))$ for $\Gamma :\mathcal{V}\text{.}$ Moreover, $\mathcal{V}$ acts on graded morphisms $\mathcal{V}(\Gamma ,\mathcal{C}(X,Y))$ via precomposition with a morphism $\mathcal{V}(\Delta ,\Gamma )\text{.}$

Finally, for an actegory $\mathcal{C}$ equipped with an action $\oslash :\mathcal{V}\times \mathcal{C}\to \mathcal{C}\text{,}$ the appropriate notion of $V\text{-graded}$ morphism is a sort of sort of “$\mathcal{V}\text{-generalized}$ morphism” $\mathcal{C}(\Gamma \oslash X,Y)$ where $\Gamma :\mathcal{V}\text{.}$ The action of $\mathcal{V}$ on these morphisms is given by functoriality of $\oslash$ and precomposition.

Locally graded categories simultaneously generalize these three related notions by combining the indexing of a displayed category with a sort of “directed transport” operation that lets us move between indices. Explicitly, a locally graded category $\mathcal{E}$ over a prebicategory $\mathcal{B}$ consists of:

• A family of objects ${\mathcal{C}}_0:{\mathcal{B}}_0\to \mathrm{Type}$ indexed by the objects of $\mathcal{B}\text{.}$
• A family of morphisms ${\mathcal{C}}_1:{\mathcal{B}}_1(X,Y)\to {\mathcal{C}}_0(X)\to {\mathcal{C}}_0(Y)\to \mathrm{Set}$ indexed by the 1-cells of $\mathcal{B}\text{.}$
• Identity and composite morphisms indexed over the identity 1-cell and composites of 1-cells.
• An action $[-]:{\mathcal{B}}_2(u,v)\to {\mathcal{C}}_1(v,X^{\prime },Y^{\prime })\to {\mathcal{C}}_1(u,X^{\prime },Y^{\prime })$ of 2-cells of $\mathcal{B}$ on morphisms of $\mathcal{C}\text{.}$

module _ (B : Prebicategory ob ℓb₁ ℓb₂) where
  private module B = Prebicategory B

  record Locally-graded-precategory
    (oe ℓe : Level)
    : Type (ob ⊔ ℓb₁ ⊔ ℓb₂ ⊔ lsuc oe ⊔ lsuc ℓe) where
    no-eta-equality
    field
      Ob[_] : B.Ob → Type oe
      Hom[_] : ∀ {a b} → a B.↦ b → Ob[ a ] → Ob[ b ] → Type ℓe
      Hom[_]-set
        : ∀ {a b} (u : a B.↦ b) (a' : Ob[ a ]) (b' : Ob[ b ])
        → is-set (Hom[ u ] a' b')

      id' : ∀ {x x'} → Hom[ B.id {x} ] x' x'
      _∘'_
        : ∀ {x y z x' y' z'}
        → {u : y B.↦ z} {v : x B.↦ y}
        → Hom[ u ] y' z' → Hom[ v ] x' y'
        → Hom[ u B.⊗ v ] x' z'

      _[_]
        : ∀ {x y x' y'} {u v : x B.↦ y}
        → Hom[ v ] x' y' → u B.⇒ v → Hom[ u ] x' y'

    infixr  _∘'_
    infix  _[_]

We also require that composition is associative and unital once suitably adjusted by an associator or unitor.

    field
      idl→
        : ∀ {x y x' y'} {u : x B.↦ y}
        → (f : Hom[ u ] x' y')
        → (id' ∘' f) [ B.λ→ u ] ≡ f
      idr→
        : ∀ {x y x' y'} {u : x B.↦ y}
        → (f : Hom[ u ] x' y')
        → (f ∘' id') [ B.ρ→ u ] ≡ f
      assoc←
        : ∀ {a b c d a' b' c' d'}
        → {u : c B.↦ d} {v : b B.↦ c} {w : a B.↦ b}
        → (f : Hom[ u ] c' d') (g : Hom[ v ] b' c') (h : Hom[ w ] a' b')
        → (f ∘' (g ∘' h)) [ B.α→ u v w ] ≡ (f ∘' g) ∘' h

Finally, we require that the action of 2-cells is functorial, and that identities and composites are sufficiently natural.

      []-id
        : ∀ {x y x' y'} {u : x B.↦ y}
        → (f : Hom[ u ] x' y')
        →  f [ B.Hom.id ] ≡ f
      []-∘
        : ∀ {x y x' y'} {u v w : x B.↦ y}
        → (α : v B.⇒ w) (β : u B.⇒ v)
        → (f : Hom[ w ] x' y')
        → f [ α B.∘ β ] ≡ f [ α ] [ β ]
      []-id'
        : ∀ {x x'}
        → (α : B.id B.⇒ B.id)
        → id' {x} {x'} [ α ] ≡ id' {x} {x'}
      []-∘'
        : ∀ {x y z x' y' z'} {t u : y B.↦ z} {v w : x B.↦ y}
        → (α : t B.⇒ u) (β : v B.⇒ w)
        → (f : Hom[ u ] y' z') (g : Hom[ w ] x' y')
        → (f ∘' g) [ α B.◆ β ] ≡ f [ α ] ∘' g [ β ]