Library UniMath.CategoryTheory.Categories.HSET.Slice

Slices of HSET

Contents

Written by: Benedikt Ahrens, Anders Mörtberg
October 2015 - January 2016

Locally cartesian closed structure


Section set_slicecat.

Local Notation "HSET / X" := (slice_cat HSET X) (only parsing).

Terminal object (Terminal_HSET_slice)

Binary products (BinProducts_HSET_slice)

General indexed products (Products_HSET_slice)

Products in Set/X
Lemma Products_HSET_slice I X : Products I (HSET / X).
Show proof.
intros F.
use make_Product.
+ use tpair.
  - exists ( x : pr1 X, i : I, hfiber_hSet (pr2 (F i)) x).
    abstract (apply isaset_total2; [apply setproperty|];
              now intros x; apply impred_isaset; intro i; apply setproperty).
  - cbn. apply pr1.
+ intros i.
  use tpair.
  - intros H; apply (pr1 (pr2 H i)).
  - abstract (now apply funextsec; intros H; apply (!pr2 (pr2 H i))).
+ intros f H.
  use unique_exists.
  - use tpair; simpl.
    * intros x.
      exists (pr2 f x).
      intros i.
      exists (pr1 (H i) x).
      abstract (exact (!toforallpaths _ _ _ (pr2 (H i)) x)).
    * abstract (now apply funextsec).
  - abstract (now intros i; apply eq_mor_slicecat, funextsec).
  - abstract (now intros g; apply impred_isaprop; intro i; apply has_homsets_slice_precat).
  - abstract(simpl; intros [y1 y2] Hy; apply eq_mor_slicecat, funextsec; intro x;
    use total2_paths_f; [apply (toforallpaths _ _ _ (!y2) x)|];
    apply funextsec; intro i; apply subtypePath; [intros w; apply setproperty|];
    destruct f as [f Hf];
    unfold hfiber;
    rewrite transportf_sec_constant, transportf_total2;
    simpl; rewrite transportf_const;
    now rewrite <- Hy).

End products_set_slice.

Exponentials (Exponentials_HSET_slice)

Direct proof that HSET/X has exponentials using explicit formula in example 2.2 of:
https://ncatlab.org/nlab/show/locally+cartesian+closed+categoryin_category_theory

Definition hfiber_fun (X : HSET) (f : HSET / X) : HSET / X HSET / X.
Show proof.
intros g.
  use tpair.
  - exists ( x, HSEThfiber_hSet (pr2 f) x,hfiber_hSet (pr2 g) x).
    abstract (apply isaset_total2; [ apply setproperty | intros x; apply has_homsets_HSET ]).
  - cbn. now apply pr1.

Definition hfiber_functor (X : HSET) (f : HSET / X) :
  functor (HSET / X) (HSET / X).
Show proof.
  use make_functor.
  + use tpair.
    * apply (hfiber_fun _ f).
    * cbn. intros a b g.
      { use tpair; simpl.
      - intros h.
        exists (pr1 h).
        intros fx.
        use tpair.
        * exact (pr1 g (pr1 (pr2 h fx))).
        * abstract (etrans; [ apply (!toforallpaths _ _ _ (pr2 g) (pr1 (pr2 h fx)))|];
                    apply (pr2 (pr2 h fx))).
      - abstract (now apply funextsec).
      }
  + split.
    - intros x; apply (eq_mor_slicecat HSET); simpl.
      apply funextsec; intros [y hy].
      use total2_paths_f; [ apply idpath |].
      apply funextsec; intros w; apply subtypePath; [|apply idpath].
      now intros XX; apply setproperty.
    - intros x y z g h; apply (eq_mor_slicecat HSET); simpl.
      apply funextsec; intros [w hw].
      use total2_paths_f; [ apply idpath |].
      apply funextsec; intros w'.
      apply subtypePath; [|apply idpath].
      now intros XX; apply setproperty.

Local Definition eta X (f : HSET / X) :
  nat_trans (functor_identity (HSET / X))
            (functor_composite (constprod_functor1 (BinProducts_HSET_slice X) f) (hfiber_functor X f)).
Show proof.
  use make_nat_trans.
  + intros g; simpl.
    use tpair.
    * intros y; simpl.
      exists (pr2 g y); intros fgy.
      exists ((pr1 fgy,,y),,(pr2 fgy)).
      abstract (now apply (pr2 fgy)).
    * abstract (now apply funextsec).
  + intros [g Hg] [h Hh] [w Hw].
    apply (eq_mor_slicecat HSET), funextsec; intro x1.
    apply (two_arg_paths_f (!toforallpaths _ _ _ Hw x1)), funextsec; intro y.
    repeat (apply subtypePath; [intros x; apply setproperty|]); cbn in *.
    now induction (! toforallpaths _ _ (λ x : g, Hh (w x)) _ _).

Local Definition eps X (f : HSET / X) :
  nat_trans (functor_composite (hfiber_functor X f) (constprod_functor1 (BinProducts_HSET_slice X) f))
            (functor_identity (HSET / X)).
Show proof.
  use make_nat_trans.
  + intros g; simpl.
    use tpair.
    * intros H; apply (pr1 ((pr2 (pr2 (pr1 H))) (pr1 (pr1 H),,pr2 H))).
    * abstract (cbn; apply funextsec; intros [[x1 [x2 x3]] x4]; simpl in *;
                now rewrite (pr2 (x3 (x1,,x4))), x4).
  + intros g h w; simpl.
    apply (eq_mor_slicecat HSET), funextsec; intro x1; cbn.
    now repeat apply maponpaths; apply setproperty.

Lemma Exponentials_HSET_slice (X : HSET) : Exponentials (BinProducts_HSET_slice X).
Show proof.
  intros f.
  exists (hfiber_functor _ f).
  use make_are_adjoints.
  - apply eta.
  - apply eps.
  - split.
    + intros x; apply eq_mor_slicecat, funextsec; intro x1.
      now apply subtypePath; [intro y; apply setproperty|]; reflexivity.
    + intros x; apply eq_mor_slicecat, funextsec; intro x1; simpl.
      use total2_paths_f; [apply idpath|]; cbn.
      apply funextsec; intro y.
      use subtypePath.
      * intro z; apply setproperty.
      * simpl.
        apply maponpaths.
        apply maponpaths.
        reflexivity.

Colimits

Binary coproducts (BinCoproducts_HSET_slice)

The forgetful functor HSET/X --> HSET is a left adjoint