Library UniMath.CategoryTheory.Elements

****************************************************************************
The category of elements of a functor "F : C ⟶ HSET"
Contents:
Originally written by: Dan Grayson Ported to CT by: Anders Mörtberg

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.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Univalence.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.

Local Open Scope cat.

Definition pointed_sets
  : category
  := total_category elements_universal.

Definition is_univalent_disp_elements_universal
  : is_univalent_disp elements_universal.
Show proof.
  use is_univalent_disp_from_fibers.
  intros X x₁ x₂.
  use isweqimplimpl.
  - exact (λ p, pr1 p).
  - apply X.
  - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
    + apply X.
    + apply isaprop_is_z_iso_disp.

Definition is_univalent_pointed_sets
  : is_univalent pointed_sets.
Show proof.
  use is_univalent_total_category.
  - apply is_univalent_HSET.
  - exact is_univalent_disp_elements_universal.

Definition pointed_sets_univalent
  : univalent_category.
Show proof.
  use make_univalent_category.
  - exact pointed_sets.
  - exact is_univalent_pointed_sets.

Definition set_of_pointed_set
  : pointed_sets_univalent ⟶ HSET_univalent_category
  := pr1_category elements_universal.

Definition is_z_iso_pointed_sets
           {X Y : pointed_sets}
           (f : X --> Y)
           (Hf : is_z_isomorphism (pr1 f))
  : is_z_isomorphism f.
