module Cat.Bi.Instances.InternalCats
  {o β„“} (C : Precategory o β„“)
  where

The bicategory of internal categoriesπŸ”—

Let be some category. The collection of internal categories in forms a bicategory, with internal functors as 1-cells, and internal natural transformations as 2-cells.

Internal-cats : Prebicategory (o βŠ” β„“) (o βŠ” β„“) (o βŠ” β„“)
Internal-cats = icats where
  open make-natural-iso

We have already shown that internal functors form a precategory, so all that remains is to construct the unitors and the associator. These are almost identity 2-cells, as internal functor composition is pointwise strictly unital and associative. Unfortunately, this does not extend to internal functor composition as a whole, so we cannot use the identity internal natural isomorphism as-is.

  Ζ› : βˆ€ {A B : Internal-cat}
    β†’ Id ≅ⁿ Right (Fi∘-functor A B B) Idi
  Ζ› {B = B} = to-natural-iso ni where
    open Cat.Internal.Reasoning B
    ni : make-natural-iso _ _
    ni .make-natural-iso.eta F = record
      { Ξ·i          = Ξ» x     β†’ idi _
      ; is-naturali = Ξ» x y f β†’ id-comm-symi
      ; Ξ·i-nat      = Ξ» x Οƒ   β†’ casti $ idi-nat Οƒ βˆ™i ap idi (F .Fiβ‚€-nat x Οƒ)
      }
    ni .make-natural-iso.inv F = record
      { Ξ·i          = Ξ» x     β†’ idi _
      ; is-naturali = Ξ» x y f β†’ id-comm-symi
      ; Ξ·i-nat      = Ξ» x Οƒ   β†’ casti $ idi-nat Οƒ βˆ™i ap idi (F .Fiβ‚€-nat x Οƒ)
      }
    ni .make-natural-iso.eta∘inv F = Internal-nat-path Ξ» x β†’ idli _
    ni .make-natural-iso.inv∘eta F = Internal-nat-path Ξ» x β†’ idli _
    ni .make-natural-iso.natural F G Ξ± = Internal-nat-path Ξ» x β†’
      idri _ βˆ™ id-commi

  ρ : βˆ€ {A B : Internal-cat}
    β†’ Id ≅ⁿ Left (Fi∘-functor A A B) Idi
  ρ {B = B} = to-natural-iso ni where
    open Cat.Internal.Reasoning B
    ni : make-natural-iso _ _
    ni .make-natural-iso.eta F = record
      { Ξ·i          = Ξ» x     β†’ idi _
      ; is-naturali = Ξ» x y f β†’ id-comm-symi
      ; Ξ·i-nat      = Ξ» x Οƒ   β†’ casti $ idi-nat Οƒ βˆ™i ap idi (F .Fiβ‚€-nat x Οƒ)
      }
    ni .make-natural-iso.inv F = record
      { Ξ·i          = Ξ» x     β†’ idi _
      ; is-naturali = Ξ» x y f β†’ id-comm-symi
      ; Ξ·i-nat      = Ξ» x Οƒ   β†’ casti $ idi-nat Οƒ βˆ™i ap idi (F .Fiβ‚€-nat x Οƒ)
      }
    ni .make-natural-iso.eta∘inv F = Internal-nat-path Ξ» x β†’ idli _
    ni .make-natural-iso.inv∘eta F = Internal-nat-path Ξ» x β†’ idli _
    ni .make-natural-iso.natural F G Ξ± = Internal-nat-path Ξ» x β†’
      idri _ βˆ™ ap (_∘i _) (G .Fi-id)

  Ξ± : {A B C D : Internal-cat}
    β†’ _≅ⁿ_
       {C = Internal-functors _ C D Γ—αΆœ Internal-functors _ B C Γ—αΆœ Internal-functors _ A B}
       (compose-assocΛ‘ (Ξ» {A} {B} {C} β†’ Fi∘-functor A B C))
       (compose-assocΚ³ Ξ» {A} {B} {C} β†’ Fi∘-functor A B C)
  Ξ± {D = D} = to-natural-iso ni where
    open Cat.Internal.Reasoning D
    ni : make-natural-iso _ _
    ni .eta (F , G , H) .Ξ·i x = idi _
    ni .eta (F , G , H) .is-naturali _ _ _ = id-comm-symi
    ni .eta (F , G , H) .Ξ·i-nat x Οƒ = casti $
      idi-nat Οƒ
      βˆ™i ap idi
        (F .Fiβ‚€-nat _ Οƒ
         βˆ™ ap (F .Fiβ‚€) (G .Fiβ‚€-nat _ Οƒ βˆ™ ap (G .Fiβ‚€) (H .Fiβ‚€-nat _ Οƒ)))
    ni .inv (F , G , H) .Ξ·i x = idi _
    ni .inv (F , G , H) .is-naturali _ _ _ = id-comm-symi
    ni .inv (F , G , H) .Ξ·i-nat x Οƒ = casti $
      idi-nat Οƒ
      βˆ™i ap idi
        (F .Fiβ‚€-nat _ Οƒ
         βˆ™ ap (F .Fiβ‚€) (G .Fiβ‚€-nat _ Οƒ βˆ™ ap (G .Fiβ‚€) (H .Fiβ‚€-nat _ Οƒ)))
    ni .eta∘inv _ = Internal-nat-path Ξ» x β†’ idli _
    ni .inv∘eta _ = Internal-nat-path Ξ» x β†’ idli _
    ni .natural (F , G , H) (J , K , L) Ξ± = Internal-nat-path Ξ» x β†’
      idri _ ·· pushli (J .Fi-∘ _ _) ·· sym (idli _)

Once we’ve got that tedium out of the way, the rest of the construction is a breeze.

  icats : Prebicategory _ _ _
  icats .Ob = Internal-cat
  icats .Hom 𝔸 𝔹 = Internal-functors C 𝔸 𝔹
  icats .id = Idi
  icats .compose = Fi∘-functor _ _ _
  icats .unitor-l = Ζ›
  icats .unitor-r = ρ
  icats .associator = Ξ±
  icats .triangle {C = C} F G = Internal-nat-path Ξ» x β†’ idri _
    where open Cat.Internal.Reasoning C
  icats .pentagon {E = E} F G H J =
    Internal-nat-path Ξ» x β†’ apβ‚‚ _∘i_
      (elimli (ap (F .Fi₁ βŠ™ G .Fi₁) (H .Fi-id) Β·Β· ap (F .Fi₁) (G .Fi-id) Β·Β· F .Fi-id))
      (elimri (elimli (F .Fi-id)))
    where open Cat.Internal.Reasoning E