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

\begin{code}
\>[0]\AgdaFunction{ker\ensuremath{_h}{-}ideal}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaSpace{}%
\AgdaBound{c₁}\AgdaSpace{}%
\AgdaBound{c₂}\AgdaSpace{}%
\AgdaBound{ℓ₁}\AgdaSpace{}%
\AgdaBound{ℓ₂}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{Level}\AgdaSymbol{\}}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{Ring}\AgdaSpace{}%
\AgdaBound{c₁}\AgdaSpace{}%
\AgdaBound{ℓ₁}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{Ring}\AgdaSpace{}%
\AgdaBound{c₂}\AgdaSpace{}%
\AgdaBound{ℓ₂}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaKeyword{let}\AgdaSpace{}%
\AgdaKeyword{open}\AgdaSpace{}%
\AgdaModule{Ring}\AgdaSpace{}%
\AgdaKeyword{in}\<%
\\
%
\>[2]\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[8]\AgdaFunction{Definitions.Morphism}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaField{Carrier}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaField{Carrier}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
%
\>[2]\AgdaSymbol{(}\AgdaBound{iRm}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{IsRingMorphism}\AgdaSpace{}%
\AgdaBound{r₁}\AgdaSpace{}%
\AgdaBound{r₂}\AgdaSpace{}%
\AgdaBound{f}\AgdaSymbol{)}\<%
\\
%
\>[2]\AgdaSymbol{→}%
\>[587I]\AgdaKeyword{let}\AgdaSpace{}%
\AgdaKeyword{open}\AgdaSpace{}%
\AgdaModule{IsRingMorphism}\AgdaSpace{}%
\AgdaBound{iRm}\AgdaSpace{}%
\AgdaKeyword{in}\AgdaSpace{}%
\AgdaKeyword{let}\<%
\\
\>[587I][@{}l@{\AgdaIndent{0}}]%
\>[7]\AgdaBound{kern}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{Kern\ensuremath{_h}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaField{IsAbelianGroupMorphism.gp{-}homo}%
\>[70]\AgdaField{+{-}abgp{-}homo}\AgdaSymbol{)}\<%
\\
\>[587I][@{}l@{\AgdaIndent{0}}]%
\>[5]\AgdaKeyword{in}\AgdaSpace{}%
\AgdaRecord{IsIdeal}\AgdaSpace{}%
\AgdaBound{kern}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaOperator{\AgdaField{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaOperator{\AgdaField{{-}\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaField{0\#}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
\AgdaField{1\#}\AgdaSymbol{)}\<%
%% \\
%% \>[0]\AgdaFunction{ker\ensuremath{_h}{-}ideal}\AgdaSpace{}%
%% \AgdaBound{r₁}\AgdaSpace{}%
%% \AgdaBound{r₂}\AgdaSpace{}%
%% \AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{iRm}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaKeyword{let}\AgdaSpace{}%
%% \AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaModule{Ring}\AgdaSpace{}%
%% \AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaKeyword{let}\AgdaSpace{}%
%% \AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaModule{IsRingMorphism}\AgdaSpace{}%
%% \AgdaBound{iRm}\AgdaSpace{}%
%% \AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaKeyword{let}\<%
%% \\
%% \>[0][@{}l@{\AgdaIndent{0}}]%
%% \>[3]\AgdaBound{groupMorphism}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{IsAbelianGroupMorphism.gp{-}homo}\AgdaSpace{}%
%% \AgdaField{+{-}abgp{-}homo}\<%
%% \\
%% %
%% \>[3]\AgdaBound{monoidMorphism}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{IsGroupMorphism.mn{-}homo}\AgdaSpace{}%
%% \AgdaBound{groupMorphism}\<%
%% \\
%% %
%% \>[3]\AgdaBound{smMorphism}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{IsMonoidMorphism.sm{-}homo}\AgdaSpace{}%
%% \AgdaBound{monoidMorphism}\<%
%% \\
%% %
%% \>[3]\AgdaBound{semi*Morphism}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{IsMonoidMorphism.sm{-}homo}\AgdaSpace{}%
%% \AgdaField{*{-}mn{-}homo}\<%
%% \\
%% %
%% \>[3]\AgdaBound{kern}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{Kern\ensuremath{_h}}\AgdaSpace{}%
%% \AgdaBound{groupMorphism}\<%
%% \\
%% %
%% \>[3]\AgdaBound{abelian₁}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{+{-}abelianGroup}\AgdaSpace{}%
%% \AgdaBound{r₁}\<%
%% \\
%% %
%% \>[3]\AgdaBound{group₁}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{AbelianGroup.group}\AgdaSpace{}%
%% \AgdaBound{abelian₁}\<%
%% \\
%% %
%% \>[3]\AgdaBound{group₂}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{AbelianGroup.group}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaFunction{+{-}abelianGroup}\AgdaSpace{}%
%% \AgdaBound{r₂}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[3]\AgdaBound{isSubGroup}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaRecord{IsSubGroup}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSpace{}%
%% \AgdaSymbol{.}\AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{kern}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSpace{}%
%% \AgdaSymbol{.}\AgdaOperator{\AgdaField{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSpace{}%
%% \AgdaSymbol{.}\AgdaField{0\#}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSpace{}%
%% \AgdaSymbol{.}\AgdaOperator{\AgdaField{{-}\AgdaUnderscore{}}}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[3]\AgdaBound{isSubGroup}%
%% \>[15]\AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaFunction{kern\ensuremath{_h}{-}induces{-}subgroup}\AgdaSpace{}%
%% \AgdaBound{group₁}\AgdaSpace{}%
%% \AgdaBound{group₂}\AgdaSpace{}%
%% \AgdaBound{groupMorphism}\<%
%% \\
%% %
%% \>[3]\AgdaBound{ideal}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{Carrier}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{x}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{Carrier}\AgdaSymbol{)\}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{kern}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{→}\AgdaSpace{}%
%% \AgdaFunction{IdealProp}\AgdaSpace{}%
%% \AgdaBound{kern}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₁}\AgdaSpace{}%
%% \AgdaSymbol{.}\AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaBound{ix}\<%
%% \\
%% %
%% \>[3]\AgdaBound{ideal}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{x}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaKeyword{let}\AgdaSpace{}%
%% \AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaModule{EqR}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaFunction{setoid}\AgdaSpace{}%
%% \AgdaBound{r₂}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaKeyword{let}\<%
%% \\
%% \>[3][@{}l@{\AgdaIndent{0}}]%
%% \>[5]\AgdaBound{frx≈0}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{0\#}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[5]\AgdaBound{frx≈0}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{begin}}\<%
%% \\
%% \>[5][@{}l@{\AgdaIndent{0}}]%
%% \>[7]\AgdaBound{f}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaField{IsSemigroupMorphism.∙{-}homo}\AgdaSpace{}%
%% \AgdaBound{semi*Morphism}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[7]\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaFunction{*{-}cong}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaFunction{refl}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{ix}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[7]\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{0\#}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{zero$^r$}\AgdaSpace{}%
%% \AgdaBound{r₂}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[7]\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{0\#}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{$\qed$}}\<%
%% \\
%% %
%% \>[5]\AgdaBound{fxr≈0}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{))}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{0\#}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[5]\AgdaBound{fxr≈0}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{begin}}\<%
%% \\
%% \>[5][@{}l@{\AgdaIndent{0}}]%
%% \>[7]\AgdaBound{f}\AgdaSpace{}%
%% \AgdaSymbol{((}\AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaField{IsSemigroupMorphism.∙{-}homo}\AgdaSpace{}%
%% \AgdaBound{semi*Morphism}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[7]\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaFunction{*{-}cong}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaFunction{refl}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[7]\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaOperator{\AgdaField{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{0\#}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{≈⟨}}\AgdaSpace{}%
%% \AgdaFunction{zero$^l$}\AgdaSpace{}%
%% \AgdaBound{r₂}\AgdaSpace{}%
%% \AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{⟩}}\<%
%% \\
%% %
%% \>[7]\AgdaSymbol{(}\AgdaBound{r₂}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{0\#}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{$\qed$}}\<%
%% \\
%% \>[3][@{}l@{\AgdaIndent{0}}]%
%% \>[4]\AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaBound{frx≈0}\AgdaSpace{}%
%% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
%% \AgdaBound{fxr≈0}\<%
%% \\
%% \>[0][@{}l@{\AgdaIndent{0}}]%
%% \>[1]\AgdaKeyword{in}\AgdaSpace{}%
%% \AgdaKeyword{record}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaSpace{}%
%% \AgdaField{isRing}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaBound{r₁}\AgdaSymbol{.}\AgdaSpace{}%
%% \AgdaField{isRing}\AgdaSpace{}%
%% \AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaField{isSubGroup}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaBound{isSubGroup}\AgdaSpace{}%
%% \AgdaSymbol{;}\AgdaSpace{}%
%% \AgdaField{idealProp}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaBound{ideal}\AgdaSpace{}%
%% \AgdaSymbol{\}}\<%
\end{code}