caterwaul

Switch Light/Dark Mode

/caterwaul/Category/Functor/liftedMonoidal

Copy path to clipboard

For any monoidal category π’ž, any π’ž-valued functor category is monoidal in the same way by β€œlifting” the monoidal structure of π’ž.

Source

{-|
For any monoidal category π’ž, any π’ž-valued functor category is monoidal in the
same way by β€œlifting” the monoidal structure of π’ž.
-}
let cat = ../Cat/semigroupal

let vObject = Type

let Category = ../Kind cat

let MonoidalCategory = ../Monoidal/Kind cat

in  Ξ»(cObject : Kind) β†’
      let dObject = Type

      in  Ξ»(v : Category Type vObject) β†’
          Ξ»(c : Category vObject cObject) β†’
          Ξ»(d : MonoidalCategory vObject dObject) β†’
            let base = ../Monoidal/extractCategory cat vObject

            let object = cat.arrow cObject dObject

            in      { unit =
                        Ξ»(x : cObject) β†’
                          ../../Functor/Constant/Type
                            dObject
                            cObject
                            { _1 = d.unit, _2 = x }
                    , product =
                        Ξ»(f : { _1 : object, _2 : object }) β†’
                        Ξ»(x : cObject) β†’
                          d.product { _1 = f._1 x, _2 = f._2 x }
                    }
                  ∧ ./category cObject dObject v c (base dObject d)
                : MonoidalCategory vObject object