{X R} `{Reflexive X R} `{forall x y, IsHProp (R x y)} (f : forall x y, R x y -> x = y) : IsHSet X. Proof. apply @hset_axiomK. intros x p. refine (_ @ concat_Vp (f x x (transport (R x) p^ (reflexivity _)))). apply moveL_Vp. refine ((transport_paths_r _ _)^ @ _). refine ((transport_arrow _ _ _)^ @ _). refine ((ap10 (apD (f x) p) (@reflexivity X R _ x)) @ _). apply ap. apply path_ishprop. Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.