A B C (S : Functor A C) (T : Functor B C) : PreCategory. Proof. refine (@Build_PreCategory (@object _ _ _ S T) (@morphism _ _ _ S T) (@identity _ _ _ S T) (@compose _ _ _ S T) _ _ _ _ ); abstract path_comma_t. 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.