fact: Definition Build_morphism abf a'b'f' g h p : morphism abf a'b'f' := @Build_morphism' abf a'b'f' g h p p^.
imports: Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Strict HoTT.Basics HoTT.Types