module Cat.Internal.Sets where

Internal categories in SetπŸ”—

Categories that are internal to set are [strict categories]: precategories with a Set of objects. Starting from a category C\mathbb{C} internal to Sets\mathbf{Sets} and ending up with a strict category is quite unremarkable:

Internal-catβ†’Precategory : βˆ€ {ΞΊ} β†’ Internal-cat (Sets ΞΊ) β†’ Precategory ΞΊ ΞΊ
Internal-cat→Precategory {κ} ℂ = cat where
  open Internal-cat β„‚
  open Internal-hom
  open Precategory

  cat : Precategory _ _
  cat .Ob = ∣ Cβ‚€ ∣
  cat .Hom x y = Homi {Cβ‚€} (Ξ» _ β†’ x) Ξ» _ β†’ y
  cat .Hom-set _ _ = Internal-hom-set (Sets ΞΊ)
  cat .id = idi _
  cat ._∘_ = _∘i_
  cat .idr f = Internal-hom-path _ (ap ihom (idri f))
  cat .idl f = Internal-hom-path _ (ap ihom (idli f))
  cat .assoc f g h = Internal-hom-path _ (ap ihom (associ f g h))

Defining an internal category from a strict category is a lot more annoying.

  : βˆ€ {o β„“}
  β†’ (C : Precategory o β„“) β†’ is-set (Precategory.Ob C)
  β†’ Internal-cat (Sets (o βŠ” β„“))
Strict-cat→Internal-cat {o} {ℓ} C ob-set = icat where

The object-of-objects is straightforward to define, since we already assumed that the category we’re internalising has a set of objects. Morphisms are a bit more complicated. Since an internal category has a single object-of-morphisms, we have to work with the total space of C(βˆ’,βˆ’)\mathcal{C}(-,-), rather than any particular fibre.

  icat : Internal-cat (Sets (o βŠ” β„“))
  icat .Cβ‚€ = el! (Lift β„“ Ob)
  icat .C₁ = el! (Ξ£[ x ∈ Ob ] Ξ£[ y ∈ Ob ] (Hom x y))
  icat .src (x , _ , _) = lift x
  icat .tgt (_ , y , _) = lift y

The internal identity morphism is simply the identity morphism.

  icat .has-internal-cat .idi x .ihom Ξ³ =
    lower (x Ξ³) , lower (x Ξ³) , id
  icat .has-internal-cat .idi x .has-src = refl
  icat .has-internal-cat .idi x .has-tgt = refl

Composition is where the complication shows up. Rather than composing two arrows f:x→yf : x \to y and g:y→zg : y \to z, we have to compose arrows f:x→yf : x \to y, g:y′→zg : y' \to z, and a path y=y′y = y'. This forces us to transport ff, which gunks up the computations.

  icat .has-internal-cat ._∘i_ f g .ihom γ =
    g .ihom Ξ³ .fst ,
    f .ihom Ξ³ .snd .fst ,
    f .ihom Ξ³ .snd .snd
    ∘ cast-cod (ap lower (g .has-tgt $β‚š Ξ³ βˆ™ sym (f .has-src $β‚š Ξ³)))
      (g .ihom Ξ³ .snd .snd)
  icat .has-internal-cat ._∘i_ f g .has-src = g .has-src
  icat .has-internal-cat ._∘i_ f g .has-tgt = f .has-tgt

As mentioned, establishing the laws is slightly hampered by the stuck transports.

  icat .has-internal-cat .idli f =
    Internal-hom-path _ $
    funext Ξ» Ξ³ β†’
    refl ,β‚š ap lower (sym (f .has-tgt $β‚š Ξ³)) ,β‚š
    to-pathp⁻ (idl _ βˆ™ recast-cod _ _)
  icat .has-internal-cat .idri f =
    Internal-hom-path _ $
    funext Ξ» Ξ³ β†’
    ap lower (sym (f .has-src $β‚š Ξ³)) ,β‚š refl ,β‚š
    to-pathp⁻ (cast-cod-idr _ _ βˆ™ recast-dom _ _)
  icat .has-internal-cat .associ f g h =
    Internal-hom-path _ $
    funext Ξ» Ξ³ β†’
    refl ,β‚š refl ,β‚š apβ‚‚ _∘_ refl (cast-cod-∘ _) βˆ™ assoc _ _ _

Fortunately, naturality does not get too far in the way.

  icat .has-internal-cat .idi-nat _ =
    Internal-hom-path _ refl
  icat .has-internal-cat .∘i-nat f g Οƒ =
    Internal-hom-path _ $
    funext Ξ» Ξ³ β†’
    refl ,β‚š refl ,β‚š apβ‚‚ _∘_ refl (recast-cod _ _)