proposition: Lemma isomorphism_inverse : forall A B, Isomorphism A B -> Isomorphism B A.
proof: Proof. intros [A R__A] [B R__B] [f H]. exists (equiv_inverse f). intros b b'. cbn. rewrite <- (eisretr f b). set (a := f^-1 b). rewrite eissect. rewrite <- (eisretr f b'). set (a' := f^-1 b'). rewrite eissect. split; apply H. Defined.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)