Library UniMath.CategoryTheory.categories.HSET.Slice

Slices of HSET

Contents

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

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.AxiomOfChoice.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.covyoneda.
Require Import UniMath.CategoryTheory.slicecat.

Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.products.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.bincoproducts.

Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.

Local Open Scope cat.

Locally cartesian closed structure


Section set_slicecat.

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

Terminal object (Terminal_HSET_slice)


Lemma Terminal_HSET_slice X : Terminal (SET / X).
Show proof.
  now apply Terminal_slice_precat.

Binary products (BinProducts_HSET_slice)


Lemma BinProducts_HSET_slice X : BinProducts (HSET / X).
Show proof.
  now apply BinProducts_slice_precat, PullbacksHSET.

General indexed products (Products_HSET_slice)


Section products_set_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, HSET⟦hfiber_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)


Lemma BinCoproducts_HSET_slice X : BinCoproducts (HSET / X).
Show proof.
  now apply BinCoproducts_slice_precat, BinCoproductsHSET.

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


Lemma is_left_adjoint_slicecat_to_cat_HSET (X : HSET) :
  is_left_adjoint (slicecat_to_cat HSET X).
Show proof.
apply is_left_adjoint_slicecat_to_cat, BinProductsHSET.

End set_slicecat.