proposition: Lemma Injection_trans X Y Z : Injection X Y -> Injection Y Z -> Injection X Z.
proof: Proof. intros [f Hf] [g Hg]. exists (fun x => g (f x)). intros x x' H. now apply Hf, Hg. Qed.
imports: HoTT.TruncType HoTT.Classes.interfaces.abstract_algebra