{A} : IsHSet A <~> axiomK A. Proof. apply (equiv_adjointify (@axiomK_hset A) (@hset_axiomK A)). - intros K. by_extensionality x. by_extensionality x'. cut (Contr (x=x)). + intro. eapply path_contr. + apply (Build_Contr _ 1). intros. symmetry; apply K. - intro K. eapply path_ishprop. Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.