issig_morphism' abf a'b'f' : (morphism_sig_T' abf a'b'f') <~> morphism abf a'b'f'. Proof. issig. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Functor.Core. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Require Import Category.Strict. Import Functor.Identity.FunctorIdentityNotations. Module Import CommaCategory.