proposition: Theorem equiv_hset_axiomK {A} : IsHSet A <~> axiomK A.
proof: 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.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow