forall A B C, Isomorphism A B -> Isomorphism B C -> Isomorphism A C. Proof. intros [A R__A] [B R__B] [C R__C]. intros [f Hf] [g Hg]. exists (equiv_compose' g f). intros a a'. split. - intros a_a'. apply Hg. apply Hf. exact a_a'. - intros gfa_gfa'. apply Hf. apply Hg. exact gfa_gfa'. Defined.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Colimits.Quotient. From HoTT Require Import HSet.