Library UniMath.CategoryTheory.categories.HSET.Limits

Limits in HSET

Contents

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

General limits


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 ].

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))]).

End limits.

Lemma LimsHSET : Lims HSET.
Show proof.
now intros g d; apply LimConeHSET.

Lemma LimsHSET_of_shape (g : graph) : Lims_of_shape g HSET.
Show proof.
now intros d; apply LimConeHSET.

Alternate definition using cats/limits


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 : Ju,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 ].

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))]).

End cats_limits.

Lemma cats_LimsHSET : cats.limits.Lims HSET.
Show proof.
now intros g d; apply cats_LimConeHSET.

Lemma cats_LimsHSET_of_shape (g : category) : cats.limits.Lims_of_shape g HSET.
Show proof.
now intros d; apply cats_LimConeHSET.

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 ]).

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 ]).

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).

Terminal object from general limits TerminalHSET_from_Lims

Pullbacks PullbacksHSET


Definition PullbackHSET_ob {A B C : HSET} (f : HSETB,A) (g : HSETC,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 ]).

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)).

Pullbacks from general limits PullbacksHSET_from_Lims

Pullbacks of arrows from unit as inverse images

The set hfiber f y is a pullback of a diagram involving an arrow from TerminalHSET, i.e. unit.
In particular, A pullback diagram of shape
      Z --- ! --> unit
      |            |
      |            | y
      V            V
      X --- f -->  Y
makes Z (isomorphic to) the inverse image of a point y : Y under f.
A translation of weqfunfromunit into the language of category theory, to make the statement of the next lemmas more concise.
Lemma weqfunfromunit_HSET (X : hSet) : HSETTerminalHSET, X X.
Show proof.
  apply weqfunfromunit.

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 : HSETX, Y)
      (y : Y) (y' := invweq (weqfunfromunit_HSET _) y) :
   H, @isPullback _ _ _ _ _ f y' (hfiberpr1 f y : HSEThfiber_hSet f y , X)
                       (TerminalArrow TerminalHSET _) H.
Show proof.
  use tpair.
  - apply funextfun; intro.
    apply hfiberpr2.
  - intros pb pbpr1 pbpr2 pbH.

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)).

Equalizers from general limits EqualizersHSET_from_Lims

HSET Pullbacks and Equalizers from limits to direct definition
Concrete construction of equalizers of sets
Definition Equalizers_in_HSET
  : 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.