`{Funext} {X Y : Type} (M : (X -> X) -> (Y -> Y)) (Mid : M idmap == idmap) (MC : forall f g, M (g o f) == M g o M f) : (X <~> X) -> (Y <~> Y). Proof. assert (MS : forall f g, g o f == idmap -> (M g) o (M f) == idmap). { intros g f s x. transitivity (M (f o g) x). + symmetry. refine (MC g f x). + transitivity (M idmap x). * apply ap10, ap, path_arrow. intros y; apply s. * apply Mid. } assert (ME : (forall f, IsEquiv f -> IsEquiv (M f))). { intros f ?. refine (isequiv_adjointify (M f) (M f^-1) _ _); apply MS; [ apply eisretr | apply eissect ]. } exact (fun f => (Build_Equiv _ _ (M f) (ME f _))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber. Require Import Truncations. Require Import Universes.BAut.