proposition: Lemma move_inv {C:category} {a a' b' b:C} {f : a --> b} {f' : a' --> b'} {i : a --> a'} {i' : a' --> a} {j : b --> b'} {j' : b' --> b} : is_inverse_in_precat i i' -> is_inverse_in_precat j j' -> j ∘ f = f' ∘ i -> j' ∘ f' = f ∘ i'.
proof: Proof. intros I J r. rewrite <- id_right. rewrite (! pr1 J). rewrite assoc. apply (maponpaths (λ k, j' ∘ k)). rewrite <- assoc. rewrite r. rewrite assoc. rewrite (pr2 I). rewrite id_left. reflexivity. Defined.
imports: UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.Foundations.Preamble UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics