forall A B, Isomorphism A B -> Isomorphism B A. 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.
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.