caterwaul

Switch Light/Dark Mode

/caterwaul/Category/Functor/liftedDuoidal

Copy path to clipboard

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

Source

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

let vObject = Type

let Category = ../Kind cat

let DuoidalCategory = ../Duoidal/Kind cat

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

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

            let object = cat.arrow cObject dObject

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