proposition: Lemma scalar_extension_binproduct_iso_inv_iscomprelrelfun : iscomprelrelfun (eqreldirprod (eqrelation X) (eqrelation X')) (eqrelation (BinProductObject _ (binproducts_monoid_action_cat M X X'))) scalar_extension_binproduct_iso_inv_data.
proof: Proof. refine (transportf (λ x, iscomprelrelfun x _ _) (eqrel_from_hreldirprod _ _ (isrefl_hrelation _) (isrefl_hrelation _)) _). apply iscomprelrelfun_eqrel_from_hrel. intros x x' Hx. set (t := terminal_element (pr21 x) (pr22 x)). set (t' := terminal_element (pr21 x') (pr22 x')). induction Hx as [Hx1 Hx2]. revert Hx1 Hx2. apply hinhfun2. intros Hx1 Hx2. epose (t'' := element_is_terminal _ _ (_ ,, _ ,, _ ,, (pr22 Hx1 @ maponpaths _ (pr1 (pr222 t')) @ !assocax _ _ _ _ @ !maponpaths (λ x, x * _) (monoidfunmul f _ _)) ,, (pr22 Hx2 @ maponpaths _ (pr2 (pr222 t')) @ !assocax _ _ _ _ @ !maponpaths (λ x, x * _) (monoidfunmul f _ _)) )). refine (pr1 t'' ,, _ ,, pr12 t''). apply pathsdirprod. - refine (maponpaths (λ x, _ x _) (pr12 Hx1) @ _). refine (!_ @ action_op _ (pr11 x) _ _). refine (!_ @ action_op _ (pr11 x) (pr1 Hx1) _). exact (!maponpaths _ (pr122 t'')). - refine (maponpaths (λ x, _ x _) (pr12 Hx2) @ _). refine (!_ @ action_op _ (pr12 x) _ _). refine (!_ @ action_op _ (pr12 x) (pr1 Hx2) _). exact (!maponpaths _ (pr222 t'')). 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