s d d' (m1 : morphism d d') (m2 : morphism s d) : morphism s d'. Proof. exists (m1.1 o m2.1). apply compose_H. Defined.
Require Import Category.Core Functor.Core. Require Import SetCategory.Core. Require Import Basics.Trunc Types.Sigma. Require Import Basics.Tactics.