Library UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleFunctor

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.TwoSidedDisplayedCats.TwoSidedDispCat.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.StructuredCospans.
Require Import UniMath.CategoryTheory.limits.pushouts.
Require Import UniMath.CategoryTheory.limits.Preservation.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCategoryBasics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleFunctor.Basics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCats.
Require Import UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleCat.

Local Open Scope cat.
Local Open Scope double_cat.

Section StructuredCospansDoubleFunctor.
  Context {A₁ A₂ X₁ X₂ : univalent_category}
          (PX₁ : Pushouts X₁)
          (PX₂ : Pushouts X₂)
          {L₁ : A₁ ⟶ X₁}
          {L₂ : A₂ ⟶ X₂}
          {FA : A₁ ⟶ A₂}
          {FX : X₁ ⟶ X₂}
          (α : FA ∙ L₂ ⟹ L₁ ∙ FX).

1. Preservation of horizontal identities
  Definition structured_cospans_double_cat_functor_id_data
    : double_functor_hor_id_data
        (twosided_disp_cat_of_struct_cospans_functor α)
        (structured_cospans_double_cat_hor_id L₁)
        (structured_cospans_double_cat_hor_id L₂).
  Show proof.
    intro x.
    use make_struct_cospan_sqr.
    - exact (α x).
    - abstract
        (split ; cbn ;
         rewrite !functor_id, !id_left, id_right ;
         apply idpath).

  Proposition structured_cospans_double_cat_functor_id_laws
    : double_functor_hor_id_laws
        structured_cospans_double_cat_functor_id_data.
  Show proof.
    intros x y f.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    apply (nat_trans_ax α _ _ f).

  Definition structured_cospans_double_cat_functor_id
    : double_functor_hor_id
        (twosided_disp_cat_of_struct_cospans_functor α)
        (structured_cospans_double_cat_hor_id L₁)
        (structured_cospans_double_cat_hor_id L₂).
  Show proof.
    use make_double_functor_hor_id.
    - exact structured_cospans_double_cat_functor_id_data.
    - exact structured_cospans_double_cat_functor_id_laws.

