Library UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleCat

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.

Local Open Scope cat.

Section StructuredCospansDoubleCat.
  Context {A X : univalent_category}
          (PX : Pushouts X)
          (L : A ⟶ X).

1. Horizontal identities
  Definition structured_cospans_double_cat_hor_id_data
    : hor_id_data (twosided_disp_cat_of_struct_cospans L).
  Show proof.
    use make_hor_id_data.
    - exact (id_struct_cospan L).
    - exact (λ x y f, id_struct_cospan_mor L f).

  Proposition structured_cospans_double_cat_hor_id_laws
    : hor_id_laws structured_cospans_double_cat_hor_id_data.
  Show proof.
    split.
    - intros a.
      use struct_cospan_sqr_eq ; cbn.
      apply functor_id.
    - intros a₁ a₂ a₃ f g.
      use struct_cospan_sqr_eq ; cbn.
      apply functor_comp.

  Definition structured_cospans_double_cat_hor_id
    : hor_id (twosided_disp_cat_of_struct_cospans L).
  Show proof.
    use make_hor_id.
    - exact structured_cospans_double_cat_hor_id_data.
    - exact structured_cospans_double_cat_hor_id_laws.

2. Horizontal composition
  Definition structured_cospans_double_cat_hor_comp_data
    : hor_comp_data (twosided_disp_cat_of_struct_cospans L).
  Show proof.
    use make_hor_comp_data.
    - exact (λ a₁ a₂ a₃ s t, comp_struct_cospan L PX s t).
    - exact (λ _ _ _ _ _ _ _ _ _ _ _ _ _ s₁ s₂, comp_struct_cospan_mor L PX s₁ s₂).

  Proposition structured_cospans_double_cat_hor_comp_laws
    : hor_comp_laws structured_cospans_double_cat_hor_comp_data.
  Show proof.
    split.
    - intros a₁ a₂ a₃ h₁ h₂.
      use struct_cospan_sqr_eq.
      use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
      + unfold mor_of_comp_struct_cospan_mor.
        rewrite PushoutArrow_PushoutIn1 ; cbn.
        rewrite id_left, id_right.
        apply idpath.
      + unfold mor_of_comp_struct_cospan_mor.
        rewrite PushoutArrow_PushoutIn2 ; cbn.
        rewrite id_left, id_right.
        apply idpath.
    - intros.
      use struct_cospan_sqr_eq.
      use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
      + rewrite !assoc.
        unfold mor_of_comp_struct_cospan_mor.
        rewrite !PushoutArrow_PushoutIn1 ; cbn.
        rewrite !assoc'.
        rewrite !PushoutArrow_PushoutIn1.
        rewrite !assoc.
        apply idpath.
      + rewrite !assoc.
        unfold mor_of_comp_struct_cospan_mor.
        rewrite !PushoutArrow_PushoutIn2 ; cbn.
        rewrite !assoc'.
        rewrite !PushoutArrow_PushoutIn2.
        rewrite !assoc.
        apply idpath.

  Definition structured_cospans_double_cat_hor_comp
    : hor_comp (twosided_disp_cat_of_struct_cospans L).
  Show proof.
    use make_hor_comp.
    - exact structured_cospans_double_cat_hor_comp_data.
    - exact structured_cospans_double_cat_hor_comp_laws.

