(** %
\section{\label{sec:commute_square}Commute Square}
% *)
Module Export commute_square.

Require Import Equality.

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

Reserved Notation "p ^"
    (at level 10).
Class CommuteSquare (pu_type1 pu_type2 : (NameSet -> NameSet -> Type))
                    {ppu_1_2 : PartPatchUniverse pu_type1 pu_type2}
                    {ppu_2_1 : PartPatchUniverse pu_type2 pu_type1}
                    {ipl : InvertiblePatchlike pu_type2}
                  : Type := mkCommuteSquare {
    commuteSquare : forall {from mid1 mid2 to : NameSet}
                           {p  : pu_type1 from mid1} {q  : pu_type2 mid1 to}
                           {q' : pu_type2 from mid2} {p' : pu_type1 mid2 to},
                    << p , q >> <~> << q' , p' >>
                 -> << invert q' , p >> <~> << p' , invert q >>
}.
Notation "p ^" := (invert p).

Lemma commuteInverses : forall {pu_type1 pu_type2 : NameSet -> NameSet -> Type}
                               {ppu_1_2 : PartPatchUniverse pu_type1 pu_type2}
                               {ppu_2_1 : PartPatchUniverse pu_type2 pu_type1}
                               {ipl1 : InvertiblePatchlike pu_type1}
                               {ipl2 : InvertiblePatchlike pu_type2}
                               {cs_1_2 : CommuteSquare pu_type1 pu_type2}
                               {cs_2_1 : CommuteSquare pu_type2 pu_type1}
                               {from mid1 mid2 to : NameSet}
                               {p  : pu_type1 from mid1} {q  : pu_type2 mid1 to}
                               {q' : pu_type2 from mid2} {p' : pu_type1 mid2 to},
                        << p , q >> <~> << q' , p' >>
                     -> << p'^ , q'^ >> <~> << q^, p^ >>.
Proof with auto.
intros.
apply commuteSquare in H.
apply commuteSquare in H...
Qed.

End commute_square.