proposition: Lemma scalar_extension_binproduct_iso_is_iso : is_inverse_in_precat (C := HSET) (a := setquotinset (eqrelation _)) (b := setdirprod (setquotinset (eqrelation _)) (setquotinset (eqrelation _))) scalar_extension_binproduct_iso_mor scalar_extension_binproduct_iso_inv.
proof: Proof. pose (prodiso := hset_equiv_weq_z_iso (setquotinset _) (setdirprod (setquotinset _) (setquotinset _)) (weqsetquottodirprod (eqrelation X) (eqrelation X'))). split. - apply funextfun. intro. refine (maponpaths _ (eqtohomot (z_iso_inv_after_z_iso prodiso) _) @ _). use (issurjsetquotpr _ x (_ ,, isasetsetquot _ _ _) _). intro y. rewrite <- (pr2 y). apply iscompsetquotpr. pose (t := terminal_element (pr21 y) (pr21 y)). pose (t' := element_is_terminal (pr21 y) (pr21 y) (pr1 t ,, pr12 t ,, pr12 t ,, pr1 (pr222 t) ,, pr1 (pr222 t))). apply (eqreltrans _ _ ((action (pr111 y) (pr12 t * pr1 t') ,, action (pr211 y) (pr122 t * pr1 t')) ,, pr1 t)). + apply eqrel_impl. apply hinhpr. use (pr1 t' ,, _ ,, pr12 t'). use pathsdirprod; exact (action_op _ _ _ _). + apply eqrelsymm. apply eqrel_impl. apply hinhpr. use (pr12 t * pr1 t' ,, _ ,, _). * apply (pathsdirprod (idpath _)). apply maponpaths. exact (pr222 t' @ !pr122 t'). * refine (pr1 (pr222 t) @ _). refine (maponpaths _ (pr12 t') @ _). refine (!assocax _ _ _ _ @ _). exact (maponpaths (λ x, x * _) (!monoidfunmul f _ _)). - apply funextfun. intro. refine (_ @ eqtohomot (z_iso_after_z_iso_inv prodiso) _). apply (maponpaths (morphism_from_z_iso _ _ prodiso)). refine ((idpath _ : _ = (λ y, setquotfun _ _ _ _ (setquotfun _ _ _ _ y)) (inv_from_z_iso prodiso x) ) @ _). use (issurjsetquotpr _ (inv_from_z_iso prodiso x) (_ ,, isasetsetquot _ _ _) _). intro y. rewrite <- (pr2 y). apply iscompsetquotpr. split. + apply eqrelsymm. apply eqrel_impl. apply hinhpr. use (pr12 (terminal_element (pr211 y) (pr221 y)) ,, idpath _ ,, _). exact (pr1 (pr222 (terminal_element (pr211 y) (pr221 y)))). + apply eqrelsymm. apply eqrel_impl. apply hinhpr. use (pr122 (terminal_element (pr211 y) (pr221 y)) ,, idpath _ ,, _). exact (pr2 (pr222 (terminal_element (pr211 y) (pr221 y)))). 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