{A : pType} `{IsHomogeneous A} : @IsCoherent A (ishspace_homogeneous). Proof. unfold IsCoherent; cbn. set (f := ishomogeneous pt). change (eisretr f pt = ap f (moveR_equiv_V pt pt (point_eq f)^) @ point_eq f). rewrite <- (point_eq f). unfold moveR_equiv_V; simpl. rhs nrapply concat_p1. lhs nrapply (eisadj f). apply ap. symmetry; apply concat_1p. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise