{X : pType} (mu nu : IsHSpace X) : Type. Proof. destruct mu as [mu mu_lid mu_rid], nu as [nu nu_lid nu_rid]. refine { h : forall x0 x1, mu x0 x1 = nu x0 x1 & prod (forall x:X, _) (forall x:X, _) }. - exact (mu_lid x = h pt x @ nu_lid x). - exact (mu_rid x = h x pt @ nu_rid x). Defined.
Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise