Library UniMath.CategoryTheory.categories.HSET.Limits
Limits in HSET
Contents
- General limits (LimsHSET)
- Alternate definition using cats/limits
- Binary products (BinProductsHSET)
- General indexed products (ProductsHSET)
- Terminal object (TerminalHSET)
- Terminal object from general limits (TerminalHSET_from_Lims)
- Pullbacks (PullbacksHSET)
- Pullbacks from general limits (PullbacksHSET_from_Lims)
- Pullbacks of arrows from unit as inverse images
- Equalizers from general limits (EqualizersHSET_from_Lims)
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.WeakEquivalences.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.pullbacks.
Require Import UniMath.CategoryTheory.limits.graphs.equalizers.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.equalizers.
Require Import UniMath.CategoryTheory.limits.products.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Local Open Scope cat.
Section limits.
Variable g : graph.
Variable D : diagram g HSET.
Definition limset_UU : UU :=
∑ (f : ∏ u : vertex g, pr1hSet (dob D u)),
∏ u v (e : edge u v), dmor D e (f u) = f v.
Definition limset : HSET.
Show proof.
exists limset_UU.
apply (isofhleveltotal2 2);
[ apply impred; intro; apply pr2
| intro f; repeat (apply impred; intro);
apply isasetaprop, setproperty ].
apply (isofhleveltotal2 2);
[ apply impred; intro; apply pr2
| intro f; repeat (apply impred; intro);
apply isasetaprop, setproperty ].
Lemma LimConeHSET : LimCone D.
Show proof.
use make_LimCone.
- apply limset.
- exists (λ u f, pr1 f u).
abstract (intros u v e; simpl; apply funextfun; intro f; simpl; apply (pr2 f)).
- intros X CC.
use tpair.
+ use tpair.
* intro x; exists (λ u, coneOut CC u x).
abstract (intros u v e; apply (toforallpaths _ _ _ (coneOutCommutes CC _ _ e))).
* abstract (intro v; apply idpath).
+ abstract (intros [t p]; apply subtypePath;
[ intro; apply impred; intro; apply isaset_set_fun_space
| apply funextfun; intro; apply subtypePath];
[ intro; repeat (apply impred; intro); apply setproperty
| apply funextsec; intro u; apply (toforallpaths _ _ _ (p u))]).
- apply limset.
- exists (λ u f, pr1 f u).
abstract (intros u v e; simpl; apply funextfun; intro f; simpl; apply (pr2 f)).
- intros X CC.
use tpair.
+ use tpair.
* intro x; exists (λ u, coneOut CC u x).
abstract (intros u v e; apply (toforallpaths _ _ _ (coneOutCommutes CC _ _ e))).
* abstract (intro v; apply idpath).
+ abstract (intros [t p]; apply subtypePath;
[ intro; apply impred; intro; apply isaset_set_fun_space
| apply funextfun; intro; apply subtypePath];
[ intro; repeat (apply impred; intro); apply setproperty
| apply funextsec; intro u; apply (toforallpaths _ _ _ (p u))]).
End limits.
Lemma LimsHSET : Lims HSET.
Show proof.
Lemma LimsHSET_of_shape (g : graph) : Lims_of_shape g HSET.
Show proof.
Require UniMath.CategoryTheory.limits.cats.limits.
Section cats_limits.
Variable J : precategory.
Variable D : functor J HSET.
Definition cats_limset_UU : UU :=
∑ (f : ∏ u, pr1hSet (D u)),
∏ u v (e : J⟦u,v⟧), # D e (f u) = f v.
Definition cats_limset : HSET.
Show proof.
exists cats_limset_UU.
apply (isofhleveltotal2 2);
[ apply impred; intro; apply pr2
| intro f; repeat (apply impred; intro);
apply isasetaprop, setproperty ].
apply (isofhleveltotal2 2);
[ apply impred; intro; apply pr2
| intro f; repeat (apply impred; intro);
apply isasetaprop, setproperty ].
Lemma cats_LimConeHSET : cats.limits.LimCone D.
Show proof.
use make_LimCone.
- apply cats_limset.
- exists (λ u f, pr1 f u).
abstract (intros u v e; apply funextfun; intro f; apply (pr2 f)).
- intros X CC.
use tpair.
+ use tpair.
* intro x; exists (λ u, coneOut CC u x).
abstract (intros u v e; apply (toforallpaths _ _ _ (coneOutCommutes CC _ _ e))).
* abstract (intro v; apply idpath).
+ abstract (intros [t p]; apply subtypePath;
[ intro; apply impred; intro; apply isaset_set_fun_space
| apply funextfun; intro x; apply subtypePath];
[ intro; repeat (apply impred; intro); apply setproperty
| simpl; apply funextsec; intro u; apply (toforallpaths _ _ _ (p u))]).
- apply cats_limset.
- exists (λ u f, pr1 f u).
abstract (intros u v e; apply funextfun; intro f; apply (pr2 f)).
- intros X CC.
use tpair.
+ use tpair.
* intro x; exists (λ u, coneOut CC u x).
abstract (intros u v e; apply (toforallpaths _ _ _ (coneOutCommutes CC _ _ e))).
* abstract (intro v; apply idpath).
+ abstract (intros [t p]; apply subtypePath;
[ intro; apply impred; intro; apply isaset_set_fun_space
| apply funextfun; intro x; apply subtypePath];
[ intro; repeat (apply impred; intro); apply setproperty
| simpl; apply funextsec; intro u; apply (toforallpaths _ _ _ (p u))]).
End cats_limits.
Lemma cats_LimsHSET : cats.limits.Lims HSET.
Show proof.
Lemma cats_LimsHSET_of_shape (g : category) : cats.limits.Lims_of_shape g HSET.
Show proof.
Binary products (BinProductsHSET)
Lemma BinProductsHSET : BinProducts HSET.
Show proof.
intros A B.
use make_BinProduct.
- apply (A × B)%set.
- simpl in *; apply pr1.
- simpl in *; intros x; apply (pr2 x).
- apply make_isBinProduct.
intros C f g; use tpair.
* exists (prodtofuntoprod (f,,g)); abstract (split; apply idpath).
* abstract (intros [t [ht1 ht2]]; apply subtypePath;
[ intros x; apply isapropdirprod; apply has_homsets_HSET
| now apply funextfun; intro x; rewrite <- ht2, <- ht1 ]).
use make_BinProduct.
- apply (A × B)%set.
- simpl in *; apply pr1.
- simpl in *; intros x; apply (pr2 x).
- apply make_isBinProduct.
intros C f g; use tpair.
* exists (prodtofuntoprod (f,,g)); abstract (split; apply idpath).
* abstract (intros [t [ht1 ht2]]; apply subtypePath;
[ intros x; apply isapropdirprod; apply has_homsets_HSET
| now apply funextfun; intro x; rewrite <- ht2, <- ht1 ]).
Require UniMath.CategoryTheory.limits.graphs.binproducts.
Binary products from limits (BinProductsHSET_from_Lims)
General indexed products (ProductsHSET)
Lemma ProductsHSET (I : UU) : Products I HSET.
Show proof.
intros A.
use make_Product.
- exists (∏ i, pr1 (A i)); apply isaset_forall_hSet.
- simpl; intros i f; apply (f i).
- apply make_isProduct; try apply homset_property.
intros C f; simpl in *.
use tpair.
* exists (λ c i, f i c); intro i; apply idpath.
* abstract (intros h; apply subtypePath; simpl;
[ intro; apply impred; intro; apply has_homsets_HSET
| destruct h as [t ht]; simpl; apply funextfun; intro x;
apply funextsec; intro i; rewrite <- ht; apply idpath ]).
use make_Product.
- exists (∏ i, pr1 (A i)); apply isaset_forall_hSet.
- simpl; intros i f; apply (f i).
- apply make_isProduct; try apply homset_property.
intros C f; simpl in *.
use tpair.
* exists (λ c i, f i c); intro i; apply idpath.
* abstract (intros h; apply subtypePath; simpl;
[ intro; apply impred; intro; apply has_homsets_HSET
| destruct h as [t ht]; simpl; apply funextfun; intro x;
apply funextsec; intro i; rewrite <- ht; apply idpath ]).
Terminal object TerminalHSET
Lemma TerminalHSET : Terminal HSET.
Show proof.
apply (make_Terminal unitHSET).
apply make_isTerminal; intro a.
exists (λ _, tt).
abstract (simpl; intro f; apply funextfun; intro x; case (f x); apply idpath).
apply make_isTerminal; intro a.
exists (λ _, tt).
abstract (simpl; intro f; apply funextfun; intro x; case (f x); apply idpath).
Terminal object from general limits TerminalHSET_from_Lims
Require UniMath.CategoryTheory.limits.graphs.terminal.
Lemma TerminalHSET_from_Lims : graphs.terminal.Terminal HSET.
Show proof.
Pullbacks PullbacksHSET
Definition PullbackHSET_ob {A B C : HSET} (f : HSET⟦B,A⟧) (g : HSET⟦C,A⟧) : HSET.
Show proof.
exists (∑ (xy : setdirprod B C), f (pr1 xy) = g (pr2 xy)).
abstract (apply isaset_total2; [ apply isasetdirprod; apply setproperty
| intros xy; apply isasetaprop, setproperty ]).
abstract (apply isaset_total2; [ apply isasetdirprod; apply setproperty
| intros xy; apply isasetaprop, setproperty ]).
Lemma PullbacksHSET : Pullbacks HSET.
Show proof.
intros A B C f g.
use make_Pullback.
+ apply (PullbackHSET_ob f g).
+ intros xy; apply (pr1 (pr1 xy)).
+ intros xy; apply (pr2 (pr1 xy)).
+ abstract (apply funextsec; intros [[x y] Hxy]; apply Hxy).
+ use make_isPullback.
intros X f1 f2 Hf12; cbn.
use unique_exists.
- intros x.
exists (f1 x,,f2 x); abstract (apply (toforallpaths _ _ _ Hf12)).
- abstract (now split).
- abstract (now intros h; apply isapropdirprod; apply has_homsets_HSET).
- abstract (intros h [H1 H2]; apply funextsec; intro x;
apply subtypePath; [intros H; apply setproperty|]; simpl;
now rewrite <- (toforallpaths _ _ _ H1 x), <- (toforallpaths _ _ _ H2 x)).
use make_Pullback.
+ apply (PullbackHSET_ob f g).
+ intros xy; apply (pr1 (pr1 xy)).
+ intros xy; apply (pr2 (pr1 xy)).
+ abstract (apply funextsec; intros [[x y] Hxy]; apply Hxy).
+ use make_isPullback.
intros X f1 f2 Hf12; cbn.
use unique_exists.
- intros x.
exists (f1 x,,f2 x); abstract (apply (toforallpaths _ _ _ Hf12)).
- abstract (now split).
- abstract (now intros h; apply isapropdirprod; apply has_homsets_HSET).
- abstract (intros h [H1 H2]; apply funextsec; intro x;
apply subtypePath; [intros H; apply setproperty|]; simpl;
now rewrite <- (toforallpaths _ _ _ H1 x), <- (toforallpaths _ _ _ H2 x)).
Pullbacks from general limits PullbacksHSET_from_Lims
Require UniMath.CategoryTheory.limits.graphs.pullbacks.
Lemma PullbacksHSET_from_Lims : graphs.pullbacks.Pullbacks HSET.
Show proof.
Pullbacks of arrows from unit as inverse images
Z --- ! --> unit | | | | y V V X --- f --> Ymakes Z (isomorphic to) the inverse image of a point y : Y under f.
Lemma weqfunfromunit_HSET (X : hSet) : HSET⟦TerminalHSET, X⟧ ≃ X.
Show proof.
Local Lemma tosecoverunit_compute {X : UU} {x : X} :
∏ t, tosecoverunit (λ _ : unit, X) x t = x.
Show proof.
Lemma hfiber_is_pullback {X Y : hSet} (f : HSET⟦X, Y⟧)
(y : Y) (y' := invweq (weqfunfromunit_HSET _) y) :
∑ H, @isPullback _ _ _ _ _ f y' (hfiberpr1 f y : HSET⟦hfiber_hSet f y , X⟧)
(TerminalArrow TerminalHSET _) H.
Show proof.
Show proof.
Local Lemma tosecoverunit_compute {X : UU} {x : X} :
∏ t, tosecoverunit (λ _ : unit, X) x t = x.
Show proof.
abstract (induction t; reflexivity).
Lemma hfiber_is_pullback {X Y : hSet} (f : HSET⟦X, Y⟧)
(y : Y) (y' := invweq (weqfunfromunit_HSET _) y) :
∑ H, @isPullback _ _ _ _ _ f y' (hfiberpr1 f y : HSET⟦hfiber_hSet f y , X⟧)
(TerminalArrow TerminalHSET _) H.
Show proof.
First, simplify what we have to prove.
Part of the condition is trivial.
use iscontrweqb.
+ exact (∑ hk : HSET ⟦ pb, hfiber_hSet f y ⟧,
hk · hfiberpr1 f y = pbpr1).
+ apply weqfibtototal; intro.
apply invweq.
apply dirprod_with_contr_r.
use make_iscontr.
* apply isapropifcontr.
apply TerminalHSET.
* intro; apply proofirrelevance; apply homset_property.
+ unfold hfiber_hSet, hfiber; cbn.
use make_iscontr.
* use tpair.
intros pb0.
use tpair.
-- exact (pbpr1 pb0).
-- cbn.
apply toforallpaths in pbH.
specialize (pbH pb0); cbn in pbH.
refine (pbH @ _).
apply tosecoverunit_compute.
-- apply idpath.
* intros t.
apply subtypePath.
-- intro; apply has_homsets_HSET.
-- cbn.
apply funextfun; intro; cbn.
apply subtypePath.
++ intro; apply setproperty.
++ apply (toforallpaths _ _ _ (pr2 t)).
+ exact (∑ hk : HSET ⟦ pb, hfiber_hSet f y ⟧,
hk · hfiberpr1 f y = pbpr1).
+ apply weqfibtototal; intro.
apply invweq.
apply dirprod_with_contr_r.
use make_iscontr.
* apply isapropifcontr.
apply TerminalHSET.
* intro; apply proofirrelevance; apply homset_property.
+ unfold hfiber_hSet, hfiber; cbn.
use make_iscontr.
* use tpair.
intros pb0.
use tpair.
-- exact (pbpr1 pb0).
-- cbn.
apply toforallpaths in pbH.
specialize (pbH pb0); cbn in pbH.
refine (pbH @ _).
apply tosecoverunit_compute.
-- apply idpath.
* intros t.
apply subtypePath.
-- intro; apply has_homsets_HSET.
-- cbn.
apply funextfun; intro; cbn.
apply subtypePath.
++ intro; apply setproperty.
++ apply (toforallpaths _ _ _ (pr2 t)).
Equalizers from general limits EqualizersHSET_from_Lims
Require UniMath.CategoryTheory.limits.graphs.equalizers.
Lemma EqualizersHSET_from_Lims : graphs.equalizers.Equalizers HSET.
Show proof.
HSET Pullbacks and Equalizers from limits to direct definition
Section HSET_Structures.
Definition HSET_Pullbacks : @limits.pullbacks.Pullbacks HSET :=
equiv_Pullbacks_2 HSET PullbacksHSET_from_Lims.
Definition HSET_Equalizers: @limits.equalizers.Equalizers HSET :=
equiv_Equalizers2 HSET EqualizersHSET_from_Lims.
End HSET_Structures.
Definition HSET_Pullbacks : @limits.pullbacks.Pullbacks HSET :=
equiv_Pullbacks_2 HSET PullbacksHSET_from_Lims.
Definition HSET_Equalizers: @limits.equalizers.Equalizers HSET :=
equiv_Equalizers2 HSET EqualizersHSET_from_Lims.
End HSET_Structures.
Concrete construction of equalizers of sets
Definition Equalizers_in_HSET
: Equalizers HSET.
Show proof.
: Equalizers HSET.
Show proof.
intros X Y f g ; cbn in *.
simple refine ((_ ,, _) ,, _ ,, _).
- exact (∑ (x : X), hProp_to_hSet (eqset (f x) (g x)))%set.
- exact (λ x, pr1 x).
- abstract
(use funextsec ;
intro z ; cbn ;
exact (pr2 z)).
- intros W h p.
use iscontraprop1.
+ abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use funextsec ;
intro w ;
use subtypePath ; [ intro ; apply setproperty | ] ;
exact (eqtohomot (pr2 φ₁ @ !(pr2 φ₂)) w)).
+ simple refine (_ ,, _).
* exact (λ w, h w ,, eqtohomot p w).
* apply idpath.
simple refine ((_ ,, _) ,, _ ,, _).
- exact (∑ (x : X), hProp_to_hSet (eqset (f x) (g x)))%set.
- exact (λ x, pr1 x).
- abstract
(use funextsec ;
intro z ; cbn ;
exact (pr2 z)).
- intros W h p.
use iscontraprop1.
+ abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use funextsec ;
intro w ;
use subtypePath ; [ intro ; apply setproperty | ] ;
exact (eqtohomot (pr2 φ₁ @ !(pr2 φ₂)) w)).
+ simple refine (_ ,, _).
* exact (λ w, h w ,, eqtohomot p w).
* apply idpath.