forall (Y : D) (f : morphism C (U Y) X), IsTerminalMorphism_morphism o (U _1 (IsTerminalMorphism_property_morphism Y f)) = f := @IsInitialMorphism_property_morphism_property C^op D^op X U^op (op_object Ap) M.
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.