proposition: Lemma hset_hOneType : forall X : Type, IsHSet X -> IsHOneType X.
proof: Proof. intros X f x y p q. pose (fun a => f x y p a) as g. assert (forall a (r : q = a), eq_trans (g q) r = g a). { intros. destruct a. subst q. reflexivity. } intros r s. pose proof (H p (eq_sym r)). pose proof (H p (eq_sym s)). rewrite <- H1 in H0. apply eq_trans_cancel in H0. rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r). rewrite H0. reflexivity. Qed.
imports: Coq.Logic.FunctionalExtensionality