Homomorphism (A / cong_ker f) (B && in_image_hom f) := BuildHomomorphism def_first_isomorphism. Global Instance embedding_first_isomorphism (s : Sort σ) : IsEmbedding ( s). Proof. apply isembedding_isinj_hset. refine (Quotient_ind_hprop (cong_ker f s) _ _). intro x. refine (Quotient_ind_hprop (cong_ker f s) _ _). intros y p. apply qglue. exact (p..1). Qed.
Require Import Import