| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Bundles
Documentation
d_SuccessorSet_8 :: p -> p -> () #
data T_SuccessorSet_8 #
Constructors
| C_SuccessorSet'46'constructor_227 (AgdaAny -> AgdaAny) AgdaAny T_IsSuccessorSet_146 |
d_Carrier_24 :: T_SuccessorSet_8 -> () #
d__'8776'__26 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny -> () #
d_suc'35'_28 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_38 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> T_IsPartialEquivalence_16 #
d_refl_40 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny #
d_reflexive_42 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_42 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_44 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> T_Setoid_44 #
d_suc'35''45'cong_46 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_50 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d__'8776'__56 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> AgdaAny -> AgdaAny -> () #
d_Carrier_58 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> () #
d_suc'35'_60 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> AgdaAny -> AgdaAny #
du_suc'35'_60 :: T_SuccessorSet_8 -> AgdaAny -> AgdaAny #
d_zero'35'_62 :: T_Level_18 -> T_Level_18 -> T_SuccessorSet_8 -> AgdaAny #
d_Magma_68 :: p -> p -> () #
data T_Magma_68 #
Constructors
| C_Magma'46'constructor_1279 (AgdaAny -> AgdaAny -> AgdaAny) T_IsMagma_176 |
d_Carrier_82 :: T_Magma_68 -> () #
d__'8776'__84 :: T_Magma_68 -> AgdaAny -> AgdaAny -> () #
d__'8729'__86 :: T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isMagma_88 :: T_Magma_68 -> T_IsMagma_176 #
d_refl_96 :: T_Magma_68 -> AgdaAny -> AgdaAny #
d_reflexive_98 :: T_Level_18 -> T_Level_18 -> T_Magma_68 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_98 :: T_Magma_68 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_100 :: T_Level_18 -> T_Level_18 -> T_Magma_68 -> T_Setoid_44 #
du_setoid_100 :: T_Magma_68 -> T_Setoid_44 #
d_trans_104 :: T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_106 :: T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_108 :: T_Level_18 -> T_Level_18 -> T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_108 :: T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_110 :: T_Level_18 -> T_Level_18 -> T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_110 :: T_Magma_68 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_rawMagma_112 :: T_Level_18 -> T_Level_18 -> T_Magma_68 -> T_RawMagma_36 #
d__'8777'__116 :: T_Level_18 -> T_Level_18 -> T_Magma_68 -> AgdaAny -> AgdaAny -> () #
d_SelectiveMagma_122 :: p -> p -> () #
data T_SelectiveMagma_122 #
Constructors
| C_SelectiveMagma'46'constructor_2287 (AgdaAny -> AgdaAny -> AgdaAny) T_IsSelectiveMagma_436 |
d_Carrier_136 :: T_SelectiveMagma_122 -> () #
d__'8776'__138 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> () #
d__'8729'__140 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_150 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> T_IsPartialEquivalence_16 #
d_refl_152 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny #
d_reflexive_154 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_154 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sel_156 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> T__'8846'__30 #
d_setoid_158 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> T_Setoid_44 #
d_trans_162 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_164 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_166 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_166 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_168 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_168 :: T_SelectiveMagma_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_170 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> T_Magma_68 #
d_rawMagma_174 :: T_Level_18 -> T_Level_18 -> T_SelectiveMagma_122 -> T_RawMagma_36 #
d_CommutativeMagma_180 :: p -> p -> () #
data T_CommutativeMagma_180 #
Constructors
| C_CommutativeMagma'46'constructor_3345 (AgdaAny -> AgdaAny -> AgdaAny) T_IsCommutativeMagma_212 |
d_Carrier_194 :: T_CommutativeMagma_180 -> () #
d__'8776'__196 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> () #
d__'8729'__198 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_204 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_210 :: T_Level_18 -> T_Level_18 -> T_CommutativeMagma_180 -> T_IsPartialEquivalence_16 #
d_refl_212 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny #
d_reflexive_214 :: T_Level_18 -> T_Level_18 -> T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_214 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_216 :: T_Level_18 -> T_Level_18 -> T_CommutativeMagma_180 -> T_Setoid_44 #
d_trans_220 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_222 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_224 :: T_Level_18 -> T_Level_18 -> T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_224 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_226 :: T_Level_18 -> T_Level_18 -> T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_226 :: T_CommutativeMagma_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_228 :: T_Level_18 -> T_Level_18 -> T_CommutativeMagma_180 -> T_Magma_68 #
d_IdempotentMagma_238 :: p -> p -> () #
data T_IdempotentMagma_238 #
Constructors
| C_IdempotentMagma'46'constructor_4403 (AgdaAny -> AgdaAny -> AgdaAny) T_IsIdempotentMagma_248 |
d_Carrier_252 :: T_IdempotentMagma_238 -> () #
d__'8776'__254 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> () #
d__'8729'__256 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny #
d_idem_262 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_268 :: T_Level_18 -> T_Level_18 -> T_IdempotentMagma_238 -> T_IsPartialEquivalence_16 #
d_refl_270 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny #
d_reflexive_272 :: T_Level_18 -> T_Level_18 -> T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_272 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_274 :: T_Level_18 -> T_Level_18 -> T_IdempotentMagma_238 -> T_Setoid_44 #
d_trans_278 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_280 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_282 :: T_Level_18 -> T_Level_18 -> T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_282 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_284 :: T_Level_18 -> T_Level_18 -> T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_284 :: T_IdempotentMagma_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_286 :: T_Level_18 -> T_Level_18 -> T_IdempotentMagma_238 -> T_Magma_68 #
d_AlternativeMagma_296 :: p -> p -> () #
data T_AlternativeMagma_296 #
Constructors
| C_AlternativeMagma'46'constructor_5457 (AgdaAny -> AgdaAny -> AgdaAny) T_IsAlternativeMagma_284 |
d_Carrier_310 :: T_AlternativeMagma_296 -> () #
d__'8776'__312 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> () #
d__'8729'__314 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny #
d_alternative'691'_322 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny #
du_alternative'691'_322 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny #
d_alternative'737'_324 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny #
du_alternative'737'_324 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_330 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> T_IsPartialEquivalence_16 #
d_refl_332 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny #
d_reflexive_334 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_334 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_336 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> T_Setoid_44 #
d_trans_340 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_342 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_344 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_344 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_346 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_346 :: T_AlternativeMagma_296 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_348 :: T_Level_18 -> T_Level_18 -> T_AlternativeMagma_296 -> T_Magma_68 #
d_FlexibleMagma_358 :: p -> p -> () #
data T_FlexibleMagma_358 #
Constructors
| C_FlexibleMagma'46'constructor_6559 (AgdaAny -> AgdaAny -> AgdaAny) T_IsFlexibleMagma_324 |
d_Carrier_372 :: T_FlexibleMagma_358 -> () #
d__'8776'__374 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> () #
d__'8729'__376 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny #
d_flex_382 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_388 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> T_IsPartialEquivalence_16 #
d_refl_390 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny #
d_reflexive_392 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_392 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_394 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> T_Setoid_44 #
d_trans_398 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_400 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_402 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_402 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_404 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_404 :: T_FlexibleMagma_358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_406 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> T_Magma_68 #
d_rawMagma_410 :: T_Level_18 -> T_Level_18 -> T_FlexibleMagma_358 -> T_RawMagma_36 #
d_MedialMagma_416 :: p -> p -> () #
data T_MedialMagma_416 #
Constructors
| C_MedialMagma'46'constructor_7617 (AgdaAny -> AgdaAny -> AgdaAny) T_IsMedialMagma_360 |
d_Carrier_430 :: T_MedialMagma_416 -> () #
d__'8776'__432 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> () #
d__'8729'__434 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_444 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> T_IsPartialEquivalence_16 #
d_medial_446 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_448 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny #
d_reflexive_450 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_450 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_452 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> T_Setoid_44 #
d_trans_456 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_458 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_460 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_460 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_462 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_462 :: T_MedialMagma_416 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_464 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> T_Magma_68 #
d_rawMagma_468 :: T_Level_18 -> T_Level_18 -> T_MedialMagma_416 -> T_RawMagma_36 #
d_SemimedialMagma_474 :: p -> p -> () #
data T_SemimedialMagma_474 #
Constructors
| C_SemimedialMagma'46'constructor_8683 (AgdaAny -> AgdaAny -> AgdaAny) T_IsSemimedialMagma_396 |
d_Carrier_488 :: T_SemimedialMagma_474 -> () #
d__'8776'__490 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> () #
d__'8729'__492 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_502 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> T_IsPartialEquivalence_16 #
d_refl_504 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny #
d_reflexive_506 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_506 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_semimedial'691'_510 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_semimedial'691'_510 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_semimedial'737'_512 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_semimedial'737'_512 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_514 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> T_Setoid_44 #
d_trans_518 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_520 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_522 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_522 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_524 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_524 :: T_SemimedialMagma_474 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_526 :: T_Level_18 -> T_Level_18 -> T_SemimedialMagma_474 -> T_Magma_68 #
d_Semigroup_536 :: p -> p -> () #
data T_Semigroup_536 #
Constructors
| C_Semigroup'46'constructor_9793 (AgdaAny -> AgdaAny -> AgdaAny) T_IsSemigroup_472 |
d_Carrier_550 :: T_Semigroup_536 -> () #
d__'8776'__552 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> () #
d__'8729'__554 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_560 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_566 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_IsPartialEquivalence_16 #
d_refl_568 :: T_Semigroup_536 -> AgdaAny -> AgdaAny #
d_reflexive_570 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_570 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_572 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Setoid_44 #
d_trans_576 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_578 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_580 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_580 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_582 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_582 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_584 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Magma_68 #
d__'8777'__588 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> AgdaAny -> AgdaAny -> () #
d_rawMagma_590 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_RawMagma_36 #
d_Band_596 :: p -> p -> () #
data T_Band_596 #
Constructors
| C_Band'46'constructor_10881 (AgdaAny -> AgdaAny -> AgdaAny) T_IsBand_508 |
d_Carrier_610 :: T_Band_596 -> () #
d__'8776'__612 :: T_Band_596 -> AgdaAny -> AgdaAny -> () #
d__'8729'__614 :: T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isBand_616 :: T_Band_596 -> T_IsBand_508 #
d_assoc_620 :: T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_idem_622 :: T_Band_596 -> AgdaAny -> AgdaAny #
d_refl_632 :: T_Band_596 -> AgdaAny -> AgdaAny #
d_reflexive_634 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_634 :: T_Band_596 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_636 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> T_Setoid_44 #
du_setoid_636 :: T_Band_596 -> T_Setoid_44 #
d_trans_640 :: T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_642 :: T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_644 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_644 :: T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_646 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_646 :: T_Band_596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_semigroup_648 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> T_Semigroup_536 #
d__'8777'__652 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> AgdaAny -> AgdaAny -> () #
d_magma_654 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> T_Magma_68 #
du_magma_654 :: T_Band_596 -> T_Magma_68 #
d_rawMagma_656 :: T_Level_18 -> T_Level_18 -> T_Band_596 -> T_RawMagma_36 #
d_CommutativeSemigroup_662 :: p -> p -> () #
data T_CommutativeSemigroup_662 #
Constructors
| C_CommutativeSemigroup'46'constructor_12035 (AgdaAny -> AgdaAny -> AgdaAny) T_IsCommutativeSemigroup_548 |
d_Carrier_676 :: T_CommutativeSemigroup_662 -> () #
d__'8776'__678 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> () #
d__'8729'__680 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_686 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_688 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_690 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> T_IsCommutativeMagma_212 #
d_isPartialEquivalence_696 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> T_IsPartialEquivalence_16 #
d_refl_700 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny #
d_reflexive_702 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_702 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_trans_708 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_710 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_712 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_712 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_714 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_714 :: T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d__'8777'__720 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> AgdaAny -> AgdaAny -> () #
d_magma_722 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> T_Magma_68 #
d_commutativeMagma_726 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemigroup_662 -> T_CommutativeMagma_180 #
d_CommutativeBand_732 :: p -> p -> () #
data T_CommutativeBand_732 #
Constructors
| C_CommutativeBand'46'constructor_13365 (AgdaAny -> AgdaAny -> AgdaAny) T_IsCommutativeBand_590 |
d_Carrier_746 :: T_CommutativeBand_732 -> () #
d__'8776'__748 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> () #
d__'8729'__750 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_756 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_758 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny #
d_idem_760 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_764 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_766 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_IsCommutativeSemigroup_548 #
d_isPartialEquivalence_772 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_IsPartialEquivalence_16 #
d_refl_776 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny #
d_reflexive_778 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_778 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_780 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_Setoid_44 #
d_trans_784 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_786 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_788 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_788 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_790 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_790 :: T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_band_792 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_Band_596 #
d__'8777'__796 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> AgdaAny -> AgdaAny -> () #
d_magma_798 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_Magma_68 #
d_commutativeSemigroup_804 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_CommutativeSemigroup_662 #
d_commutativeMagma_808 :: T_Level_18 -> T_Level_18 -> T_CommutativeBand_732 -> T_CommutativeMagma_180 #
d_UnitalMagma_814 :: p -> p -> () #
data T_UnitalMagma_814 #
Constructors
| C_UnitalMagma'46'constructor_14927 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsUnitalMagma_642 |
d_Carrier_830 :: T_UnitalMagma_814 -> () #
d__'8776'__832 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> () #
d__'8729'__834 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_836 :: T_UnitalMagma_814 -> AgdaAny #
d_identity'691'_844 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> AgdaAny -> AgdaAny #
du_identity'691'_844 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny #
d_identity'737'_846 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> AgdaAny -> AgdaAny #
du_identity'737'_846 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_852 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> T_IsPartialEquivalence_16 #
d_refl_854 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny #
d_reflexive_856 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_856 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_858 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> T_Setoid_44 #
d_trans_862 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_864 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_866 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_866 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_868 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_868 :: T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_870 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> T_Magma_68 #
d__'8777'__874 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> AgdaAny -> AgdaAny -> () #
d_rawMagma_876 :: T_Level_18 -> T_Level_18 -> T_UnitalMagma_814 -> T_RawMagma_36 #
d_Monoid_882 :: p -> p -> () #
data T_Monoid_882 #
Constructors
| C_Monoid'46'constructor_16157 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsMonoid_686 |
d_Carrier_898 :: T_Monoid_882 -> () #
d__'8776'__900 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> () #
d__'8729'__902 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_904 :: T_Monoid_882 -> AgdaAny #
d_assoc_910 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity_912 :: T_Monoid_882 -> T_Σ_14 #
d_identity'691'_914 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> AgdaAny -> AgdaAny #
du_identity'691'_914 :: T_Monoid_882 -> AgdaAny -> AgdaAny #
d_identity'737'_916 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> AgdaAny -> AgdaAny #
du_identity'737'_916 :: T_Monoid_882 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_922 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_IsPartialEquivalence_16 #
d_refl_928 :: T_Monoid_882 -> AgdaAny -> AgdaAny #
d_reflexive_930 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_930 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_932 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Setoid_44 #
d_trans_936 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_938 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_940 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_940 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_942 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_942 :: T_Monoid_882 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_semigroup_944 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Semigroup_536 #
d__'8777'__948 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> AgdaAny -> AgdaAny -> () #
d_magma_950 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Magma_68 #
du_magma_950 :: T_Monoid_882 -> T_Magma_68 #
d_rawMagma_952 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_RawMagma_36 #
d_rawMonoid_954 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_RawMonoid_64 #
d_unitalMagma_956 :: T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_UnitalMagma_814 #
d_CommutativeMonoid_962 :: p -> p -> () #
data T_CommutativeMonoid_962 #
Constructors
| C_CommutativeMonoid'46'constructor_17931 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsCommutativeMonoid_736 |
d_Carrier_978 :: T_CommutativeMonoid_962 -> () #
d__'8776'__980 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> () #
d__'8729'__982 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_990 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_992 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_996 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny #
d_identity'737'_998 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_1000 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_1002 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_IsCommutativeSemigroup_548 #
d_isPartialEquivalence_1010 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_IsPartialEquivalence_16 #
d_isUnitalMagma_1014 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_IsUnitalMagma_642 #
d_refl_1016 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny #
d_reflexive_1018 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1018 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_1020 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_Setoid_44 #
d_sym_1022 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1024 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1026 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1028 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1028 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1030 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1030 :: T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d__'8777'__1036 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> AgdaAny -> AgdaAny -> () #
d_magma_1038 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_Magma_68 #
d_commutativeSemigroup_1048 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeSemigroup_662 #
d_commutativeMagma_1052 :: T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMagma_180 #
d_IdempotentMonoid_1058 :: p -> p -> () #
data T_IdempotentMonoid_1058 #
Constructors
| C_IdempotentMonoid'46'constructor_19753 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsIdempotentMonoid_796 |
d_Carrier_1074 :: T_IdempotentMonoid_1058 -> () #
d__'8776'__1076 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> () #
d__'8729'__1078 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_1086 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_idem_1088 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny #
d_identity'691'_1092 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny #
d_identity'737'_1094 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_1104 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> T_IsPartialEquivalence_16 #
d_isUnitalMagma_1108 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> T_IsUnitalMagma_642 #
d_refl_1110 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny #
d_reflexive_1112 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1112 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_1114 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> T_Setoid_44 #
d_sym_1116 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1118 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1120 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1122 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1122 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1124 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1124 :: T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d__'8777'__1130 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> AgdaAny -> AgdaAny -> () #
d_magma_1132 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> T_Magma_68 #
d_band_1142 :: T_Level_18 -> T_Level_18 -> T_IdempotentMonoid_1058 -> T_Band_596 #
d_IdempotentCommutativeMonoid_1148 :: p -> p -> () #
d__'8776'__1166 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> () #
d_isIdempotentCommutativeMonoid_1172 :: T_IdempotentCommutativeMonoid_1148 -> T_IsIdempotentCommutativeMonoid_852 #
d_assoc_1176 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_1178 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_1184 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny #
d_identity'737'_1186 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny #
d_isCommutativeBand_1190 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeBand_590 #
d_isCommutativeMagma_1192 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_1196 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeSemigroup_548 #
du_isCommutativeSemigroup_1196 :: T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeSemigroup_548 #
d_isIdempotentMonoid_1200 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsIdempotentMonoid_796 #
d_isPartialEquivalence_1206 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsPartialEquivalence_16 #
d_isUnitalMagma_1210 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsUnitalMagma_642 #
d_reflexive_1214 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1214 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_1218 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1220 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1222 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1224 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1224 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1226 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1226 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_commutativeMonoid_1228 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962 #
d_idempotentMonoid_1230 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentMonoid_1058 #
d_commutativeBand_1232 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeBand_732 #
d__'8777'__1236 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> () #
d_commutativeMagma_1238 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMagma_180 #
d_commutativeSemigroup_1240 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeSemigroup_662 #
d_rawMagma_1246 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_RawMagma_36 #
d_rawMonoid_1248 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_RawMonoid_64 #
d_semigroup_1250 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_Semigroup_536 #
d_unitalMagma_1252 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_UnitalMagma_814 #
d_BoundedLattice_1258 :: T_Level_18 -> T_Level_18 -> () #
d__'8776'__1270 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> () #
d__'8777'__1272 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> () #
d_assoc_1276 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_1280 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny #
d_commutativeBand_1282 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeBand_732 #
d_commutativeMagma_1284 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMagma_180 #
d_commutativeMonoid_1286 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_1288 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeSemigroup_662 #
d_idempotentMonoid_1292 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentMonoid_1058 #
d_identity'691'_1296 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny #
d_identity'737'_1298 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny #
d_isCommutativeBand_1302 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeBand_590 #
d_isCommutativeMagma_1304 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_1308 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeSemigroup_548 #
du_isCommutativeSemigroup_1308 :: T_IdempotentCommutativeMonoid_1148 -> T_IsCommutativeSemigroup_548 #
d_isIdempotentCommutativeMonoid_1312 :: T_IdempotentCommutativeMonoid_1148 -> T_IsIdempotentCommutativeMonoid_852 #
d_isIdempotentMonoid_1314 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsIdempotentMonoid_796 #
d_isPartialEquivalence_1320 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsPartialEquivalence_16 #
d_isUnitalMagma_1324 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IsUnitalMagma_642 #
d_rawMagma_1330 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_RawMagma_36 #
d_rawMonoid_1332 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_RawMonoid_64 #
d_reflexive_1336 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1336 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_semigroup_1338 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_Semigroup_536 #
d_sym_1342 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1344 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unitalMagma_1346 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_UnitalMagma_814 #
d_'8729''45'cong_1350 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1352 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1352 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1354 :: T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1354 :: T_IdempotentCommutativeMonoid_1148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_InvertibleMagma_1360 :: p -> p -> () #
data T_InvertibleMagma_1360 #
Constructors
| C_InvertibleMagma'46'constructor_24127 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny (AgdaAny -> AgdaAny) T_IsInvertibleMagma_924 |
d_Carrier_1378 :: T_InvertibleMagma_1360 -> () #
d__'8776'__1380 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> () #
d__'8729'__1382 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny #
d_inverse'691'_1394 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny #
d_inverse'737'_1396 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_1402 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> T_IsPartialEquivalence_16 #
d_refl_1404 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny #
d_reflexive_1406 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1406 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_1408 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> T_Setoid_44 #
d_sym_1410 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1412 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8315''185''45'cong_1414 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1416 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1418 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1418 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1420 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1420 :: T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_1422 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> T_Magma_68 #
d__'8777'__1426 :: T_Level_18 -> T_Level_18 -> T_InvertibleMagma_1360 -> AgdaAny -> AgdaAny -> () #
d_InvertibleUnitalMagma_1434 :: p -> p -> () #
data T_InvertibleUnitalMagma_1434 #
Constructors
| C_InvertibleUnitalMagma'46'constructor_25619 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny (AgdaAny -> AgdaAny) T_IsInvertibleUnitalMagma_976 |
d_Carrier_1452 :: T_InvertibleUnitalMagma_1434 -> () #
d__'8776'__1454 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> () #
d__'8729'__1456 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_1468 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny #
d_identity'737'_1470 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny #
d_inverse'691'_1474 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny #
d_inverse'737'_1476 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_1484 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> T_IsPartialEquivalence_16 #
d_isUnitalMagma_1486 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> T_IsUnitalMagma_642 #
d_reflexive_1490 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1490 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_1494 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1496 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8315''185''45'cong_1498 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1500 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1502 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1502 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1504 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1504 :: T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_invertibleMagma_1506 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> T_InvertibleMagma_1360 #
d__'8777'__1510 :: T_Level_18 -> T_Level_18 -> T_InvertibleUnitalMagma_1434 -> AgdaAny -> AgdaAny -> () #
d_Group_1520 :: p -> p -> () #
data T_Group_1520 #
Constructors
| C_Group'46'constructor_27303 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny (AgdaAny -> AgdaAny) T_IsGroup_1036 |
d_Carrier_1538 :: T_Group_1520 -> () #
d__'8776'__1540 :: T_Group_1520 -> AgdaAny -> AgdaAny -> () #
d__'8729'__1542 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_1544 :: T_Group_1520 -> AgdaAny #
d__'8315''185'_1546 :: T_Group_1520 -> AgdaAny -> AgdaAny #
d__'45'__1552 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'45'__1552 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__1554 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'47''47'__1554 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__1556 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'92''92'__1556 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_1558 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity_1560 :: T_Group_1520 -> T_Σ_14 #
d_identity'691'_1562 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny #
du_identity'691'_1562 :: T_Group_1520 -> AgdaAny -> AgdaAny #
d_identity'737'_1564 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny #
du_identity'737'_1564 :: T_Group_1520 -> AgdaAny -> AgdaAny #
d_inverse_1566 :: T_Group_1520 -> T_Σ_14 #
d_inverse'691'_1568 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny #
du_inverse'691'_1568 :: T_Group_1520 -> AgdaAny -> AgdaAny #
d_inverse'737'_1570 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny #
du_inverse'737'_1570 :: T_Group_1520 -> AgdaAny -> AgdaAny #
d_isInvertibleUnitalMagma_1576 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_IsInvertibleUnitalMagma_976 #
d_isPartialEquivalence_1582 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_IsPartialEquivalence_16 #
d_refl_1588 :: T_Group_1520 -> AgdaAny -> AgdaAny #
d_reflexive_1590 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1590 :: T_Group_1520 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_1592 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Setoid_44 #
d_sym_1594 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1596 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'691''45''8315''185'_1598 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'691''45''8315''185'_1598 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'737''45''8315''185'_1600 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'737''45''8315''185'_1600 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8315''185''45'cong_1602 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1604 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1606 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1606 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1608 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1608 :: T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_rawGroup_1610 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_RawGroup_96 #
d_monoid_1612 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Monoid_882 #
d__'8777'__1616 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> AgdaAny -> AgdaAny -> () #
d_magma_1618 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Magma_68 #
du_magma_1618 :: T_Group_1520 -> T_Magma_68 #
d_rawMagma_1620 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_RawMagma_36 #
d_rawMonoid_1622 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_RawMonoid_64 #
d_semigroup_1624 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Semigroup_536 #
d_unitalMagma_1626 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_UnitalMagma_814 #
d_invertibleUnitalMagma_1630 :: T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_InvertibleUnitalMagma_1434 #
d_AbelianGroup_1636 :: p -> p -> () #
data T_AbelianGroup_1636 #
Constructors
| C_AbelianGroup'46'constructor_29855 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny (AgdaAny -> AgdaAny) T_IsAbelianGroup_1132 |
d_Carrier_1654 :: T_AbelianGroup_1636 -> () #
d__'8776'__1656 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> () #
d__'8729'__1658 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_1660 :: T_AbelianGroup_1636 -> AgdaAny #
d__'47''47'__1668 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'47''47'__1668 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny #
d_assoc_1670 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_1672 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_1676 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny #
d_identity'737'_1678 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny #
d_inverse'691'_1682 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny #
d_inverse'737'_1684 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_1686 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_IsCommutativeMagma_212 #
d_isCommutativeMonoid_1688 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_1690 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_IsCommutativeSemigroup_548 #
d_isInvertibleMagma_1696 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_IsInvertibleMagma_924 #
d_isInvertibleUnitalMagma_1698 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_IsInvertibleUnitalMagma_976 #
d_isPartialEquivalence_1704 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_IsPartialEquivalence_16 #
d_refl_1710 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny #
d_reflexive_1712 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1712 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_1714 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_Setoid_44 #
d_sym_1716 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1718 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'691''45''8315''185'_1720 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'691''45''8315''185'_1720 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'737''45''8315''185'_1722 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'737''45''8315''185'_1722 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8315''185''45'cong_1724 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1726 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1728 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1728 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1730 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1730 :: T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_group_1732 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_Group_1520 #
d__'8777'__1736 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> AgdaAny -> AgdaAny -> () #
d_invertibleMagma_1738 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_InvertibleMagma_1360 #
d_invertibleUnitalMagma_1740 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_InvertibleUnitalMagma_1434 #
d_magma_1742 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_Magma_68 #
d_monoid_1744 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_Monoid_882 #
d_rawGroup_1746 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_RawGroup_96 #
d_rawMagma_1748 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_RawMagma_36 #
d_commutativeMonoid_1754 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_CommutativeMonoid_962 #
d_commutativeMagma_1758 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_CommutativeMagma_180 #
d_commutativeSemigroup_1760 :: T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_CommutativeSemigroup_662 #
d_NearSemiring_1766 :: p -> p -> () #
data T_NearSemiring_1766 #
Constructors
| C_NearSemiring'46'constructor_32269 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsNearSemiring_1218 |
d_Carrier_1784 :: T_NearSemiring_1766 -> () #
d__'8776'__1786 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> () #
d__'43'__1788 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__1790 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'assoc_1798 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_1800 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1802 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1802 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1804 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1804 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'isSemigroup_1808 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_IsSemigroup_472 #
d_assoc_1810 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_1812 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1814 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1814 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1816 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1816 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_1820 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny #
d_identity'737'_1822 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny #
d_distrib'691'_1832 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_1836 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_IsPartialEquivalence_16 #
d_refl_1838 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny #
d_reflexive_1840 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1840 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_1842 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_Setoid_44 #
d_sym_1844 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1846 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'737'_1848 :: T_NearSemiring_1766 -> AgdaAny -> AgdaAny #
d_rawNearSemiring_1850 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_RawNearSemiring_134 #
d__'8777'__1856 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> AgdaAny -> AgdaAny -> () #
d_magma_1858 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_Magma_68 #
d_rawMagma_1860 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_RawMagma_36 #
d_magma_1872 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_Magma_68 #
d_rawMagma_1874 :: T_Level_18 -> T_Level_18 -> T_NearSemiring_1766 -> T_RawMagma_36 #
d_SemiringWithoutOne_1880 :: p -> p -> () #
data T_SemiringWithoutOne_1880 #
Constructors
| C_SemiringWithoutOne'46'constructor_34609 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsSemiringWithoutOne_1298 |
d_Carrier_1898 :: T_SemiringWithoutOne_1880 -> () #
d__'8776'__1900 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> () #
d__'43'__1902 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__1904 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'8776'__1912 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> () #
d__'8777'__1914 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> () #
d_'42''45'assoc_1916 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_1918 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_1920 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_1920 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_1922 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_1922 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'isSemigroup_1926 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_IsSemigroup_472 #
d_comm_1928 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_1930 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_1934 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_IsCommutativeSemigroup_548 #
d_Carrier_1938 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> () #
d_isEquivalence_1942 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_IsEquivalence_26 #
d_isNearSemiring_1944 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_1946 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_IsPartialEquivalence_16 #
d_partialSetoid_1948 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_PartialSetoid_10 #
d_refl_1950 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny #
du_refl_1950 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny #
d_reflexive_1952 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_1952 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_1956 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_sym_1956 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_1958 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_trans_1958 :: T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_1962 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny #
d_zero'737'_1964 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> AgdaAny -> AgdaAny #
d_nearSemiring_1966 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_NearSemiring_1766 #
d_magma_1970 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_Magma_68 #
d_'42''45'semigroup_1974 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_Semigroup_536 #
d_magma_1976 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_Magma_68 #
d_rawNearSemiring_1988 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_RawNearSemiring_134 #
d_'43''45'commutativeMonoid_1990 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_CommutativeMonoid_962 #
d_commutativeMagma_1994 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_CommutativeMagma_180 #
d_commutativeSemigroup_1996 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutOne_1880 -> T_CommutativeSemigroup_662 #
d_CommutativeSemiringWithoutOne_2002 :: p -> p -> () #
data T_CommutativeSemiringWithoutOne_2002 #
Constructors
| C_CommutativeSemiringWithoutOne'46'constructor_36869 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsCommutativeSemiringWithoutOne_1382 |
d__'8776'__2022 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> () #
d_isCommutativeSemiringWithoutOne_2030 :: T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeSemiringWithoutOne_1382 #
d__'8776'__2034 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> () #
d__'8777'__2036 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> () #
d_'42''45'assoc_2038 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_2042 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2044 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2044 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2046 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2046 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2048 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeMagma_212 #
d_'42''45'isCommutativeSemigroup_2050 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeSemigroup_548 #
du_'42''45'isCommutativeSemigroup_2050 :: T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeSemigroup_548 #
d_'42''45'isMagma_2052 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsMagma_176 #
d_'42''45'isSemigroup_2054 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsSemigroup_472 #
d_isCommutativeMagma_2058 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeMagma_212 #
d_'43''45'isCommutativeMonoid_2060 :: T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_2062 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeSemigroup_548 #
du_isCommutativeSemigroup_2062 :: T_CommutativeSemiringWithoutOne_2002 -> T_IsCommutativeSemigroup_548 #
d_Carrier_2066 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> () #
d_isEquivalence_2070 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsEquivalence_26 #
d_isNearSemiring_2072 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_2074 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_IsPartialEquivalence_16 #
d_isSemiringWithoutOne_2076 :: T_CommutativeSemiringWithoutOne_2002 -> T_IsSemiringWithoutOne_1298 #
d_partialSetoid_2078 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_PartialSetoid_10 #
d_refl_2080 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny #
d_reflexive_2082 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_2082 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_2086 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_sym_2086 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_2088 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_trans_2088 :: T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_2092 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny #
d_zero'737'_2094 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> AgdaAny -> AgdaAny #
d_semiringWithoutOne_2096 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_SemiringWithoutOne_1880 #
d_rawMagma_2102 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_RawMagma_36 #
d_'42''45'semigroup_2104 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_Semigroup_536 #
d_'43''45'commutativeMonoid_2106 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_CommutativeMonoid_962 #
du_'43''45'commutativeMonoid_2106 :: T_CommutativeSemiringWithoutOne_2002 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_2108 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_CommutativeSemigroup_662 #
du_commutativeSemigroup_2108 :: T_CommutativeSemiringWithoutOne_2002 -> T_CommutativeSemigroup_662 #
d_'43''45'monoid_2112 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_Monoid_882 #
d_rawMagma_2114 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_RawMagma_36 #
d_rawMonoid_2116 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_RawMonoid_64 #
d_semigroup_2118 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_Semigroup_536 #
d_unitalMagma_2120 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_UnitalMagma_814 #
d_nearSemiring_2122 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_NearSemiring_1766 #
d_rawNearSemiring_2124 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiringWithoutOne_2002 -> T_RawNearSemiring_134 #
d_SemiringWithoutAnnihilatingZero_2130 :: p -> p -> () #
d__'8776'__2152 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> () #
d_isSemiringWithoutAnnihilatingZero_2162 :: T_SemiringWithoutAnnihilatingZero_2130 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_'42''45'assoc_2166 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_2168 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2170 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2170 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2172 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2172 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2176 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny #
d_identity'737'_2178 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny #
d_'42''45'isMagma_2180 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsMagma_176 #
d_'42''45'isMonoid_2182 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsMonoid_686 #
d_'42''45'isSemigroup_2184 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsSemigroup_472 #
d_assoc_2186 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_2190 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2192 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2192 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2194 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2194 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2198 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny #
d_identity'737'_2200 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2202 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsCommutativeMagma_212 #
d_'43''45'isCommutativeMonoid_2204 :: T_SemiringWithoutAnnihilatingZero_2130 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_2206 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsCommutativeSemigroup_548 #
du_isCommutativeSemigroup_2206 :: T_SemiringWithoutAnnihilatingZero_2130 -> T_IsCommutativeSemigroup_548 #
d_isUnitalMagma_2214 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsUnitalMagma_642 #
d_distrib'691'_2218 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_2218 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_2220 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_2220 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_2224 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_IsPartialEquivalence_16 #
du_isPartialEquivalence_2224 :: T_SemiringWithoutAnnihilatingZero_2130 -> T_IsPartialEquivalence_16 #
d_reflexive_2228 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_2228 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_2230 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_Setoid_44 #
d_sym_2232 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_2234 :: T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_rawSemiring_2236 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_RawSemiring_174 #
d_rawNearSemiring_2240 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_RawNearSemiring_134 #
d_'43''45'commutativeMonoid_2242 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_CommutativeMonoid_962 #
du_'43''45'commutativeMonoid_2242 :: T_SemiringWithoutAnnihilatingZero_2130 -> T_CommutativeMonoid_962 #
d__'8777'__2246 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> AgdaAny -> AgdaAny -> () #
d_commutativeMagma_2248 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_CommutativeMagma_180 #
d_commutativeSemigroup_2250 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_CommutativeSemigroup_662 #
du_commutativeSemigroup_2250 :: T_SemiringWithoutAnnihilatingZero_2130 -> T_CommutativeSemigroup_662 #
d_monoid_2254 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_Monoid_882 #
d_rawMagma_2256 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_RawMagma_36 #
d_rawMonoid_2258 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_RawMonoid_64 #
d_semigroup_2260 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_Semigroup_536 #
d_unitalMagma_2262 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_UnitalMagma_814 #
d_'42''45'monoid_2264 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_Monoid_882 #
d_rawMagma_2270 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_RawMagma_36 #
d_rawMonoid_2272 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_RawMonoid_64 #
d_semigroup_2274 :: T_Level_18 -> T_Level_18 -> T_SemiringWithoutAnnihilatingZero_2130 -> T_Semigroup_536 #
d_Semiring_2280 :: p -> p -> () #
data T_Semiring_2280 #
Constructors
| C_Semiring'46'constructor_41765 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsSemiring_1570 |
d_Carrier_2300 :: T_Semiring_2280 -> () #
d__'8776'__2302 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> () #
d__'43'__2304 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__2306 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny #
d_0'35'_2308 :: T_Semiring_2280 -> AgdaAny #
d_1'35'_2310 :: T_Semiring_2280 -> AgdaAny #
d_'42''45'assoc_2316 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_2318 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2320 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2320 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2322 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2322 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2326 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny #
du_identity'691'_2326 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_identity'737'_2328 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny #
du_identity'737'_2328 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_assoc_2336 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_2338 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_2340 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2342 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2342 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2344 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2344 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2348 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny #
du_identity'691'_2348 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_identity'737'_2350 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny #
du_identity'737'_2350 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2352 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_2356 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_IsCommutativeSemigroup_548 #
d_distrib_2366 :: T_Semiring_2280 -> T_Σ_14 #
d_distrib'691'_2368 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_2368 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_2370 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_2370 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_2376 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_IsPartialEquivalence_16 #
d_isSemiringWithoutAnnihilatingZero_2378 :: T_Semiring_2280 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_2380 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_IsSemiringWithoutOne_1298 #
d_refl_2382 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_reflexive_2384 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_2384 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_2386 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_Setoid_44 #
d_sym_2388 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_2390 :: T_Semiring_2280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero_2392 :: T_Semiring_2280 -> T_Σ_14 #
d_zero'691'_2394 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny #
du_zero'691'_2394 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_zero'737'_2396 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny #
du_zero'737'_2396 :: T_Semiring_2280 -> AgdaAny -> AgdaAny #
d_semiringWithoutAnnihilatingZero_2398 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_SemiringWithoutAnnihilatingZero_2130 #
du_semiringWithoutAnnihilatingZero_2398 :: T_Semiring_2280 -> T_SemiringWithoutAnnihilatingZero_2130 #
d__'8777'__2402 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> AgdaAny -> AgdaAny -> () #
d_magma_2404 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_Magma_68 #
d_rawMagma_2408 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_RawMagma_36 #
d_rawMonoid_2410 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_RawMonoid_64 #
d_semigroup_2412 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_Semigroup_536 #
d_'43''45'commutativeMonoid_2416 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_2418 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_CommutativeSemigroup_662 #
d_magma_2420 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_Magma_68 #
d_monoid_2422 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_Monoid_882 #
d_rawMagma_2424 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_RawMagma_36 #
d_rawMonoid_2426 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_RawMonoid_64 #
d_semigroup_2428 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_Semigroup_536 #
d_semiringWithoutOne_2436 :: T_Level_18 -> T_Level_18 -> T_Semiring_2280 -> T_SemiringWithoutOne_1880 #
d_CommutativeSemiring_2446 :: p -> p -> () #
data T_CommutativeSemiring_2446 #
Constructors
| C_CommutativeSemiring'46'constructor_44731 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsCommutativeSemiring_1678 |
d_Carrier_2466 :: T_CommutativeSemiring_2446 -> () #
d__'8776'__2468 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> () #
d__'43'__2470 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__2472 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'assoc_2482 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'comm_2484 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_2486 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2488 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2488 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2490 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2490 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2494 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d_identity'737'_2496 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2498 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsCommutativeMagma_212 #
d_'42''45'isCommutativeMonoid_2500 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsCommutativeMonoid_736 #
d_'42''45'isCommutativeSemigroup_2502 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsCommutativeSemigroup_548 #
du_'42''45'isCommutativeSemigroup_2502 :: T_CommutativeSemiring_2446 -> T_IsCommutativeSemigroup_548 #
d_'42''45'isMonoid_2506 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsMonoid_686 #
d_'42''45'isSemigroup_2508 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsSemigroup_472 #
d_assoc_2510 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_2512 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_2514 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2516 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2516 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2518 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2518 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2522 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d_identity'737'_2524 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2526 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_2530 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsCommutativeSemigroup_548 #
d_isUnitalMagma_2538 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsUnitalMagma_642 #
d_distrib'691'_2542 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_2542 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_2544 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_2544 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isCommutativeSemiringWithoutOne_2546 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsCommutativeSemiringWithoutOne_1382 #
du_isCommutativeSemiringWithoutOne_2546 :: T_CommutativeSemiring_2446 -> T_IsCommutativeSemiringWithoutOne_1382 #
d_isNearSemiring_2550 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_2552 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsPartialEquivalence_16 #
d_isSemiringWithoutAnnihilatingZero_2556 :: T_CommutativeSemiring_2446 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_2558 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_IsSemiringWithoutOne_1298 #
d_refl_2560 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d_reflexive_2562 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_2562 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_2566 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_2568 :: T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_2572 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d_zero'737'_2574 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny #
d__'8777'__2580 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> AgdaAny -> AgdaAny -> () #
d_commutativeMagma_2592 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeMagma_180 #
d_'43''45'commutativeMonoid_2594 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_2596 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeSemigroup_662 #
d_nearSemiring_2610 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_NearSemiring_1766 #
d_semiringWithoutAnnihilatingZero_2614 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_SemiringWithoutAnnihilatingZero_2130 #
du_semiringWithoutAnnihilatingZero_2614 :: T_CommutativeSemiring_2446 -> T_SemiringWithoutAnnihilatingZero_2130 #
d_semiringWithoutOne_2616 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_SemiringWithoutOne_1880 #
d_'42''45'commutativeMonoid_2618 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeMonoid_962 #
d_commutativeMagma_2622 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeMagma_180 #
d_commutativeSemigroup_2624 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeSemigroup_662 #
d_commutativeSemiringWithoutOne_2626 :: T_Level_18 -> T_Level_18 -> T_CommutativeSemiring_2446 -> T_CommutativeSemiringWithoutOne_2002 #
du_commutativeSemiringWithoutOne_2626 :: T_CommutativeSemiring_2446 -> T_CommutativeSemiringWithoutOne_2002 #
d_CancellativeCommutativeSemiring_2632 :: p -> p -> () #
d__'8776'__2654 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> () #
d_isCancellativeCommutativeSemiring_2664 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCancellativeCommutativeSemiring_1798 #
d_'42''45'assoc_2668 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cancel'691''45'nonZero_2670 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny #
du_'42''45'cancel'691''45'nonZero_2670 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny #
d_'42''45'cancel'737''45'nonZero_2672 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny #
d_'42''45'cong_2676 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2678 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2678 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2680 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2680 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2684 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny #
d_identity'737'_2686 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2688 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeMagma_212 #
d_'42''45'isCommutativeMonoid_2690 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeMonoid_736 #
du_'42''45'isCommutativeMonoid_2690 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeMonoid_736 #
d_'42''45'isCommutativeSemigroup_2692 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemigroup_548 #
du_'42''45'isCommutativeSemigroup_2692 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemigroup_548 #
d_'42''45'isMagma_2694 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsMagma_176 #
d_'42''45'isMonoid_2696 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsMonoid_686 #
d_'42''45'isSemigroup_2698 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsSemigroup_472 #
d_assoc_2700 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_2704 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2706 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2706 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2708 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2708 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2712 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny #
d_identity'737'_2714 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_2716 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeMagma_212 #
d_'43''45'isCommutativeMonoid_2718 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_2720 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemigroup_548 #
du_isCommutativeSemigroup_2720 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemigroup_548 #
d_isUnitalMagma_2728 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsUnitalMagma_642 #
d_distrib'691'_2732 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_2732 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_2734 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_2734 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isCommutativeSemiring_2736 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemiring_1678 #
d_isCommutativeSemiringWithoutOne_2738 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemiringWithoutOne_1382 #
du_isCommutativeSemiringWithoutOne_2738 :: T_CancellativeCommutativeSemiring_2632 -> T_IsCommutativeSemiringWithoutOne_1382 #
d_isNearSemiring_2742 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_2744 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsPartialEquivalence_16 #
du_isPartialEquivalence_2744 :: T_CancellativeCommutativeSemiring_2632 -> T_IsPartialEquivalence_16 #
d_isSemiringWithoutAnnihilatingZero_2748 :: T_CancellativeCommutativeSemiring_2632 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_2750 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_IsSemiringWithoutOne_1298 #
du_isSemiringWithoutOne_2750 :: T_CancellativeCommutativeSemiring_2632 -> T_IsSemiringWithoutOne_1298 #
d_reflexive_2754 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_2754 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_2756 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_Setoid_44 #
d_sym_2758 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_2760 :: T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_2764 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny #
d_zero'737'_2766 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny #
d_commutativeSemiring_2768 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeSemiring_2446 #
du_commutativeSemiring_2768 :: T_CancellativeCommutativeSemiring_2632 -> T_CommutativeSemiring_2446 #
d__'8777'__2772 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> AgdaAny -> AgdaAny -> () #
d_commutativeMagma_2774 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeMagma_180 #
d_'42''45'commutativeMonoid_2776 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeMonoid_962 #
du_'42''45'commutativeMonoid_2776 :: T_CancellativeCommutativeSemiring_2632 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_2778 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeSemigroup_662 #
du_commutativeSemigroup_2778 :: T_CancellativeCommutativeSemiring_2632 -> T_CommutativeSemigroup_662 #
d_'42''45'monoid_2782 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_Monoid_882 #
d_rawMagma_2784 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_RawMagma_36 #
d_rawMonoid_2786 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_RawMonoid_64 #
d_semigroup_2788 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_Semigroup_536 #
d_commutativeMagma_2790 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeMagma_180 #
d_'43''45'commutativeMonoid_2792 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeMonoid_962 #
du_'43''45'commutativeMonoid_2792 :: T_CancellativeCommutativeSemiring_2632 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_2794 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_CommutativeSemigroup_662 #
du_commutativeSemigroup_2794 :: T_CancellativeCommutativeSemiring_2632 -> T_CommutativeSemigroup_662 #
d_monoid_2798 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_Monoid_882 #
d_rawMagma_2800 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_RawMagma_36 #
d_rawMonoid_2802 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_RawMonoid_64 #
d_semigroup_2804 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_Semigroup_536 #
d_unitalMagma_2806 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_UnitalMagma_814 #
d_nearSemiring_2808 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_NearSemiring_1766 #
d_rawSemiring_2810 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_RawSemiring_174 #
d_semiring_2812 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_Semiring_2280 #
d_semiringWithoutAnnihilatingZero_2814 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_SemiringWithoutAnnihilatingZero_2130 #
du_semiringWithoutAnnihilatingZero_2814 :: T_CancellativeCommutativeSemiring_2632 -> T_SemiringWithoutAnnihilatingZero_2130 #
d_semiringWithoutOne_2816 :: T_Level_18 -> T_Level_18 -> T_CancellativeCommutativeSemiring_2632 -> T_SemiringWithoutOne_1880 #
d_IdempotentSemiring_2822 :: p -> p -> () #
data T_IdempotentSemiring_2822 #
Constructors
| C_IdempotentSemiring'46'constructor_51015 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsIdempotentSemiring_1922 |
d_Carrier_2842 :: T_IdempotentSemiring_2822 -> () #
d__'8776'__2844 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> () #
d__'43'__2846 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__2848 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'assoc_2858 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_2860 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2862 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2862 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2864 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2864 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2868 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d_identity'737'_2870 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d_'42''45'isMonoid_2874 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsMonoid_686 #
d_'42''45'isSemigroup_2876 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsSemigroup_472 #
d_assoc_2878 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_2880 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_2882 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_2884 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_2884 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_2886 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_2886 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_2892 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d_identity'737'_2894 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d_isCommutativeBand_2898 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsCommutativeBand_590 #
d_isCommutativeMagma_2900 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_2904 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsCommutativeSemigroup_548 #
d_'43''45'isIdempotentCommutativeMonoid_2906 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsIdempotentCommutativeMonoid_852 #
du_'43''45'isIdempotentCommutativeMonoid_2906 :: T_IdempotentSemiring_2822 -> T_IsIdempotentCommutativeMonoid_852 #
d_isIdempotentMonoid_2908 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsIdempotentMonoid_796 #
d_isUnitalMagma_2916 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsUnitalMagma_642 #
d_distrib'691'_2920 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_2920 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_2922 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_2922 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isNearSemiring_2926 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_2928 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsPartialEquivalence_16 #
d_isSemiringWithoutAnnihilatingZero_2932 :: T_IdempotentSemiring_2822 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_2934 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IsSemiringWithoutOne_1298 #
d_refl_2936 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d_reflexive_2938 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_2938 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_2942 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_2944 :: T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_2948 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d_zero'737'_2950 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny #
d__'8777'__2956 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> AgdaAny -> AgdaAny -> () #
d_magma_2958 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_Magma_68 #
d_commutativeMagma_2968 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_CommutativeMagma_180 #
d_'43''45'commutativeMonoid_2970 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_2972 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_CommutativeSemigroup_662 #
d_magma_2974 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_Magma_68 #
d_nearSemiring_2986 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_NearSemiring_1766 #
d_semiringWithoutAnnihilatingZero_2990 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_SemiringWithoutAnnihilatingZero_2130 #
du_semiringWithoutAnnihilatingZero_2990 :: T_IdempotentSemiring_2822 -> T_SemiringWithoutAnnihilatingZero_2130 #
d_semiringWithoutOne_2992 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_SemiringWithoutOne_1880 #
d_'43''45'idempotentCommutativeMonoid_2994 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IdempotentCommutativeMonoid_1148 #
du_'43''45'idempotentCommutativeMonoid_2994 :: T_IdempotentSemiring_2822 -> T_IdempotentCommutativeMonoid_1148 #
d_band_2998 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_Band_596 #
d_commutativeBand_3000 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_CommutativeBand_732 #
d_idempotentMonoid_3002 :: T_Level_18 -> T_Level_18 -> T_IdempotentSemiring_2822 -> T_IdempotentMonoid_1058 #
d_KleeneAlgebra_3008 :: p -> p -> () #
data T_KleeneAlgebra_3008 #
d_Carrier_3030 :: T_KleeneAlgebra_3008 -> () #
d__'8776'__3032 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> () #
d__'43'__3034 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__3036 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'8902'_3038 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_'42''45'assoc_3048 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_3050 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3052 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3052 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3054 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3054 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3058 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_identity'737'_3060 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_'42''45'isSemigroup_3066 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsSemigroup_472 #
d_assoc_3068 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_3070 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_3072 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3074 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3074 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3076 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3076 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3082 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_identity'737'_3084 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_isBand_3086 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsBand_508 #
d_isCommutativeBand_3088 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsCommutativeBand_590 #
d_isCommutativeMagma_3090 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsCommutativeMagma_212 #
d_isCommutativeSemigroup_3094 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsCommutativeSemigroup_548 #
d_'43''45'isIdempotentCommutativeMonoid_3096 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsIdempotentCommutativeMonoid_852 #
du_'43''45'isIdempotentCommutativeMonoid_3096 :: T_KleeneAlgebra_3008 -> T_IsIdempotentCommutativeMonoid_852 #
d_isIdempotentMonoid_3098 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsIdempotentMonoid_796 #
d_distrib'691'_3110 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_3110 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_3112 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_3112 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isNearSemiring_3118 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_3120 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsPartialEquivalence_16 #
d_isSemiringWithoutAnnihilatingZero_3124 :: T_KleeneAlgebra_3008 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_3126 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IsSemiringWithoutOne_1298 #
d_refl_3128 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_reflexive_3130 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_3130 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_3132 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_Setoid_44 #
d_starDestructive'691'_3136 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_starDestructive'691'_3136 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_starDestructive'737'_3138 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_starDestructive'737'_3138 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_starExpansive'691'_3142 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_starExpansive'737'_3144 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_sym_3146 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_3148 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_3152 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
du_zero'691'_3152 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_zero'737'_3154 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
du_zero'737'_3154 :: T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny #
d_idempotentSemiring_3156 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_IdempotentSemiring_2822 #
d__'8777'__3160 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> AgdaAny -> AgdaAny -> () #
d_magma_3162 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_Magma_68 #
d_commutativeMagma_3172 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_CommutativeMagma_180 #
d_'43''45'commutativeMonoid_3174 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_3176 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_CommutativeSemigroup_662 #
d_magma_3178 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_Magma_68 #
d_monoid_3180 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_Monoid_882 #
d_semiringWithoutAnnihilatingZero_3196 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_SemiringWithoutAnnihilatingZero_2130 #
du_semiringWithoutAnnihilatingZero_3196 :: T_KleeneAlgebra_3008 -> T_SemiringWithoutAnnihilatingZero_2130 #
d_semiringWithoutOne_3198 :: T_Level_18 -> T_Level_18 -> T_KleeneAlgebra_3008 -> T_SemiringWithoutOne_1880 #
d_Quasiring_3204 :: p -> p -> () #
data T_Quasiring_3204 #
Constructors
| C_Quasiring'46'constructor_57285 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsQuasiring_2180 |
d_Carrier_3224 :: T_Quasiring_3204 -> () #
d__'8776'__3226 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> () #
d__'43'__3228 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__3230 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny #
d_0'35'_3232 :: T_Quasiring_3204 -> AgdaAny #
d_1'35'_3234 :: T_Quasiring_3204 -> AgdaAny #
d_'42''45'assoc_3240 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_3242 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3244 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3244 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3246 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3246 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3250 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_identity'691'_3250 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_identity'737'_3252 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_identity'737'_3252 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_assoc_3260 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_3262 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3264 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3264 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3266 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3266 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3270 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_identity'691'_3270 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_identity'737'_3272 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_identity'737'_3272 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_distrib'691'_3284 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_3284 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_3286 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_3286 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3288 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_identity'691'_3288 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_identity'737'_3290 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_identity'737'_3290 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_3294 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_IsPartialEquivalence_16 #
d_refl_3296 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_reflexive_3298 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_3298 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_3300 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_Setoid_44 #
d_sym_3302 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_3304 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero_3306 :: T_Quasiring_3204 -> T_Σ_14 #
d_zero'691'_3308 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_zero'691'_3308 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d_zero'737'_3310 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny #
du_zero'737'_3310 :: T_Quasiring_3204 -> AgdaAny -> AgdaAny #
d__'8777'__3316 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> AgdaAny -> AgdaAny -> () #
d_magma_3318 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_Magma_68 #
d_rawMagma_3320 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_RawMagma_36 #
d_rawMonoid_3322 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_RawMonoid_64 #
d_semigroup_3324 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_Semigroup_536 #
d_magma_3332 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_Magma_68 #
d_rawMagma_3334 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_RawMagma_36 #
d_rawMonoid_3336 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_RawMonoid_64 #
d_semigroup_3338 :: T_Level_18 -> T_Level_18 -> T_Quasiring_3204 -> T_Semigroup_536 #
d_RingWithoutOne_3344 :: p -> p -> () #
data T_RingWithoutOne_3344 #
d_Carrier_3364 :: T_RingWithoutOne_3344 -> () #
d__'8776'__3366 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> () #
d__'43'__3368 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__3370 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'45'__3372 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d__'47''47'__3380 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'47''47'__3380 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'assoc_3382 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_3384 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3386 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3386 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3388 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3388 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'isSemigroup_3392 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsSemigroup_472 #
d_assoc_3394 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_3396 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_3398 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3400 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3400 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3402 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3402 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3406 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_identity'737'_3408 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_3412 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsCommutativeMagma_212 #
d_isCommutativeMonoid_3414 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_3416 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsCommutativeSemigroup_548 #
d_isInvertibleMagma_3420 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsInvertibleMagma_924 #
d_isInvertibleUnitalMagma_3422 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsInvertibleUnitalMagma_976 #
d_'8315''185''45'cong_3432 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_inverse'691'_3436 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_inverse'737'_3438 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_distrib'691'_3442 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_3442 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_3444 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_3444 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_3448 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_IsPartialEquivalence_16 #
d_refl_3450 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_reflexive_3452 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_3452 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_3454 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_Setoid_44 #
d_sym_3456 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_3458 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'691''45''8315''185'_3460 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'691''45''8315''185'_3460 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'737''45''8315''185'_3462 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'737''45''8315''185'_3462 :: T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero_3464 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_Σ_14 #
d_zero'691'_3466 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_zero'737'_3468 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> AgdaAny -> AgdaAny #
d_'43''45'abelianGroup_3470 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_AbelianGroup_1636 #
d_group_3476 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_Group_1520 #
d_invertibleMagma_3478 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_InvertibleMagma_1360 #
d_invertibleUnitalMagma_3480 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_InvertibleUnitalMagma_1434 #
d_magma_3484 :: T_Level_18 -> T_Level_18 -> T_RingWithoutOne_3344 -> T_Magma_68 #
d_NonAssociativeRing_3492 :: p -> p -> () #
d_Carrier_3514 :: T_NonAssociativeRing_3492 -> () #
d__'8776'__3516 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> () #
d__'43'__3518 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__3520 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'45'__3522 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d__'47''47'__3532 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'47''47'__3532 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_3534 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3536 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3536 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3538 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3538 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'identity'691'_3542 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_'42''45'identity'737'_3544 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_'42''45'isUnitalMagma_3548 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsUnitalMagma_642 #
d_assoc_3550 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_3552 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_3554 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3556 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3556 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3558 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3558 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3562 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_identity'737'_3564 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_3568 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsCommutativeMagma_212 #
d_isCommutativeMonoid_3570 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_3572 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsCommutativeSemigroup_548 #
d_isInvertibleMagma_3576 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsInvertibleMagma_924 #
d_isInvertibleUnitalMagma_3578 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsInvertibleUnitalMagma_976 #
d_isUnitalMagma_3586 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsUnitalMagma_642 #
d_'8315''185''45'cong_3588 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_inverse'691'_3592 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_inverse'737'_3594 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_distrib'691'_3598 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_3598 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_3600 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_3600 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_3604 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_IsPartialEquivalence_16 #
d_refl_3606 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_reflexive_3608 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_3608 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_sym_3612 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_3614 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'691''45''8315''185'_3616 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'691''45''8315''185'_3616 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'737''45''8315''185'_3618 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'737''45''8315''185'_3618 :: T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero'691'_3622 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_zero'737'_3624 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> AgdaAny -> AgdaAny #
d_'43''45'abelianGroup_3626 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_AbelianGroup_1636 #
d_invertibleMagma_3632 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_InvertibleMagma_1360 #
d_invertibleUnitalMagma_3634 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_InvertibleUnitalMagma_1434 #
d_'42''45'unitalMagma_3636 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_UnitalMagma_814 #
d_identity_3640 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_Σ_14 #
d_magma_3642 :: T_Level_18 -> T_Level_18 -> T_NonAssociativeRing_3492 -> T_Magma_68 #
d_Nearring_3648 :: p -> p -> () #
data T_Nearring_3648 #
d_Carrier_3670 :: T_Nearring_3648 -> () #
d__'8776'__3672 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> () #
d__'43'__3674 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__3676 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'45'__3678 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_0'35'_3680 :: T_Nearring_3648 -> AgdaAny #
d_1'35'_3682 :: T_Nearring_3648 -> AgdaAny #
d_'42''45'assoc_3688 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_3690 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3692 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3692 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3694 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3694 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3698 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_identity'691'_3698 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_identity'737'_3700 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_identity'737'_3700 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_assoc_3708 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_3710 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3712 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3712 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3714 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3714 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3718 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_identity'691'_3718 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_identity'737'_3720 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_identity'737'_3720 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_'43''45'inverse'691'_3724 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_'43''45'inverse'737'_3726 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_distrib_3736 :: T_Nearring_3648 -> T_Σ_14 #
d_distrib'691'_3738 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_3738 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_3740 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_3740 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3742 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_identity'691'_3742 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_identity'737'_3744 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_identity'737'_3744 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_3748 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_IsPartialEquivalence_16 #
d_refl_3752 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_reflexive_3754 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_3754 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_3756 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_Setoid_44 #
d_sym_3758 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_3760 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero_3762 :: T_Nearring_3648 -> T_Σ_14 #
d_zero'691'_3764 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_zero'691'_3764 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_zero'737'_3766 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny #
du_zero'737'_3766 :: T_Nearring_3648 -> AgdaAny -> AgdaAny #
d_'8315''185''45'cong_3768 :: T_Nearring_3648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_quasiring_3770 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_Quasiring_3204 #
d__'8777'__3774 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> AgdaAny -> AgdaAny -> () #
d_magma_3776 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_Magma_68 #
d_rawMagma_3780 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_RawMagma_36 #
d_semigroup_3782 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_Semigroup_536 #
d_magma_3784 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_Magma_68 #
d_rawMagma_3788 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_RawMagma_36 #
d_rawMonoid_3790 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_RawMonoid_64 #
d_semigroup_3792 :: T_Level_18 -> T_Level_18 -> T_Nearring_3648 -> T_Semigroup_536 #
d_Ring_3800 :: p -> p -> () #
data T_Ring_3800 #
d_Carrier_3822 :: T_Ring_3800 -> () #
d__'8776'__3824 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> () #
d__'43'__3826 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__3828 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'45'__3830 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_0'35'_3832 :: T_Ring_3800 -> AgdaAny #
d_1'35'_3834 :: T_Ring_3800 -> AgdaAny #
d__'47''47'__3840 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'47''47'__3840 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'assoc_3842 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_3844 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3846 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3846 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3848 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3848 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_3852 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_identity'691'_3852 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_identity'737'_3854 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_identity'737'_3854 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_'42''45'isMagma_3856 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsMagma_176 #
d_assoc_3862 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_assoc_3862 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_3864 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny #
du_comm_3864 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_3866 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong_3866 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_3868 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_3868 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_3870 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_3870 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity_3872 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Σ_14 #
du_identity_3872 :: T_Ring_3800 -> T_Σ_14 #
d_identity'691'_3874 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_identity'691'_3874 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_identity'737'_3876 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_identity'737'_3876 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_isCommutativeMonoid_3882 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_3884 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsCommutativeSemigroup_548 #
d_isGroup_3886 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsGroup_1036 #
d_isInvertibleUnitalMagma_3890 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsInvertibleUnitalMagma_976 #
d_isMagma_3892 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsMagma_176 #
d_isMonoid_3894 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsMonoid_686 #
d_isSemigroup_3896 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsSemigroup_472 #
d_'8315''185''45'cong_3900 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8315''185''45'cong_3900 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_inverse_3902 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Σ_14 #
du_inverse_3902 :: T_Ring_3800 -> T_Σ_14 #
d_inverse'691'_3904 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_inverse'691'_3904 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_inverse'737'_3906 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_inverse'737'_3906 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_distrib_3908 :: T_Ring_3800 -> T_Σ_14 #
d_distrib'691'_3910 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_3910 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_3912 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_3912 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_3918 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsPartialEquivalence_16 #
d_isSemiring_3922 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsSemiring_1570 #
d_isSemiringWithoutAnnihilatingZero_3924 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
du_isSemiringWithoutAnnihilatingZero_3924 :: T_Ring_3800 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_3926 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_IsSemiringWithoutOne_1298 #
d_refl_3928 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_refl_3928 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_reflexive_3930 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_3930 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_3932 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Setoid_44 #
d_sym_3934 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_sym_3934 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_3936 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_trans_3936 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'691''45''8315''185'_3938 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'691''45''8315''185'_3938 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'737''45''8315''185'_3940 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'737''45''8315''185'_3940 :: T_Ring_3800 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero_3942 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Σ_14 #
du_zero_3942 :: T_Ring_3800 -> T_Σ_14 #
d_zero'691'_3944 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_zero'691'_3944 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_zero'737'_3946 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny #
du_zero'737'_3946 :: T_Ring_3800 -> AgdaAny -> AgdaAny #
d_semiring_3952 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Semiring_2280 #
d__'8777'__3956 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> AgdaAny -> AgdaAny -> () #
d_magma_3958 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Magma_68 #
du_magma_3958 :: T_Ring_3800 -> T_Magma_68 #
d_'42''45'monoid_3960 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Monoid_882 #
d_rawMagma_3962 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_RawMagma_36 #
d_rawMonoid_3964 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_RawMonoid_64 #
d_semigroup_3966 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Semigroup_536 #
d_'43''45'commutativeMonoid_3970 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_3972 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_CommutativeSemigroup_662 #
d_magma_3974 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Magma_68 #
du_magma_3974 :: T_Ring_3800 -> T_Magma_68 #
d_monoid_3976 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Monoid_882 #
d_rawMagma_3978 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_RawMagma_36 #
d_rawMonoid_3980 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_RawMonoid_64 #
d_semigroup_3982 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Semigroup_536 #
d_unitalMagma_3984 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_UnitalMagma_814 #
d_semiringWithoutAnnihilatingZero_3988 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_SemiringWithoutAnnihilatingZero_2130 #
d_group_3998 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Group_1520 #
d_invertibleUnitalMagma_4002 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_InvertibleUnitalMagma_1434 #
d_rawRing_4004 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_RawRing_268 #
d_'43''45'rawGroup_4008 :: T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_RawGroup_96 #
d_CommutativeRing_4016 :: p -> p -> () #
data T_CommutativeRing_4016 #
d_Carrier_4038 :: T_CommutativeRing_4016 -> () #
d__'8776'__4040 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> () #
d__'43'__4042 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'42'__4044 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'45'__4046 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d__'47''47'__4056 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
du__'47''47'__4056 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'assoc_4058 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'comm_4060 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'42''45'cong_4062 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4064 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4064 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4066 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4066 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_4070 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_identity'737'_4072 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_4074 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeMagma_212 #
d_'42''45'isCommutativeMonoid_4076 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeMonoid_736 #
d_'42''45'isCommutativeSemigroup_4078 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeSemigroup_548 #
d_'42''45'isSemigroup_4084 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsSemigroup_472 #
d_assoc_4086 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_assoc_4086 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_comm_4088 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
du_comm_4088 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4090 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong_4090 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4092 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4092 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4094 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4094 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity_4096 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Σ_14 #
d_identity'691'_4098 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_identity'737'_4100 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_isCommutativeMagma_4104 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeMagma_212 #
d_isCommutativeMonoid_4106 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeMonoid_736 #
d_isCommutativeSemigroup_4108 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeSemigroup_548 #
d_isInvertibleMagma_4112 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsInvertibleMagma_924 #
d_isInvertibleUnitalMagma_4114 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsInvertibleUnitalMagma_976 #
d_'8315''185''45'cong_4124 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8315''185''45'cong_4124 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_inverse_4126 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Σ_14 #
d_inverse'691'_4128 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_inverse'737'_4130 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_distrib'691'_4134 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'691'_4134 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_distrib'737'_4136 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_distrib'737'_4136 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isCommutativeSemiring_4138 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeSemiring_1678 #
d_isCommutativeSemiringWithoutOne_4140 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsCommutativeSemiringWithoutOne_1382 #
du_isCommutativeSemiringWithoutOne_4140 :: T_CommutativeRing_4016 -> T_IsCommutativeSemiringWithoutOne_1382 #
d_isNearSemiring_4144 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsNearSemiring_1218 #
d_isPartialEquivalence_4146 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsPartialEquivalence_16 #
d_isRingWithoutOne_4150 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsRingWithoutOne_2286 #
d_isSemiringWithoutAnnihilatingZero_4154 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
du_isSemiringWithoutAnnihilatingZero_4154 :: T_CommutativeRing_4016 -> T_IsSemiringWithoutAnnihilatingZero_1468 #
d_isSemiringWithoutOne_4156 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_IsSemiringWithoutOne_1298 #
d_refl_4158 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
du_refl_4158 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_reflexive_4160 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4160 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_setoid_4162 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Setoid_44 #
d_sym_4164 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_sym_4164 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4166 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_trans_4166 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'691''45''8315''185'_4168 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'691''45''8315''185'_4168 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_unique'737''45''8315''185'_4170 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_unique'737''45''8315''185'_4170 :: T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_zero_4172 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Σ_14 #
d_zero'691'_4174 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_zero'737'_4176 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny #
d_ring_4178 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Ring_3800 #
d__'8777'__4182 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> AgdaAny -> AgdaAny -> () #
d_'43''45'abelianGroup_4184 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_AbelianGroup_1636 #
d_group_4186 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Group_1520 #
d_invertibleMagma_4188 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_InvertibleMagma_1360 #
d_invertibleUnitalMagma_4190 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_InvertibleUnitalMagma_1434 #
d_commutativeSemiring_4194 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeSemiring_2446 #
d_commutativeMagma_4198 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeMagma_180 #
d_'42''45'commutativeMonoid_4200 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_4202 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeSemigroup_662 #
d_magma_4204 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Magma_68 #
d_commutativeMagma_4214 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeMagma_180 #
d_'43''45'commutativeMonoid_4216 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeMonoid_962 #
d_commutativeSemigroup_4218 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeSemigroup_662 #
d_magma_4220 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Magma_68 #
d_monoid_4222 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_Monoid_882 #
d_commutativeSemiringWithoutOne_4232 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_CommutativeSemiringWithoutOne_2002 #
du_commutativeSemiringWithoutOne_4232 :: T_CommutativeRing_4016 -> T_CommutativeSemiringWithoutOne_2002 #
d_semiringWithoutAnnihilatingZero_4238 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_SemiringWithoutAnnihilatingZero_2130 #
du_semiringWithoutAnnihilatingZero_4238 :: T_CommutativeRing_4016 -> T_SemiringWithoutAnnihilatingZero_2130 #
d_semiringWithoutOne_4240 :: T_Level_18 -> T_Level_18 -> T_CommutativeRing_4016 -> T_SemiringWithoutOne_1880 #
d_Quasigroup_4246 :: p -> p -> () #
data T_Quasigroup_4246 #
d_Carrier_4264 :: T_Quasigroup_4246 -> () #
d__'8776'__4266 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> () #
d__'8729'__4268 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__4270 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__4272 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong_4278 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'691'_4280 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'691'_4280 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'737'_4282 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'737'_4282 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong_4284 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'691'_4286 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'691'_4286 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'737'_4288 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'737'_4288 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_4294 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> T_IsPartialEquivalence_16 #
d_leftDivides'691'_4298 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'691'_4298 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'737'_4300 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'737'_4300 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_4302 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny #
d_reflexive_4304 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4304 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_rightDivides'691'_4308 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'691'_4308 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'737'_4310 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'737'_4310 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_4312 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> T_Setoid_44 #
d_sym_4314 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4316 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4318 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4320 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4320 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4322 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4322 :: T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_magma_4324 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> T_Magma_68 #
d__'8777'__4328 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> AgdaAny -> AgdaAny -> () #
d_rawMagma_4330 :: T_Level_18 -> T_Level_18 -> T_Quasigroup_4246 -> T_RawMagma_36 #
d_Loop_4346 :: p -> p -> () #
data T_Loop_4346 #
d_Carrier_4366 :: T_Loop_4346 -> () #
d__'8776'__4368 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> () #
d__'8729'__4370 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__4372 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__4374 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_4376 :: T_Loop_4346 -> AgdaAny #
d_'47''47''45'cong_4382 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'691'_4384 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'691'_4384 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'737'_4386 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'737'_4386 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong_4388 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'691'_4390 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'691'_4390 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'737'_4392 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'737'_4392 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity_4394 :: T_Loop_4346 -> T_Σ_14 #
d_identity'691'_4396 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny #
du_identity'691'_4396 :: T_Loop_4346 -> AgdaAny -> AgdaAny #
d_identity'737'_4398 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny #
du_identity'737'_4398 :: T_Loop_4346 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_4404 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> T_IsPartialEquivalence_16 #
d_leftDivides_4408 :: T_Loop_4346 -> T_Σ_14 #
d_leftDivides'691'_4410 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'691'_4410 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'737'_4412 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'737'_4412 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_4414 :: T_Loop_4346 -> AgdaAny -> AgdaAny #
d_reflexive_4416 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4416 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_rightDivides'691'_4420 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'691'_4420 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'737'_4422 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'737'_4422 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_4424 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> T_Setoid_44 #
d_sym_4426 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4428 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4430 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4432 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4432 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4434 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4434 :: T_Loop_4346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_rawLoop_4436 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> T_RawLoop_366 #
d_quasigroup_4438 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> T_Quasigroup_4246 #
d__'8777'__4442 :: T_Level_18 -> T_Level_18 -> T_Loop_4346 -> AgdaAny -> AgdaAny -> () #
d_LeftBolLoop_4454 :: p -> p -> () #
data T_LeftBolLoop_4454 #
d_Carrier_4474 :: T_LeftBolLoop_4454 -> () #
d__'8776'__4476 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> () #
d__'8729'__4478 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__4480 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__4482 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_4484 :: T_LeftBolLoop_4454 -> AgdaAny #
d_'47''47''45'cong_4490 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'691'_4492 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'691'_4492 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'737'_4494 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'737'_4494 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong_4496 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'691'_4498 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'691'_4498 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'737'_4500 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'737'_4500 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_4504 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny #
d_identity'737'_4506 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_4514 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> T_IsPartialEquivalence_16 #
d_leftBol_4518 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'691'_4522 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'691'_4522 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'737'_4524 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'737'_4524 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_4526 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny #
d_reflexive_4528 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4528 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_rightDivides'691'_4532 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'691'_4532 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'737'_4534 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'737'_4534 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_4536 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> T_Setoid_44 #
d_sym_4538 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4540 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4542 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4544 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4544 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4546 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4546 :: T_LeftBolLoop_4454 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_loop_4548 :: T_Level_18 -> T_Level_18 -> T_LeftBolLoop_4454 -> T_Loop_4346 #
d_RightBolLoop_4558 :: p -> p -> () #
data T_RightBolLoop_4558 #
d_Carrier_4578 :: T_RightBolLoop_4558 -> () #
d__'8776'__4580 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> () #
d__'8729'__4582 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__4584 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__4586 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_4588 :: T_RightBolLoop_4558 -> AgdaAny #
d_'47''47''45'cong_4594 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'691'_4596 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'691'_4596 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'737'_4598 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'737'_4598 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong_4600 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'691'_4602 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'691'_4602 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'737'_4604 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'737'_4604 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_4608 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny #
d_identity'737'_4610 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_4618 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> T_IsPartialEquivalence_16 #
d_leftDivides'691'_4624 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'691'_4624 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'737'_4626 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'737'_4626 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_4628 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny #
d_reflexive_4630 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4630 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_rightBol_4632 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'691'_4636 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'691'_4636 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'737'_4638 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'737'_4638 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_4640 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> T_Setoid_44 #
d_sym_4642 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4644 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4646 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4648 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4648 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4650 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4650 :: T_RightBolLoop_4558 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_loop_4652 :: T_Level_18 -> T_Level_18 -> T_RightBolLoop_4558 -> T_Loop_4346 #
d_MoufangLoop_4662 :: p -> p -> () #
data T_MoufangLoop_4662 #
d_Carrier_4682 :: T_MoufangLoop_4662 -> () #
d__'8776'__4684 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> () #
d__'8729'__4686 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__4688 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__4690 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_4692 :: T_MoufangLoop_4662 -> AgdaAny #
d_'47''47''45'cong_4698 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'691'_4700 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'691'_4700 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'737'_4702 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'737'_4702 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong_4704 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'691'_4706 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'691'_4706 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'737'_4708 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'737'_4708 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identical_4710 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_4714 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny #
d_identity'737'_4716 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_4726 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> T_IsPartialEquivalence_16 #
d_leftBol_4730 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'691'_4734 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'691'_4734 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'737'_4736 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'737'_4736 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_4738 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny #
d_reflexive_4740 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4740 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_rightBol_4742 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'691'_4746 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'691'_4746 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'737'_4748 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'737'_4748 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_4750 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> T_Setoid_44 #
d_sym_4752 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4754 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4756 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4758 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4758 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4760 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4760 :: T_MoufangLoop_4662 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_loop_4766 :: T_Level_18 -> T_Level_18 -> T_MoufangLoop_4662 -> T_Loop_4346 #
d_MiddleBolLoop_4772 :: p -> p -> () #
data T_MiddleBolLoop_4772 #
d_Carrier_4792 :: T_MiddleBolLoop_4772 -> () #
d__'8776'__4794 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> () #
d__'8729'__4796 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'92''92'__4798 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d__'47''47'__4800 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d_ε_4802 :: T_MiddleBolLoop_4772 -> AgdaAny #
d_'47''47''45'cong_4808 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'691'_4810 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'691'_4810 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'47''47''45'cong'737'_4812 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'47''47''45'cong'737'_4812 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong_4814 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'691'_4816 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'691'_4816 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'92''92''45'cong'737'_4818 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'92''92''45'cong'737'_4818 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_identity'691'_4822 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny #
d_identity'737'_4824 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny #
d_isPartialEquivalence_4832 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> T_IsPartialEquivalence_16 #
d_leftDivides'691'_4838 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'691'_4838 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d_leftDivides'737'_4840 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
du_leftDivides'737'_4840 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d_middleBol_4842 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_refl_4844 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny #
d_reflexive_4846 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_reflexive_4846 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
d_rightDivides'691'_4850 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'691'_4850 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d_rightDivides'737'_4852 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
du_rightDivides'737'_4852 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny #
d_setoid_4854 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> T_Setoid_44 #
d_sym_4856 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_4858 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong_4860 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'691'_4862 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'691'_4862 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_'8729''45'cong'737'_4864 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_'8729''45'cong'737'_4864 :: T_MiddleBolLoop_4772 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_loop_4866 :: T_Level_18 -> T_Level_18 -> T_MiddleBolLoop_4772 -> T_Loop_4346 #