Library UniMath.CategoryTheory.Core.PosetCat

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.CategoryEquality.

Local Open Scope cat.

1. Posetal categories

Definition is_poset_category
           (C : univalent_category)
  : UU
  := ∏ (x y : C), isaprop (x --> y).

Proposition isaprop_is_poset_category
            (C : univalent_category)
  : isaprop (is_poset_category C).
Show proof.
  do 2 (use impred ; intro).
  apply isapropisaprop.

Definition poset_category
  : UU
  := ∑ (C : univalent_category), is_poset_category C.

Definition make_poset_category
           (C : univalent_category)
           (HC : is_poset_category C)
  : poset_category
  := C ,, HC.

Coercion poset_category_to_category
         (C : poset_category)
  : univalent_category
  := pr1 C.

Definition is_poset_poset_category
           (C : poset_category)
  : is_poset_category C
  := pr2 C.

Definition isaset_ob_poset
           (C : poset_category)
  : isaset C.
Show proof.
  intros x y.
  use (isofhlevelweqb 1 (make_weq _ (univalent_category_is_univalent C x y))).
  use isaproptotal2.
  - intro.
    apply isaprop_is_z_isomorphism.
  - intros.
    apply is_poset_poset_category.

Definition z_iso_poset_category
           {C : poset_category}
           {x y : C}
           (f : x --> y)
           (g : y --> x)
  : z_iso x y.
Show proof.
  use make_z_iso.
  - exact f.
  - exact g.
  - split.
    + apply is_poset_poset_category.
    + apply is_poset_poset_category.

Definition ob_eq_poset_category
           {C : poset_category}
           {x y : C}
           (f : x --> y)
           (g : y --> x)
  : x = y.
Show proof.
  use (isotoid C (univalent_category_is_univalent C)).
  exact (z_iso_poset_category f g).

2. Every posetal category is a poset

Definition poset_category_to_poset
           (C : poset_category)
  : Poset.
Show proof.
  use make_Poset.
  - use make_hSet.
    + exact C.
    + exact (isaset_ob_poset C).
  - use make_PartialOrder.
    + refine (λ x y, make_hProp (x --> y) _).
      apply is_poset_poset_category.
    + repeat split.
      * abstract
          (intros x y z f g ; cbn in * ;
           exact (f · g)).
      * abstract
          (intro x ; cbn in * ;
           apply identity).
      * abstract
          (intros x y f g ; cbn in * ;
           exact (ob_eq_poset_category f g)).

3. Every poset is a posetal category

Section ToPosetCategory.
  Context (P : Poset).

  Definition poset_to_precategory_data
    : precategory_data.
  Show proof.
    use make_precategory_data.
    - use make_precategory_ob_mor.
      + exact P.
      + exact (λ x y, x ≤ y)%poset.
    - use isrefl_posetRelation.
    - use istrans_posetRelation.

  Definition poset_to_precategory
    : precategory.
  Show proof.
    use make_precategory.
    - exact poset_to_precategory_data.
    - abstract (repeat split ; intro ; intros ; apply propproperty).

  Definition poset_to_category
    : category.
  Show proof.
    use make_category.
    - exact poset_to_precategory.
    - abstract
        (intros x y ;
         apply isasetaprop ;
         apply propproperty).

  Proposition is_univalent_poset_to_category
    : is_univalent poset_to_category.
  Show proof.
    intros x y.
    use isweqimplimpl.
    - intro f.
      use isantisymm_posetRelation.
      + apply f.
      + exact (inv_from_z_iso f).
    - apply setproperty.
    - use isaproptotal2.
      + intro.
        apply isaprop_is_z_isomorphism.
      + intros.
        apply propproperty.

  Definition poset_to_univalent_category
    : univalent_category.
  Show proof.
    use make_univalent_category.
    - exact poset_to_category.
    - exact is_univalent_poset_to_category.

  Definition poset_to_poset_category
    : poset_category.
  Show proof.
    use make_poset_category.
    - exact poset_to_univalent_category.
    - intros x y.
      apply propproperty.
End ToPosetCategory.

4. Equivalence between posetal categories and posets

Definition poset_category_weq_poset_left
           (C : poset_category)
  : poset_to_poset_category (poset_category_to_poset C) = C.
Show proof.
  use subtypePath.
  {
    intro.
    use isaprop_is_poset_category.
  }
  use subtypePath.
  {
    intro.
    apply isaprop_is_univalent.
  }
  use subtypePath.
  {
    intro.
    apply isaprop_has_homsets.
  }
  use (invmap (path_precat _ _ (homset_property C))).
  use total2_paths_f.
  - apply idpath.
  - cbn.
    use pathsdirprod.
    + use funextsec ; intro.
      apply (is_poset_poset_category C).
    + repeat (use funextsec ; intro).
      apply (is_poset_poset_category C).

Proposition poset_category_weq_poset_right
            (P : Poset)
  : poset_category_to_poset (poset_to_poset_category P) = P.
Show proof.
  use total2_paths_f.
  - use total2_paths_f.
    + apply idpath.
    + apply isapropisaset.
  - use subtypePath.
    {
      intro.
      apply isaprop_isPartialOrder.
    }
    etrans.
    {
      apply (@pr1_transportf hSet hrel).
    }
    etrans.
    {
      apply transportf_total2_paths_f.
    }
    cbn.
    apply idpath.

Definition poset_category_weq_poset
  : poset_category ≃ Poset.
Show proof.
  use weq_iso.
  - exact poset_category_to_poset.
  - exact poset_to_poset_category.
  - exact poset_category_weq_poset_left.
  - exact poset_category_weq_poset_right.