`{Funext} {X : pType} (mu nu : IsHSpace X) : path_ishspace_type mu nu <~> (mu = nu). Proof. destruct mu as [mu mu_lid mu_rid], nu as [nu nu_lid nu_rid]; unfold path_ishspace_type. nrefine (equiv_ap_inv' issig_ishspace _ _ oE _). nrefine (equiv_path_sigma _ _ _ oE _); cbn. apply (equiv_functor_sigma' (equiv_path_arrow2 _ _)); intro h; cbn. nrefine (equiv_concat_l _ _ oE _). 1: apply transport_binop_lr_id. nrefine (equiv_path_prod _ _ oE _); cbn. apply equiv_functor_prod'; nrefine (equiv_path_forall _ _ oE _); apply equiv_functor_forall_id; intro x. all: nrefine (equiv_moveR_Vp _ _ _ oE _); apply equiv_concat_r; apply whiskerR; symmetry; apply ap100_path_arrow2. Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise