path_object' (x y : object) : forall (Ha : x.(a) = y.(a)) (Hb : x.(b) = y.(b)), transport (fun X => morphism C (S X) _) Ha (transport (fun Y => morphism C _ (T Y)) Hb x.(f)) = y.(f) -> x = y. Proof. destruct x, y; simpl. intros; path_induction; reflexivity. 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.