open import Cat.Internal.Base

open import Cat.Instances.Sets
open import Cat.Instances.StrictCat
open import Cat.Prelude

import Cat.Strict.Reasoning

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 $\mathbb{C}$ internal to $\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.

Strict-catβInternal-cat
: β {o β}
β (C : Precategory o β) β is-set (Precategory.Ob C)
β Internal-cat (Sets (o β β))
Strict-catβInternal-cat {o} {β} C ob-set = icat where

  open Precategory C
open Cat.Strict.Reasoning C ob-set
open Internal-cat
open Internal-cat-on
open Internal-hom
open Lift
instance
H-Level-Ob : β {n} β H-Level Ob (2 + n)
H-Level-Ob = basic-instance 2 ob-set


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 $\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 \to y$ and $g : y \to z$, we have to compose arrows $f : x \to y$, $g : y' \to z$, and a path $y = y'$. This forces us to transport $f$, 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 _ _)