proposition: Lemma scalar_extension_binproduct_iso_mor_iscomprelrelfun : iscomprelrelfun (eqrelation (BinProductObject _ (binproducts_monoid_action_cat M X X'))) (eqreldirprod (eqrelation X) (eqrelation X')) scalar_extension_binproduct_iso_mor_data.
proof: Proof. refine (transportf (λ x, iscomprelrelfun _ x _) (eqrel_from_hreldirprod _ _ (isrefl_hrelation _) (isrefl_hrelation _)) _). apply iscomprelrelfun_eqrel_from_hrel. intros x x' Hx. split. - revert Hx. apply hinhfun. intro Hx. exists (pr1 Hx). split. ++ exact (base_paths _ _ (pr12 Hx)). ++ exact (pr22 Hx). - revert Hx. apply hinhfun. intro Hx. exists (pr1 Hx). split. ++ refine (!maponpaths (λ x, x _) (transportf_const _ _) @ fiber_paths (pr12 Hx)). ++ exact (pr22 Hx). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total