fact: Definition path_isomorphic (i j : Isomorphic s d) : @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences