proposition: Lemma transitive_Isomorphism : forall A B C, Isomorphism A B -> Isomorphism B C -> Isomorphism A C.
proof: 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.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)