2. Preservation of horizontal composition
  Definition structured_cospans_double_cat_functor_comp_data
    : double_functor_hor_comp_data
        (twosided_disp_cat_of_struct_cospans_functor α)
        (structured_cospans_double_cat_hor_comp PX₁ L₁)
        (structured_cospans_double_cat_hor_comp PX₂ L₂).
  Show proof.
    intros x y z h k.
    use make_struct_cospan_sqr.
    - use PushoutArrow ; cbn.
      + exact (#FX (PushoutIn1 _)).
      + exact (#FX (PushoutIn2 _)).
      + abstract
          (rewrite !assoc' ;
           apply maponpaths ;
           rewrite <- !functor_comp ;
           apply maponpaths ;
           apply PushoutSqrCommutes).
    - abstract
        (split ;
         [ cbn ;
           rewrite !assoc' ;
           rewrite functor_id, id_left ;
           rewrite PushoutArrow_PushoutIn1 ;
           rewrite <- !functor_comp ;
           apply idpath
         | cbn ;
           rewrite !assoc' ;
           rewrite functor_id, id_left ;
           rewrite PushoutArrow_PushoutIn2 ;
           rewrite <- !functor_comp ;
           apply idpath ]).

  Proposition structured_cospans_double_cat_functor_comp_laws
    : double_functor_hor_comp_laws
        structured_cospans_double_cat_functor_comp_data.
  Show proof.
    intro ; intros.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn.
    - unfold mor_of_comp_struct_cospan_mor.
      rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn1.
      cbn.
      rewrite <- !functor_comp.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite <- !functor_comp.
      apply idpath.
    - unfold mor_of_comp_struct_cospan_mor.
      rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn2.
      cbn.
      rewrite <- !functor_comp.
      rewrite !PushoutArrow_PushoutIn2.
      rewrite !assoc'.
      rewrite !PushoutArrow_PushoutIn2.
      rewrite <- !functor_comp.
      apply idpath.

  Definition structured_cospans_double_cat_functor_comp
    : double_functor_hor_comp
        (twosided_disp_cat_of_struct_cospans_functor α)
        (structured_cospans_double_cat_hor_comp PX₁ L₁)
        (structured_cospans_double_cat_hor_comp PX₂ L₂).
  Show proof.
    use make_double_functor_hor_comp.
    - exact structured_cospans_double_cat_functor_comp_data.
    - exact structured_cospans_double_cat_functor_comp_laws.

3. The coherences
  Proposition structured_cospans_double_cat_functor_lunitor
    : double_functor_lunitor
        (structured_cospans_double_cat_lunitor PX₁ L₁)
        (structured_cospans_double_cat_lunitor PX₂ L₂)
        structured_cospans_double_cat_functor_id
        structured_cospans_double_cat_functor_comp.
  Show proof.
    intros x y f.
    use struct_cospan_sqr_eq.
    rewrite transportf_disp_mor2_struct_cospan ; cbn.
    unfold struct_cospan_lunitor_mor, mor_of_comp_struct_cospan_mor.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn.
    - rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)).
      rewrite PushoutArrow_PushoutIn1.
      rewrite <- functor_comp.
      rewrite PushoutArrow_PushoutIn1.
      apply idpath.
    - rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn2.
      rewrite !assoc'.
      rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)).
      rewrite PushoutArrow_PushoutIn2.
      rewrite <- functor_comp.
      rewrite PushoutArrow_PushoutIn2.
      rewrite functor_id.
      rewrite id_left.
      apply idpath.

  Proposition structured_cospans_double_cat_functor_runitor
    : double_functor_runitor
        (structured_cospans_double_cat_runitor PX₁ L₁)
        (structured_cospans_double_cat_runitor PX₂ L₂)
        structured_cospans_double_cat_functor_id
        structured_cospans_double_cat_functor_comp.
  Show proof.
    intros x y f.
    use struct_cospan_sqr_eq.
    rewrite transportf_disp_mor2_struct_cospan ; cbn.
    unfold struct_cospan_runitor_mor, mor_of_comp_struct_cospan_mor.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn.
    - rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)).
      rewrite PushoutArrow_PushoutIn1.
      rewrite <- functor_comp.
      rewrite PushoutArrow_PushoutIn1.
      rewrite functor_id, id_left.
      apply idpath.
    - rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn2.
      rewrite !assoc'.
      rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)).
      rewrite PushoutArrow_PushoutIn2.
      rewrite <- functor_comp.
      rewrite PushoutArrow_PushoutIn2.
      apply idpath.

  Proposition structured_cospans_double_cat_functor_associator
    : double_functor_associator
        (structured_cospans_double_cat_associator PX₁ L₁)
        (structured_cospans_double_cat_associator PX₂ L₂)
        structured_cospans_double_cat_functor_comp.
  Show proof.
    intro ; intros.
    use struct_cospan_sqr_eq.
    rewrite transportf_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn.
    - refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn1.
      }
      do 2 refine (assoc' _ _ _ @ _).
      etrans.
      {
        apply maponpaths.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn1.
      }
      refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn1.
      }
      refine (assoc' _ _ _ @ _).
      etrans.
      {
        apply maponpaths.
        apply PushoutArrow_PushoutIn1.
      }
      refine (!_).
      refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn1.
      }
      do 2 refine (assoc' _ _ _ @ _).
      etrans.
      {
        apply maponpaths.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn1.
      }
      etrans.
      {
        apply maponpaths.
        refine (!(functor_comp _ _ _) @ _).
        apply maponpaths.
        apply PushoutArrow_PushoutIn1.
      }
      refine (_ @ functor_comp _ _ _).
      refine (_ @ id_left _).
      apply maponpaths_2 ; cbn.
      apply idpath.
    - refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn2.
      }
      refine (!_).
      refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply PushoutArrow_PushoutIn2.
      }
      use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn.
      + refine (assoc _ _ _ @ _).
        etrans.
        {
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn1.
        }
        do 2 refine (assoc' _ _ _ @ _).
        etrans.
        {
          apply maponpaths.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn2.
        }
        etrans.
        {
          apply maponpaths.
          refine (!(functor_comp _ _ _) @ _).
          apply maponpaths.
          apply PushoutArrow_PushoutIn2.
        }
        etrans.
        {
          refine (!(functor_comp _ _ _) @ _).
          apply maponpaths.
          apply PushoutArrow_PushoutIn1.
        }
        refine (!_).
        refine (assoc _ _ _ @ _).
        etrans.
        {
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn1.
        }
        do 2 refine (assoc' _ _ _ @ _).
        etrans.
        {
          apply maponpaths.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn1.
        }
        refine (assoc _ _ _ @ _).
        etrans.
        {
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn2.
        }
        refine (assoc' _ _ _ @ _).
        etrans.
        {
          apply maponpaths.
          apply PushoutArrow_PushoutIn1.
        }
        exact (!(functor_comp _ _ _)).
      + refine (assoc _ _ _ @ _).
        etrans.
        {
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn2.
        }
        do 2 refine (assoc' _ _ _ @ _).
        etrans.
        {
          apply maponpaths.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn2.
        }
        etrans.
        {
          apply maponpaths.
          refine (!(functor_comp _ _ _) @ _).
          apply maponpaths.
          apply PushoutArrow_PushoutIn2.
        }
        etrans.
        {
          refine (!(functor_comp _ _ _) @ _).
          apply maponpaths.
          apply PushoutArrow_PushoutIn2.
        }
        refine (!_).
        refine (assoc _ _ _ @ _).
        etrans.
        {
          apply maponpaths_2.
          refine (assoc _ _ _ @ _).
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn2.
        }
        etrans.
        {
          apply maponpaths_2.
          apply PushoutArrow_PushoutIn2.
        }
        refine (assoc' _ _ _ @ _).
        refine (id_left _ @ _).
        apply PushoutArrow_PushoutIn2.

4. The double functors between the double categories of structured cospans
  Definition structured_cospans_double_cat_functor
    : lax_double_functor
        (structured_cospans_double_cat PX₁ L₁)
        (structured_cospans_double_cat PX₂ L₂).
  Show proof.
    use make_lax_double_functor.
    - exact FA.
    - exact (twosided_disp_cat_of_struct_cospans_functor α).
    - exact structured_cospans_double_cat_functor_id.
    - exact structured_cospans_double_cat_functor_comp.
    - exact structured_cospans_double_cat_functor_lunitor.
    - exact structured_cospans_double_cat_functor_runitor.
    - exact structured_cospans_double_cat_functor_associator.

5. Conditions under which this double functor is strong
  Context (Hα : is_nat_z_iso α)
          (HFX : preserves_pushout FX).

  Definition structured_cospans_double_cat_functor_unit_iso
             (x : A₁)
    : is_iso_twosided_disp
        (identity_is_z_iso _)
        (identity_is_z_iso _)
        (lax_double_functor_id_h structured_cospans_double_cat_functor x).
  Show proof.
    use is_iso_twosided_disp_struct_cospan_sqr.
    apply Hα.

  Section PreservesComp.
    Context {x y z : structured_cospans_double_cat PX₁ L₁}
            (h : x -->h y)
            (k : y -->h z).

    Local Lemma structured_cospans_double_cat_functor_comp_iso_inv_eq
      : # FX (mor_right_of_struct_cospan L₁ h)
        · # FX (PushoutIn1 (comp_struct_cospan_Pushout L₁ PX₁ h k))
        =
        # FX (mor_left_of_struct_cospan L₁ k)
        · # FX (PushoutIn2 (comp_struct_cospan_Pushout L₁ PX₁ h k)).
    Show proof.
      rewrite <- !functor_comp.
      apply maponpaths.
      apply PushoutSqrCommutes.

    Let P : Pushout
              (# FX (mor_right_of_struct_cospan L₁ h))
              (# FX (mor_left_of_struct_cospan L₁ k))
      := make_Pushout
           _ _ _ _ _
           structured_cospans_double_cat_functor_comp_iso_inv_eq
           (HFX
              _ _ _ _ _ _ _ _ _ _
              (isPushout_Pushout (comp_struct_cospan_Pushout L₁ PX₁ h k))).

    Definition structured_cospans_double_cat_functor_comp_iso_inv
      : FX (comp_struct_cospan_Pushout L₁ PX₁ h k)
        -->
        comp_struct_cospan_Pushout
          L₂ PX₂
          (functor_on_struct_cospan α h) (functor_on_struct_cospan α k).
    Show proof.
      use (PushoutArrow P).
      - exact (PushoutIn1 _).
      - exact (PushoutIn2 _).
      - abstract
          (use (cancel_z_iso' (make_z_iso _ _ (Hα y))) ;
           rewrite !assoc ;
           apply PushoutSqrCommutes).

    Proposition structured_cospans_double_cat_functor_comp_iso_inv_laws
      : is_inverse_in_precat
          (struct_cospan_sqr_ob_mor L₂
             (lax_double_functor_comp_h
                structured_cospans_double_cat_functor h k))
          structured_cospans_double_cat_functor_comp_iso_inv.
    Show proof.
      split ; unfold structured_cospans_double_cat_functor_comp_iso_inv.
      - use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn.
        + rewrite !assoc.
          rewrite PushoutArrow_PushoutIn1.
          rewrite id_right.
          apply (PushoutArrow_PushoutIn1 P).
        + rewrite !assoc.
          rewrite PushoutArrow_PushoutIn2.
          rewrite id_right.
          apply (PushoutArrow_PushoutIn2 P).
      - use (MorphismsOutofPushoutEqual (isPushout_Pushout P)) ; cbn.
        + rewrite !assoc.
          rewrite (PushoutArrow_PushoutIn1 P).
          rewrite PushoutArrow_PushoutIn1.
          rewrite id_right.
          apply idpath.
        + rewrite !assoc.
          rewrite (PushoutArrow_PushoutIn2 P).
          rewrite PushoutArrow_PushoutIn2.
          rewrite id_right.
          apply idpath.

    Definition structured_cospans_double_cat_functor_comp_iso
      : is_iso_twosided_disp
          (identity_is_z_iso _)
          (identity_is_z_iso _)
          (lax_double_functor_comp_h structured_cospans_double_cat_functor h k).
    Show proof.
      use is_iso_twosided_disp_struct_cospan_sqr.
      use make_is_z_isomorphism.
      - exact structured_cospans_double_cat_functor_comp_iso_inv.
      - exact structured_cospans_double_cat_functor_comp_iso_inv_laws.
  End PreservesComp.

  Definition is_strong_structured_cospans_double_cat_functor
    : is_strong_double_functor structured_cospans_double_cat_functor.
  Show proof.
    split.
    - exact structured_cospans_double_cat_functor_unit_iso.
    - exact (λ x y z h k, structured_cospans_double_cat_functor_comp_iso h k).
End StructuredCospansDoubleFunctor.