fact: Definition p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper__to_inverse X (H' : X = @Build_Isomorphic (_ -> _) _ _ _ p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper) : @morphism_inverse _ _ _ _ X = inv := ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i)) H'.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Morphisms FunctorCategory.Morphisms Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Isomorphisms NaturalTransformation.Paths FunctorCategory.Core Pseudofunctor.Core HoTT.Tactics