caterwaul

Switch Light/Dark Mode

/caterwaul/Category/Functor/liftedRig

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 RigCategory = ../Rig/Kind cat

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

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

            let object = cat.arrow cObject dObject

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