Library UniMath.CategoryTheory.categories.HSET.Colimits

Colimits in HSET

Minimal equivalence relations
General colimits ColimsHSET
Binary coproducs BinCoproductsHSET
General indexed coproducs CoproductsHSET
- Binary coproducts from colimits BinCoproductsHSET_from_Colims
Pushouts from colimits PushoutsHSET_from_Colims
Initial object InitialHSET
- Initial object from colimits InitialHSET_from_Colims
Every set is the colimit of its finite subsets is_colimit_finite_subsets_cocone

Written by: Benedikt Ahrens, Anders Mörtberg

October 2015 - January 2016

General colimits ColimsHSET

Section colimits.

Variable g : graph.
Variable D : diagram g HSET.

Local Definition cobase : UU := ∑ j : vertex g , pr1hSet (dob D j).

Local Definition rel0 : hrel cobase := λ (ia jb : cobase ),
∥(∑ f : edge (pr1 ia) (pr1 jb), dmor D f (pr2 ia) = pr2 jb )∥.

Local Definition rel : hrel cobase := eqrel_from_hrel rel0.

Lemma iseqrel_rel : iseqrel rel.
Show proof.

now apply iseqrel_eqrel_from_hrel.

Local Definition eqr : eqrel cobase := make_eqrel _ iseqrel_rel.

Definition colimHSET : HSET :=
make_hSet (setquot eqr) (isasetsetquot _).

Local Definition injections j : HSET ⟦dob D j , colimHSET ⟧.
Show proof.

intros Fj; apply (setquotpr _).
exact (j,,Fj).

Section from_colim.

Variables (c : HSET) (cc : cocone D c).

Local Definition from_cobase : cobase -> pr1hSet c.
Show proof.

now intro iA; apply (coconeIn cc (pr1 iA) (pr2 iA)).

Local Definition from_cobase_rel : hrel cobase.
Show proof.

intros x x'; exists (from_cobase x = from_cobase x').
now apply setproperty.

Local Definition from_cobase_eqrel : eqrel cobase.
Show proof.

  exists from_cobase_rel.
  abstract (
  repeat split;
  [ intros x y z H1 H2 ;
    exact (pathscomp0 H1 H2)
  |
    intros x y H;
    exact (pathsinv0 H)
  ]).

Lemma rel0_impl a b (Hab : rel0 a b) : from_cobase_eqrel a b.
Show proof.

  use Hab. clear Hab.
  intro H; simpl.
  destruct H as [f Hf].
  generalize (toforallpaths _ _ _ (coconeInCommutes cc (pr1 a) (pr1 b) f) (pr2 a)).
  unfold compose, from_cobase; simpl; intro H.
  rewrite <- H.
  rewrite <- Hf.
  apply idpath.

Lemma rel_impl a b (Hab : rel a b) : from_cobase_eqrel a b.
Show proof.

now apply (@minimal_eqrel_from_hrel _ rel0); [apply rel0_impl|].

Lemma iscomprel_from_base : iscomprelfun rel from_cobase.
Show proof.

now intros a b; apply rel_impl.

Definition from_colimHSET : HSET ⟦colimHSET , c ⟧.
Show proof.

now simpl; apply (setquotuniv _ _ from_cobase iscomprel_from_base).

End from_colim.

Definition colimCoconeHSET : cocone D colimHSET.
Show proof.

  use make_cocone.
  - now apply injections.
  - abstract (intros u v e;
              apply funextfun; intros Fi; simpl;
              unfold compose, injections; simpl;
              apply (weqpathsinsetquot eqr), (eqrelsymm eqr), eqrel_impl, hinhpr; simpl;
              now exists e).

Definition ColimHSETArrow (c : HSET) (cc : cocone D c) :
∑ x : HSET ⟦ colimHSET , c ⟧, ∏ v : vertex g , injections v · x = coconeIn cc v.
Show proof.

  exists (from_colimHSET _ cc).
  abstract (intro i; simpl; unfold injections, compose, from_colimHSET; simpl;
            apply funextfun; intro Fi; now rewrite (setquotunivcomm eqr)).

Definition ColimCoconeHSET : ColimCocone D.
Show proof.

  apply (make_ColimCocone _ colimHSET colimCoconeHSET); intros c cc.
  exists (ColimHSETArrow _ cc).
  abstract (intro f; apply subtypePath;
            [ intro; now apply impred; intro i; apply has_homsets_HSET
            | apply funextfun; intro x; simpl;
              apply (surjectionisepitosets (setquotpr eqr));
                [now apply issurjsetquotpr | now apply pr2 | ];
              intro y; destruct y as [u fu]; destruct f as [f Hf];
              now apply (toforallpaths _ _ _ (Hf u) fu)]).

