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 and then equip those morphisms with an action of

For a displayed category our morphisms are the displayed hom sets over indexed over a The action of 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 our morphisms are generalized elements for Moreover, acts on graded morphisms via precomposition with a morphism

Finally, for an actegory equipped with an action the appropriate notion of morphism is a sort of sort of β€œ morphism” where The action of on these morphisms is given by functoriality of 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 over a prebicategory consists of:

  • A family of objects indexed by the objects of
  • A family of morphisms indexed by the 1-cells of
  • Identity and composite morphisms indexed over the identity 1-cell and composites of 1-cells.
  • An action of 2-cells of on morphisms of 
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 30 _∘'_
    infix 35 _[_]

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 [ Ξ² ]