Library UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor


Require Import UniMath.Foundations.All.
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.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.PrecompEquivalence.
Require Import UniMath.CategoryTheory.catiso.

Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.

Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.

Require Import UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts.

Local Open Scope mor_disp.
Local Open Scope cat.

Section TensorRezk.

  Context {C D E : category} {H : functor C D}
          (Duniv : is_univalent D)
          (Euniv : is_univalent E)
          (H_eso : essentially_surjective H)
          (H_ff : fully_faithful H).

  Context (TC : functor (C ⊠ C) C)
          (TE : functor (E ⊠ E) E).

  Local Notation HH := (pair_functor H H).
  Let HH_eso := pair_functor_eso H H H_eso H_eso.
  Let HH_ff := pair_functor_ff H H H_ff H_ff.

  Definition TransportedTensor
    : functor (D ⊠ D) D
    := lift_functor_along (_,,Duniv) HH HH_eso HH_ff (functor_composite TC H).

  Definition TransportedTensorComm
    : nat_z_iso (HH ∙ TransportedTensor)
                (functor_composite TC H)
    := lift_functor_along_comm (_,,Duniv) HH HH_eso HH_ff (functor_composite TC H).

  Let TD := TransportedTensor.

  Definition precompT_data
    : disp_functor_data (pre_composition_functor _ _ E H)
                   (functor_tensor_disp_cat TD TE)
                   (functor_tensor_disp_cat TC TE).
  Show proof.
    exists (λ G GG, functor_tensor_composition (pr1 (TransportedTensorComm)) GG).
    intros G1 G2 GG1 GG2 β ββ.
    intros x y.
    simpl.
    rewrite assoc.
    etrans. { apply maponpaths_2 ; exact (ββ (H x) (H y)). }
    do 2 rewrite assoc'.
    apply maponpaths.
    exact (! pr2 β _ _ (pr1 (pr1 (TransportedTensorComm)) (x, y))).

  Definition HT
    : disp_functor (pre_composition_functor _ _ E H)
                   (functor_tensor_disp_cat TD TE)
                   (functor_tensor_disp_cat TC TE).
  Show proof.
    exists precompT_data.
    abstract (split ; intro ; intros ; apply isaprop_is_nat_trans_tensor).

  Definition lifted_functor_tensor
             {G : D ⟶ E}
             (HGG : functor_tensor TC TE (functor_compose H G))
    : functor_tensor TD TE G.
  Show proof.
    use (lift_nat_trans_along (_,,Euniv) _ HH_eso HH_ff).
    use (nat_trans_comp _ _ _ HGG _).
    exact (post_whisker (nat_z_iso_inv TransportedTensorComm) G).

  Definition HT_eso : disp_functor_disp_ess_split_surj HT.
  Show proof.
    intros G HGG.
    exists (lifted_functor_tensor HGG).
    use Isos.make_z_iso_disp.
    - intros c1 c2.
      simpl.
      rewrite id_right.
      rewrite (functor_id TE).
      rewrite id_left.

      set (β :=
             nat_trans_comp
               (functor_tensor_map_dom TE (functor_compose H G))
               (functor_tensor_map_codom TC (functor_compose H G))
               (HH ∙ functor_tensor_map_codom TD G) HGG
               (post_whisker
                  (nat_z_iso_inv TransportedTensorComm)
                  G
               )
             : (nat_trans
                                 (HH ∙ ((pair_functor G G) ∙ TE))
                                 ( HH ∙ functor_tensor_map_codom TD G))
          ).

      set (p := toforallpaths _ _ _ (base_paths _ _
                                                (lift_nat_trans_along_comm (_,,Euniv) _ HH_eso HH_ff β)) (c1,c2)).
      etrans.
      2: {
        apply maponpaths_2.
        exact (! p).
      }
      clear p.
      unfold β.

      unfold nat_trans_comp.
      unfold pr1.
      rewrite assoc'.
      etrans.
      2: {
        apply maponpaths.
        apply (functor_comp G).
      }

      etrans.
      2: {
        do 2 apply maponpaths.
        apply (! pr22 (pr2 (TransportedTensorComm) (c1,c2))).
      }
      rewrite functor_id.
      apply (! id_right _).
    - use tpair.
      2: { split ; apply isaprop_is_nat_trans_tensor. }
      intros c1 c2.
      simpl.
      rewrite id_right.
      rewrite (functor_id TE).
      rewrite id_left.
      unfold lifted_functor_tensor.

      set (β :=
             nat_trans_comp
               (functor_tensor_map_dom TE (functor_compose H G))
               (functor_tensor_map_codom TC (functor_compose H G))
               (HH ∙ functor_tensor_map_codom TD G) HGG
               (post_whisker
                  (nat_z_iso_inv TransportedTensorComm)
                  G
               )
             : (nat_trans
                                 (HH ∙ ((pair_functor G G) ∙ TE))
                                 ( HH ∙ functor_tensor_map_codom TD G))
          ).

      set (p := toforallpaths _ _ _ (base_paths _ _
                                                (lift_nat_trans_along_comm (_,,Euniv) _ HH_eso HH_ff β)) (c1,c2)).
      etrans. {
        apply maponpaths_2.
        exact p.
      }
      clear p.
      unfold β.

      unfold nat_trans_comp.
      unfold pr1.
      rewrite assoc'.
      etrans. {
        apply maponpaths.
        apply (! functor_comp G _ _).
      }

      etrans. {
        do 2 apply maponpaths.
        apply (pr22 (pr2 (TransportedTensorComm) (c1,c2))).
      }
      rewrite functor_id.
      apply id_right.

  Definition HT_is_faithful
             {G1 G2 : [D, E]}
             (GG1 : functor_tensor_disp_cat TD TE G1)
             (GG2 : functor_tensor_disp_cat TD TE G2)
             (β : [D, E] ⟦ G1, G2 ⟧)
    : isincl (λ ff : GG1 -->[ β] GG2, ♯ HT ff).
  Show proof.
    do 3 intro.
    assert (p : isaset ( hfiber (λ ff : GG1 -->[ β] GG2, ♯ HT ff) y)).
    {
      use isaset_hfiber ; use isasetaprop ; apply isaprop_is_nat_trans_tensor.
    }

    use tpair.
    + use total2_paths_f.
      { apply isaprop_is_nat_trans_tensor. }
      use proofirrelevance.
      use hlevelntosn.
      apply isaprop_is_nat_trans_tensor.
    + intro ; apply p.

  Definition HT_is_full
             {G1 G2 : [D, E]}
             (GG1 : functor_tensor_disp_cat TD TE G1)
             (GG2 : functor_tensor_disp_cat TD TE G2)
             (β : [D, E] ⟦ G1, G2 ⟧)
    : issurjective (λ ff : GG1 -->[ β] GG2, ♯ HT ff).
  Show proof.
    intro βHH.
    apply hinhpr.
    use tpair.
    2: apply isaprop_is_nat_trans_tensor.

    use is_nat_trans_tensor_to_characterization.
    use (lift_nat_trans_eq_along (_,,Euniv) _ HH_eso HH_ff).
    use nat_trans_eq.
    { apply homset_property. }
    intro cc.

    set (t := βHH (pr1 cc) (pr2 cc)).
    simpl.

    transparent assert ( ff : (E ⟦ functor_tensor_map_codom TC (pre_composition_functor C D E H G2) (pr1 cc, pr2 cc),
                                   functor_tensor_map_codom TD G2 (H (pr1 cc), H (pr2 cc)) ⟧) ).
    {
      apply #(pr1 G2).
      exact (pr1 (pr2 TransportedTensorComm (pr1 cc, pr2 cc))).
    }

    assert (p : pr1 GG2 (H (pr1 cc), H (pr2 cc)) = (pr1 (HT G2 GG2) (pr1 cc, pr2 cc)) · ff).
    {
      etrans.
      2: {
        simpl.
        rewrite assoc'.
        apply maponpaths.
        unfold ff.
        rewrite <- (functor_comp G2).
        apply maponpaths.
        simpl.
        apply (! pr12 (pr2 TransportedTensorComm _)).
      }
      rewrite (functor_id G2).
      apply (! id_right _).
    }

    etrans. { apply maponpaths ; exact p. }
    clear p.
    rewrite assoc.
    etrans. { apply maponpaths_2 ; exact t. }
    clear t.
    simpl.
    do 2 rewrite assoc'.
    apply maponpaths.
    unfold ff.
    set (q := pr2 β _ _ (pr1 (pr2 TransportedTensorComm (pr1 cc, pr2 cc)))).
    etrans. {
      apply maponpaths.
      exact (! q).
    }
    clear q.

    rewrite assoc.
    rewrite <- (functor_comp G1).
    etrans. {
      apply maponpaths_2.
      apply maponpaths.
      apply (pr2 TransportedTensorComm).
    }
    rewrite functor_id.
    apply id_left.

  Definition HT_ff : disp_functor_ff HT.
  Show proof.
    intro ; intros.
    apply isweqinclandsurj.
    - apply HT_is_faithful.
    - apply HT_is_full.

  Definition precomp_tensor_is_ff
    : fully_faithful (total_functor HT).
  Show proof.
    use disp_functor_ff_to_total_ff.
    - apply precomp_fully_faithful.pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful.
      + exact H_eso.
      + exact H_ff.
    - exact HT_ff.

  Definition precomp_tensor_is_eso
    : essentially_surjective (total_functor HT).
  Show proof.
    use disp_functor_eso_to_total_eso.
    - apply precomp_ess_surj.pre_composition_essentially_surjective.
      + exact Euniv.
      + exact H_eso.
      + exact H_ff.
    - exact HT_eso.
    - use Fibrations.iso_cleaving_category.
      apply is_univalent_functor_category.
      exact Euniv.

  Definition precomp_tensor_adj_equiv
    : adj_equivalence_of_cats (total_functor HT).
  Show proof.
    apply rad_equivalence_of_cats.
    - apply is_univalent_total_category.
      + apply is_univalent_functor_category.
        exact Euniv.
      + apply functor_tensor_disp_cat_is_univalent.
    - exact precomp_tensor_is_ff.
    - exact precomp_tensor_is_eso.

  Definition precomp_tensor_catiso
    : catiso (total_category (functor_tensor_disp_cat TransportedTensor TE))
             (total_category (functor_tensor_disp_cat TC TE)).
  Show proof.
    use (adj_equivalence_of_cats_to_cat_iso precomp_tensor_adj_equiv _ _).
    - apply (is_univalent_total_category (is_univalent_functor_category _ _ Euniv) (functor_tensor_disp_cat_is_univalent _ _)).
    - apply (is_univalent_total_category (is_univalent_functor_category _ _ Euniv) (functor_tensor_disp_cat_is_univalent _ _)).

End TensorRezk.