123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159 |
- \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}\<
- \end{code}
|