(Ap : object (U / X)) : Type := @IsInitialMorphism (C^op) _ X (U^op) (op_object Ap).
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.