Library UniMath.CategoryTheory.DisplayedCats.Examples.Cartesian

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.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Categories.StandardCategories.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma.
Require Import UniMath.CategoryTheory.DisplayedCats.Limits.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.

Local Open Scope cat.
Local Open Scope mor_disp.

1. One can consider any category as a displayed category over the unit category

Section over_terminal_category.

  Variable C : category.

  Definition disp_over_unit_data : disp_cat_data unit_category.
  Show proof.
    use tpair.
    - use tpair.
      + intro. apply (ob C).
      + simpl. intros x y c c' e. apply (C ⟦c, c'⟧).
    - use tpair.
      + simpl. intros. apply identity.
      + intros ? ? ? ? ? a b c f g.
        apply (compose (C:=C) f g ).

  Definition disp_over_unit_axioms : disp_cat_axioms _ disp_over_unit_data.
  Show proof.
    repeat split; cbn; intros.
    - apply id_left.
    - etrans. apply id_right.
      apply pathsinv0. unfold mor_disp. cbn.
      apply (eqtohomot (transportf_const _ _)).
    - etrans. apply assoc.
      apply pathsinv0. unfold mor_disp. cbn.
      apply (eqtohomot (transportf_const _ _)).
    - apply homset_property.

  Definition disp_over_unit : disp_cat _ := _ ,, disp_over_unit_axioms.

1.1. Univalence of the category over the unit category


  Lemma isweq_z_iso_to_z_iso_disp
    (a : disp_over_unit tt)
    (b : disp_over_unit tt)
    : isweq (X := z_iso a b) (Y := z_iso_disp (identity_z_iso (tt : unit_category)) a b)
      (λ f, (_ ,, _ ,, z_iso_after_z_iso_inv f ,, z_iso_inv_after_z_iso f)).
  Show proof.
    use isweq_iso.
    - intro f.
      exact (make_z_iso _ _ (inv_mor_after_z_iso_disp f ,, z_iso_disp_after_inv_mor f)).
    - intro.
      now apply z_iso_eq.
    - intro.
      now apply eq_z_iso_disp.

  Proposition is_univalent_disp_disp_over_unit
    (HC : is_univalent C)
    : is_univalent_disp disp_over_unit.
  Show proof.
    intros a b e aa bb.
    induction e, a.
    use weqhomot.
    - exact (weqcomp (make_weq _ (HC _ _)) (make_weq _ (isweq_z_iso_to_z_iso_disp aa bb))).
    - intro ee.
      induction ee.
      apply eq_z_iso_disp.
      apply idpath.

End over_terminal_category.

Lemma disp_over_unit_fiber_equals_cat
  (C : category)
  (u : unit)
  : (disp_over_unit C)[{u}] = C.
