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

\begin{code}
\>[0]\AgdaFunction{IsNormalIn}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[396I]\AgdaSymbol{\{}\AgdaBound{a}\AgdaSpace{}%
\AgdaBound{b}\AgdaSpace{}%
\AgdaBound{c}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{Level}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{a}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{normalInWhat}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Pred}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{c}\AgdaSymbol{)}\<%
\\
\>[.]\<[396I]%
\>[13]\AgdaSymbol{(}\AgdaBound{I}\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{(}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{Op₁}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}%
\AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
\AgdaBound{b}\AgdaSpace{}%
\AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
\AgdaBound{c}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaFunction{IsNormalIn}%
\>[429I]\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{normalInWhat}\AgdaSpace{}%
\AgdaBound{I}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{normalInWhat}\AgdaSpace{}%
\AgdaBound{a}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[.]\<[429I]%
\>[11]\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{I}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{I}\AgdaSpace{}%
\AgdaSymbol{((}\AgdaBound{a}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{∙}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}%
\AgdaOperator{\AgdaBound{⁻¹}}\AgdaSymbol{)))}\<%
%% \\
%% %
%% \\[\AgdaEmptyExtraSkip]%
%% \>[0]\AgdaFunction{IsNormalInG}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{a}\AgdaSpace{}%
%% \AgdaBound{b}\AgdaSpace{}%
%% \AgdaBound{ℓ}\AgdaSpace{}%
%% \AgdaBound{c}\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{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{I}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaFunction{Pred}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSpace{}%
%% \AgdaBound{b}\AgdaSymbol{\}}\<%
%% \\
%% \>[0][@{}l@{\AgdaIndent{0}}]%
%% \>[2]\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{\}}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{isSubG}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaRecord{IsSubGroup}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{I}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaBound{\ensuremath{\epsilon}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSymbol{)}\<%
%% \\
%% %
%% \>[2]\AgdaSymbol{(}\AgdaBound{normalInWhat}\AgdaSpace{}%
%% \AgdaSymbol{:}\AgdaSpace{}%
%% \AgdaFunction{Pred}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSpace{}%
%% \AgdaBound{c}\AgdaSymbol{)}\AgdaSpace{}%
%% \AgdaSymbol{→}\AgdaSpace{}%
%% \AgdaPrimitiveType{Set}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}%
%% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
%% \AgdaBound{b}\AgdaSpace{}%
%% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
%% \AgdaBound{c}\AgdaSymbol{)}\<%
%% \\
%% \>[0]\AgdaFunction{IsNormalInG}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{a}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{b}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{ℓ}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{c}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{A}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{subsetPred}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaBound{\ensuremath{\epsilon}}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaSymbol{\{}\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\AgdaSymbol{\}}\AgdaSpace{}%
%% \AgdaBound{isSubG}\AgdaSpace{}%
%% \AgdaBound{normalInWhat}\AgdaSpace{}%
%% \AgdaSymbol{=}\<%
%% \\
%% \>[0][@{}l@{\AgdaIndent{0}}]%
%% \>[2]\AgdaFunction{IsNormalIn}\AgdaSpace{}%
%% \AgdaBound{A}\AgdaSpace{}%
%% \AgdaBound{normalInWhat}\AgdaSpace{}%
%% \AgdaBound{subsetPred}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}∙\AgdaUnderscore{}}}\AgdaSpace{}%
%% \AgdaOperator{\AgdaBound{\AgdaUnderscore{}⁻¹}}\<%
\end{code}