Library UniMath.CategoryTheory.Categories.HSET.Slice
Slices of HSET
Contents
- Locally cartesian closed structure
- Terminal object (Terminal_HSET_slice)
- Binary products (BinProducts_HSET_slice)
- General indexed products (Products_HSET_slice)
- Exponentials (Exponentials_HSET_slice)
- Colimits
- Binary coproducts (BinCoproducts_HSET_slice)
- The forgetful functor HSET/X --> HSET is a left adjoint (is_left_adjoint_slicecat_to_cat)
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.
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.
End products_set_slice.
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).
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)
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.
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.
+ 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)) _ _).
+ 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.
+ 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.
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.
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.
End set_slicecat.