Library UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory

organizes the (action-based) strong functors between two fixed categories into a category

Author: Ralph Matthes 2021

Require Import UniMath.Foundations.PartD.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.

Require Import UniMath.Bicategories.MonoidalCategories.Actions.
Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength.

Local Open Scope cat.

Section Strong_Functor_Category.

Context (Mon_V : monoidal_cat).

Context {A A': category}.
Context (actn : action Mon_V A)(actn' : action Mon_V A').

Local Definition odot := pr1 actn.
Local Definition odot' := pr1 actn'.

Notation "X ⊙ Y" := (odot (X , Y)) (at level 31).
Notation "f #⊙ g" := (#odot (f #, g )) (at level 31).
Notation "X ⊙' Y" := (odot' (X , Y)) (at level 31).
Notation "f #⊙' g" := (#odot' (f #, g )) (at level 31).

Local Definition ζ (FF : actionbased_strong_functor Mon_V actn actn') := pr12 FF.

Section Strong_Functor_Category_mor.

  Context (FF GG : actionbased_strong_functor Mon_V actn actn').

  Context (η : FF ⟹ GG).

  Definition Strong_Functor_Category_mor_diagram (a: A) (v: Mon_V) : UU :=
    ζ FF (a ,v ) · η (a ⊙ v) = η a #⊙' id v · ζ GG (a ,v ).

  Definition quantified_strong_functor_category_mor_diagram : UU :=
    ∏ (a: A) (v: Mon_V ), Strong_Functor_Category_mor_diagram a v.

End Strong_Functor_Category_mor.

Local Lemma Strong_Functor_Category_Mor_id_subproof (FF : actionbased_strong_functor Mon_V actn actn') a v :
  Strong_Functor_Category_mor_diagram FF FF (nat_trans_id FF) a v.
Show proof.

  red.
  change (ζ FF (a, v) · nat_trans_id FF (a ⊙ v) = # odot' (id (FF a , v )) · ζ FF (a, v)).
  rewrite functor_id.
  now rewrite id_left, id_right.

Local Lemma Strong_Functor_Category_Mor_comp_subproof (FF GG HH : actionbased_strong_functor Mon_V actn actn')
      (η : FF ⟹ GG) (η': GG ⟹ HH):
  quantified_strong_functor_category_mor_diagram FF GG η ->
  quantified_strong_functor_category_mor_diagram GG HH η' ->
  quantified_strong_functor_category_mor_diagram FF HH (nat_trans_comp _ _ _ η η').
Show proof.

  intros ηisstrong η'isstrong.
  red. intros a v. red.
  rewrite <- (id_left (id v)).
  change (ζ FF (a, v) · (η (a ⊙ v) · η' (a ⊙ v)) = # odot' ((η a #, id v ) · (η' a #, id v )) · ζ HH (a, v)).
  rewrite functor_comp.
  etrans.
  { rewrite assoc. apply cancel_postcomposition. apply ηisstrong. }
  do 2 rewrite <- assoc.
  apply maponpaths.
  apply η'isstrong.

Section AsDisplayedCategory.

Definition Strong_Functor_category_displayed : disp_cat (functor_category A A').
Show proof.

    use disp_cat_from_SIP_data.
    - intro F.
      exact (actionbased_strength Mon_V actn actn' F).
    - intros F1 F2 FF1 FF2 η.
      exact (∏ a v , Strong_Functor_Category_mor_diagram (F1,,FF1) (F2,,FF2) η a v).
    - intros F1 F2 FF1 FF2 η.
      do 2 (apply impred; intro).
      apply homset_property.
    - intros F FF a v.
      apply Strong_Functor_Category_Mor_id_subproof.
    - intros F G H FF GG HH η η' ηmor η'mor a v. simpl in ηmor, η'mor.
      exact (Strong_Functor_Category_Mor_comp_subproof (F,,FF) (G,,GG) (H,,HH) η η' ηmor η'mor a v).

  Definition Strong_Functor_category : category := total_category Strong_Functor_category_displayed.

  Lemma Strong_Functor_category_ob_ok :
    ob Strong_Functor_category = actionbased_strong_functor Mon_V actn actn'.
  Show proof.

apply idpath.

  Definition Strong_Functor_Category_Mor :
    actionbased_strong_functor Mon_V actn actn' -> actionbased_strong_functor Mon_V actn actn' -> UU.
  Show proof.

exact (pr2 (precategory_ob_mor_from_precategory_data Strong_Functor_category)).

  Lemma Strong_Functor_Category_Mor_ok (FF GG: actionbased_strong_functor Mon_V actn actn') :
    Strong_Functor_Category_Mor FF GG = total2 (quantified_strong_functor_category_mor_diagram FF GG).
  Show proof.

apply idpath.

  Definition Strong_Functor_Category_Mor_to_nat_trans (FF GG: actionbased_strong_functor Mon_V actn actn') :
    Strong_Functor_Category_Mor FF GG -> FF ⟹ GG.
  Show proof.

intro sη.
exact (pr1 sη).

  Coercion Strong_Functor_Category_Mor_to_nat_trans : Strong_Functor_Category_Mor >-> nat_trans.

  Lemma Strong_Functor_Category_Mor_eq (FF GG : actionbased_strong_functor Mon_V actn actn')
        (sη sη' : Strong_Functor_Category_Mor FF GG) :
    pr1 sη = pr1 sη' -> sη = sη'.
  Show proof.

    intros H.
    apply subtypePath; trivial.
    now intros α; repeat (apply impred; intro); apply homset_property.

  Definition Strong_FunctorForgetfulFunctor:
    functor Strong_Functor_category (functor_category A A').
  Show proof.

    use tpair.
    - use tpair.
      + intros FF; apply FF.
      + intros FF GG η; apply η.
    - abstract (now split).

  Lemma Strong_FunctorForgetfulFunctorFaithful:
    faithful Strong_FunctorForgetfulFunctor.
  Show proof.

    intros FF GG.
    apply isinclbetweensets.
    + apply Strong_Functor_category.
    + apply functor_category_has_homsets.
    + apply Strong_Functor_Category_Mor_eq.

towards univalence

Lemma Strong_Functor_category_Pisset (F : [A , A']) : isaset (actionbased_strength Mon_V actn actn' F).
Show proof.

    change isaset with (isofhlevel 2).
    apply isofhleveltotal2.
    - use (functor_category_has_homsets (A ⊠ Mon_V)). apply homset_property.
    - intro ϛ.
      apply isasetaprop.
      apply isapropdirprod.
      + apply isaprop_actionbased_strength_triangle_eq.
      + apply isaprop_actionbased_strength_pentagon_eq.

  Lemma Strong_Functor_category_Hstandard (F : [A , A']) (sη sη' : actionbased_strength Mon_V actn actn' F) :
    (∏ (a : A) (v : Mon_V ), Strong_Functor_Category_mor_diagram (F ,,sη) (F ,,sη') (id F) a v )
  → (∏ (a : A) (v : Mon_V ), Strong_Functor_Category_mor_diagram (F ,,sη') (F ,,sη) (id F) a v ) → sη = sη'.
  Show proof.

    intros leq geq.
    apply actionbased_strength_eq.
    apply nat_trans_eq_alt.
    intro av.
    assert (leqinst := leq (pr1 av) (pr2 av)).
    clear leq geq.
    etrans.
    { apply pathsinv0.
      apply id_right. }
    etrans.
    { exact leqinst. }
    clear leqinst.
    etrans.
    2: { apply id_left. }
    apply cancel_postcomposition.
    show_id_type.
    change (# odot' (id (pr1 F (pr1 av ), pr2 av )) = id actionbased_strength_dom Mon_V actn' F av).
    rewrite functor_id.
    apply idpath.

Definition is_univalent_Strong_Functor_category_displayed : is_univalent_disp Strong_Functor_category_displayed.
Show proof.

    use is_univalent_disp_from_SIP_data.
    - exact Strong_Functor_category_Pisset.
    - exact Strong_Functor_category_Hstandard.

End AsDisplayedCategory.

End Strong_Functor_Category.

Definition is_univalent_Strong_Functor_category (Mon_V : monoidal_cat) (A : category)
(A' : univalent_category) (actn : action Mon_V A) (actn' : action Mon_V A') :
is_univalent (Strong_Functor_category Mon_V actn actn').
Show proof.

  apply SIP.
  - exact (is_univalent_functor_category A _ (pr2 A')).
  - apply Strong_Functor_category_Pisset.
  - apply Strong_Functor_category_Hstandard.