Library UniMath.Bicategories.PseudoFunctors.Examples.PseudofunctorFromMonoidal

  • Construction of a pseudofunctor from a strong monoidal functor - between the bicategories (trivially) generated from the monoidal categories.
  • And the opposite direction: We fix two bicategories and a pseudofunctor between them and an object in the domain bicategory. This gives rise to a strong monoidal functor between the associated monoidal categories of endomorphisms for the fixed object and its image.
Author: Ralph Matthes 2021
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored.
Require Import UniMath.Bicategories.Core.Bicat.
Require Import UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal.
Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Import PseudoFunctor.Notations.

Local Open Scope cat.

Section monoidal_functor_to_psfunctor.

  Context (M N : monoidal_cat).

  Local Definition M_as_bicat := bicat_from_monoidal M.
  Local Definition N_as_bicat := bicat_from_monoidal N.

  Context (smF : strong_monoidal_functor M N).

Definition monoidal_functor_to_psfunctor_map_data: psfunctor_data M_as_bicat N_as_bicat.
Show proof.
  use make_psfunctor_data.
  - cbn. exact (fun x => x).
  - intros a b. cbn.
    exact (functor_on_objects smF).
  - intros a b f g. cbn.
    exact (functor_on_morphisms smF).
  - intros a. cbn. exact (lax_monoidal_functor_ϵ smF).
  - intros a b c f g. cbn. apply (lax_monoidal_functor_μ smF (f,g)).

