module Cat.Instances.OuterFunctor
  {o β„“} {C : Precategory o β„“}

The category of outer functorsπŸ”—

Like most constructions in category theory, outer functors, and outer natural transformations between them, can also be regarded as a category. By a rote calculation, we can define the identity and composite outer natural transformations.

  idnto : βˆ€ {F : Outer-functor β„‚} β†’ F =>o F
  idnto {F = F} .Ξ·o px = px
  idnto {F = F} .Ξ·o-fib _ = refl
  idnto {F = F} .is-naturalo px y f =
    ap (F .P₁ px) (Internal-hom-path refl)
  idnto {F = F} .Ξ·o-nat _ _ = refl

  _∘nto_ : βˆ€ {F G H : Outer-functor β„‚} β†’ G =>o H β†’ F =>o G β†’ F =>o H
  _∘nto_ α β .ηo x = α .ηo (β .ηo x)
  _∘nto_ Ξ± Ξ² .Ξ·o-fib px = Ξ± .Ξ·o-fib (Ξ² .Ξ·o px) βˆ™ Ξ² .Ξ·o-fib px
  _∘nto_ {H = H} α β .is-naturalo px y f =
    ap (Ξ± .Ξ·o) (Ξ² .is-naturalo px y f)
    βˆ™ Ξ± .is-naturalo (Ξ² .Ξ·o px) y (adjusti (sym (Ξ² .Ξ·o-fib px)) refl f)
    βˆ™ ap (H .P₁ _) (Internal-hom-path refl)
  (Ξ± ∘nto Ξ²) .Ξ·o-nat px Οƒ =
    Ξ± .Ξ·o-nat (Ξ² .Ξ·o px) Οƒ βˆ™ ap (Ξ± .Ξ·o) (Ξ² .Ξ·o-nat px Οƒ)

These are almost definitionally a precategory, requiring only an appeal to extensionality to establish the laws.

  Outer-functors : Precategory (o βŠ” β„“) (o βŠ” β„“)
  Outer-functors .Precategory.Ob = Outer-functor β„‚
  Outer-functors .Precategory.Hom = _=>o_
  Outer-functors .Precategory.Hom-set _ _ = hlevel 2
  Outer-functors = idnto
  Outer-functors .Precategory._∘_ = _∘nto_
  Outer-functors .Precategory.idr Ξ± = Outer-nat-path (Ξ» _ β†’ refl)
  Outer-functors .Precategory.idl Ξ± = Outer-nat-path (Ξ» _ β†’ refl)
  Outer-functors .Precategory.assoc Ξ± Ξ² Ξ³ = Outer-nat-path (Ξ» _ β†’ refl)

The constant-functor functorπŸ”—

If is a category with products, and is a category internal to then we can construct a constant outer-functor functor

  Ξ”o : Functor C (Outer-functors β„‚)
  Ξ”o .Fβ‚€ = ConstO prods
  Ξ”o .F₁ = const-nato prods
  Ξ”o .F-id = Outer-nat-path Ξ» px β†’
    apβ‚‚ ⟨_,_⟩ (idl _) refl
    βˆ™ sym (⟨⟩∘ px)
    βˆ™ eliml ⟨⟩-Ξ·
  Ξ”o .F-∘ f g = Outer-nat-path Ξ» px β†’
    ⟨ (f ∘ g) ∘ π₁ ∘ px , Ο€β‚‚ ∘ px ⟩                                        β‰‘βŸ¨ products! C prods βŸ©β‰‘
    ⟨ f ∘ π₁ ∘ ⟨ g ∘ π₁ ∘ px , Ο€β‚‚ ∘ px ⟩ , Ο€β‚‚ ∘ ⟨ g ∘ π₁ ∘ px , Ο€β‚‚ ∘ px ⟩ ⟩ ∎