Library UniMath.CategoryTheory.Categories.HSET.Univalence

HSET is a univalent_category (is_univalent_HSET)

HSET is a univalent_category.

The map precat_paths_to_iso for which we need to show isweq is actually equal to the carrier of the weak equivalence we constructed above. We use this fact to show that that precat_paths_to_iso is an equivalence.

Lemma hset_id_weq_iso_is (A B : ob HSET):
    @idtoiso _ A B = pr1 (hset_id_weq_z_iso A B).
Show proof.
  apply funextfun.
  intro p; elim p.
  apply z_iso_eq; simpl.
  - apply funextfun;
    intro x;
    destruct A.
    apply idpath.

Lemma is_weq_precat_paths_to_iso_hset (A B : ob HSET):
   isweq (@idtoiso _ A B).
Show proof.
  rewrite hset_id_weq_iso_is.
  apply (pr2 (hset_id_weq_z_iso A B)).

Definition category_HSET : category := make_category HSET has_homsets_HSET.

Lemma is_univalent_HSET : is_univalent category_HSET.
Show proof.
  intros a b.
  apply (is_weq_precat_paths_to_iso_hset a b).

Definition HSET_univalent_category : univalent_category := _ ,, is_univalent_HSET.