(x y : comma_category) : x ≅ y -> x = y. Proof. intro i. destruct i as [i [i' ? ?]]. hnf in *. destruct i, i'. simpl in *. Global Instance comma_category_IsCategory `{IsCategory A, IsCategory B} : IsCategory comma_category. Proof. hnf. unfold IsStrictCategory in *. typeclasses eauto. 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.