Library UniMath.CategoryTheory.ElementsOp

****************************************************************************
The category of elements of a presheaf "F : C^op ⟶ HSET"
Contents:
Originally written by: Matthew Weaver (based on Elements.v by Dan Grayson) Ported to CT by: Anders Mörtberg

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.FunctorCategory.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Presheaf.

Local Open Scope cat.

Section cat_of_elems_def.

Context {C : category} (X : C^op ⟶ HSET).

Definition cat_of_elems_ob_mor : precategory_ob_mor.
Show proof.
exists (∑ (c : C), X c : hSet).
intros a b.
apply (∑ (f : C⟦pr1 a,pr1 b⟧), (pr2 a) = # X f (pr2 b)).

Definition cat_of_elems_data : precategory_data.
Show proof.
exists cat_of_elems_ob_mor.
split.
+ intros a.
  exists (identity (pr1 a)).
  abstract (exact (eqtohomot (!(functor_id X) (pr1 a)) (pr2 a))).
+ intros a b c f g.
  exists (pr1 f · pr1 g).
  abstract (exact ((pr2 f) @ maponpaths (#X (pr1 f)) (pr2 g)
                    @ (eqtohomot (!(functor_comp X) (pr1 g) (pr1 f)) (pr2 c)))).

Definition get_mor {x y : cat_of_elems_data} (f : _⟦x,y⟧) := pr1 f.

Lemma cat_of_elems_mor_eq (x y : cat_of_elems_data) (f g : _⟦x,y⟧) :
  get_mor f = get_mor g → f = g.
Show proof.
intros p.
apply subtypePath.
- intro r; apply setproperty.
- exact p.

Lemma is_precategory_cat_of_elems_data : is_precategory cat_of_elems_data.
Show proof.
split; [split|split]; intros; apply cat_of_elems_mor_eq.
+ apply id_left.
+ apply id_right.
+ apply assoc.
+ apply assoc'.

Definition precat_of_elems : precategory :=
  (cat_of_elems_data,,is_precategory_cat_of_elems_data).

End cat_of_elems_def.

Arguments get_mor {_ _ _ _} _.

Lemma has_homsets_cat_of_elems {C : category} (X : C^op ⟶ HSET)
  : has_homsets (precat_of_elems X).
Show proof.
intros a b.
apply isaset_total2.
- apply C.
- intro f. apply isasetaprop, setproperty.

Definition cat_of_elems {C : category} (X : C^op ⟶ HSET) : category
  := make_category _ (has_homsets_cat_of_elems X).

Type as \int in Agda mode
Notation "∫ X" := (cat_of_elems X) (at level 3) : cat.

Section cat_of_elems_theory.

Context {C : category} {X Y : C^op ⟶ HSET}.

Definition get_ob (x : ∫ X) : C := pr1 x.
Definition get_el (x : ∫ X) : X (get_ob x) : hSet := pr2 x.
Definition get_eqn {x y : ∫ X} (f : (∫ X)⟦x,y⟧) :
  get_el x = # X (get_mor f) (get_el y) := pr2 f.

Definition make_ob (c : C) (x : X c : hSet) : ∫ X := (c,,x).
Definition make_mor (r s : ∫ X) (f : C⟦get_ob r,get_ob s⟧)
  (i : get_el r = # X f (get_el s)) : (∫ X)⟦r,s⟧ := (f,,i).

Definition mor_to_el_mor {I J : C} (f : J --> I) (ρ : pr1 X I : hSet) :
  ∫ X ⟦ make_ob J (# (pr1 X) f ρ), make_ob I ρ ⟧ :=
  make_mor (J,,# (pr1 X) f ρ) (I,,ρ) f (idpath (# (pr1 X) f ρ)).

Lemma base_paths_maponpaths_make_ob {I : C} x y (e : x = y) :
  base_paths _ _ (maponpaths (make_ob I) e) = idpath I.
Show proof.
now induction e.

Lemma transportf_make_ob_eq {I J} (f : C⟦J,I⟧) {a b} (e : make_ob J a = make_ob J b) :
  transportf (λ x : ∫ X, C⟦pr1 x,I⟧) e f = transportf (λ x, C⟦x,I⟧) (base_paths _ _ e) f.
Show proof.
now induction e.

Lemma transportf_make_ob {A : PreShv (∫ X)} {I : C} {x y} (e : x = y)
  (u : pr1 (pr1 A (make_ob I x))) :
    transportf (λ x, pr1 (pr1 A (make_ob I x))) e u =
    transportf (λ x, pr1 (pr1 A x)) (maponpaths (make_ob I) e) u.
Show proof.
now induction e.

Lemma make_ob_identity_eq {I : C} (ρ : pr1 (pr1 X I)) :
  make_ob I (# (pr1 X) (identity I) ρ) = make_ob I ρ.
Show proof.
exact (maponpaths (make_ob I) (eqtohomot (functor_id X I) ρ)).

Lemma mor_to_el_mor_id {I : C} (ρ : pr1 (pr1 X I)) :
  mor_to_el_mor (identity I) ρ =
  transportb (λ Z, ∫ X⟦Z, make_ob I ρ⟧) (make_ob_identity_eq ρ) (identity _).
Show proof.
apply (@transportf_transpose_right _ (λ Z : ∫ X, ∫ X ⟦Z,_⟧)), cat_of_elems_mor_eq; simpl.
unfold transportb; rewrite pathsinv0inv0.
rewrite transportf_total2; simpl; rewrite transportf_make_ob_eq.
now unfold make_ob_identity_eq; rewrite base_paths_maponpaths_make_ob, idpath_transportf.

Lemma make_ob_comp_eq {I J K} (ρ : pr1 (pr1 X I)) (f : C^op⟦I,J⟧) (g : C^op⟦J,K⟧) :
  make_ob _ (# (pr1 X) (f · g) ρ) = make_ob _ (# (pr1 X) g (# (pr1 X) f ρ)).
Show proof.
exact (maponpaths (make_ob K) (eqtohomot (functor_comp X f g) ρ)).

Lemma mor_to_el_mor_comp {I J K} (ρ : pr1 (pr1 X I)) (f : C^op⟦I,J⟧) (g : C^op⟦J,K⟧) :
  mor_to_el_mor (f · g) ρ =
  transportb (λ Z, ∫ X⟦Z,_⟧) (make_ob_comp_eq ρ f g)
             (mor_to_el_mor g (# (pr1 X) f ρ) · mor_to_el_mor f ρ).
Show proof.
apply (@transportf_transpose_right _ (λ Z : ∫ X, ∫ X ⟦Z,_⟧)), cat_of_elems_mor_eq; simpl.
unfold transportb; rewrite pathsinv0inv0.
rewrite transportf_total2; simpl; rewrite transportf_make_ob_eq.
now unfold make_ob_comp_eq; rewrite base_paths_maponpaths_make_ob, idpath_transportf.

Functoriality of the construction of the category of elements
Definition cat_of_elems_on_nat_trans_data (α : X ⟹ Y) :
  functor_data (∫ X) (∫ Y).
Show proof.
exists (λ a, (get_ob a,, α (get_ob a) (get_el a))).
intros b c f.
exists (get_mor f).
abstract (exact (maponpaths (α (get_ob b)) (get_eqn f)
                @ eqtohomot (pr2 α (get_ob c) (get_ob b) (get_mor f)) (get_el c))).

Lemma cat_of_elems_on_nat_trans_is_functor (α : X ⟹ Y) :
  is_functor (cat_of_elems_on_nat_trans_data α).
Show proof.
split.
- now intros a; apply cat_of_elems_mor_eq.
- now intros a b c f g; apply cat_of_elems_mor_eq.

Definition cat_of_elems_on_nat_trans (α : X ⟹ Y) : ∫ X ⟶ ∫ Y :=
  (cat_of_elems_on_nat_trans_data α,, cat_of_elems_on_nat_trans_is_functor α).


The forgetful functor from the category of elements to C
Definition cat_of_elems_forgetful : ∫ X ⟶ C.
Show proof.
use make_functor.
- exists pr1.
  intros a b; apply pr1.
- now split.

Lemma reflects_isos_cat_of_elems_forgetful : reflects_isos cat_of_elems_forgetful.
Show proof.
intros [c x] [d y] f Hf.
destruct f as [f i]; destruct Hf as [f' j].
assert (i' : y = #X f' x).
{ intermediate_path (#X (identity d) y).
  - exact (eqtohomot (!functor_id X d) y).
  - intermediate_path (#X (f ∘ f') y).
    + exact (eqtohomot (!maponpaths #X (pr2 j)) y).
    + intermediate_path (#X f' (#X f y)).
      * exact (eqtohomot ((functor_comp X) f f') y).
      * exact (maponpaths (#X f') (!i)).
}
exists (f',,i').
split; apply cat_of_elems_mor_eq; [ exact (pr1 j) | exact (pr2 j) ].

End cat_of_elems_theory.