s d d' (gh : morphism d d') (g'h' : morphism s d) : morphism s d' := Build_morphism' s d' (gh.
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.