From Coq Require Import ssreflect ssrfun FunctionalExtensionality.

Record Isomorphism (A B : Type) := {
    Forward : A -> B;
    Backward : B -> A;
    BF : cancel Forward Backward;
    FB : cancel Backward Forward;
}.

Infix "<-->" := Isomorphism (at level 95, no associativity).

Definition iso_refl {A : Type} : A <--> A := {|
    Forward x := x;
    Backward x := x;
    BF x := eq_refl;
    FB x := eq_refl;
|}.

Definition iso_sym {A B : Type} (α : A <--> B) : B <--> A := {|
    Forward x := Backward _ _ α x;
    Backward x := Forward _ _ α x;
    BF x := FB _ _ α x;
    FB x := BF _ _ α x;
|}.

Definition iso_trans {A B C : Type} (α : A <--> B) (β : B <--> C) : A <--> C.
Proof.
    refine ({|
        Forward x := Forward _ _ β (Forward _ _ α x);
        Backward x := Backward _ _ α (Backward _ _ β x);
        BF x := _;
        FB x := _;
    |}).
    - by rewrite BF BF.
    - by rewrite FB FB.
Qed.

Definition iso_exp {A B C : Type} (α : A <--> B) : (A -> C) <--> (B -> C).
Proof.
    refine ({|
        Forward f x := f (Backward _ _ α x);
        Backward f x := f (Forward _ _ α x);
        BF f := _;
        FB f := _;
    |}).
    - apply functional_extensionality => x.
        by rewrite BF.
    - apply functional_extensionality => x.
        by rewrite FB.
Qed.