Product of categories

Stream: Is there code for X?

[Success Moses]

How to define a projection out of a product category? Please any advice on how to proceed.

import Mathlib.CategoryTheory.Category.Cat.Limit
import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
import Mathlib.CategoryTheory.Enriched.Basic

import Mathlib.CategoryTheory.Monoidal.NaturalTransformation

open CategoryTheory Limits MonoidalCategoryStruct

attribute [local instance] monoidalOfHasFiniteProducts

variable (X Y Z : Type) [Category X] [Category Y] [Category Z]
variable [MonoidalCategory X] [MonoidalCategory Y] [MonoidalCategory Z]

#check Cat.of <| LaxMonoidalFunctor X Y -- has type `Cat`
#check Cat.of <| LaxMonoidalFunctor Y Z -- has type `Cat`

#check tensorObj (Cat.of <| LaxMonoidalFunctor X Y) (Cat.of <| LaxMonoidalFunctor Y Z) -- has type `Cat`

-- Given an object in x in the product category:
variable (x : tensorObj (Cat.of <| LaxMonoidalFunctor X Y) (Cat.of <| LaxMonoidalFunctor Y Z))

-- you have two monoidal functor 'inside' x, i am trying to compose them.
#check LaxMonoidalFunctor.of <|(LaxMonoidalFunctor.toFunctor (Functor.obj (prod.fst) x)) ⋙ (LaxMonoidalFunctor.toFunctor (Functor.obj (prod.snd) x))

/-
Error msg:
failed to synthesize instance of type class
  Category.{?u.28048, 0} (tensorObj ↑(Cat.of (LaxMonoidalFunctor X Y)) ↑(Cat.of (LaxMonoidalFunctor Y Z)))
-/

This is the original code

import Mathlib.CategoryTheory.Category.Cat.Limit
import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
import Mathlib.CategoryTheory.Enriched.Basic

import Mathlib.CategoryTheory.Monoidal.NaturalTransformation

open CategoryTheory Limits MonoidalCategoryStruct

attribute [local instance] monoidalOfHasFiniteProducts

def StrictBicategory (C : Type*) := EnrichedCategory Cat C

-- 0-cells: bundled monoidal categories
structure MonCat where
  carrier : Type*
  [cat      : Category carrier]
  [monoidal : MonoidalCategory carrier]

attribute [instance] MonCat.cat MonCat.monoidal

-- This lets you write X where Type* is expected, instead of X.carrier
instance : CoeSort MonCat (Type*) := ⟨MonCat.carrier⟩

attribute [coe] MonCat.carrier

abbrev MonCat.of (X : Type*) [Category X] [MonoidalCategory X] : MonCat := ⟨X⟩

instance : StrictBicategory MonCat where
  Hom X Y := Cat.of <| LaxMonoidalFunctor X Y
  id X := by
    refine {toFunctor := {obj := fun _ => LaxMonoidalFunctor.of (𝟭 X), map := fun _ => 𝟙 _, map_id := ?_, map_comp := ?_}}
    · aesop_cat
    · aesop_cat
  comp X Y Z := by
    refine {toFunctor := {obj := ?_, map := ?_, map_id := ?_, map_comp := ?_}}
    · exact fun x =>
      LaxMonoidalFunctor.of <| (LaxMonoidalFunctor.toFunctor (Functor.obj (prod.fst) x)) ⋙ (LaxMonoidalFunctor.toFunctor (Functor.obj (prod.snd) x))
    · sorry
    · sorry
    · sorry

[Edward van de Meent]

why are you using tensorObj here? can't you work with Limits.prod?

[Edward van de Meent]

if you really want the MonoidalCategory Cat instance with projections from tensorObj, i'd advise you to derive it via CartesianMonoidalCategory

[Edward van de Meent]

the other bit that you're missing is that morphisms in Cat aren't definitionally equal to Functors.

[Edward van de Meent]

instead, you have to cast them. you can write Cat.Hom.toFunctor f or just f.toFunctor to turn a morphism in Cat into a functor, and you can get a morphism in cat from a functor with Functor.toCatHom (or F.toCatHom, again using dot notation)

[Robin Carlier]

You also shouldn't be reproving the fact that the composition of lax monoidal functors has a lax monoidal structure. Mathlib has docs#CategoryTheory.Functor.LaxMonoidal.comp

[Edward van de Meent]

thinking about this more, don't we already have a definition of strict bicategories?

[Edward van de Meent]

@loogle "Bicategory.IsStrict"

[loogle]

:shrug: nothing found

[Edward van de Meent]

@loogle Bicategory.Strict

[loogle]

:exclamation: unknown identifier 'Bicategory.Strict'
Did you mean "Bicategory.Strict", CategoryTheory.Bicategory.Strict, or something else?

[Edward van de Meent]

that's the one