open import Cat.Diagram.Product.Solver
open import Cat.Internal.Functor.Outer
open import Cat.Diagram.Product
open import Cat.Prelude

import Cat.Internal.Reasoning
import Cat.Internal.Base
import Cat.Reasoning

module Cat.Instances.OuterFunctor
{o β} {C : Precategory o β}
where

open Cat.Reasoning C
open Cat.Internal.Base C
open Functor
open Outer-functor
open _=>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.

module _ {β : Internal-cat} where
open Internal-cat β

  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.

module _ (β : Internal-cat) where
open Internal-cat β

  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 .Precategory.id = 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)

module _ (prods : has-products C) (β : Internal-cat) where
open Internal-cat β
open Binary-products C prods


## 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 β© β© β