{A B : Type} {s : A -> B} {r : B -> A} (H : r o s == idmap) : IsInjective s. Proof. intros a a' alpha. exact ((H a)^ @ ap r alpha @ H a'). Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.