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

\begin{code}
\>[0]\AgdaKeyword{record}\AgdaSpace{}%
\AgdaRecord{IsIdeal}%
\>[154I]\AgdaSymbol{\{}\AgdaBound{a}\AgdaSpace{}%
\AgdaBound{p}\AgdaSpace{}%
\AgdaBound{ℓ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{Level}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{a}\AgdaSpace{}%
\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{I}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Pred}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{p}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Rel}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{ℓ}\AgdaSymbol{)}\<%
\\
\>[.]\<[154I]%
\>[15]\AgdaSymbol{(}\AgdaBound{+}\AgdaSpace{}%
\AgdaBound{∙}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Op₂}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaOperator{\AgdaBound{{-}\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Op₁}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{0\#}\AgdaSpace{}%
\AgdaBound{1\#}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}%
\AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
\AgdaBound{ℓ}\AgdaSpace{}%
\AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
\AgdaBound{p}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{field}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaField{isRing}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{IsRing}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{+}\AgdaSpace{}%
\AgdaBound{∙}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{{-}\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{0\#}\AgdaSpace{}%
\AgdaBound{1\#}\<%
\\
%
\>[4]\AgdaField{isSubGroup}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{IsSubGroup}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaBound{I}\AgdaSpace{}%
\AgdaBound{+}\AgdaSpace{}%
\AgdaBound{0\#}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{{-}\AgdaUnderscore{}}}\<%
\\
%
\>[4]\AgdaField{idealProp}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{r}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{ix}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{I}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{IdealProp}\AgdaSpace{}%
\AgdaBound{I}\AgdaSpace{}%
\AgdaBound{∙}\AgdaSpace{}%
\AgdaBound{r}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaBound{ix}\<%
%% \\
%% %
%% \\[\AgdaEmptyExtraSkip]%
%% %
%% \>[2]\AgdaFunction{ideal$^l$}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{x}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{I}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{→}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{∙}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{∈}}\AgdaSpace{}%
%% \AgdaBound{I}\<%
%% \\
%% %
%% \>[2]\AgdaFunction{ideal$^l$}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{x}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₁}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaField{idealProp}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{ix}\<%
%% \\
%% %
%% \>[2]\AgdaFunction{ideal$^r$}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{r}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{x}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaBound{I}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{→}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{∙}\AgdaSpace{}%
%% \AgdaBound{x}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{∈}}\AgdaSpace{}%
%% \AgdaBound{I}\<%
%% \\
%% %
%% \>[2]\AgdaFunction{ideal$^r$}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{x}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaBound{ix}\AgdaSpace{}%
%% \AgdaSymbol{=}\AgdaSpace{}%
%% \AgdaField{proj₂}\AgdaSpace{}%
%% \AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
%% \AgdaField{idealProp}\AgdaSpace{}%
%% \AgdaBound{r}\AgdaSpace{}%
%% \AgdaBound{ix}\<%  
\end{code}