Przemebra/praca-magisterska/agda-tex/CosetLRnorm.tex

\begin{code}%
\>[0]\AgdaFunction{normalGroup⇒cosetsEq}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{a}\AgdaSpace{}%
\AgdaBound{b}\AgdaSpace{}%
\AgdaBound{ℓ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{Level}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{a}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Rel}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{ℓ}\AgdaSymbol{)}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaSymbol{(}\AgdaBound{subsetPred}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Pred}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{b}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Op₂}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{\ensuremath{\epsilon}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Op₁}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\<%
\\
%
\>[2]\AgdaSymbol{(}\AgdaBound{isNormalSubGroup}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{IsNormalSubGroup}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{subsetPred}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{\ensuremath{\epsilon}}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
%
\>[2]\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
%
\>[2]\AgdaKeyword{let}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaBound{leftCosetP}\AgdaSpace{}%
\AgdaSymbol{=}%
\>[18]\AgdaFunction{leftCosetPred}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{subsetPred}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{g}\<%
\\
%
\>[4]\AgdaBound{rightCosetP}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{rightCosetPred}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{subsetPred}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{g}\<%
\\
%
\>[4]\AgdaBound{l→r}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{leftCosetP}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{rightCosetP}\AgdaSpace{}%
\AgdaBound{x}\<%
\\
%
\>[4]\AgdaBound{r→l}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{rightCosetP}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{leftCosetP}\AgdaSpace{}%
\AgdaBound{x}\<%
\\
%
\>[2]\AgdaKeyword{in}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{l→r}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaBound{r→l}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaComment{{-}{-} Uwaga: to nie musi być biekcja! (tzn: l→r \$ r→l ≠ x→x)}\<%
%% \\
%% \>[0]\AgdaFunction{normalGroup⇒cosetsEq}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaArgument{A}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{subsetPred}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{\ensuremath{\epsilon}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSpace{}%
%% \AgdaBound{isNormalSubGroup}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaSymbol{=}\<%
%% \\
%% \>[0][@{}l@{\AgdaIndent{0}}]%
%% \>[2]\AgdaKeyword{let}\AgdaSpace{}%
%% \AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaModule{IsNormalSubGroup}\AgdaSpace{}%
%% \AgdaBound{isNormalSubGroup}\AgdaSpace{}%
%% \AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaKeyword{let}\AgdaSpace{}%
%% \AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaModule{EqR}\AgdaSpace{}%
%% \AgdaFunction{setoid}\AgdaSpace{}%
%% \AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaKeyword{let}\<%
%% \\
%% \>[2][@{}l@{\AgdaIndent{0}}]%
%% \>[4]\AgdaBound{leftCosetP}\AgdaSpace{}%
%% \AgdaSymbol{=}%
%% \>[18]\AgdaFunction{leftCosetPred}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{subsetPred}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{g}\<%
%% \\
%% %
%% \>[4]\AgdaBound{rightCosetP}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{rightCosetPred}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{subsetPred}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{g}\<%
%% \\
%% %
%% \>[4]\AgdaBound{l→r}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{leftCosetP}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaSymbol{→}\AgdaSpace{}%
%% \AgdaBound{rightCosetP}\AgdaSpace{}%
%% \AgdaBound{x}\<%
%% \\
%% %
%% \>[4]\AgdaBound{l→r}\AgdaSpace{}%
%% \AgdaBound{lP}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaKeyword{let}\<%
%% \\
%% \>[4][@{}l@{\AgdaIndent{0}}]%
%% \>[6]\AgdaBound{h}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₁}\AgdaSpace{}%
%% \AgdaBound{lP}\<%
%% \\
%% %
%% \>[6]\AgdaBound{hP}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₁}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
%% \AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaBound{lP}\<%
%% \\
%% %
%% \>[6]\AgdaBound{x≈gh}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{≈}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[6]\AgdaBound{x≈gh}\AgdaSpace{}%
%% \AgdaSymbol{=}%
%% \>[14]\AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
%% \AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaBound{lP}\<%
%% \\
%% %
%% \>[6]\AgdaBound{transformation}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{≈}}\AgdaSpace{}%
%% \AgdaSymbol{(((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[6]\AgdaBound{transformation}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{begin}}\<%
%% \\
%% \>[6][@{}l@{\AgdaIndent{0}}]%
%% \>[8]\AgdaBound{x}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaBound{x≈gh}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[8]\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{sym}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaFunction{identity$^r$}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[8]\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{\ensuremath{\epsilon}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}%
%% \>[24]\AgdaFunction{∙{-}cong}\AgdaSpace{}%
%% \AgdaFunction{refl}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaFunction{sym}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaFunction{inverse$^l$}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[8]\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{sym}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaFunction{assoc}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[8]\AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{$\qed$}}\<%
%% \\
%% %
%% \>[6]\AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
%% \AgdaFunction{isNormal}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSpace{}%
%% \AgdaBound{hP}\AgdaSpace{}%
%% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
%% \AgdaBound{transformation}\<%
%% \\
%% %
%% \>[4]\AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaModule{GroupProperties}%
%% \>[448I]\AgdaSymbol{(}\AgdaKeyword{record}\AgdaSpace{}%
%% \AgdaComment{{-}{-} te kilka wierszy jest tylko po ⁻¹{-}involutive}\<%
%% \\
%% \>[448I][@{}l@{\AgdaIndent{0}}]%
%% \>[28]\AgdaSymbol{\{}\AgdaSpace{}%
%% \AgdaField{Carrier}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaBound{A}\<%
%% \\
%% %
%% \>[28]\AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\<%
%% \\
%% %
%% \>[28]\AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\<%
%% \\
%% %
%% \>[28]\AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaField{\ensuremath{\epsilon}}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaBound{\ensuremath{\epsilon}}\<%
%% \\
%% %
%% \>[28]\AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}⁻¹}}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\<%
%% \\
%% %
%% \>[28]\AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaField{isGroup}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{isGroup}\<%
%% \\
%% %
%% \>[28]\AgdaSymbol{\})}\<%
%% \\
%% %
%% \>[4]\AgdaBound{r→l}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{rightCosetP}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaSymbol{→}\AgdaSpace{}%
%% \AgdaBound{leftCosetP}\AgdaSpace{}%
%% \AgdaBound{x}\<%
%% \\
%% %
%% \>[4]\AgdaBound{r→l}%
%% \>[474I]\AgdaBound{rP}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaKeyword{let}\<%
%% \\
%% \>[.]\<[474I]%
%% \>[8]\AgdaBound{h}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₁}\AgdaSpace{}%
%% \AgdaBound{rP}\<%
%% \\
%% %
%% \>[8]\AgdaBound{hP}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₁}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
%% \AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaBound{rP}\<%
%% \\
%% %
%% \>[8]\AgdaBound{x≈hg}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{≈}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[8]\AgdaBound{x≈hg}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
%% \AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaBound{rP}\<%
%% \\
%% %
%% \>[8]\AgdaBound{transformation}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{begin}}\<%
%% \\
%% \>[8][@{}l@{\AgdaIndent{0}}]%
%% \>[10]\AgdaBound{x}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaBound{x≈hg}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[10]\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{sym}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaFunction{identity$^l$}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[10]\AgdaBound{\ensuremath{\epsilon}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{∙{-}cong}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaFunction{sym}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaFunction{inverse$^r$}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{})}\AgdaSpace{}%
%% \AgdaFunction{refl}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[10]\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{assoc}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[10]\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{$\qed$}}\<%
%% \\
%% %
%% \>[8]\AgdaBound{predFulfilment}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{subsetPred}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{))}\<%
%% \\
%% %
%% \>[8]\AgdaBound{predFulfilment}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈\AgdaUnderscore{}respect}}\<%
%% \\
%% \>[8][@{}l@{\AgdaIndent{0}}]%
%% \>[10]\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{begin}}\<%
%% \\
%% \>[10][@{}l@{\AgdaIndent{0}}]%
%% \>[12]\AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSpace{}%
%% \AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSpace{}%
%% \AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{assoc}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[12]\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSpace{}%
%% \AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSpace{}%
%% \AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{∙{-}cong}\AgdaSpace{}%
%% \AgdaFunction{refl}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaFunction{∙{-}cong}\AgdaSpace{}%
%% \AgdaFunction{refl}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaFunction{⁻¹{-}involutive}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[12]\AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{$\qed$}}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[10]\AgdaSymbol{(}\AgdaFunction{isNormal}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{h}\AgdaSpace{}%
%% \AgdaBound{hP}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[8]\AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{g}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{h}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
%% \AgdaBound{g}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{predFulfilment}\AgdaSpace{}%
%% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
%% \AgdaBound{transformation}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[2]\AgdaKeyword{in}\<%
%% \\
%% %
%% \>[2]\AgdaBound{l→r}\AgdaSpace{}%
%% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
%% \AgdaBound{r→l}\<%
\end{code}