# Characterizations of monos, epis, and isos in HSET

## Contents

• Points as global elements
• Monomorphisms are exactly injective functions MonosAreInjective_HSET
• Epimorphisms are exactly surjective functions EpisAreSurjective_HSET
• Equivalence between isomorphisms and weak equivalences

## Points as global elements

See https://ncatlab.org/nlab/show/global+element

Local Definition global_element_HSET {A : hSet} (a : A) : HSETunitset, A :=
invweq (weqfunfromunit A) a.

TODO: I think there is a name in UniMath for the constant function at a, what is it?

Local Definition global_element_HSET_paths_weq {A : hSet} (x y : A) :
(x = y) (global_element_HSET x = global_element_HSET y).
Proof.
apply weqonpaths.
Qed.

Local Definition global_element_HSET_comp {A B : hSet} (f : HSETA, B) (x : A) :
global_element_HSET x · f = global_element_HSET (f x).
Proof.
abstract (apply funextfun; intro z; induction z; reflexivity).
Qed.

Local Definition global_element_HSET_fun_weq {A B : hSet} (f : HSETA, B) (x y : A) :
(f x = f y) (global_element_HSET x · f = global_element_HSET y · f).
Proof.
abstract (do 2 rewrite global_element_HSET_comp;
apply global_element_HSET_paths_weq).
Qed.

## Monomorphisms are exactly injective functions MonosAreInjective_HSET

Lemma MonosAreInjective_HSET {A B : HSET} (f: HSET A, B ) :
isMonic f isInjective f.
Proof.
apply weqimplimpl.
- intro isM.
apply incl_injectivity; intros b.
apply invproofirrelevance; intros a1 a2.
apply subtypePath; [intro; apply setproperty|].
apply global_element_HSET_paths_weq.
apply isM.
apply funextsec; intro t.
abstract (induction t; exact (pr2 a1 @ ! pr2 a2)).
- intro isI.
unfold isMonic.
intros ? ? ? eq.
apply funextfun; intro.
apply (invweq (Injectivity _ isI _ _)).
apply toforallpaths in eq.
apply eq.
- apply isapropisMonic, has_homsets_HSET.
- apply isaprop_isInjective.
Qed.

## Epimorphisms are exactly surjective functions EpisAreSurjective_HSET

Lemma EpisAreSurjective_HSET {A B : HSET} (f: HSET A, B ) :
isEpi f issurjective f.
Proof.
apply weqimplimpl.
- intro epif.
apply epiissurjectiontosets; [apply setproperty|].
intros ? ? ? ?.
apply toforallpaths.
apply epif.
now apply funextfun.
- intros is_surj_f.
intros C g h H.
apply funextfun; intro.

Get the point x' in the fiber above x
specialize (is_surj_f x).
apply (squash_to_prop is_surj_f); [apply setproperty|].
intro x'.

Replace x with f x'
refine (!maponpaths _ (hfiberpr2 _ _ x') @ _).
refine (_ @ maponpaths _ (hfiberpr2 _ _ x')).

apply toforallpaths in H.
apply H.
- apply isapropisEpi.
apply has_homsets_HSET.
- apply isapropissurjective.
Qed.

## Equivalence between isomorphisms and weak equivalences of two hSets.

Given an iso, we construct a weak equivalence. This is basically unpacking and packing again.

Lemma hset_iso_is_equiv (A B : ob HSET)
(f : iso A B) : isweq (pr1 f).
Proof.
apply (isweq_iso _ (inv_from_iso f)).
- intro x.
set (T:=iso_inv_after_iso f).
set (T':=toforallpaths _ _ _ T). apply T'.
- intro x.
apply (toforallpaths _ _ _ (iso_after_iso_inv f)).
Defined.

Lemma hset_iso_equiv (A B : ob HSET) : iso A B (pr1 A) (pr1 B).
Proof.
intro f.
(pr1 f).
apply hset_iso_is_equiv.
Defined.

Given a weak equivalence, we construct an iso. Again mostly unwrapping and packing.

Lemma hset_equiv_is_iso (A B : hSet)
(f : (pr1 A) (pr1 B)) :
is_iso (C:=HSET) (pr1 f).
Proof.
apply (is_iso_qinv (C:=HSET) _ (invmap f)).
split; simpl.
- apply funextfun; intro x; simpl in ×.
unfold compose, identity; simpl.
apply homotinvweqweq.
- apply funextfun; intro x; simpl in ×.
unfold compose, identity; simpl.
apply homotweqinvweq.
Defined.

Lemma hset_equiv_iso (A B : ob HSET) : (pr1 A) (pr1 B) iso A B.
Proof.
intro f.
simpl in ×.
(pr1 f).
apply hset_equiv_is_iso.
Defined.

Both maps defined above are weak equivalences.

Lemma hset_iso_equiv_is_equiv (A B : ob HSET) : isweq (hset_iso_equiv A B).
Proof.
apply (isweq_iso _ (hset_equiv_iso A B)).
intro; apply eq_iso.
- reflexivity.
- intro; apply subtypePath.
+ intro; apply isapropisweq.
+ reflexivity.
Qed.

Definition hset_iso_equiv_weq (A B : ob HSET) : (iso A B) ((pr1 A) (pr1 B)).
Proof.
(hset_iso_equiv A B).
apply hset_iso_equiv_is_equiv.
Defined.

Lemma hset_equiv_iso_is_equiv (A B : ob HSET) : isweq (hset_equiv_iso A B).
Proof.
apply (isweq_iso _ (hset_iso_equiv A B)).
{ intro f.
apply subtypePath.
{ intro; apply isapropisweq. }
reflexivity. }
intro; apply eq_iso.
reflexivity.
Qed.

Definition hset_equiv_weq_iso (A B : ob HSET) :
(pr1 A pr1 B) iso A B.
Proof.
(hset_equiv_iso A B).
apply hset_equiv_iso_is_equiv.
Defined.