proposition: Lemma are_inverses_from_Pushout_to_Pushout {a b c : C} {f : C⟦a, b⟧} {g : C⟦a, c⟧} (Po Po': Pushout f g) : is_inverse_in_precat (from_Pushout_to_Pushout Po Po') (from_Pushout_to_Pushout Po' Po).
proof: Proof. split; apply pathsinv0; apply PushoutEndo_is_identity; rewrite assoc; unfold from_Pushout_to_Pushout; repeat rewrite PushoutArrow_PushoutIn1; repeat rewrite PushoutArrow_PushoutIn2; auto. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Pushouts