abf a'b'f' (gh g'h' : morphism abf a'b'f') : gh.(g) = g'h'.(g) -> gh.(h) = g'h'.(h) -> gh = g'h'. Proof. destruct gh, g'h'; simpl. intros; path_induction. f_ap. all:exact (center _). Qed.
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.