End colimits.

Opaque from_colimHSET.

Lemma ColimsHSET : Colims HSET.
Show proof.

now intros g d; apply ColimCoconeHSET.

Lemma ColimsHSET_of_shape (g : graph) :
Colims_of_shape g HSET.
Show proof.

now intros d; apply ColimCoconeHSET.

Binary coproducs BinCoproductsHSET

Lemma BinCoproductIn1CommutesHSET (A B : HSET) (CC : BinCoproduct A B)(C : HSET)
(f : A --> C)(g: B --> C) (a:pr1 A):
BinCoproductArrow CC f g (BinCoproductIn1 CC a) = f a.
Show proof.

  set (H1 := BinCoproductIn1Commutes _ _ _ CC _ f g).
  apply toforallpaths in H1.
  now apply H1.

Lemma BinCoproductIn2CommutesHSET (A B : HSET) (CC : BinCoproduct A B)(C : HSET)
(f : A --> C)(g: B --> C) (b:pr1 B):
BinCoproductArrow CC f g (BinCoproductIn2 CC b) = g b.
Show proof.

  set (H1 := BinCoproductIn2Commutes _ _ _ CC _ f g).
  apply toforallpaths in H1.
  now apply H1.

Lemma postcompWithBinCoproductArrowHSET {A B : HSET} (CCAB : BinCoproduct A B) {C : HSET}
(f : A --> C) (g : B --> C) {X : HSET} (k : C --> X) z:
k (BinCoproductArrow CCAB f g z) = BinCoproductArrow CCAB (f · k) (g · k) z.
Show proof.

  set (H1 := postcompWithBinCoproductArrow _ CCAB f g k).
  apply toforallpaths in H1.
  now apply H1.

Lemma BinCoproductsHSET : BinCoproducts HSET.
Show proof.

  intros A B.
  use make_BinCoproduct.
  - apply (setcoprod A B).
  - simpl in *; apply ii1.
  - simpl in *; intros x; apply (ii2 x).
  - apply (make_isBinCoproduct _ HSET).
    intros C f g; simpl in *.
    use tpair.
    * exists (sumofmaps f g); abstract (split; apply idpath).
    * abstract (intros h; apply subtypePath;
      [ intros x; apply isapropdirprod; apply has_homsets_HSET
      | destruct h as [t [ht1 ht2]]; simpl;
                apply funextfun; intro x;
                rewrite <- ht2, <- ht1; unfold compose; simpl;
                case x; intros; apply idpath]).

General indexed coproducs CoproductsHSET

Lemma CoproductsHSET (I : UU) (HI : isaset I) : Coproducts I HSET.
Show proof.

  intros A.
  use make_Coproduct.
  - exists (∑ i , pr1 (A i)).
    apply (isaset_total2 _ HI); intro i; apply setproperty.
  - simpl; apply tpair.
  - apply (make_isCoproduct _ _ HSET).
    intros C f; simpl in *.
    use tpair.
    * exists (λ X , f (pr1 X) (pr2 X)); abstract (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; rewrite <- ht; destruct x; apply idpath]).

Binary coproducts from colimits BinCoproductsHSET_from_Colims

Require UniMath.CategoryTheory.limits.graphs.bincoproducts.

Lemma BinCoproductsHSET_from_Colims : graphs.bincoproducts.BinCoproducts HSET.
Show proof.

now apply bincoproducts.BinCoproducts_from_Colims, ColimsHSET_of_shape.

Pushouts from colimits PushoutsHSET_from_Colims

Lemma PushoutsHSET_from_Colims : graphs.pushouts.Pushouts HSET.
Show proof.

red; intros; apply ColimsHSET_of_shape.

Initial object InitialHSET

Lemma InitialHSET : Initial HSET.
Show proof.

  apply (make_Initial emptyHSET).
  apply make_isInitial; intro a.
  use tpair.
  - simpl; intro e; induction e.
  - abstract (intro f; apply funextfun; intro e; induction e).

Initial object from colimits InitialHSET_from_Colims

Require UniMath.CategoryTheory.limits.graphs.initial.

Lemma InitialHSET_from_Colims : graphs.initial.Initial HSET.
Show proof.

apply initial.Initial_from_Colims, ColimsHSET_of_shape.

