{-|
If there is a natural transformation from `n` to `m`, then a m-Star functor can
be made into an n-Star functor.
-}
let kCat = ../../Category/Cat/semigroupal

let vObject = Type

let v =
      ../../Category/Monoidal/Cartesian/extractMonoidal
        kCat
        Type
        vObject
        ../../Category/Set/monoidal/cartesian

let Set =
      ../../Category/Monoidal/Cartesian/extractCategory
        kCat
        vObject
        Type
        ../../Category/Set/monoidal/cartesian

in  λ(object : Kind) →
    λ(cat : ../../Category/Kind kCat vObject object) →
    λ(category : ../../Category/Type object v cat) →
      let vBase = ../../Category/Monoidal/extractCategory kCat Type vObject v

      let endoObject = kCat.arrow object object

      let endo =
            ../../Category/Monoidal/extractCategory
              kCat
              vObject
              endoObject
              (../../Category/Endofunctor/monoidal/monadic object vBase cat)

      in  λ(f : endoObject) →
              { map =
                  λ(m : endoObject) →
                  λ(n : endoObject) →
                  λ(natural : endo.arrow { _1 = n, _2 = m }) →
                  λ(star : ./Type vObject object vBase cat m f) →
                    { map =
                        λ(a : object) →
                        λ(b : object) →
                        λ(fn : cat.arrow { _1 = a, _2 = n b }) →
                          star.map
                            a
                            b
                            ( category.product
                                { _1 = a, _2 = m b }
                                ( λ(r : Type) →
                                  λ ( arrowsOut
                                    : ∀(z : object) →
                                      cat.arrow { _1 = z, _2 = m b } →
                                      cat.arrow { _1 = a, _2 = z } →
                                        r
                                    ) →
                                    arrowsOut (n b) (natural b) fn
                                )
                            )
                    }
              }
            : ../../Functor/Contravariant
                vObject
                endoObject
                Type
                vBase
                endo
                Set
                (λ(a : endoObject) → ./Type vObject object vBase cat a f)