open import Cat.Instances.Product
open import Cat.Prelude

import Cat.Instances.InternalFunctor
import Cat.Internal.Reasoning
import Cat.Internal.Base as Internal

module Cat.Instances.InternalFunctor.Compose where

Functoriality of internal functor composition🔗

Internal functor composition is functorial, when viewed as an operation on internal functor categories. This mirrors the similar results for composition of ordinary functors.

To show this, we will need to define whiskering and horizontal composition of internal natural transformations.

module _ {o ℓ} {C : Precategory o ℓ} {𝔸 𝔹 ℂ : Internal.Internal-cat C} where
  open Precategory C
  open Internal C
  open Internal-functor
  open _=>i_
  private
    module 𝔸 = Cat.Internal.Reasoning 𝔸
    module 𝔹 = Cat.Internal.Reasoning 𝔹
    module ℂ = Cat.Internal.Reasoning ℂ

  _◂i_
    : {F G : Internal-functor 𝔹 ℂ}
    → F =>i G → (H : Internal-functor 𝔸 𝔹) → F Fi∘ H =>i G Fi∘ H

  _▸i_
    : {F G : Internal-functor 𝔸 𝔹}
    → (H : Internal-functor 𝔹 ℂ) → F =>i G → H Fi∘ F =>i H Fi∘ G

  _◆i_
    : {F G : Internal-functor 𝔹 ℂ} {H K : Internal-functor 𝔸 𝔹}
    → F =>i G → H =>i K → F Fi∘ H =>i G Fi∘ K

These are almost identical to their 1-categorical counterparts, so we omit their definitions.

  (α ◂i H) .ηi x = α .ηi (H .Fi₀ x)
  (α ◂i H) .is-naturali x y f = α .is-naturali _ _ _
  (α ◂i H) .ηi-nat x σ = ℂ.begini
    α .ηi (H .Fi₀ x) [ σ ] ℂ.≡i⟨ α .ηi-nat _ σ ⟩ℂ.≡i
    α .ηi (H .Fi₀ x ∘ σ)   ℂ.≡i⟨ ap (α .ηi) (H .Fi₀-nat x σ) ⟩ℂ.≡i
    α .ηi (H .Fi₀ (x ∘ σ)) ∎

  (H ▸i α) .ηi x = H .Fi₁ (α .ηi x)
  (H ▸i α) .is-naturali x y f =
    sym (H .Fi-∘ _ _) ∙ ap (H .Fi₁) (α .is-naturali _ _ _) ∙ H .Fi-∘ _ _
  (H ▸i α) .ηi-nat x σ = ℂ.casti $
    H .Fi₁-nat _ σ ℂ.∙i λ i → H .Fi₁ (α .ηi-nat x σ i)

  _◆i_ {F} {G} {H} {K} α β .ηi x = G .Fi₁ (β .ηi x) ℂ.∘i α .ηi (H .Fi₀ x)
  _◆i_ {F} {G} {H} {K} α β .is-naturali x y f =
    (G .Fi₁ (β .ηi _) ℂ.∘i α .ηi _) ℂ.∘i F .Fi₁ (H .Fi₁ f)   ≡⟨ ℂ.pullri (α .is-naturali _ _ _) ⟩≡
    G .Fi₁ (β .ηi _) ℂ.∘i (G .Fi₁ (H .Fi₁ f) ℂ.∘i α .ηi _)   ≡⟨ ℂ.pullli (sym (G .Fi-∘ _ _) ∙ ap (G .Fi₁) (β .is-naturali _ _ _)) ⟩≡
    G .Fi₁ (K .Fi₁ f 𝔹.∘i β .ηi _) ℂ.∘i α .ηi _              ≡⟨ ℂ.pushli (G .Fi-∘ _ _) ⟩≡
    G .Fi₁ (K .Fi₁ f) ℂ.∘i (G .Fi₁ (β .ηi _) ℂ.∘i α .ηi _)   ∎
  _◆i_ {F} {G} {H} {K} α β .ηi-nat x σ = ℂ.begini
    (G .Fi₁ (β .ηi x) ℂ.∘i α .ηi (H .Fi₀ x)) [ σ ]       ℂ.≡i⟨ ℂ.∘i-nat _ _ _ ⟩ℂ.≡i
    G .Fi₁ (β .ηi x) [ σ ] ℂ.∘i α .ηi (H .Fi₀ x) [ σ ]   ℂ.≡i⟨ (λ i → G .Fi₁-nat (β .ηi x) σ i ℂ.∘i α .ηi-nat (H .Fi₀ x) σ i) ⟩ℂ.≡i
    G .Fi₁ (β .ηi x [ σ ]) ℂ.∘i α .ηi (H .Fi₀ x ∘ σ)     ℂ.≡i⟨ (λ i → G .Fi₁ (β .ηi-nat x σ i) ℂ.∘i α .ηi (H .Fi₀-nat x σ i)) ⟩ℂ.≡i
    G .Fi₁ (β .ηi (x ∘ σ)) ℂ.∘i α .ηi (H .Fi₀ (x ∘ σ))   ∎

With that out of the way, we can prove the main result.

module _ {o ℓ} {C : Precategory o ℓ} (𝔸 𝔹 ℂ : Internal.Internal-cat C) where
  open Precategory C
  open Internal C
  open Cat.Instances.InternalFunctor C
  open Functor
  open Internal-functor
  open _=>i_
  private
    module 𝔸 = Cat.Internal.Reasoning 𝔸
    module 𝔹 = Cat.Internal.Reasoning 𝔹
    module ℂ = Cat.Internal.Reasoning ℂ

  Fi∘-functor
    : Functor (Internal-functors 𝔹 ℂ ×ᶜ Internal-functors 𝔸 𝔹) (Internal-functors 𝔸 ℂ)
  Fi∘-functor .F₀ (F , G) = F Fi∘ G

Much like whiskering and horizontal composition, this is identical to the result involving functor composition. The only difference is the addition of extra naturality conditions, which are easy to prove.

  Fi∘-functor .F₁ {F , G} {H , K} (α , β) = α ◆i β
  Fi∘-functor .F-id {F , G} = Internal-nat-path λ x →
    F .Fi₁ (𝔹.idi _) ℂ.∘i ℂ.idi _ ≡⟨ ap (ℂ._∘i ℂ.idi _) (F .Fi-id) ⟩≡
    ℂ.idi _ ℂ.∘i ℂ.idi _          ≡⟨ ℂ.idli _ ⟩≡
    ℂ.idi _ ∎
  Fi∘-functor .F-∘ {F , G} {H , J} {K , L} (α , β) (γ , τ) = Internal-nat-path λ x →
    K .Fi₁ (β .ηi _ 𝔹.∘i τ .ηi _) ℂ.∘i α .ηi _ ℂ.∘i γ .ηi _            ≡⟨ ℂ.pushli (K .Fi-∘ _ _) ⟩≡
    K .Fi₁ (β .ηi _) ℂ.∘i K .Fi₁ (τ .ηi _) ℂ.∘i α .ηi _ ℂ.∘i γ .ηi _   ≡⟨ ℂ.extend-inneri (sym (α .is-naturali _ _ _)) ⟩≡
    K .Fi₁ (β .ηi _) ℂ.∘i α .ηi _ ℂ.∘i H .Fi₁ (τ .ηi _) ℂ.∘i γ .ηi _   ≡⟨ ℂ.associ _ _ _ ⟩≡
    (K .Fi₁ (β .ηi x) ℂ.∘i α .ηi _) ℂ.∘i H .Fi₁ (τ .ηi _) ℂ.∘i γ .ηi _ ∎