Homomorphism ((A&&P) / Ψ) ((A/Φ) && Q) := BuildHomomorphism def_second_isomorphism. Global Instance embedding_second_isomorphism (s : Sort σ) : IsEmbedding ( s). Proof. apply isembedding_isinj_hset. refine (Quotient_ind_hprop (Ψ s) _ _). intro x. refine (Quotient_ind_hprop (Ψ s) _ _). intros y p. apply qglue. exact (related_quotient_paths (Φ s) (i s x) (i s y) (p..1)). Qed.
Require Import Import