3. The unitors and associators
  Definition structured_cospans_double_cat_lunitor_data
    : double_lunitor_data
        structured_cospans_double_cat_hor_id
        structured_cospans_double_cat_hor_comp.
  Show proof.
    intros x y h.
    simple refine (_ ,, _).
    - exact (struct_cospan_lunitor L PX h).
    - use is_iso_twosided_disp_struct_cospan_sqr ; cbn.
      apply is_z_iso_struct_cospan_lunitor_mor.

  Proposition structured_cospans_double_cat_lunitor_laws
    : double_lunitor_laws structured_cospans_double_cat_lunitor_data.
  Show proof.
    intros x₁ x₂ y₁ y₂ h₁ h₂ v₁ v₂ sq.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
    - rewrite !assoc.
      unfold struct_cospan_lunitor_mor, mor_of_comp_struct_cospan_mor.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn1.
      exact (struct_cospan_sqr_mor_left _ sq).
    - rewrite !assoc.
      unfold struct_cospan_lunitor_mor, mor_of_comp_struct_cospan_mor.
      rewrite !PushoutArrow_PushoutIn2.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn2.
      rewrite id_left, id_right.
      apply idpath.

  Definition structured_cospans_double_cat_lunitor
    : double_cat_lunitor
        structured_cospans_double_cat_hor_id
        structured_cospans_double_cat_hor_comp.
  Show proof.
    use make_double_lunitor.
    - exact structured_cospans_double_cat_lunitor_data.
    - exact structured_cospans_double_cat_lunitor_laws.

  Definition structured_cospans_double_cat_runitor_data
    : double_runitor_data
        structured_cospans_double_cat_hor_id
        structured_cospans_double_cat_hor_comp.
  Show proof.
    intros x y h.
    simple refine (_ ,, _).
    - exact (struct_cospan_runitor L PX h).
    - use is_iso_twosided_disp_struct_cospan_sqr ; cbn.
      apply is_z_iso_struct_cospan_runitor_mor.

  Proposition structured_cospans_double_cat_runitor_laws
    : double_runitor_laws structured_cospans_double_cat_runitor_data.
  Show proof.
    intros x₁ x₂ y₁ y₂ h₁ h₂ v₁ v₂ sq.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
    - rewrite !assoc.
      unfold struct_cospan_runitor_mor, mor_of_comp_struct_cospan_mor.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn1.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc.
      unfold struct_cospan_runitor_mor, mor_of_comp_struct_cospan_mor.
      rewrite !PushoutArrow_PushoutIn2.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn2.
      exact (struct_cospan_sqr_mor_right _ sq).

  Definition structured_cospans_double_cat_runitor
    : double_cat_runitor
        structured_cospans_double_cat_hor_id
        structured_cospans_double_cat_hor_comp.
  Show proof.
    use make_double_runitor.
    - exact structured_cospans_double_cat_runitor_data.
    - exact structured_cospans_double_cat_runitor_laws.

  Definition structured_cospans_double_cat_associator_data
    : double_associator_data structured_cospans_double_cat_hor_comp.
  Show proof.
    intros w x y z h₁ h₂ h₃.
    simple refine (_ ,, _).
    - exact (struct_cospan_associator L PX h₁ h₂ h₃).
    - use is_iso_twosided_disp_struct_cospan_sqr ; cbn.
      apply is_z_iso_struct_cospan_associator_mor.

  Proposition structured_cospans_double_cat_associator_laws
    : double_associator_laws structured_cospans_double_cat_associator_data.
  Show proof.
    intros w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ h₁ h₂ j₁ j₂ k₁ k₂ vw vx vy vz sq₁ sq₂ sq₃.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
    - rewrite !assoc.
      unfold struct_cospan_associator_mor, mor_of_comp_struct_cospan_mor ; cbn.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn1.
      unfold mor_of_comp_struct_cospan_mor.
      rewrite !assoc.
      rewrite PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn1.
      apply idpath.
    - rewrite !assoc.
      unfold struct_cospan_associator_mor, mor_of_comp_struct_cospan_mor.
      rewrite !PushoutArrow_PushoutIn2.
      use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
      + rewrite !assoc.
        rewrite PushoutArrow_PushoutIn1.
        rewrite !assoc'.
        rewrite PushoutArrow_PushoutIn1.
        unfold mor_of_comp_struct_cospan_mor.
        rewrite !assoc.
        rewrite PushoutArrow_PushoutIn1.
        rewrite PushoutArrow_PushoutIn2.
        rewrite !assoc'.
        rewrite PushoutArrow_PushoutIn2.
        rewrite PushoutArrow_PushoutIn1.
        apply idpath.
      + rewrite !assoc.
        unfold mor_of_comp_struct_cospan_mor.
        rewrite !PushoutArrow_PushoutIn2.
        rewrite !assoc'.
        rewrite !PushoutArrow_PushoutIn2.
        apply idpath.

  Definition structured_cospans_double_cat_associator
    : double_cat_associator structured_cospans_double_cat_hor_comp.
  Show proof.
    use make_double_associator.
    - exact structured_cospans_double_cat_associator_data.
    - exact structured_cospans_double_cat_associator_laws.