Show proof.
  apply (subtypePath (λ _, isaprop_has_homsets _)).
  refine (subtypePairEquality' _ (isaprop_is_precategory _ (homset_property C))).
  induction C as [C Hhomsets].
  induction C as [Cdata Hisprecategory].
  exact (maponpaths (λ x, (pr1 Cdata) ,, x) (pathsdirprod (idpath _) (idpath _))).

2. The cartesian product as a displayed category over the first component

Section cartesian_product_pb.
  Variable C C' : category.

  Definition disp_cartesian : disp_cat C
    := reindex_disp_cat (functor_to_unit C) (disp_over_unit C').

  Lemma comp_disp_cartesian
    (D := disp_cartesian)
    {c c' c'' : C}
    {F : C⟦c, c'⟧} {F' : C⟦c', c''⟧}
    {A : D c} {A' : D c'} {A'' : D c''}
    (G : A -->[F] A') (G' : A' -->[F'] A'')
    : (G ;; G') = G · G'.
  Show proof.
    unfold comp_disp.
    simpl.
    unfold transportb.
    rewrite transportf_set.
    - apply idpath.
    - apply isasetaprop,
        isasetunit.

  Definition cartesian : category := total_category disp_cartesian.

  Lemma cartesian_is_binproduct
    : cartesian = category_binproduct C C'.
  Show proof.
    apply subtypePairEquality';
      [ | apply isaprop_has_homsets].
    apply subtypePairEquality';
      [ | apply isaprop_is_precategory, has_homsets_precategory_binproduct; apply homset_property].
    apply (maponpaths (tpair _ _)).
    use pathsdirprod.
    - apply funextsec.
      intro.
      apply (maponpaths (tpair _ _)).
      exact (transportf_set _ _ _ (isasetaprop (isasetunit _ _))).
    - do 5 (apply funextsec; intro).
      apply (maponpaths (tpair _ _)).
      exact (transportf_set _ _ _ (isasetaprop (isasetunit _ _))).

  Definition pr2_functor
    : cartesian ⟶ C'.
  Show proof.
    use make_functor.
    - use make_functor_data.
      + exact pr2.
      + exact (λ _ _, pr2).
    - abstract (
        use tpair;
        repeat intro;
        cbn;
        exact (maponpaths (λ x, x _) (transportf_const _ _))
      ).

2.1 The cartesian product creates limits


  Section Limits.

    Context {J : graph}.
    Context {d : diagram J cartesian}.
    Context (L : LimCone (mapdiagram (pr1_category _) d)).
    Context (L' : LimCone (mapdiagram pr2_functor d)).

    Definition cartesian_limit_tip
      : disp_cartesian (lim L)
      := lim L'.

    Definition cartesian_limit_cone
      (j : vertex J)
      : cartesian_limit_tip -->[ limOut L j] pr2 (dob d j)
      := limOut L' j.

    Definition cartesian_limit_forms_cone
      : forms_cone d (λ j, (limOut L j,, cartesian_limit_cone j) : cartesian ⟦_ ,, _, _ ,, _⟧).
    Show proof.
      intros u v e.
      use total2_paths_f.
      + apply (limOutCommutes L).
      + refine (maponpaths (λ x, x _ ) (transportf_const _ _) @ _).
        refine (comp_disp_cartesian _ _ @ _).
        apply (limOutCommutes L').

    Section Arrow.
      Context (tip': total_category disp_cartesian).
      Context (cone': cone d tip').

      Definition cartesian_limit_arrow
        : total_category disp_cartesian ⟦ tip', pr11 L,, cartesian_limit_tip ⟧.
      Show proof.
        use tpair.
        - apply (limArrow L _ (mapcone (pr1_category _) d cone')).
        - apply (limArrow L' _ (mapcone (pr2_functor) d cone')).

      Lemma cartesian_limit_arrow_commutes
        : is_cone_mor cone' (make_cone _ cartesian_limit_forms_cone) cartesian_limit_arrow.
      Show proof.
        intro u.
        use total2_paths2.
        - apply (limArrowCommutes L).
        - exact (maponpaths (λ x, x _ ) (transportf_const _ _) @ limArrowCommutes L' _ _ _ ).

      Lemma cartesian_limit_arrow_unique
        (arrow' : cartesian ⟦ tip', lim L,, cartesian_limit_tip ⟧)
        (arrow'_commutes : is_cone_mor cone' (make_cone _ cartesian_limit_forms_cone) arrow')
        : (arrow' ,, arrow'_commutes) = (cartesian_limit_arrow ,, cartesian_limit_arrow_commutes).
      Show proof.
        use total2_paths_f.
        - use total2_paths2.
          + apply (limArrowUnique L).
            intro u.
            exact (maponpaths pr1 (arrow'_commutes u)).
          + apply (limArrowUnique L').
            intro u.
            refine (maponpaths (λ x, x _) (!transportf_const _ _) @ _).
            refine (_ @ fiber_paths (arrow'_commutes u)).
            exact (maponpaths (λ x, x _) (!transportf_const _ _)).
        - apply impred_isaprop;
          intro;
          apply (homset_property (total_category _)).

    End Arrow.

    Definition creates_limits_disp_cartesian
      : creates_limit d L.
    Show proof.
      use make_creates_limit.
      - exact cartesian_limit_tip.
      - exact cartesian_limit_cone.
      - exact cartesian_limit_forms_cone.
      - intros tip' cone'.
        use ((
          cartesian_limit_arrow _ cone' ,,
          cartesian_limit_arrow_commutes _ _) ,,
          λ _, cartesian_limit_arrow_unique _ cone' _ _).

    Definition limits_cartesian
      : LimCone d
      := total_limit _ creates_limits_disp_cartesian.

  End Limits.

End cartesian_product_pb.

3. The arrow category


Section arrow.

  Variable C : category.

  Definition disp_arrow_data : disp_cat_data (cartesian C C).
  Show proof.
    use tpair.
    - use tpair.
      + intro H.
        exact (pr1 H --> pr2 H).
      + cbn. intros xy ab f g h.
        exact (compose f (pr2 h) = compose (pr1 h) g ).
    - split.
      + abstract (
          intros;
          apply pathsinv0;
          refine (id_left xx @ _);
          refine (!id_right xx @ _);
          apply maponpaths, pathsinv0;
          apply (eqtohomot (transportf_const _ (C⟦_, _⟧)))
        ).
      + abstract (
          intros;
          refine (maponpaths (λ x, _ (x _)) (transportf_const _ (C⟦_, _⟧)) @ _);
          refine (assoc _ _ _ @ _);
          refine (maponpaths_2 _ X _ @ _);
          refine (!assoc _ _ _ @ _);
          refine (maponpaths _ X0 @ _);
          apply assoc
        ).

  Definition disp_arrow_axioms : disp_cat_axioms _ disp_arrow_data.
  Show proof.
    repeat split; intros;
      try apply homset_property.
    apply isasetaprop.
    apply homset_property.

  Definition disp_arrow : disp_cat (cartesian C C) := _ ,, disp_arrow_axioms.

  Definition arrow : category := total_category disp_arrow.

  Definition disp_domain : disp_cat C := sigma_disp_cat disp_arrow.

  Definition total_domain := total_category disp_domain.

End arrow.

4. A direct definition of the product category as a displayed category


Section cartesian_product.

  Variables C C' : category.

  Definition disp_cartesian_ob_mor : disp_cat_ob_mor C.
  Show proof.
    use tpair.
    - exact (λ _, C').
    - exact (λ _ _ c d _, C'⟦c, d⟧).

  Definition disp_cartesian_data : disp_cat_data C.
  Show proof.
    exists disp_cartesian_ob_mor.
    use tpair.
    - exact (λ _, identity).
    - exact (λ _ _ _ _ _ _ _ _, compose).

  Definition disp_cartesian_axioms : disp_cat_axioms _ disp_cartesian_data.
  Show proof.
    repeat split; intros.
    - exact (id_left _ @ !eqtohomot (transportf_const _ _) _).
    - exact (id_right _ @ !eqtohomot (transportf_const _ _) _).
    - exact (assoc _ _ _ @ !eqtohomot (transportf_const _ _) _).
    - apply homset_property.

  Definition disp_cartesian' : disp_cat C := _ ,, disp_cartesian_axioms.

  Definition is_univalent_disp_cartesian'
    (H : is_univalent C')
    : is_univalent_disp disp_cartesian'.
  Show proof.
    apply is_univalent_disp_iff_fibers_are_univalent.
    intros T A A'.
    use isweq_iso.
    - intro f.
      apply (isotoid _ H).
      use make_z_iso.
      + exact f.
      + exact (z_iso_inv f).
      + split.
        * refine (!_ @ z_iso_inv_after_z_iso f).
          exact (eqtohomot (transportf_const _ _) _).
        * refine (!_ @ z_iso_after_z_iso_inv f).
          exact (eqtohomot (transportf_const _ _) _).
    - intro e.
      refine (_ @ isotoid_idtoiso _ H _ _ _).
      apply maponpaths.
      apply z_iso_eq.
      now induction e.
    - intro y.
      apply z_iso_eq.
      set (f := make_z_iso (C := C') _ _ _).
      refine (_ @ maponpaths (λ x, z_iso_mor x) (idtoiso_isotoid _ H _ _ f)).
      now induction (isotoid C' H f).

  Definition cartesian' : category := total_category disp_cartesian'.

  Lemma is_univalent_cartesian'
    (H : is_univalent C)
    (H' : is_univalent C')
    : is_univalent cartesian'.
  Show proof.
    use is_univalent_total_category.
    - exact H.
    - apply is_univalent_disp_cartesian'.
      exact H'.

  Definition pr2_functor'
    : cartesian' ⟶ C'.
  Show proof.
    use make_functor.
    - use make_functor_data.
      + exact pr2.
      + exact (λ _ _, pr2).
    - abstract (
        split;
        now repeat intro
      ).

4.1. This cartesian has limits as well


  Section Limits.

    Context {J : graph}.
    Context {d : diagram J cartesian'}.
    Context (L : LimCone (mapdiagram (pr1_category _) d)).
    Context (L' : LimCone (mapdiagram pr2_functor' d)).

    Definition cartesian'_limit_tip
      : disp_cartesian' (lim L)
      := lim L'.

    Definition cartesian'_limit_cone
      (j : vertex J)
      : cartesian'_limit_tip -->[ limOut L j] pr2 (dob d j)
      := limOut L' j.

    Definition cartesian'_limit_forms_cone
      : forms_cone d (λ j, (limOut L j,, cartesian'_limit_cone j) : cartesian' ⟦_ ,, _, _ ,, _⟧).
    Show proof.
      intros u v e.
      use total2_paths_f.
      + apply (limOutCommutes L).
      + refine (maponpaths (λ x, x _ ) (transportf_const _ _) @ _).
        apply (limOutCommutes L').

    Section Arrow.
      Context (tip': total_category disp_cartesian').
      Context (cone': cone d tip').

      Definition cartesian'_limit_arrow
        : total_category disp_cartesian' ⟦ tip', pr11 L,, cartesian'_limit_tip ⟧.
      Show proof.
        use tpair.
        - apply (limArrow L _ (mapcone (pr1_category _) d cone')).
        - apply (limArrow L' _ (mapcone (pr2_functor') d cone')).

      Lemma cartesian'_limit_arrow_commutes
        : is_cone_mor cone' (make_cone _ cartesian'_limit_forms_cone) cartesian'_limit_arrow.
      Show proof.
        intro u.
        use total2_paths2.
        - apply (limArrowCommutes L).
        - exact (limArrowCommutes L' _ _ _ ).

      Lemma cartesian'_limit_arrow_unique
        (arrow' : cartesian' ⟦ tip', lim L,, cartesian'_limit_tip ⟧)
        (arrow'_commutes : is_cone_mor cone' (make_cone _ cartesian'_limit_forms_cone) arrow')
        : (arrow' ,, arrow'_commutes) = (cartesian'_limit_arrow ,, cartesian'_limit_arrow_commutes).
      Show proof.
        use total2_paths_f.
        - use total2_paths2.
          + apply (limArrowUnique L).
            intro u.
            exact (maponpaths pr1 (arrow'_commutes u)).
          + apply (limArrowUnique L').
            intro u.
            refine (maponpaths (λ x, x _) (!transportf_const _ _) @ _).
            exact (fiber_paths (arrow'_commutes u)).
        - apply impred_isaprop;
          intro;
          apply (homset_property (total_category _)).

    End Arrow.

    Definition creates_limits_disp_cartesian'
      : creates_limit d L.
    Show proof.
      use make_creates_limit.
      - exact cartesian'_limit_tip.
      - exact cartesian'_limit_cone.
      - exact cartesian'_limit_forms_cone.
      - intros tip' cone'.
        use ((
          cartesian'_limit_arrow _ cone' ,,
          cartesian'_limit_arrow_commutes _ _) ,,
          λ _, cartesian'_limit_arrow_unique _ cone' _ _).

    Definition limits_cartesian'
      : LimCone d
      := total_limit _ creates_limits_disp_cartesian'.

  End Limits.

End cartesian_product.