{-|
Any functor `p : C → C'` induces a functor between functor categories
`[C', D] → [C, D]`.
-}
let cat = ../Cat/semigroupal

let Compose = ../../Compose/Type

let Functor = ../../Functor/Type

let FunctorCategory = ./category

let NaturalTransformation = ../../NaturalTransformation/Type

let Set = ../Set/monoidal/cartesian

let Category = ../Kind cat

let vObject = Type

let v = Set.{ arrow, constraint }

in  λ(cObject : Kind) →
    λ(c : Category vObject cObject) →
    λ(cpObject : Kind) →
    λ(cp : Category vObject cpObject) →
    λ(p : cat.arrow cObject cpObject) →
    λ(dObject : Kind) →
    λ(d : Category vObject dObject) →
        { map =
            λ(a : cat.arrow cpObject dObject) →
            λ(b : cat.arrow cpObject dObject) →
            λ ( fn
              : NaturalTransformation cpObject dObject d { _1 = a, _2 = b }
              ) →
            λ(i : cObject) →
              fn (p i)
        }
      : Functor
          vObject
          (cat.arrow cpObject dObject)
          (cat.arrow cObject dObject)
          v
          (FunctorCategory cpObject dObject v cp d)
          (FunctorCategory cObject dObject v c d)
          ( λ(h : cat.arrow cpObject dObject) →
              Compose cObject cpObject dObject { _1 = h, _2 = p }
          )