X Y Z : Injection X Y -> Injection Y Z -> Injection X Z. Proof. intros [f Hf] [g Hg]. exists (fun x => g (f x)). intros x x' H. by apply Hf, Hg. Qed.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.