4. The triangle and pentagon equations
  Proposition structured_cospans_double_cat_triangle
    : triangle_law
        structured_cospans_double_cat_lunitor
        structured_cospans_double_cat_runitor
        structured_cospans_double_cat_associator.
  Show proof.
    intro ; intros.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
    - unfold struct_cospan_associator_mor, mor_of_comp_struct_cospan_mor ; cbn.
      rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite PushoutArrow_PushoutIn1.
      rewrite id_left.
      unfold struct_cospan_runitor_mor.
      rewrite !assoc.
      rewrite PushoutArrow_PushoutIn1.
      apply id_left.
    - unfold struct_cospan_associator_mor, mor_of_comp_struct_cospan_mor ; cbn.
      rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn2.
      unfold struct_cospan_lunitor_mor, struct_cospan_runitor_mor.
      use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
      + rewrite !assoc.
        rewrite !PushoutArrow_PushoutIn1.
        rewrite !assoc'.
        rewrite !PushoutArrow_PushoutIn1.
        rewrite !assoc.
        rewrite !PushoutArrow_PushoutIn2.
        rewrite PushoutSqrCommutes.
        apply idpath.
      + rewrite !assoc.
        rewrite !PushoutArrow_PushoutIn2.
        rewrite !id_left.
        apply idpath.

  Proposition structured_cospans_double_cat_pentagon
    : pentagon_law structured_cospans_double_cat_associator.
  Show proof.
    intro ; intros.
    use struct_cospan_sqr_eq.
    rewrite transportb_disp_mor2_struct_cospan ; cbn.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
    - unfold struct_cospan_associator_mor, mor_of_comp_struct_cospan_mor ; cbn.
      rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite id_left.
      rewrite !PushoutArrow_PushoutIn1.
      rewrite !assoc'.
      rewrite !PushoutArrow_PushoutIn1.
      unfold struct_cospan_associator_mor.
      rewrite !assoc.
      rewrite PushoutArrow_PushoutIn1.
      apply idpath.
    - unfold struct_cospan_associator_mor, mor_of_comp_struct_cospan_mor ; cbn.
      rewrite !assoc.
      rewrite !PushoutArrow_PushoutIn2.
      unfold struct_cospan_associator_mor.
      use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
      + rewrite !assoc.
        rewrite !PushoutArrow_PushoutIn1.
        rewrite !assoc'.
        rewrite !PushoutArrow_PushoutIn1.
        refine (!_).
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !assoc.
          rewrite !PushoutArrow_PushoutIn2.
          apply idpath.
        }
        etrans.
        {
          apply maponpaths.
          rewrite !assoc.
          rewrite !PushoutArrow_PushoutIn1.
          refine (assoc' _ _ _ @ _).
          rewrite !PushoutArrow_PushoutIn1.
          refine (assoc _ _ _ @ _).
          rewrite !PushoutArrow_PushoutIn2.
          apply idpath.
        }
        rewrite !assoc.
        rewrite !PushoutArrow_PushoutIn1.
        apply idpath.
      + rewrite !assoc.
        rewrite !PushoutArrow_PushoutIn2.
        use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX _ _ _ _ _))) ; cbn.
        * rewrite !assoc.
          rewrite !PushoutArrow_PushoutIn1.
          refine (!_).
          rewrite !assoc'.
          etrans.
          {
            do 2 apply maponpaths.
            rewrite !assoc.
            rewrite !PushoutArrow_PushoutIn2.
            apply idpath.
          }
          etrans.
          {
            apply maponpaths.
            rewrite !assoc.
            rewrite !PushoutArrow_PushoutIn1.
            refine (assoc' _ _ _ @ _).
            rewrite !PushoutArrow_PushoutIn1.
            refine (assoc _ _ _ @ _).
            rewrite !PushoutArrow_PushoutIn2.
            apply idpath.
          }
          rewrite !assoc.
          rewrite !PushoutArrow_PushoutIn2.
          apply idpath.
        * rewrite !assoc.
          rewrite !PushoutArrow_PushoutIn2.
          refine (!_).
          rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            rewrite !assoc.
            rewrite !PushoutArrow_PushoutIn2.
            apply idpath.
          }
          rewrite !assoc.
          rewrite !PushoutArrow_PushoutIn2.
          rewrite id_left.
          apply idpath.

5. The double category of structured cospans
  Definition structured_cospans_double_cat
    : double_cat.
  Show proof.
    use make_double_cat.
    - exact A.
    - exact (twosided_disp_cat_of_struct_cospans L).
    - exact structured_cospans_double_cat_hor_id.
    - exact structured_cospans_double_cat_hor_comp.
    - exact structured_cospans_double_cat_lunitor.
    - exact structured_cospans_double_cat_runitor.
    - exact structured_cospans_double_cat_associator.
    - exact structured_cospans_double_cat_triangle.
    - exact structured_cospans_double_cat_pentagon.
    - apply univalent_category_is_univalent.
    - use is_univalent_struct_cospans_twosided_disp_cat.
      apply univalent_category_is_univalent.
End StructuredCospansDoubleCat.