(A : D) (p : morphism C X (U A)) (Ap := CommaCategory.Build_object !X U tt A p) (UniversalProperty : forall (A' : D) (p' : morphism C X (U A')), Contr { m : morphism D A A' | U _1 m o p = p' }) : IsInitialMorphism Ap. Proof. intro x. specialize (UniversalProperty (CommaCategory.b x) (CommaCategory.f x)). eapply istrunc_equiv_istrunc. - apply CommaCategory.issig_morphism. - apply contr_inhabited_hprop. + abstract univ_hprop_t UniversalProperty. + (exists tt). (exists (@center _ UniversalProperty).1). abstract (progress rewrite ?right_identity, ?left_identity; exact (@center _ UniversalProperty).2). Defined.
Require Import Category.Core Functor.Core. Require Import Category.Dual Functor.Dual. Require Import Category.Objects. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Import Comma.Core. Require Import Trunc Types.Sigma HoTT.Tactics. Require Import Basics.Tactics.