Library UniMath.CategoryTheory.Categories.HSET.Univalence
HSET is a univalent_category (is_univalent_HSET)
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.Foundations.HLevels.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso.
Local Open Scope cat.
Definition hset_id_weq_z_iso (A B : ob HSET) :
(A = B) ≃ (z_iso A B) :=
weqcomp (UA_for_HLevels 2 A B) (hset_equiv_weq_z_iso A B).
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.
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.
Definition category_HSET : category := make_category HSET has_homsets_HSET.
Lemma is_univalent_HSET : is_univalent category_HSET.
Show proof.
Definition HSET_univalent_category : univalent_category := _ ,, is_univalent_HSET.