# 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.
Proof.
limset_UU.
apply (isofhleveltotal2 2);
[ apply impred; intro; apply pr2
| intro f; repeat (apply impred; intro);
apply isasetaprop, setproperty ].
Defined.

Lemma LimConeHSET : LimCone D.
Proof.
use make_LimCone.
- apply limset.
- (λ 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; (λ 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))]).
Defined.

End limits.

Lemma LimsHSET : Lims HSET.
Proof.
now intros g d; apply LimConeHSET.
Defined.

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

### 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.
Proof.
cats_limset_UU.
apply (isofhleveltotal2 2);
[ apply impred; intro; apply pr2
| intro f; repeat (apply impred; intro);
apply isasetaprop, setproperty ].
Defined.

Lemma cats_LimConeHSET : cats.limits.LimCone D.
Proof.
use make_LimCone.
- apply cats_limset.
- (λ 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; (λ 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))]).
Defined.

End cats_limits.

Lemma cats_LimsHSET : cats.limits.Lims HSET.
Proof.
now intros g d; apply cats_LimConeHSET.
Defined.

Lemma cats_LimsHSET_of_shape (g : precategory) : cats.limits.Lims_of_shape g HSET.
Proof.
now intros d; apply cats_LimConeHSET.
Defined.

## Binary products (BinProductsHSET)

Lemma BinProductsHSET : BinProducts HSET.
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 _ has_homsets_HSET).
intros C f g; use tpair.
× (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 ]).
Defined.

Require UniMath.CategoryTheory.limits.graphs.binproducts.

## General indexed products (ProductsHSET)

Lemma ProductsHSET (I : UU) : Products I HSET.
Proof.
intros A.
use make_Product.
- ( i, pr1 (A i)); apply isaset_forall_hSet.
- simpl; intros i f; apply (f i).
- apply (make_isProduct _ _ has_homsets_HSET).
intros C f; simpl in ×.
use tpair.
× (λ 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 ]).
Defined.

## Terminal object TerminalHSET

Lemma TerminalHSET : Terminal HSET.
Proof.
apply (make_Terminal unitHSET).
apply make_isTerminal; intro a.
(λ _, tt).
abstract (simpl; intro f; apply funextfun; intro x; case (f x); apply idpath).
Defined.

## Pullbacks PullbacksHSET

Definition PullbackHSET_ob {A B C : HSET} (f : HSETB,A) (g : HSETC,A) : HSET.
Proof.
( (xy : setdirprod B C), f (pr1 xy) = g (pr2 xy)).
abstract (apply isaset_total2; [ apply isasetdirprod; apply setproperty
| intros xy; apply isasetaprop, setproperty ]).
Defined.

Lemma PullbacksHSET : Pullbacks HSET.
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.
(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)).
Defined.

### 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.
Proof.
apply weqfunfromunit.
Defined.

The hfiber of a function between sets is also a set.
Definition hfiber_hSet {X Y : hSet} (f : HSETX, Y) (y : Y) : hSet.
Proof.
use make_hSet.
- exact (hfiber f y).
- apply isaset_hfiber; apply setproperty.
Defined.

Local Lemma tosecoverunit_compute {X : UU} {x : X} :
t, tosecoverunit (λ _ : unit, X) x t = x.
Proof.
abstract (induction t; reflexivity).
Qed.

Local Definition hfiber_hSet_pr1 {X Y : hSet} (f : HSETX, Y) (y : Y) :
HSEThfiber_hSet f y, X := hfiberpr1 f y.

Lemma hfiber_is_pullback {X Y : hSet} (f : HSETX, Y)
(y : Y) (y' := invweq (weqfunfromunit_HSET _) y) :
H, isPullback f y' (hfiber_hSet_pr1 f y)
(TerminalArrow TerminalHSET _) H.
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 · hfiber_hSet_pr1 f y = pbpr1).
+ apply weqfibtototal; intro.
apply invweq.
apply dirprod_with_contr_r.
use make_iscontr.
× apply proofirrelevance.
apply hlevelntosn.
apply (pr2 TerminalHSET).
TODO: should be an accessor
× intro; apply proofirrelevance; apply setproperty.
+ 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 funextfun; intro; reflexivity.
× intros t.
apply subtypePath.
-- intro; apply has_homsets_HSET.
-- cbn.
apply funextfun; intro; cbn.
apply subtypePath.
++ intro; apply setproperty.
++ apply (toforallpaths _ _ _ (pr2 t)).
Defined.

## Equalizers from general limits EqualizersHSET_from_Lims

HSET Pullbacks and Equalizers from limits to direct definition