Show proof.
  use tpair.
  - simple refine (_ ,, _).
    + exact (inv_from_z_iso (make_z_iso' _ Hf)).
    + abstract
        (cbn ;
         pose (pr2 f) as p ;
         cbn in p ;
         rewrite <- p ;
         exact (eqtohomot (z_iso_inv_after_z_iso (make_z_iso' _ Hf)) (pr2 X))).
  - split.
    + abstract
        (use subtypePath ; [ intro ; apply (pr1 X) | ] ;
         exact (z_iso_inv_after_z_iso (make_z_iso' _ Hf))).
    + abstract
        (use subtypePath ; [ intro ; apply (pr1 Y) | ] ;
         exact (z_iso_after_z_iso_inv (make_z_iso' _ Hf))).

Section CategoryOfElements.
  Context {C : category}
          (F : C ⟶ HSET).

  Definition disp_cat_of_elems_ob_mor
    : disp_cat_ob_mor C.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ c, (F c : hSet)).
    - exact (λ c₁ c₂ x y f, #F f x = y).

  Definition disp_cat_of_elems_id_comp
    : disp_cat_id_comp C disp_cat_of_elems_ob_mor.
  Show proof.
    split.
    - exact (λ c x, eqtohomot (functor_id F c) x).
    - refine (λ c₁ c₂ c₃ f g x₁ x₂ x₃ p q, _) ; cbn in *.
      refine (eqtohomot (functor_comp F f g) x₁ @ _) ; cbn.
      exact (maponpaths (# F g) p @ q).

  Definition disp_cat_of_elems_data
    : disp_cat_data C.
  Show proof.
    simple refine (_ ,, _).
    - exact disp_cat_of_elems_ob_mor.
    - exact disp_cat_of_elems_id_comp.

  Definition disp_mor_elems_isaprop
             {c₁ c₂ : C}
             (f : c₁ --> c₂)
             (x₁ : disp_cat_of_elems_data c₁)
             (x₂ : disp_cat_of_elems_data c₂)
    : isaprop (x₁ -->[ f ] x₂).
  Show proof.
    use invproofirrelevance.
    intros φ₁ φ₂.
    cbn in *.
    apply (F c₂).

  Definition disp_cat_of_elems_axioms
    : disp_cat_axioms C disp_cat_of_elems_data.
  Show proof.
    repeat split ; intros ; cbn.
    - apply disp_mor_elems_isaprop.
    - apply disp_mor_elems_isaprop.
    - apply disp_mor_elems_isaprop.
    - apply isasetaprop.
      apply disp_mor_elems_isaprop.

  Definition disp_cat_of_elems
    : disp_cat C.
  Show proof.
    simple refine (_ ,, _).
    - exact disp_cat_of_elems_data.
    - exact disp_cat_of_elems_axioms.

  Definition is_univalent_disp_disp_cat_of_elems
    : is_univalent_disp disp_cat_of_elems.
  Show proof.
    use is_univalent_disp_from_fibers.
    intros c x₁ x₂.
    use isweqimplimpl.
    - intro f.
      exact (!(eqtohomot (functor_id F c) x₁) @ pr1 f).
    - apply (F c).
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
      + apply disp_mor_elems_isaprop.
      + apply isaprop_is_z_iso_disp.

  Definition is_z_iso_disp_cat_of_elems
             {c₁ c₂ : C}
             {f : z_iso c₁ c₂}
             {x : disp_cat_of_elems c₁}
             {y : disp_cat_of_elems c₂}
             (p : x -->[ f ] y)
    : is_z_iso_disp f p.
  Show proof.
    simple refine (_ ,, (_ ,, _)) ; cbn in *.
    - rewrite <- p.
      refine (!(eqtohomot (functor_comp F f (inv_from_z_iso f)) x) @ _).
      rewrite z_iso_inv_after_z_iso.
      apply (eqtohomot (functor_id F c₁) x).
    - apply disp_mor_elems_isaprop.
    - apply disp_mor_elems_isaprop.

  Definition disp_cat_of_elems_is_opcartesian
             {c₁ c₂ : C}
             {f : c₁ --> c₂}
             {x₁ : disp_cat_of_elems c₁}
             {x₂ : disp_cat_of_elems c₂}
             (p : x₁ -->[ f ] x₂)
    : is_opcartesian p.
  Show proof.
    intros c₃ x₃ g hh.
    use iscontraprop1.
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; cbn -[isaprop].
      + apply disp_mor_elems_isaprop.
      + apply disp_cat_of_elems.
    - simple refine (_ ,, _) ; cbn in *.
      + refine (_ @ hh).
        refine (maponpaths (#F g) (!p) @ _).
        exact (!(eqtohomot (functor_comp F f g) x₁)).
      + apply disp_mor_elems_isaprop.

  Definition disp_cat_of_elems_opcleaving
    : opcleaving disp_cat_of_elems.
  Show proof.
    intros c₁ c₂ x₁ f ; cbn in *.
    simple refine (_ ,, _ ,, _) ; cbn.
    - exact (#F f x₁).
    - apply idpath.
    - apply disp_cat_of_elems_is_opcartesian.

  Definition cat_of_elems_path_lift
             {x₁ x₂ : C}
             (p : x₁ = x₂)
             (y : disp_cat_of_elems x₂)
    : disp_cat_of_elems x₁.
  Show proof.
    induction p.
    exact y.

  Definition cat_of_elems_path_path
             {x₁ x₂ : C}
             (p : x₁ = x₂)
             (y : disp_cat_of_elems x₂)
    : #F (idtoiso p) (cat_of_elems_path_lift p y) = y.
  Show proof.
    induction p.
    cbn.
    exact (eqtohomot (functor_id F x₁) y).

  Definition cat_of_elems_path_natural
             {x₁ x₂ x₁' x₂' : C}
             (f₁ : x₁ --> x₁')
             (f₂ : x₂ --> x₂')
             (p : x₁ = x₂)
             (p' : x₁' = x₂')
             (y : disp_cat_of_elems x₂)
             (y' : disp_cat_of_elems x₂')
             (q : f₁ · idtoiso p' = idtoiso p · f₂)
             (r : y' = # F f₂ y)
    : cat_of_elems_path_lift p' y'
      =
      #F f₁ (cat_of_elems_path_lift p y).
  Show proof.
    induction p, p'.
    cbn ; cbn in *.
    rewrite id_left, id_right in q.
    rewrite q.
    exact r.

  Section CatOfElemsIsoCleaving.
    Context (HC : is_univalent C)
            {x₁ x₂ : C}
            (f : x₁ --> x₂)
            (Hf : is_z_isomorphism f)
            (y : disp_cat_of_elems x₂).

    Definition cat_of_elems_iso_lift
      : disp_cat_of_elems x₁
      := cat_of_elems_path_lift (isotoid _ HC (make_z_iso' _ Hf)) y.

    Definition cat_of_elems_iso_path
      : #F f cat_of_elems_iso_lift = y.
    Show proof.
      refine (_ @ cat_of_elems_path_path (isotoid _ HC (make_z_iso' _ Hf)) y).
      apply maponpaths_2.
      rewrite idtoiso_isotoid.
      apply idpath.
  End CatOfElemsIsoCleaving.

  Definition cat_of_elems_z_iso_natural
             (HC : is_univalent C)
             {x₁ x₂ x₁' x₂' : C}
             (f₁ : x₁ --> x₁')
             (f₂ : x₂ --> x₂')
             (g₁ : x₁ --> x₂)
             (Hg₁ : is_z_isomorphism g₁)
             (g₂ : x₁' --> x₂')
             (Hg₂ : is_z_isomorphism g₂)
             (y : disp_cat_of_elems x₂)
             (y' : disp_cat_of_elems x₂')
             (q : f₁ · g₂ = g₁ · f₂)
             (r : y' = # F f₂ y)
    : cat_of_elems_iso_lift HC g₂ Hg₂ y'
      =
      #F f₁ (cat_of_elems_iso_lift HC g₁ Hg₁ y).
  Show proof.
    use (cat_of_elems_path_natural f₁ f₂).
    rewrite !idtoiso_isotoid ; cbn.
    - exact q.
    - exact r.

  Definition cat_of_elems
    : category
    := total_category disp_cat_of_elems.

  Definition is_univalent_cat_of_elems
             (HC : is_univalent C)
    : is_univalent cat_of_elems.
  Show proof.
    use is_univalent_total_category.
    - exact HC.
    - exact is_univalent_disp_disp_cat_of_elems.

  Definition is_z_iso_cat_of_elems
             {cx₁ cx₂ : cat_of_elems}
             (f : cx₁ --> cx₂)
             (Hf : is_z_isomorphism (pr1 f))
    : is_z_isomorphism f.
  Show proof.
    use tpair.
    - simple refine (inv_from_z_iso (make_z_iso' _ Hf) ,, _).
      abstract
        (cbn ;
         pose (pr2 f) as p ;
         cbn in p ;
         rewrite <- p ;
         exact (eqtohomot
                  (z_iso_inv_after_z_iso
                     (functor_on_z_iso F (make_z_iso' _ Hf))) (pr2 cx₁))).
    - split.
      + abstract
          (use subtypePath ; [ intro ; apply (F _) | ] ;
           apply (z_iso_inv_after_z_iso (make_z_iso' _ Hf))).
      + abstract
          (use subtypePath ; [ intro ; apply (F _) | ] ;
           apply (z_iso_after_z_iso_inv (make_z_iso' _ Hf))).

  Definition cat_of_elems_forgetful
    : cat_of_elems ⟶ C
    := pr1_category disp_cat_of_elems.

  Definition cat_of_elems_to_pointed_data
    : functor_data cat_of_elems pointed_sets.
  Show proof.
    use make_functor_data.
    - exact (λ cx, F (pr1 cx) ,, pr2 cx).
    - exact (λ cx₁ cx₂ fp, #F (pr1 fp) ,, pr2 fp).

  Definition cat_of_elems_to_pointed_is_functor
    : is_functor cat_of_elems_to_pointed_data.
  Show proof.
    split.
    - intros cx ; cbn in *.
      use subtypePath.
      {
        intro.
        apply (F _).
      }
      cbn.
      use funextsec.
      intro x.
      exact (eqtohomot (functor_id F (pr1 cx)) x).
    - intros cx₁ cx₂ cx₃ fp₁ fp₂ ; cbn in *.
      use subtypePath.
      {
        intro.
        apply (F _).
      }
      cbn.
      use funextsec.
      intro x.
      exact (eqtohomot (functor_comp F _ _) x).

  Definition cat_of_elems_to_pointed
    : cat_of_elems ⟶ pointed_sets.
  Show proof.
    use make_functor.
    - exact cat_of_elems_to_pointed_data.
    - exact cat_of_elems_to_pointed_is_functor.

  Definition cat_of_elems_commute
    : cat_of_elems_to_pointed ∙ set_of_pointed_set
      ⟹
      cat_of_elems_forgetful ∙ F.
  Show proof.
    use make_nat_trans.
    - exact (λ _, identity _).
    - abstract
        (intros cx₁ cx₂ f ; cbn ;
         apply idpath).

  Definition cat_of_elems_commute_z_iso
    : nat_z_iso
        (cat_of_elems_to_pointed ∙ set_of_pointed_set)
        (cat_of_elems_forgetful ∙ F).
  Show proof.
    use make_nat_z_iso.
    - exact cat_of_elems_commute.
    - intro.
      apply identity_is_z_iso.

  Section FunctorToCatOfElems.
    Context {C' : category}
            (G₁ : C' ⟶ pointed_sets)
            (G₂ : C' ⟶ C)
            (γ : nat_z_iso
                   (G₁ ∙ set_of_pointed_set)
                   (G₂ ∙ F)).

    Definition functor_to_cat_of_elems_data
      : functor_data C' cat_of_elems.
    Show proof.
      use make_functor_data.
      - exact (λ c, G₂ c ,, γ c (pr2 (G₁ c))).
      - refine (λ c₁ c₂ f, # G₂ f ,, _).
        abstract
          (cbn ;
           refine (!(eqtohomot (nat_trans_ax γ _ _ f) (pr2 (G₁ c₁))) @ _) ; cbn ;
           apply maponpaths ;
           exact (pr2 (# G₁ f))).

    Definition functor_to_cat_of_elems_is_functor
      : is_functor functor_to_cat_of_elems_data.
    Show proof.
      split.
      - intro x ; cbn.
        use subtypePath.
        {
          intro.
          apply (F _).
        }
        cbn.
        apply functor_id.
      - intros x y z f g ; cbn.
        use subtypePath.
        {
          intro.
          apply (F _).
        }
        cbn.
        apply functor_comp.

    Definition functor_to_cat_of_elems
      : C' ⟶ cat_of_elems.
    Show proof.
      use make_functor.
      - exact functor_to_cat_of_elems_data.
      - exact functor_to_cat_of_elems_is_functor.

    Definition functor_to_cat_of_elems_pointed_nat_trans
      : functor_to_cat_of_elems ∙ cat_of_elems_to_pointed ⟹ G₁.
    Show proof.
      use make_nat_trans.
      - refine (λ x, inv_from_z_iso (nat_z_iso_pointwise_z_iso γ x) ,, _) ; cbn.
        abstract
          (exact (eqtohomot
                    (z_iso_inv_after_z_iso
                       (nat_z_iso_pointwise_z_iso γ x))
                    (pr2 (G₁ x)))).
      - abstract
          (intros c₁ c₂ f ; cbn ;
           use subtypePath ;
             [ intro ;
               apply (pr1 (G₁ c₂))
             | ] ;
           cbn ;
           use funextsec ;
           intro x ;
           exact (eqtohomot (nat_trans_ax (nat_z_iso_to_trans_inv γ) _ _ f) x)).

    Definition functor_to_cat_of_elems_pointed
      : nat_z_iso
          (functor_to_cat_of_elems ∙ cat_of_elems_to_pointed)
          G₁.
    Show proof.
      use make_nat_z_iso.
      - exact functor_to_cat_of_elems_pointed_nat_trans.
      - intro.
        use is_z_iso_pointed_sets.
        apply is_z_iso_inv_from_z_iso.

    Definition functor_to_cat_of_elems_forgetful_nat_trans
      : functor_to_cat_of_elems ∙ cat_of_elems_forgetful ⟹ G₂.
    Show proof.
      use make_nat_trans.
      - exact (λ x, identity _).
      - abstract
          (intros x y f ; cbn ;
           rewrite id_left, id_right ;
           apply idpath).

    Definition functor_to_cat_of_elems_forgetful
      : nat_z_iso
          (functor_to_cat_of_elems ∙ cat_of_elems_forgetful)
          G₂.
    Show proof.
      use make_nat_z_iso.
      - exact functor_to_cat_of_elems_forgetful_nat_trans.
      - intro.
        apply identity_is_z_iso.

    Definition functor_to_cat_of_elems_commute
               (c : C')
      : cat_of_elems_commute (functor_to_cat_of_elems c)
        =
        # set_of_pointed_set (functor_to_cat_of_elems_pointed_nat_trans c) · γ c.
    Show proof.
      use funextsec.
      intro x ; cbn.
      exact (!(eqtohomot (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso γ c)) x)).
  End FunctorToCatOfElems.

  Section NatTransToCatOfElems.
    Context {C' : category}
            {G₁ G₂ : C' ⟶ cat_of_elems}
            (τ₁ : G₁ ∙ cat_of_elems_to_pointed
                  ⟹
                  G₂ ∙ cat_of_elems_to_pointed)
            (τ₂ : G₁ ∙ cat_of_elems_forgetful
                  ⟹
                  G₂ ∙ cat_of_elems_forgetful)
            (p : ∏ (x : C'),
                 # F (τ₂ x) (pr2 (G₁ x))
                 =
                 pr1 (τ₁ x) (pr2 (G₁ x))).

    Definition nat_trans_to_cat_of_elems
      : G₁ ⟹ G₂.
    Show proof.
      use make_nat_trans.
      - simple refine (λ x, τ₂ x ,, _) ; cbn.
        abstract
          (exact (p x @ pr2 (τ₁ x))).
      - abstract
          (intros x y f ; cbn ;
           use subtypePath ; [ intro ; apply (F _) | ] ; cbn ;
           exact (nat_trans_ax τ₂ _ _ f)).
  End NatTransToCatOfElems.
End CategoryOfElements.

Definition univalent_cat_of_elems
           {C : univalent_category}
           (F : C ⟶ SET)
  : univalent_category.
Show proof.
  use make_univalent_category.
  - exact (cat_of_elems F).
  - apply is_univalent_cat_of_elems.
    apply C.