Przemebra/praca-magisterska/agda-tex/Kern-induces-subgroup.tex

\begin{code}
\>[2]\AgdaFunction{kern\ensuremath{_h}{-}induces{-}subgroup}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{IsSubGroup}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}≈\ensuremath{_k}\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaFunction{Kern\ensuremath{_h}}%
\>[50]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}∙\ensuremath{_k}\AgdaUnderscore{}}}%
\>[56]\AgdaFunction{\ensuremath{\epsilon}\ensuremath{_k}}%
\>[60]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}⁻¹\ensuremath{_k}}}\<%
\\
%
\>[2]\AgdaFunction{kern\ensuremath{_h}{-}induces{-}subgroup}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaKeyword{record}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaSymbol{\{}%
\>[468I]\AgdaField{isGroup}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{isGroup\ensuremath{_k}}\<%
\\
\>[.]\<[468I]%
\>[6]\AgdaSymbol{;}\AgdaSpace{}%
\AgdaField{isSubMonoid}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaKeyword{record}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaSpace{}%
\AgdaField{isMonoid}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{isMonoid\ensuremath{_k}}\<%
\\
%
\>[6]\AgdaSymbol{;}%
\>[478I]\AgdaOperator{\AgdaField{∙\AgdaUnderscore{}isSubStructure}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{λ}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{x}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{y}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaBound{k\ensuremath{_x}}\AgdaSpace{}%
\AgdaBound{ky}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{begin}}\<%
\\
\>[.]\<[478I]%
\>[8]\AgdaSymbol{(}\AgdaBound{fn}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{∙\ensuremath{_k}}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{))}%
\>[29]\AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
\AgdaFunction{∙{-}homo}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟩}}\<%
\\
%
\>[8]\AgdaSymbol{(}\AgdaBound{fn}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaField{∙\ensuremath{_h}}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{fn}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}%
\>[30]\AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
\AgdaFunction{∙{-}cong\ensuremath{_h}}\AgdaSpace{}%
\AgdaBound{k\ensuremath{_x}}\AgdaSpace{}%
\AgdaBound{ky}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟩}}\<%
\\
%
\>[8]\AgdaField{\ensuremath{\epsilon}\ensuremath{_h}}\AgdaSpace{}%
\AgdaOperator{\AgdaField{∙\ensuremath{_h}}}\AgdaSpace{}%
\AgdaField{\ensuremath{\epsilon}\ensuremath{_h}}%
\>[18]\AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
\AgdaFunction{identity$^r$\ensuremath{_h}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟩}}\<%
\\
%
\>[8]\AgdaField{\ensuremath{\epsilon}\ensuremath{_h}}%
\>[30]\AgdaOperator{\AgdaFunction{$\qed$}}\<%
\\
%
\>[6]\AgdaSymbol{;}\AgdaSpace{}%
\AgdaOperator{\AgdaField{≈\AgdaUnderscore{}respect}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{λ}\AgdaSpace{}%
\AgdaBound{x≈y}\AgdaSpace{}%
\AgdaBound{k\ensuremath{_x}}\AgdaSpace{}%
\AgdaSymbol{→}%
\>[32]\AgdaFunction{trans\ensuremath{_h}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{sym\ensuremath{_h}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{⟦⟧{-}cong}\AgdaSpace{}%
\AgdaBound{x≈y}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaBound{k\ensuremath{_x}}\<%
\\
%
\>[6]\AgdaSymbol{;}\AgdaSpace{}%
\AgdaField{\ensuremath{\epsilon}InSubset}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{\ensuremath{\epsilon}{-}homo}\<%
\\
%
\>[4]\AgdaSymbol{\}}\<%
\\
%
\>[4]\AgdaSymbol{;}%
\>[520I]\AgdaOperator{\AgdaField{⁻¹\AgdaUnderscore{}isSubStructure}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{λ}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{x}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaBound{k\ensuremath{_x}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{begin}}\<%
\\
\>[520I][@{}l@{\AgdaIndent{0}}]%
\>[7]\AgdaBound{fn}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⁻¹\ensuremath{_k}}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
\AgdaFunction{⁻¹{-}homo}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟩}}\<%
\\
%
\>[7]\AgdaSymbol{(}\AgdaBound{fn}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaField{⁻¹\ensuremath{_h}}}%
\>[20]\AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
\AgdaFunction{⁻¹{-}cong\ensuremath{_h}}\AgdaSpace{}%
\AgdaBound{k\ensuremath{_x}}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟩}}\<%
\\
%
\>[7]\AgdaField{\ensuremath{\epsilon}\ensuremath{_h}}\AgdaSpace{}%
\AgdaOperator{\AgdaField{⁻¹\ensuremath{_h}}}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
\AgdaFunction{\ensuremath{\epsilon}⁻¹≈\ensuremath{\epsilon}}\AgdaSpace{}%
\AgdaBound{h}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟩}}\<%
\\
%
\>[7]\AgdaField{\ensuremath{\epsilon}\ensuremath{_h}}%
\>[20]\AgdaOperator{\AgdaFunction{$\qed$}}\<%
\\
%
\>[4]\AgdaSymbol{\}}\<%
\end{code}