(s : Sort σ) : (A / cong_ker f) s → (B && in_image_hom f) s. Proof. refine (Quotient_rec (cong_ker f s) _ (λ x, (f s x; tr (x; idpath))) _). intros x y p. by apply path_sigma_hprop. Defined.
Require Import Import