fact: Definition iso_moveL_Vp `(p : morphism C x y) `(q : morphism C x z) `(@IsIsomorphism C _ _ r) : (r o q) = p -> q = (r^-1 o p).
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences