proposition: Lemma inverse_unique (m_inv0 m_inv1 : morphism C d s) (left_inverse_0 : m_inv0 o m = identity _) (right_inverse_1 : m o m_inv1 = identity _) : m_inv0 = m_inv1.
proof: Proof. transitivity (m_inv0 o m o m_inv1); try solve [ by (rewrite -> ?associativity; rewrite_hyp; autorewrite with morphism) | by (rewrite <- ?associativity; rewrite_hyp; autorewrite with morphism) ]. Qed.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences