(** %
\section{\label{sec:invertible_patch_universe}Invertible Patch Universe}
% *)
Module Export invertible_patch_universe.

Require Import Equality.

Require Import names.
Require Import patch_universes.
Require Import invertible_patchlike.

Class InvertiblePatchUniverse {pu_type : (NameSet -> NameSet -> Type)}
                              {ppu : PartPatchUniverse pu_type pu_type}
                              {pui : PatchUniverseInv ppu ppu}
                              (pu : PatchUniverse pui)
                              (ipl : InvertiblePatchlike pu_type)
                            : Type := mkInvertiblePatchUniverse {
    nameOfInverse : forall {from to : NameSet}
                           (p : pu_type from to),
                    pu_nameOf (p ^) = signedNameInverse (pu_nameOf p)
}.

End invertible_patch_universe.