Library UniMath.CategoryTheory.IsoCommaCategory

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.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Groupoids.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.

Local Open Scope cat.

Section IsoCommaCategory.
  Context {C₁ C₂ C₃ : category}
          (F : C₁ ⟶ C₃)
          (G : C₂ ⟶ C₃).

Definition of iso comma categories via displayed categories
  Definition iso_comma_disp_cat_ob_mor
    : disp_cat_ob_mor (category_binproduct C₁ C₂).
  Show proof.
    simple refine (_ ,, _).
    - exact (λ x, z_iso (F (pr1 x)) (G (pr2 x))).
    - exact (λ x y i₁ i₂ f, #F (pr1 f) · i₂ = i₁ · #G (pr2 f)).

  Definition iso_comma_disp_cat_id_comp
    : disp_cat_id_comp _ iso_comma_disp_cat_ob_mor.
  Show proof.
    simple refine (_ ,, _).
    - intros x i ; cbn.
      rewrite !functor_id.
      rewrite id_left, id_right.
      apply idpath.
    - cbn ; intros x y z f g i₁ i₂ i₃ p q.
      rewrite !functor_comp.
      rewrite !assoc'.
      rewrite q.
      rewrite !assoc.
      rewrite p.
      apply idpath.

  Definition iso_comma_disp_cat_data
    : disp_cat_data (category_binproduct C₁ C₂).
  Show proof.
    simple refine (_ ,, _).
    - exact iso_comma_disp_cat_ob_mor.
    - exact iso_comma_disp_cat_id_comp.

  Definition iso_comma_disp_cat_axioms
    : disp_cat_axioms _ iso_comma_disp_cat_data.
  Show proof.
    repeat split ; intros ; try (apply homset_property).
    apply isasetaprop.
    apply homset_property.

  Definition iso_comma_disp_cat
    : disp_cat (category_binproduct C₁ C₂).
  Show proof.
    simple refine (_ ,, _).
    - exact iso_comma_disp_cat_data.
    - exact iso_comma_disp_cat_axioms.

  Definition iso_comma
    : category
    := total_category iso_comma_disp_cat.

  Definition eq_iso_comma_mor
             {x y : iso_comma}
             {f g : x --> y}
             (p : pr11 f = pr11 g)
             (q : pr21 f = pr21 g)
    : f = g.
  Show proof.
    use subtypePath.
    {
      intro.
      apply homset_property.
    }
    use pathsdirprod.
    - exact p.
    - exact q.

  Definition is_z_iso_iso_comma
             {x y : iso_comma}
             (f : x --> y)
             (H₁ : is_z_isomorphism (pr11 f))
             (H₂ : is_z_isomorphism (pr21 f))
    : is_z_isomorphism f.
  Show proof.
    simple refine ((_ ,, _) ,, _).
    split.
    - exact (inv_from_z_iso (_ ,, H₁)).
    - exact (inv_from_z_iso (_ ,, H₂)).
    - abstract
          (cbn ;
           rewrite !functor_on_inv_from_z_iso ;
           use z_iso_inv_on_left ;
           rewrite assoc' ;
           refine (!_) ;
           use z_iso_inv_on_right ;
           cbn ;
           refine (!_) ;
           apply (pr2 f)).
    - split.
      + abstract
          (use eq_iso_comma_mor ;
           cbn ;
           [ apply (z_iso_inv_after_z_iso (make_z_iso' _ H₁))
           | apply (z_iso_inv_after_z_iso (make_z_iso' _ H₂)) ]).
      + abstract
          (use eq_iso_comma_mor ;
           cbn ;
           [ apply (z_iso_after_z_iso_inv (make_z_iso' _ H₁))
           | apply (z_iso_after_z_iso_inv (make_z_iso' _ H₂)) ]).

  Definition is_pregroupoid_iso_comma
             (HC₁ : is_pregroupoid C₁)
             (HC₂ : is_pregroupoid C₂)
    : is_pregroupoid iso_comma.
  Show proof.
    intros x y f.
    apply is_z_iso_iso_comma.
    - apply HC₁.
    - apply HC₂.

Univalence of the iso-comma category
  Definition is_univalent_disp_iso_comma_disp_cat
             (HC₃ : is_univalent C₃)
    : is_univalent_disp iso_comma_disp_cat.
  Show proof.
    intros x y p i₁ i₂.
    induction p.
    use isweqimplimpl.
    - intros p.
      pose (pr1 p) as m.
      cbn in m.
      rewrite !functor_id in m.
      rewrite id_left, id_right in m.
      use subtypePath.
      {
        intro ; apply isaprop_is_z_isomorphism.
      }
      exact (!m).
    - apply isaset_z_iso.
    - use isaproptotal2.
      + intro.
        apply isaprop_is_z_iso_disp.
      + intros.
        apply homset_property.

  Definition is_univalent_iso_comma
             (HC₁ : is_univalent C₁)
             (HC₂ : is_univalent C₂)
             (HC₃ : is_univalent C₃)
    : is_univalent iso_comma.
  Show proof.
    use is_univalent_total_category.
    - apply is_univalent_category_binproduct.
      + exact HC₁.
      + exact HC₂.
    - exact (is_univalent_disp_iso_comma_disp_cat HC₃).

Projection functors
  Definition iso_comma_pr1
    : iso_comma ⟶ C₁
    := pr1_category iso_comma_disp_cat ∙ pr1_functor C₁ C₂.

  Definition iso_comma_pr2
    : iso_comma ⟶ C₂
    := pr1_category iso_comma_disp_cat ∙ pr2_functor C₁ C₂.

Natural isomorphism witnessing the commutation
  Definition iso_comma_commute_nat_trans_data
    : nat_trans_data (iso_comma_pr1 ∙ F) (iso_comma_pr2 ∙ G).
  Show proof.
    intros x ; cbn in x.
    exact (pr2 x).

  Definition iso_comma_commute_is_nat_trans
    : is_nat_trans _ _ iso_comma_commute_nat_trans_data.
  Show proof.
    intros x y f ; unfold iso_comma_commute_nat_trans_data ; cbn ; cbn in f.
    exact (pr2 f).

  Definition iso_comma_commute_nat_trans
    : iso_comma_pr1 ∙ F ⟹ iso_comma_pr2 ∙ G.
  Show proof.
    use make_nat_trans.
    - exact iso_comma_commute_nat_trans_data.
    - exact iso_comma_commute_is_nat_trans.

  Definition iso_comma_commute
    : nat_z_iso
        (iso_comma_pr1 ∙ F)
        (iso_comma_pr2 ∙ G).
  Show proof.
    use make_nat_z_iso.
    - exact iso_comma_commute_nat_trans.
    - intros x.
      apply z_iso_is_z_isomorphism.

Mapping property of iso-comma category
We need to check three mapping properties:
  • The first one gives the existence of a functor
  • The second one gives the existence of a natural transformation
  • The third one can be used to show that two natural transformations are equal
  Section UniversalMappingProperty.
    Context {D : category}
            (P : D ⟶ C₁)
            (Q : D ⟶ C₂)
            (η : nat_z_iso (P ∙ F) (Q ∙ G)).

The functor witnessing the universal property
    Definition iso_comma_ump1_data
      : functor_data D iso_comma.
    Show proof.
      use make_functor_data.
      - exact (λ d, (P d ,, Q d) ,, nat_z_iso_pointwise_z_iso η d).
      - exact (λ d₁ d₂ f, (#P f ,, #Q f) ,, nat_trans_ax η _ _ f).

    Definition iso_comma_ump1_is_functor
      : is_functor iso_comma_ump1_data.
    Show proof.
      split.
      - intro x ; cbn.
        use subtypePath.
        {
          intro ; apply homset_property.
        }
        cbn.
        rewrite !functor_id.
        apply idpath.
      - intros x y z f g ; cbn.
        use subtypePath.
        {
          intro ; apply homset_property.
        }
        cbn.
        rewrite !functor_comp.
        apply idpath.

    Definition iso_comma_ump1
      : D ⟶ iso_comma.
    Show proof.
      use make_functor.
      - exact iso_comma_ump1_data.
      - exact iso_comma_ump1_is_functor.

The computation rules
    Definition iso_comma_ump1_pr1_nat_trans_data
      : nat_trans_data (iso_comma_ump1 ∙ iso_comma_pr1) P
      := λ x, identity _.

    Definition iso_comma_ump1_pr1_is_nat_trans
      : is_nat_trans _ _ iso_comma_ump1_pr1_nat_trans_data.
    Show proof.
      intros x y f ; cbn ; unfold iso_comma_ump1_pr1_nat_trans_data.
      rewrite id_left, id_right.
      apply idpath.

    Definition iso_comma_ump1_pr1_nat_trans
      : iso_comma_ump1 ∙ iso_comma_pr1 ⟹ P.
    Show proof.
      use make_nat_trans.
      - exact iso_comma_ump1_pr1_nat_trans_data.
      - exact iso_comma_ump1_pr1_is_nat_trans.

Computation rule for first projection
    Definition iso_comma_ump1_pr1
      : nat_z_iso (iso_comma_ump1 ∙ iso_comma_pr1) P.
    Show proof.
      use make_nat_z_iso.
      - exact iso_comma_ump1_pr1_nat_trans.
      - intro.
        apply identity_is_z_iso.

    Definition iso_comma_ump1_pr2_nat_trans_data
      : nat_trans_data (iso_comma_ump1 ∙ iso_comma_pr2) Q
      := λ x, identity _.

    Definition iso_comma_ump1_pr2_is_nat_trans
      : is_nat_trans _ _ iso_comma_ump1_pr2_nat_trans_data.
    Show proof.
      intros x y f ; cbn ; unfold iso_comma_ump1_pr2_nat_trans_data.
      rewrite id_left, id_right.
      apply idpath.

    Definition iso_comma_ump1_pr2_nat_trans
      : iso_comma_ump1 ∙ iso_comma_pr2 ⟹ Q.
    Show proof.
      use make_nat_trans.
      - exact iso_comma_ump1_pr2_nat_trans_data.
      - exact iso_comma_ump1_pr2_is_nat_trans.

Computation rule for second projection
    Definition iso_comma_ump1_pr2
      : nat_z_iso (iso_comma_ump1 ∙ iso_comma_pr2) Q.
    Show proof.
      use make_nat_z_iso.
      - exact iso_comma_ump1_pr2_nat_trans.
      - intro.
        apply identity_is_z_iso.

Computation rule for natural iso
    Definition iso_comma_ump1_commute
      : pre_whisker iso_comma_ump1 iso_comma_commute
        =
        nat_trans_comp
          _ _ _
          (nat_trans_functor_assoc_inv _ _ _)
          (nat_trans_comp
             _ _ _
             (post_whisker iso_comma_ump1_pr1 F)
             (nat_trans_comp
                _ _ _
                η
                (nat_trans_comp
                   _ _ _
                   (post_whisker (nat_z_iso_inv iso_comma_ump1_pr2) G)
                   (nat_trans_functor_assoc _ _ _)))).
    Show proof.
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro ; cbn ; unfold iso_comma_ump1_pr1_nat_trans_data.
      rewrite (functor_id F), (functor_id G).
      rewrite !id_left.
      rewrite id_right.
      apply idpath.

Now we look at the second universal mapping property
    Context (Φ₁ Φ₂ : D ⟶ iso_comma)
            (τ₁ : Φ₁ ∙ iso_comma_pr1 ⟹ Φ₂ ∙ iso_comma_pr1)
            (τ₂ : Φ₁ ∙ iso_comma_pr2 ⟹ Φ₂ ∙ iso_comma_pr2)
            (p : ∏ (x : D),
                 pr12 (Φ₁ x) · #G (τ₂ x)
                 =
                 #F (τ₁ x) · pr12 (Φ₂ x)).

    Definition iso_comma_ump2_nat_trans_data
      : nat_trans_data Φ₁ Φ₂.
    Show proof.
      intro x.
      simple refine ((_ ,, _) ,, _) ; cbn.
      - exact (τ₁ x).
      - exact (τ₂ x).
      - abstract
          (exact (!(p x))).

    Definition iso_comma_ump2_is_nat_trans
      : is_nat_trans _ _ iso_comma_ump2_nat_trans_data.
    Show proof.
      intros x y f.
      use eq_iso_comma_mor.
      - exact (nat_trans_ax τ₁ _ _ f).
      - exact (nat_trans_ax τ₂ _ _ f).

    Definition iso_comma_ump2
      : Φ₁ ⟹ Φ₂.
    Show proof.
      use make_nat_trans.
      - exact iso_comma_ump2_nat_trans_data.
      - exact iso_comma_ump2_is_nat_trans.

The computation rules
    Definition iso_comma_ump2_pr1
      : post_whisker iso_comma_ump2 iso_comma_pr1 = τ₁.
    Show proof.
      use nat_trans_eq.
      {
        intro ; apply homset_property.
      }
      intro x ; cbn.
      apply idpath.

    Definition iso_comma_ump2_pr2
      : post_whisker iso_comma_ump2 iso_comma_pr2 = τ₂.
    Show proof.
      use nat_trans_eq.
      {
        intro ; apply homset_property.
      }
      intro x ; cbn.
      apply idpath.

The uniqueness
    Context {n₁ n₂ : Φ₁ ⟹ Φ₂}
            (n₁_pr1 : post_whisker n₁ iso_comma_pr1 = τ₁)
            (n₁_pr2 : post_whisker n₁ iso_comma_pr2 = τ₂)
            (n₂_pr1 : post_whisker n₂ iso_comma_pr1 = τ₁)
            (n₂_pr2 : post_whisker n₂ iso_comma_pr2 = τ₂).

    Definition iso_comma_ump_eq
      : n₁ = n₂.
    Show proof.
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x.
      use eq_iso_comma_mor.
      - pose (nat_trans_eq_pointwise n₁_pr1 x) as q₁.
        pose (nat_trans_eq_pointwise n₂_pr1 x) as q₂.
        cbn in q₁, q₂.
        exact (q₁ @ !q₂).
      - pose (nat_trans_eq_pointwise n₁_pr2 x) as q₁.
        pose (nat_trans_eq_pointwise n₂_pr2 x) as q₂.
        cbn in q₁, q₂.
        exact (q₁ @ !q₂).
  End UniversalMappingProperty.
End IsoCommaCategory.

Definition univalent_iso_comma
           {C₁ C₂ C₃ : univalent_category}
           (F : C₁ ⟶ C₃)
           (G : C₂ ⟶ C₃)
  : univalent_category.
Show proof.
  use make_univalent_category.
  - exact (iso_comma F G).
  - apply is_univalent_iso_comma.
    + exact (pr2 C₁).
    + exact (pr2 C₂).
    + exact (pr2 C₃).

Essentially surjective functors are closed under pullback
Definition iso_comma_essentially_surjective
           {C₁ C₂ C₃ : category}
           (F : C₁ ⟶ C₃)
           (HF : essentially_surjective F)
           (G : C₂ ⟶ C₃)
  : essentially_surjective (iso_comma_pr2 F G).
Show proof.
  intros y.
  use (factor_through_squash _ _ (HF (G y))).
  - apply isapropishinh.
  - intros x.
    induction x as [ x i ].
    apply hinhpr.
    simple refine (((_ ,, _) ,, _) ,, _) ; cbn.
    + exact x.
    + exact y.
    + exact i.
    + apply identity_z_iso.