(** %
\section{\label{sec:invertible_patchlike}Invertible Patchlike}
% *)
Module Export invertible_patchlike.

Require Import Equality.

Require Import names.
Require Import patch_universes.

Reserved Notation "p ^"
    (at level 10).
Class InvertiblePatchlike (pu_type : (NameSet -> NameSet -> Type))
                        : Type := mkInvertiblePatchlike {
    invert : forall {from to : NameSet},
             pu_type from to -> pu_type to from;

    invertInverse : forall {from to : NameSet}
                           (p : pu_type from to),
                    invert (invert p) = p
}.
Notation "p ^" := (invert p).

End invertible_patchlike.