Definition monoidal_functor_to_psfunctor_map_laws: psfunctor_laws monoidal_functor_to_psfunctor_map_data.
Show proof.
  repeat split; red; cbn.
  - intros H0 H1 a. apply functor_id.
  - intros H0 H1 a b c f g. apply functor_comp.
  - intros H0 H1 a. apply lax_monoidal_functor_unital.
  - intros H0 H1 a. apply (lax_monoidal_functor_unital smF a).
  - intros H0 H1 H2 H3 a b c.
    do 2 rewrite <- assoc. apply pathsinv0.
    apply (z_iso_inv_on_right _ _ _ (nat_z_iso_pointwise_z_iso (monoidal_cat_associator N) ((smF a, smF b), smF c))).
    do 2 rewrite assoc.
    etrans.
    2: { apply maponpaths. apply functor_on_inv_from_z_iso'. }
    apply z_iso_inv_on_left.
    cbn.
    apply pathsinv0.
    apply lax_monoidal_functor_assoc.
  - intros H0 H1 H2 a b1 b2 g. red in g.
    apply pathsinv0.
    assert (Heq := nat_trans_ax (lax_monoidal_functor_μ smF) (a,,b1) (a,,b2) (id a,,g)).
    cbn in Heq.
    rewrite functor_id in Heq.
    exact Heq.
  - intros H0 H1 H2 a1 a2 b f.
    apply pathsinv0.
    assert (Heq := nat_trans_ax (lax_monoidal_functor_μ smF) (a1,,b) (a2,,b) (f,,id b)).
    cbn in Heq.
    rewrite functor_id in Heq.
    exact Heq.

Definition monoidal_functor_to_psfunctor: psfunctor M_as_bicat N_as_bicat.
Show proof.
  use make_psfunctor.
    - exact (monoidal_functor_to_psfunctor_map_data).
    - exact (monoidal_functor_to_psfunctor_map_laws).
    - split ; red; cbn.
      + intros H0. unfold two_cells_from_monoidal.
        exists (strong_monoidal_functor_ϵ_inv smF).
        exact (pr2 (strong_monoidal_functor_ϵ_is_z_iso smF)).
      + intros H0 H1 H2 a b. unfold two_cells_from_monoidal.
        exists (strong_monoidal_functor_μ_inv smF (a,,b)).
        exact (pr2 (strong_monoidal_functor_μ_is_nat_z_iso smF (a,,b))).

End monoidal_functor_to_psfunctor.

Going into the opposite direction

see the description in the file header

Section psfunctor_to_monoidal_functor.

Local Open Scope bicategory_scope.
Import Bicat.Notations.

Context {C : bicat}.
Context (c0: ob C).
Context {D : bicat}.
Context (psF: psfunctor C D).

Local Definition d0 : D := psF c0.
Local Definition M : monoidal_cat := monoidal_cat_from_bicat_and_ob c0.
Local Definition N : monoidal_cat := monoidal_cat_from_bicat_and_ob d0.

Definition psfunctor_to_lax_monoidal_functor_data: functor_data M N.
Show proof.
  use make_functor_data.
  - cbn. intro f. exact (# psF f).
  - intros a b f. red in f. cbn in f.
    cbn. exact (##psF f).

Lemma psfunctor_to_lax_monoidal_functor_data_is_functor : is_functor psfunctor_to_lax_monoidal_functor_data.
Show proof.
  split; red; cbn.
  - intros a. apply psF.
  - intros a b c f g. apply psF.

Definition psfunctor_to_lax_monoidal_functor_functor : M ⟶ N.
Show proof.
  use make_functor.
  - exact psfunctor_to_lax_monoidal_functor_data.
  - exact psfunctor_to_lax_monoidal_functor_data_is_functor.

Local Definition auxμ : nat_trans_data (monoidal_functor_map_dom M N psfunctor_to_lax_monoidal_functor_functor)
                                       (monoidal_functor_map_codom M N psfunctor_to_lax_monoidal_functor_functor).
Show proof.
  red. cbn. intro fg.
  exact (psfunctor_comp psF (pr1 fg) (pr2 fg)).

Local Lemma auxμ_is_nat_trans: is_nat_trans _ _ auxμ.
Show proof.
  red. cbn. intros gh gh' αβ.
  red in αβ. cbn in αβ.
  change (## psF (pr2 αβ) ⋆⋆ ## psF (pr1 αβ) • psfunctor_comp psF (pr1 gh') (pr2 gh') =
          psfunctor_comp psF (pr1 gh) (pr2 gh) • ## psF (pr2 αβ ⋆⋆ pr1 αβ)).
  apply pathsinv0.
  apply (psfunctor_comp_natural psF).

Local Definition μ : monoidal_functor_map M N psfunctor_to_lax_monoidal_functor_functor
  := (auxμ,, auxμ_is_nat_trans).

Lemma psfunctor_to_lax_monoidal_functor_laws :
  monoidal_functor_associativity M N psfunctor_to_lax_monoidal_functor_functor μ
  × monoidal_functor_unitality M N psfunctor_to_lax_monoidal_functor_functor (pr1(psfunctor_id psF c0)) μ.
Show proof.
  split.
  * red. cbn. intros x y z. unfold rassociator_fun'. cbn.
    assert (Hyp := psfunctor_rassociator psF x y z).
    change ((id₂ (# psF z) ⋆⋆ psfunctor_comp psF x y • psfunctor_comp psF (x · y) z)
              • ## psF (rassociator x y z) =
            (rassociator (# psF x) (# psF y) (# psF z) • psfunctor_comp psF y z ⋆⋆ id₂ (# psF x))
              • psfunctor_comp psF x (y · z)).
    rewrite hcomp_identity_right.
    rewrite hcomp_identity_left.
    exact Hyp.
  * red. cbn. intro x.
    split.
    -- change (lunitor (# psF x) =
               (id₂ (# psF x) ⋆⋆ psfunctor_id psF c0 • psfunctor_comp psF (id₁ c0) x)
                 • ## psF (lunitor x)).
       rewrite hcomp_identity_right.
       apply psfunctor_lunitor.
    -- change (runitor (# psF x) =
               (psfunctor_id psF c0 ⋆⋆ id₂ (# psF x) • psfunctor_comp psF x (id₁ c0))
                 • ## psF (runitor x)).
       rewrite hcomp_identity_left.
       apply psfunctor_runitor.

Definition psfunctor_to_lax_monoidal_functor: lax_monoidal_functor M N.
Show proof.
  exists psfunctor_to_lax_monoidal_functor_functor.
  cbn.
    exists (psfunctor_id psF c0).
    exists μ.
    exact psfunctor_to_lax_monoidal_functor_laws.

Definition psfunctor_to_monoidal_functor: strong_monoidal_functor M N.
Show proof.
  exists psfunctor_to_lax_monoidal_functor.
  split.
  - exact (pr2 (psfunctor_id psF c0)).
  - intro c. exact (pr2 (psfunctor_comp psF (pr1 c) (pr2 c))).

End psfunctor_to_monoidal_functor.