Section finite_subsets.

  Local Open Scope subtype.
  Local Open Scope logic.

  Definition finite_subsets_graph (X : hSet) : graph.
  Show proof.

    use make_graph.
    - exact(finite_subset X).
    - exact(λ (A B : finite_subset X), A ⊆ B).

  Definition finite_subsets_diagram (X : hSet)
    : diagram (finite_subsets_graph X) HSET.
  Show proof.

    use make_diagram.
    - exact(λ (A : finite_subset X), carrier_subset A).
    - exact(λ (A B : finite_subset X)
              (E : A ⊆ B ),
             subtype_inc E).

  Definition finite_subsets_cocone (X : hSet)
    : cocone (finite_subsets_diagram X) X.
  Show proof.

    use make_cocone.
    - exact(λ (A : finite_subset X), pr1carrier A).
    - red ; intros ; apply idpath.

  Definition is_colimit_finite_subsets_cocone (X : hSet)
    : isColimCocone (finite_subsets_diagram X) X (finite_subsets_cocone X).
  Show proof.

    set (D := finite_subsets_diagram X).
    intros Y CC.
    use unique_exists.
    - exact(λ (x : X), coconeIn CC (finite_singleton x) singleton_point).
    - intros A.
      apply funextfun ; intro a.

      set (a_in_A := finite_singleton_is_in (A : finite_subset X) a).

      assert(p : dmor D a_in_A · coconeIn CC A = coconeIn CC (finite_singleton (pr1 a)))
        by apply coconeInCommutes.

      apply(eqtohomot (!p)).
    - intro ; apply isaprop_is_cocone_mor.
    - intros f fmor.
      apply funextfun ; intro x.
      exact(eqtohomot (fmor (finite_singleton x)) singleton_point).

End finite_subsets.

Concrete construction of coequalizers of sets

Section HSETCoequalizer.
  Context {X Y : hSet}
          (f g : X → Y).

  Definition coequalizer_eqrel
    : eqrel Y.
  Show proof.

    use make_eqrel.
    - exact (eqrel_from_hrel (λ y₁ y₂ , ∃ (x : X ) , f x = y₁ × g x = y₂)).
    - apply iseqrel_eqrel_from_hrel.

  Definition coequalizer_hSet
    : hSet
    := setquotinset coequalizer_eqrel.

  Definition coequalizer_map_hSet
    : Y → coequalizer_hSet
    := setquotpr coequalizer_eqrel.

  Proposition coequalizer_eq_hSet
              (x : X)
    : coequalizer_map_hSet (f x)
      =
      coequalizer_map_hSet (g x).
  Show proof.

    apply iscompsetquotpr.
    use eqrel_impl.
    apply hinhpr.
    exists x.
    split.
    - apply idpath.
    - apply idpath.

  Lemma coequalizer_out_hSet_equality
        (Z : hSet)
        (h : Y → Z)
        (p : ∏ (x : X ), h(f x) = h(g x))
    : iscomprelfun coequalizer_eqrel h.
  Show proof.

    intros y₁ y₂ q.
    cbn in *.
    use (q (make_eqrel (λ y₁ y₂ , make_hProp (h y₁ = h y₂) _) _)).
    - apply setproperty.
    - repeat split.
      + exact (λ _ _ _ r₁ r₂ , r₁ @ r₂).
      + exact (λ _ _ r , !r).
    - intros x y ; cbn.
      use factor_through_squash.
      {
        apply setproperty.
      }
      intros r.
      rewrite <- (pr12 r).
      rewrite <- (pr22 r).
      apply p.

  Definition coequalizer_out_hSet
             {Z : hSet}
             (h : Y → Z)
             (p : ∏ (x : X ), h(f x) = h(g x))
    : coequalizer_hSet → Z.
  Show proof.

    use setquotuniv.
    - exact h.
    - exact (coequalizer_out_hSet_equality Z h p).

End HSETCoequalizer.

Definition Coequalizers_HSET
: Coequalizers HSET.
Show proof.

  intros X Y f g.
  use make_Coequalizer.
  - exact (coequalizer_hSet f g).
  - exact (coequalizer_map_hSet f g).
  - abstract
      (use funextsec ;
       intro x ;
       cbn ;
       exact (coequalizer_eq_hSet f g x)).
  - intros Z h p.
    use iscontraprop1.
    + abstract
        (use invproofirrelevance ;
         intros φ₁ φ₂ ;
         use subtypePath ; [ intro ; apply homset_property | ] ;
         use funextsec ;
         use setquotunivprop' ; [ intro ; apply setproperty | ] ;
         intro x ; cbn ;
         exact (eqtohomot (pr2 φ₁ @ !(pr2 φ₂)) x)).
    + simple refine (_ ,, _).
      * exact (coequalizer_out_hSet f g h (eqtohomot p)).
      * abstract
          (apply idpath).