s d d' (m : morphism d d') (m' : morphism s d) : morphism s d'. Proof. revert m'; apply Trunc_rec; intro m'. revert m; apply Trunc_rec; intro m. apply tr. exact (m' @ m). Defined.
Require Import Category.Core. Require Import HoTT.Truncations.Core. Require Import HoTT.Basics.