Documentation

d_RawMagma_8 :: p1 -> p2 -> () Source #

newtype T_RawMagma_8 Source #

d_Carrier_20 :: T_RawMagma_8 -> () Source #

d__'8776'__22 :: T_RawMagma_8 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__24 :: T_RawMagma_8 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8777'__26 :: T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> AgdaAny -> AgdaAny -> () Source #

d_Magma_36 :: p1 -> p2 -> () Source #

data T_Magma_36 Source #

d_Carrier_50 :: T_Magma_36 -> () Source #

d__'8776'__52 :: T_Magma_36 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__54 :: T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagma_56 :: T_Magma_36 -> T_IsMagma_98 Source #

d_isEquivalence_60 :: T_Magma_36 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_62 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_62 :: T_Magma_36 -> T_IsPartialEquivalence_16 Source #

d_refl_64 :: T_Magma_36 -> AgdaAny -> AgdaAny Source #

d_reflexive_66 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_66 :: T_Magma_36 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_68 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> T_Setoid_44 Source #

du_setoid_68 :: T_Magma_36 -> T_Setoid_44 Source #

d_sym_70 :: T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_72 :: T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_74 :: T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_76 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_76 :: T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_78 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_78 :: T_Magma_36 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_rawMagma_80 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> T_RawMagma_8 Source #

du_rawMagma_80 :: T_Magma_36 -> T_RawMagma_8 Source #

d__'8777'__84 :: T_Level_14 -> T_Level_14 -> T_Magma_36 -> AgdaAny -> AgdaAny -> () Source #

d_SelectiveMagma_90 :: p1 -> p2 -> () Source #

data T_SelectiveMagma_90 Source #

d_Carrier_104 :: T_SelectiveMagma_90 -> () Source #

d__'8776'__106 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__108 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSelectiveMagma_110 :: T_SelectiveMagma_90 -> T_IsSelectiveMagma_170 Source #

d_isEquivalence_114 :: T_SelectiveMagma_90 -> T_IsEquivalence_26 Source #

d_isMagma_116 :: T_SelectiveMagma_90 -> T_IsMagma_98 Source #

d_isPartialEquivalence_118 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_118 :: T_SelectiveMagma_90 -> T_IsPartialEquivalence_16 Source #

d_refl_120 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny Source #

d_reflexive_122 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_122 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sel_124 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #

d_setoid_126 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> T_Setoid_44 Source #

du_setoid_126 :: T_SelectiveMagma_90 -> T_Setoid_44 Source #

d_sym_128 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_130 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_132 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_134 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_134 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_136 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_136 :: T_SelectiveMagma_90 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_magma_138 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> T_Magma_36 Source #

du_magma_138 :: T_SelectiveMagma_90 -> T_Magma_36 Source #

d_rawMagma_142 :: T_Level_14 -> T_Level_14 -> T_SelectiveMagma_90 -> T_RawMagma_8 Source #

du_rawMagma_142 :: T_SelectiveMagma_90 -> T_RawMagma_8 Source #

d_CommutativeMagma_148 :: p1 -> p2 -> () Source #

data T_CommutativeMagma_148 Source #

d_Carrier_162 :: T_CommutativeMagma_148 -> () Source #

d__'8776'__164 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__166 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_168 :: T_CommutativeMagma_148 -> T_IsCommutativeMagma_134 Source #

d_comm_172 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_174 :: T_CommutativeMagma_148 -> T_IsEquivalence_26 Source #

d_isMagma_176 :: T_CommutativeMagma_148 -> T_IsMagma_98 Source #

d_isPartialEquivalence_178 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_178 :: T_CommutativeMagma_148 -> T_IsPartialEquivalence_16 Source #

d_refl_180 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny Source #

d_reflexive_182 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_182 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_184 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> T_Setoid_44 Source #

du_setoid_184 :: T_CommutativeMagma_148 -> T_Setoid_44 Source #

d_sym_186 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_188 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_190 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_192 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_192 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_194 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_194 :: T_CommutativeMagma_148 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_magma_196 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> T_Magma_36 Source #

du_magma_196 :: T_CommutativeMagma_148 -> T_Magma_36 Source #

d_rawMagma_200 :: T_Level_14 -> T_Level_14 -> T_CommutativeMagma_148 -> T_RawMagma_8 Source #

du_rawMagma_200 :: T_CommutativeMagma_148 -> T_RawMagma_8 Source #

d_Semigroup_206 :: p1 -> p2 -> () Source #

data T_Semigroup_206 Source #

d_Carrier_220 :: T_Semigroup_206 -> () Source #

d__'8776'__222 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__224 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemigroup_226 :: T_Semigroup_206 -> T_IsSemigroup_206 Source #

d_assoc_230 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_232 :: T_Semigroup_206 -> T_IsEquivalence_26 Source #

d_isMagma_234 :: T_Semigroup_206 -> T_IsMagma_98 Source #

d_isPartialEquivalence_236 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_236 :: T_Semigroup_206 -> T_IsPartialEquivalence_16 Source #

d_refl_238 :: T_Semigroup_206 -> AgdaAny -> AgdaAny Source #

d_reflexive_240 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_240 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_242 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Setoid_44 Source #

du_setoid_242 :: T_Semigroup_206 -> T_Setoid_44 Source #

d_sym_244 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_246 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_248 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_250 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_250 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_252 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_252 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_magma_254 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Magma_36 Source #

du_magma_254 :: T_Semigroup_206 -> T_Magma_36 Source #

d__'8777'__258 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> AgdaAny -> AgdaAny -> () Source #

d_rawMagma_260 :: T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_RawMagma_8 Source #

du_rawMagma_260 :: T_Semigroup_206 -> T_RawMagma_8 Source #

d_Band_266 :: p1 -> p2 -> () Source #

data T_Band_266 Source #

d_Carrier_280 :: T_Band_266 -> () Source #

d__'8776'__282 :: T_Band_266 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__284 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isBand_286 :: T_Band_266 -> T_IsBand_242 Source #

d_assoc_290 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_292 :: T_Band_266 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_294 :: T_Band_266 -> T_IsEquivalence_26 Source #

d_isMagma_296 :: T_Band_266 -> T_IsMagma_98 Source #

d_isPartialEquivalence_298 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_298 :: T_Band_266 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_300 :: T_Band_266 -> T_IsSemigroup_206 Source #

d_refl_302 :: T_Band_266 -> AgdaAny -> AgdaAny Source #

d_reflexive_304 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_304 :: T_Band_266 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_306 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> T_Setoid_44 Source #

du_setoid_306 :: T_Band_266 -> T_Setoid_44 Source #

d_sym_308 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_310 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_312 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_314 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_314 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_316 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_316 :: T_Band_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semigroup_318 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> T_Semigroup_206 Source #

du_semigroup_318 :: T_Band_266 -> T_Semigroup_206 Source #

d__'8777'__322 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> AgdaAny -> AgdaAny -> () Source #

d_magma_324 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> T_Magma_36 Source #

du_magma_324 :: T_Band_266 -> T_Magma_36 Source #

d_rawMagma_326 :: T_Level_14 -> T_Level_14 -> T_Band_266 -> T_RawMagma_8 Source #

du_rawMagma_326 :: T_Band_266 -> T_RawMagma_8 Source #

d_CommutativeSemigroup_332 :: p1 -> p2 -> () Source #

data T_CommutativeSemigroup_332 Source #

d_Carrier_346 :: T_CommutativeSemigroup_332 -> () Source #

d__'8776'__348 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__350 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemigroup_352 :: T_CommutativeSemigroup_332 -> T_IsCommutativeSemigroup_282 Source #

d_assoc_356 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_358 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_360 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_360 :: T_CommutativeSemigroup_332 -> T_IsCommutativeMagma_134 Source #

d_isEquivalence_362 :: T_CommutativeSemigroup_332 -> T_IsEquivalence_26 Source #

d_isMagma_364 :: T_CommutativeSemigroup_332 -> T_IsMagma_98 Source #

d_isPartialEquivalence_366 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_366 :: T_CommutativeSemigroup_332 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_368 :: T_CommutativeSemigroup_332 -> T_IsSemigroup_206 Source #

d_refl_370 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny Source #

d_reflexive_372 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_372 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_374 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_Setoid_44 Source #

du_setoid_374 :: T_CommutativeSemigroup_332 -> T_Setoid_44 Source #

d_sym_376 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_378 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_380 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_382 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_382 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_384 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_384 :: T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semigroup_386 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_Semigroup_206 Source #

du_semigroup_386 :: T_CommutativeSemigroup_332 -> T_Semigroup_206 Source #

d__'8777'__390 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> AgdaAny -> AgdaAny -> () Source #

d_magma_392 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_Magma_36 Source #

du_magma_392 :: T_CommutativeSemigroup_332 -> T_Magma_36 Source #

d_rawMagma_394 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_RawMagma_8 Source #

du_rawMagma_394 :: T_CommutativeSemigroup_332 -> T_RawMagma_8 Source #

d_commutativeMagma_396 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemigroup_332 -> T_CommutativeMagma_148 Source #

du_commutativeMagma_396 :: T_CommutativeSemigroup_332 -> T_CommutativeMagma_148 Source #

d_RawMonoid_402 :: p1 -> p2 -> () Source #

data T_RawMonoid_402 Source #

d_Carrier_416 :: T_RawMonoid_402 -> () Source #

d__'8776'__418 :: T_RawMonoid_402 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__420 :: T_RawMonoid_402 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_422 :: T_RawMonoid_402 -> AgdaAny Source #

d_rawMagma_424 :: T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMagma_8 Source #

du_rawMagma_424 :: T_RawMonoid_402 -> T_RawMagma_8 Source #

d__'8777'__428 :: T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> AgdaAny -> AgdaAny -> () Source #

d_UnitalMagma_434 :: p1 -> p2 -> () Source #

data T_UnitalMagma_434 Source #

d_Carrier_450 :: T_UnitalMagma_434 -> () Source #

d__'8776'__452 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__454 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_456 :: T_UnitalMagma_434 -> AgdaAny Source #

d_isUnitalMagma_458 :: T_UnitalMagma_434 -> T_IsUnitalMagma_326 Source #

d_identity_462 :: T_UnitalMagma_434 -> T_Σ_14 Source #

d_identity'691'_464 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> AgdaAny -> AgdaAny Source #

du_identity'691'_464 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny Source #

d_identity'737'_466 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> AgdaAny -> AgdaAny Source #

du_identity'737'_466 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_468 :: T_UnitalMagma_434 -> T_IsEquivalence_26 Source #

d_isMagma_470 :: T_UnitalMagma_434 -> T_IsMagma_98 Source #

d_isPartialEquivalence_472 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_472 :: T_UnitalMagma_434 -> T_IsPartialEquivalence_16 Source #

d_refl_474 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny Source #

d_reflexive_476 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_476 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_478 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> T_Setoid_44 Source #

du_setoid_478 :: T_UnitalMagma_434 -> T_Setoid_44 Source #

d_sym_480 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_482 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_484 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_486 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_486 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_488 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_488 :: T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_magma_490 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> T_Magma_36 Source #

du_magma_490 :: T_UnitalMagma_434 -> T_Magma_36 Source #

d__'8777'__494 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> AgdaAny -> AgdaAny -> () Source #

d_rawMagma_496 :: T_Level_14 -> T_Level_14 -> T_UnitalMagma_434 -> T_RawMagma_8 Source #

du_rawMagma_496 :: T_UnitalMagma_434 -> T_RawMagma_8 Source #

d_Monoid_502 :: p1 -> p2 -> () Source #

data T_Monoid_502 Source #

d_Carrier_518 :: T_Monoid_502 -> () Source #

d__'8776'__520 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__522 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_524 :: T_Monoid_502 -> AgdaAny Source #

d_isMonoid_526 :: T_Monoid_502 -> T_IsMonoid_370 Source #

d_assoc_530 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_532 :: T_Monoid_502 -> T_Σ_14 Source #

d_identity'691'_534 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> AgdaAny -> AgdaAny Source #

du_identity'691'_534 :: T_Monoid_502 -> AgdaAny -> AgdaAny Source #

d_identity'737'_536 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> AgdaAny -> AgdaAny Source #

du_identity'737'_536 :: T_Monoid_502 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_538 :: T_Monoid_502 -> T_IsEquivalence_26 Source #

d_isMagma_540 :: T_Monoid_502 -> T_IsMagma_98 Source #

d_isPartialEquivalence_542 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_542 :: T_Monoid_502 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_544 :: T_Monoid_502 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_546 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_546 :: T_Monoid_502 -> T_IsUnitalMagma_326 Source #

d_refl_548 :: T_Monoid_502 -> AgdaAny -> AgdaAny Source #

d_reflexive_550 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_550 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_552 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Setoid_44 Source #

du_setoid_552 :: T_Monoid_502 -> T_Setoid_44 Source #

d_sym_554 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_556 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_558 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_560 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_560 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_562 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_562 :: T_Monoid_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semigroup_564 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Semigroup_206 Source #

du_semigroup_564 :: T_Monoid_502 -> T_Semigroup_206 Source #

d__'8777'__568 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> AgdaAny -> AgdaAny -> () Source #

d_magma_570 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Magma_36 Source #

du_magma_570 :: T_Monoid_502 -> T_Magma_36 Source #

d_rawMagma_572 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_RawMagma_8 Source #

du_rawMagma_572 :: T_Monoid_502 -> T_RawMagma_8 Source #

d_rawMonoid_574 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_RawMonoid_402 Source #

du_rawMonoid_574 :: T_Monoid_502 -> T_RawMonoid_402 Source #

d_unitalMagma_576 :: T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_UnitalMagma_434 Source #

du_unitalMagma_576 :: T_Monoid_502 -> T_UnitalMagma_434 Source #

d_CommutativeMonoid_582 :: p1 -> p2 -> () Source #

data T_CommutativeMonoid_582 Source #

d_Carrier_598 :: T_CommutativeMonoid_582 -> () Source #

d__'8776'__600 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__602 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_604 :: T_CommutativeMonoid_582 -> AgdaAny Source #

d_isCommutativeMonoid_606 :: T_CommutativeMonoid_582 -> T_IsCommutativeMonoid_420 Source #

d_assoc_610 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_612 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_614 :: T_CommutativeMonoid_582 -> T_Σ_14 Source #

d_identity'691'_616 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny Source #

du_identity'691'_616 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny Source #

d_identity'737'_618 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny Source #

du_identity'737'_618 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_620 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_620 :: T_CommutativeMonoid_582 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeSemigroup_622 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_622 :: T_CommutativeMonoid_582 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_624 :: T_CommutativeMonoid_582 -> T_IsEquivalence_26 Source #

d_isMagma_626 :: T_CommutativeMonoid_582 -> T_IsMagma_98 Source #

d_isMonoid_628 :: T_CommutativeMonoid_582 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_630 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_630 :: T_CommutativeMonoid_582 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_632 :: T_CommutativeMonoid_582 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_634 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_634 :: T_CommutativeMonoid_582 -> T_IsUnitalMagma_326 Source #

d_refl_636 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny Source #

d_reflexive_638 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_638 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_640 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_Setoid_44 Source #

du_setoid_640 :: T_CommutativeMonoid_582 -> T_Setoid_44 Source #

d_sym_642 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_644 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_646 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_648 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_648 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_650 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_650 :: T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_monoid_652 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_Monoid_502 Source #

du_monoid_652 :: T_CommutativeMonoid_582 -> T_Monoid_502 Source #

d__'8777'__656 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> AgdaAny -> AgdaAny -> () Source #

d_magma_658 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_Magma_36 Source #

du_magma_658 :: T_CommutativeMonoid_582 -> T_Magma_36 Source #

d_rawMagma_660 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_RawMagma_8 Source #

du_rawMagma_660 :: T_CommutativeMonoid_582 -> T_RawMagma_8 Source #

d_rawMonoid_662 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_RawMonoid_402 Source #

du_rawMonoid_662 :: T_CommutativeMonoid_582 -> T_RawMonoid_402 Source #

d_semigroup_664 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_Semigroup_206 Source #

du_semigroup_664 :: T_CommutativeMonoid_582 -> T_Semigroup_206 Source #

d_unitalMagma_666 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_UnitalMagma_434 Source #

du_unitalMagma_666 :: T_CommutativeMonoid_582 -> T_UnitalMagma_434 Source #

d_commutativeSemigroup_668 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_668 :: T_CommutativeMonoid_582 -> T_CommutativeSemigroup_332 Source #

d_commutativeMagma_672 :: T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMagma_148 Source #

du_commutativeMagma_672 :: T_CommutativeMonoid_582 -> T_CommutativeMagma_148 Source #

d_IdempotentCommutativeMonoid_678 :: p1 -> p2 -> () Source #

data T_IdempotentCommutativeMonoid_678 Source #

d_Carrier_694 :: T_IdempotentCommutativeMonoid_678 -> () Source #

d__'8776'__696 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__698 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_700 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny Source #

d_isIdempotentCommutativeMonoid_702 :: T_IdempotentCommutativeMonoid_678 -> T_IsIdempotentCommutativeMonoid_480 Source #

d_assoc_706 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_708 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_710 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_identity_712 :: T_IdempotentCommutativeMonoid_678 -> T_Σ_14 Source #

d_identity'691'_714 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

du_identity'691'_714 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_identity'737'_716 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

du_identity'737'_716 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_isBand_718 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsBand_242 Source #

du_isBand_718 :: T_IdempotentCommutativeMonoid_678 -> T_IsBand_242 Source #

d_isCommutativeMagma_720 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_720 :: T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_722 :: T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_724 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_724 :: T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_726 :: T_IdempotentCommutativeMonoid_678 -> T_IsEquivalence_26 Source #

d_isMagma_728 :: T_IdempotentCommutativeMonoid_678 -> T_IsMagma_98 Source #

d_isMonoid_730 :: T_IdempotentCommutativeMonoid_678 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_732 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_732 :: T_IdempotentCommutativeMonoid_678 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_734 :: T_IdempotentCommutativeMonoid_678 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_736 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_736 :: T_IdempotentCommutativeMonoid_678 -> T_IsUnitalMagma_326 Source #

d_refl_738 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_reflexive_740 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_740 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_742 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Setoid_44 Source #

du_setoid_742 :: T_IdempotentCommutativeMonoid_678 -> T_Setoid_44 Source #

d_sym_744 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_746 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_748 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_750 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_750 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_752 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_752 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_commutativeMonoid_754 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

du_commutativeMonoid_754 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

d__'8777'__758 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> () Source #

d_commutativeMagma_760 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeMagma_148 Source #

du_commutativeMagma_760 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeMagma_148 Source #

d_commutativeSemigroup_762 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_762 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeSemigroup_332 Source #

d_magma_764 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Magma_36 Source #

du_magma_764 :: T_IdempotentCommutativeMonoid_678 -> T_Magma_36 Source #

d_monoid_766 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

du_monoid_766 :: T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

d_rawMagma_768 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_RawMagma_8 Source #

du_rawMagma_768 :: T_IdempotentCommutativeMonoid_678 -> T_RawMagma_8 Source #

d_rawMonoid_770 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_RawMonoid_402 Source #

du_rawMonoid_770 :: T_IdempotentCommutativeMonoid_678 -> T_RawMonoid_402 Source #

d_semigroup_772 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Semigroup_206 Source #

du_semigroup_772 :: T_IdempotentCommutativeMonoid_678 -> T_Semigroup_206 Source #

d_unitalMagma_774 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_UnitalMagma_434 Source #

du_unitalMagma_774 :: T_IdempotentCommutativeMonoid_678 -> T_UnitalMagma_434 Source #

d_BoundedLattice_776 :: T_Level_14 -> T_Level_14 -> () Source #

d__'8729'__786 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__788 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__790 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_792 :: T_IdempotentCommutativeMonoid_678 -> () Source #

d_assoc_794 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_796 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_commutativeMagma_798 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeMagma_148 Source #

du_commutativeMagma_798 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeMagma_148 Source #

d_commutativeMonoid_800 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

du_commutativeMonoid_800 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_802 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_802 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeSemigroup_332 Source #

d_idem_804 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_identity_806 :: T_IdempotentCommutativeMonoid_678 -> T_Σ_14 Source #

d_identity'691'_808 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

du_identity'691'_808 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_identity'737'_810 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

du_identity'737'_810 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_isBand_812 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsBand_242 Source #

du_isBand_812 :: T_IdempotentCommutativeMonoid_678 -> T_IsBand_242 Source #

d_isCommutativeMagma_814 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_814 :: T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_816 :: T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_818 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_818 :: T_IdempotentCommutativeMonoid_678 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_820 :: T_IdempotentCommutativeMonoid_678 -> T_IsEquivalence_26 Source #

d_isIdempotentCommutativeMonoid_822 :: T_IdempotentCommutativeMonoid_678 -> T_IsIdempotentCommutativeMonoid_480 Source #

d_isMagma_824 :: T_IdempotentCommutativeMonoid_678 -> T_IsMagma_98 Source #

d_isMonoid_826 :: T_IdempotentCommutativeMonoid_678 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_828 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_828 :: T_IdempotentCommutativeMonoid_678 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_830 :: T_IdempotentCommutativeMonoid_678 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_832 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_832 :: T_IdempotentCommutativeMonoid_678 -> T_IsUnitalMagma_326 Source #

d_magma_834 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Magma_36 Source #

du_magma_834 :: T_IdempotentCommutativeMonoid_678 -> T_Magma_36 Source #

d_monoid_836 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

du_monoid_836 :: T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

d_rawMagma_838 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_RawMagma_8 Source #

du_rawMagma_838 :: T_IdempotentCommutativeMonoid_678 -> T_RawMagma_8 Source #

d_rawMonoid_840 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_RawMonoid_402 Source #

du_rawMonoid_840 :: T_IdempotentCommutativeMonoid_678 -> T_RawMonoid_402 Source #

d_refl_842 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny Source #

d_reflexive_844 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_844 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_semigroup_846 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Semigroup_206 Source #

du_semigroup_846 :: T_IdempotentCommutativeMonoid_678 -> T_Semigroup_206 Source #

d_setoid_848 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_Setoid_44 Source #

du_setoid_848 :: T_IdempotentCommutativeMonoid_678 -> T_Setoid_44 Source #

d_sym_850 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_852 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unitalMagma_854 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_UnitalMagma_434 Source #

du_unitalMagma_854 :: T_IdempotentCommutativeMonoid_678 -> T_UnitalMagma_434 Source #

d_ε_856 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny Source #

d_'8729''45'cong_858 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_860 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_860 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_862 :: T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_862 :: T_IdempotentCommutativeMonoid_678 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_RawGroup_868 :: p1 -> p2 -> () Source #

data T_RawGroup_868 Source #

d_Carrier_884 :: T_RawGroup_868 -> () Source #

d__'8776'__886 :: T_RawGroup_868 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__888 :: T_RawGroup_868 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_890 :: T_RawGroup_868 -> AgdaAny Source #

d__'8315''185'_892 :: T_RawGroup_868 -> AgdaAny -> AgdaAny Source #

d_rawMonoid_894 :: T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawMonoid_402 Source #

du_rawMonoid_894 :: T_RawGroup_868 -> T_RawMonoid_402 Source #

d__'8777'__898 :: T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> AgdaAny -> AgdaAny -> () Source #

d_rawMagma_900 :: T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawMagma_8 Source #

du_rawMagma_900 :: T_RawGroup_868 -> T_RawMagma_8 Source #

d_InvertibleMagma_906 :: p1 -> p2 -> () Source #

data T_InvertibleMagma_906 Source #

d_Carrier_924 :: T_InvertibleMagma_906 -> () Source #

d__'8776'__926 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__928 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_930 :: T_InvertibleMagma_906 -> AgdaAny Source #

d__'8315''185'_932 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny Source #

d_isInvertibleMagma_934 :: T_InvertibleMagma_906 -> T_IsInvertibleMagma_546 Source #

d_inverse_938 :: T_InvertibleMagma_906 -> T_Σ_14 Source #

d_inverse'691'_940 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_940 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_942 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_942 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_944 :: T_InvertibleMagma_906 -> T_IsEquivalence_26 Source #

d_isMagma_946 :: T_InvertibleMagma_906 -> T_IsMagma_98 Source #

d_isPartialEquivalence_948 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_948 :: T_InvertibleMagma_906 -> T_IsPartialEquivalence_16 Source #

d_refl_950 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny Source #

d_reflexive_952 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_952 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_954 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> T_Setoid_44 Source #

du_setoid_954 :: T_InvertibleMagma_906 -> T_Setoid_44 Source #

d_sym_956 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_958 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_960 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_962 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_962 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_964 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_964 :: T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_magma_966 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> T_Magma_36 Source #

du_magma_966 :: T_InvertibleMagma_906 -> T_Magma_36 Source #

d__'8777'__970 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> AgdaAny -> AgdaAny -> () Source #

d_rawMagma_972 :: T_Level_14 -> T_Level_14 -> T_InvertibleMagma_906 -> T_RawMagma_8 Source #

du_rawMagma_972 :: T_InvertibleMagma_906 -> T_RawMagma_8 Source #

d_InvertibleUnitalMagma_978 :: p1 -> p2 -> () Source #

data T_InvertibleUnitalMagma_978 Source #

d_Carrier_996 :: T_InvertibleUnitalMagma_978 -> () Source #

d__'8776'__998 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__1000 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_1002 :: T_InvertibleUnitalMagma_978 -> AgdaAny Source #

d__'8315''185'_1004 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

d_isInvertibleUnitalMagma_1006 :: T_InvertibleUnitalMagma_978 -> T_IsInvertibleUnitalMagma_594 Source #

d_identity_1010 :: T_InvertibleUnitalMagma_978 -> T_Σ_14 Source #

d_identity'691'_1012 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1012 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1014 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1014 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

d_inverse_1016 :: T_InvertibleUnitalMagma_978 -> T_Σ_14 Source #

d_inverse'691'_1018 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1018 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1020 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1020 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1022 :: T_InvertibleUnitalMagma_978 -> T_IsEquivalence_26 Source #

d_isInvertibleMagma_1024 :: T_InvertibleUnitalMagma_978 -> T_IsInvertibleMagma_546 Source #

d_isMagma_1026 :: T_InvertibleUnitalMagma_978 -> T_IsMagma_98 Source #

d_isPartialEquivalence_1028 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1028 :: T_InvertibleUnitalMagma_978 -> T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1030 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1030 :: T_InvertibleUnitalMagma_978 -> T_IsUnitalMagma_326 Source #

d_refl_1032 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny Source #

d_reflexive_1034 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1034 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1036 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> T_Setoid_44 Source #

du_setoid_1036 :: T_InvertibleUnitalMagma_978 -> T_Setoid_44 Source #

d_sym_1038 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1040 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1042 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1044 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1044 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1046 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1046 :: T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_invertibleMagma_1048 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> T_InvertibleMagma_906 Source #

du_invertibleMagma_1048 :: T_InvertibleUnitalMagma_978 -> T_InvertibleMagma_906 Source #

d__'8777'__1052 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> AgdaAny -> AgdaAny -> () Source #

d_magma_1054 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> T_Magma_36 Source #

du_magma_1054 :: T_InvertibleUnitalMagma_978 -> T_Magma_36 Source #

d_rawMagma_1056 :: T_Level_14 -> T_Level_14 -> T_InvertibleUnitalMagma_978 -> T_RawMagma_8 Source #

du_rawMagma_1056 :: T_InvertibleUnitalMagma_978 -> T_RawMagma_8 Source #

d_Group_1062 :: p1 -> p2 -> () Source #

data T_Group_1062 Source #

d_Carrier_1080 :: T_Group_1062 -> () Source #

d__'8776'__1082 :: T_Group_1062 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__1084 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_1086 :: T_Group_1062 -> AgdaAny Source #

d__'8315''185'_1088 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_isGroup_1090 :: T_Group_1062 -> T_IsGroup_652 Source #

d__'45'__1094 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__1094 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_1096 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1098 :: T_Group_1062 -> T_Σ_14 Source #

d_identity'691'_1100 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1100 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1102 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1102 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_inverse_1104 :: T_Group_1062 -> T_Σ_14 Source #

d_inverse'691'_1106 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1106 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1108 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1108 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1110 :: T_Group_1062 -> T_IsEquivalence_26 Source #

d_isInvertibleMagma_1112 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_1112 :: T_Group_1062 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_1114 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_1114 :: T_Group_1062 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_1116 :: T_Group_1062 -> T_IsMagma_98 Source #

d_isMonoid_1118 :: T_Group_1062 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_1120 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1120 :: T_Group_1062 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1122 :: T_Group_1062 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1124 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1124 :: T_Group_1062 -> T_IsUnitalMagma_326 Source #

d_refl_1126 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_reflexive_1128 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1128 :: T_Group_1062 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1130 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Setoid_44 Source #

du_setoid_1130 :: T_Group_1062 -> T_Setoid_44 Source #

d_sym_1132 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1134 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_1136 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_1136 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_1138 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_1138 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8315''185''45'cong_1140 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1142 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1144 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1144 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1146 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1146 :: T_Group_1062 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_rawGroup_1148 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_RawGroup_868 Source #

du_rawGroup_1148 :: T_Group_1062 -> T_RawGroup_868 Source #

d_monoid_1150 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Monoid_502 Source #

du_monoid_1150 :: T_Group_1062 -> T_Monoid_502 Source #

d__'8777'__1154 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> AgdaAny -> AgdaAny -> () Source #

d_magma_1156 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Magma_36 Source #

du_magma_1156 :: T_Group_1062 -> T_Magma_36 Source #

d_rawMagma_1158 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_RawMagma_8 Source #

du_rawMagma_1158 :: T_Group_1062 -> T_RawMagma_8 Source #

d_rawMonoid_1160 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_RawMonoid_402 Source #

du_rawMonoid_1160 :: T_Group_1062 -> T_RawMonoid_402 Source #

d_semigroup_1162 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Semigroup_206 Source #

du_semigroup_1162 :: T_Group_1062 -> T_Semigroup_206 Source #

d_unitalMagma_1164 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_UnitalMagma_434 Source #

du_unitalMagma_1164 :: T_Group_1062 -> T_UnitalMagma_434 Source #

d_invertibleMagma_1166 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_InvertibleMagma_906 Source #

du_invertibleMagma_1166 :: T_Group_1062 -> T_InvertibleMagma_906 Source #

d_invertibleUnitalMagma_1168 :: T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_InvertibleUnitalMagma_978 Source #

du_invertibleUnitalMagma_1168 :: T_Group_1062 -> T_InvertibleUnitalMagma_978 Source #

d_AbelianGroup_1174 :: p1 -> p2 -> () Source #

data T_AbelianGroup_1174 Source #

d_Carrier_1192 :: T_AbelianGroup_1174 -> () Source #

d__'8776'__1194 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__1196 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_1198 :: T_AbelianGroup_1174 -> AgdaAny Source #

d__'8315''185'_1200 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

d_isAbelianGroup_1202 :: T_AbelianGroup_1174 -> T_IsAbelianGroup_740 Source #

d__'45'__1206 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__1206 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_1208 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1210 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1212 :: T_AbelianGroup_1174 -> T_Σ_14 Source #

d_identity'691'_1214 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1214 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1216 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1216 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

d_inverse_1218 :: T_AbelianGroup_1174 -> T_Σ_14 Source #

d_inverse'691'_1220 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1220 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1222 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1222 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1224 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1224 :: T_AbelianGroup_1174 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_1226 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_1226 :: T_AbelianGroup_1174 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1228 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1228 :: T_AbelianGroup_1174 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_1230 :: T_AbelianGroup_1174 -> T_IsEquivalence_26 Source #

d_isGroup_1232 :: T_AbelianGroup_1174 -> T_IsGroup_652 Source #

d_isInvertibleMagma_1234 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_1234 :: T_AbelianGroup_1174 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_1236 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_1236 :: T_AbelianGroup_1174 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_1238 :: T_AbelianGroup_1174 -> T_IsMagma_98 Source #

d_isMonoid_1240 :: T_AbelianGroup_1174 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_1242 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1242 :: T_AbelianGroup_1174 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1244 :: T_AbelianGroup_1174 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1246 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1246 :: T_AbelianGroup_1174 -> T_IsUnitalMagma_326 Source #

d_refl_1248 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny Source #

d_reflexive_1250 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1250 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1252 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_Setoid_44 Source #

du_setoid_1252 :: T_AbelianGroup_1174 -> T_Setoid_44 Source #

d_sym_1254 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1256 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_1258 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_1258 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_1260 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_1260 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8315''185''45'cong_1262 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1264 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1266 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1266 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1268 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1268 :: T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_group_1270 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_Group_1062 Source #

du_group_1270 :: T_AbelianGroup_1174 -> T_Group_1062 Source #

d__'8777'__1274 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> AgdaAny -> AgdaAny -> () Source #

d_invertibleMagma_1276 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_InvertibleMagma_906 Source #

du_invertibleMagma_1276 :: T_AbelianGroup_1174 -> T_InvertibleMagma_906 Source #

d_invertibleUnitalMagma_1278 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_InvertibleUnitalMagma_978 Source #

du_invertibleUnitalMagma_1278 :: T_AbelianGroup_1174 -> T_InvertibleUnitalMagma_978 Source #

d_magma_1280 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_Magma_36 Source #

du_magma_1280 :: T_AbelianGroup_1174 -> T_Magma_36 Source #

d_monoid_1282 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_Monoid_502 Source #

du_monoid_1282 :: T_AbelianGroup_1174 -> T_Monoid_502 Source #

d_rawGroup_1284 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_RawGroup_868 Source #

du_rawGroup_1284 :: T_AbelianGroup_1174 -> T_RawGroup_868 Source #

d_rawMagma_1286 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_RawMagma_8 Source #

du_rawMagma_1286 :: T_AbelianGroup_1174 -> T_RawMagma_8 Source #

d_rawMonoid_1288 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_RawMonoid_402 Source #

du_rawMonoid_1288 :: T_AbelianGroup_1174 -> T_RawMonoid_402 Source #

d_semigroup_1290 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_Semigroup_206 Source #

du_semigroup_1290 :: T_AbelianGroup_1174 -> T_Semigroup_206 Source #

d_commutativeMonoid_1292 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_CommutativeMonoid_582 Source #

du_commutativeMonoid_1292 :: T_AbelianGroup_1174 -> T_CommutativeMonoid_582 Source #

d_commutativeMagma_1296 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_CommutativeMagma_148 Source #

du_commutativeMagma_1296 :: T_AbelianGroup_1174 -> T_CommutativeMagma_148 Source #

d_commutativeSemigroup_1298 :: T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_1298 :: T_AbelianGroup_1174 -> T_CommutativeSemigroup_332 Source #

d_RawNearSemiring_1304 :: p1 -> p2 -> () Source #

data T_RawNearSemiring_1304 Source #

d_Carrier_1320 :: T_RawNearSemiring_1304 -> () Source #

d__'8776'__1322 :: T_RawNearSemiring_1304 -> AgdaAny -> AgdaAny -> () Source #

d__'43'__1324 :: T_RawNearSemiring_1304 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'42'__1326 :: T_RawNearSemiring_1304 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_1328 :: T_RawNearSemiring_1304 -> AgdaAny Source #

d_'43''45'rawMonoid_1330 :: T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawMonoid_402 Source #

du_'43''45'rawMonoid_1330 :: T_RawNearSemiring_1304 -> T_RawMonoid_402 Source #

d__'8777'__1334 :: T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> AgdaAny -> AgdaAny -> () Source #

d_rawMagma_1336 :: T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawMagma_8 Source #

du_rawMagma_1336 :: T_RawNearSemiring_1304 -> T_RawMagma_8 Source #

d_'42''45'rawMagma_1338 :: T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawMagma_8 Source #

du_'42''45'rawMagma_1338 :: T_RawNearSemiring_1304 -> T_RawMagma_8 Source #

d_NearSemiring_1344 :: p1 -> p2 -> () Source #

data T_NearSemiring_1344 Source #

d_Carrier_1362 :: T_NearSemiring_1344 -> () Source #

d__'8776'__1364 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> () Source #

d__'43'__1366 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'42'__1368 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_1370 :: T_NearSemiring_1344 -> AgdaAny Source #

d_isNearSemiring_1372 :: T_NearSemiring_1344 -> T_IsNearSemiring_826 Source #

d_'42''45'assoc_1376 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1378 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1380 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1380 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1382 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1382 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1384 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1384 :: T_NearSemiring_1344 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_1386 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1386 :: T_NearSemiring_1344 -> T_IsSemigroup_206 Source #

d_assoc_1388 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1390 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1392 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1392 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1394 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1394 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1396 :: T_NearSemiring_1344 -> T_Σ_14 Source #

d_identity'691'_1398 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1398 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1400 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1400 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny Source #

d_isMagma_1402 :: T_NearSemiring_1344 -> T_IsMagma_98 Source #

d_'43''45'isMonoid_1404 :: T_NearSemiring_1344 -> T_IsMonoid_370 Source #

d_isSemigroup_1406 :: T_NearSemiring_1344 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1408 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1408 :: T_NearSemiring_1344 -> T_IsUnitalMagma_326 Source #

d_distrib'691'_1410 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1412 :: T_NearSemiring_1344 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1414 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1414 :: T_NearSemiring_1344 -> T_IsPartialEquivalence_16 Source #

d_refl_1416 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny Source #

d_reflexive_1418 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1418 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1420 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_Setoid_44 Source #

du_setoid_1420 :: T_NearSemiring_1344 -> T_Setoid_44 Source #

d_sym_1422 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1424 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'737'_1426 :: T_NearSemiring_1344 -> AgdaAny -> AgdaAny Source #

d_rawNearSemiring_1428 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_RawNearSemiring_1304 Source #

du_rawNearSemiring_1428 :: T_NearSemiring_1344 -> T_RawNearSemiring_1304 Source #

d_'43''45'monoid_1430 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_Monoid_502 Source #

du_'43''45'monoid_1430 :: T_NearSemiring_1344 -> T_Monoid_502 Source #

d__'8777'__1434 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> AgdaAny -> AgdaAny -> () Source #

d_magma_1436 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_Magma_36 Source #

du_magma_1436 :: T_NearSemiring_1344 -> T_Magma_36 Source #

d_rawMagma_1438 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_RawMagma_8 Source #

du_rawMagma_1438 :: T_NearSemiring_1344 -> T_RawMagma_8 Source #

d_rawMonoid_1440 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_RawMonoid_402 Source #

du_rawMonoid_1440 :: T_NearSemiring_1344 -> T_RawMonoid_402 Source #

d_semigroup_1442 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_Semigroup_206 Source #

du_semigroup_1442 :: T_NearSemiring_1344 -> T_Semigroup_206 Source #

d_unitalMagma_1444 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_UnitalMagma_434 Source #

du_unitalMagma_1444 :: T_NearSemiring_1344 -> T_UnitalMagma_434 Source #

d_'42''45'semigroup_1446 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_Semigroup_206 Source #

du_'42''45'semigroup_1446 :: T_NearSemiring_1344 -> T_Semigroup_206 Source #

d_magma_1450 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_Magma_36 Source #

du_magma_1450 :: T_NearSemiring_1344 -> T_Magma_36 Source #

d_rawMagma_1452 :: T_Level_14 -> T_Level_14 -> T_NearSemiring_1344 -> T_RawMagma_8 Source #

du_rawMagma_1452 :: T_NearSemiring_1344 -> T_RawMagma_8 Source #

d_SemiringWithoutOne_1458 :: p1 -> p2 -> () Source #

data T_SemiringWithoutOne_1458 Source #

d_Carrier_1476 :: T_SemiringWithoutOne_1458 -> () Source #

d__'8776'__1478 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> () Source #

d__'43'__1480 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'42'__1482 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_1484 :: T_SemiringWithoutOne_1458 -> AgdaAny Source #

d_isSemiringWithoutOne_1486 :: T_SemiringWithoutOne_1458 -> T_IsSemiringWithoutOne_906 Source #

d_'42''45'assoc_1490 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1492 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1494 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1494 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1496 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1496 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1498 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1498 :: T_SemiringWithoutOne_1458 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_1500 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1500 :: T_SemiringWithoutOne_1458 -> T_IsSemigroup_206 Source #

d_comm_1502 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1504 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1504 :: T_SemiringWithoutOne_1458 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1506 :: T_SemiringWithoutOne_1458 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1508 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1508 :: T_SemiringWithoutOne_1458 -> T_IsCommutativeSemigroup_282 Source #

d_isMonoid_1510 :: T_SemiringWithoutOne_1458 -> T_IsMonoid_370 Source #

d_distrib_1512 :: T_SemiringWithoutOne_1458 -> T_Σ_14 Source #

d_isEquivalence_1514 :: T_SemiringWithoutOne_1458 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1516 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1516 :: T_SemiringWithoutOne_1458 -> T_IsNearSemiring_826 Source #

d_zero_1518 :: T_SemiringWithoutOne_1458 -> T_Σ_14 Source #

d_zero'691'_1520 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1520 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1522 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1522 :: T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny Source #

d_nearSemiring_1524 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_NearSemiring_1344 Source #

du_nearSemiring_1524 :: T_SemiringWithoutOne_1458 -> T_NearSemiring_1344 Source #

d__'8777'__1528 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> AgdaAny -> AgdaAny -> () Source #

d_magma_1530 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_Magma_36 Source #

du_magma_1530 :: T_SemiringWithoutOne_1458 -> T_Magma_36 Source #

d_rawMagma_1532 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_RawMagma_8 Source #

du_rawMagma_1532 :: T_SemiringWithoutOne_1458 -> T_RawMagma_8 Source #

d_'42''45'semigroup_1534 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_Semigroup_206 Source #

du_'42''45'semigroup_1534 :: T_SemiringWithoutOne_1458 -> T_Semigroup_206 Source #

d_magma_1536 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_Magma_36 Source #

du_magma_1536 :: T_SemiringWithoutOne_1458 -> T_Magma_36 Source #

d_'43''45'monoid_1538 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_Monoid_502 Source #

du_'43''45'monoid_1538 :: T_SemiringWithoutOne_1458 -> T_Monoid_502 Source #

d_rawMagma_1540 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_RawMagma_8 Source #

du_rawMagma_1540 :: T_SemiringWithoutOne_1458 -> T_RawMagma_8 Source #

d_rawMonoid_1542 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_RawMonoid_402 Source #

du_rawMonoid_1542 :: T_SemiringWithoutOne_1458 -> T_RawMonoid_402 Source #

d_semigroup_1544 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_Semigroup_206 Source #

du_semigroup_1544 :: T_SemiringWithoutOne_1458 -> T_Semigroup_206 Source #

d_unitalMagma_1546 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_UnitalMagma_434 Source #

du_unitalMagma_1546 :: T_SemiringWithoutOne_1458 -> T_UnitalMagma_434 Source #

d_rawNearSemiring_1548 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_RawNearSemiring_1304 Source #

du_rawNearSemiring_1548 :: T_SemiringWithoutOne_1458 -> T_RawNearSemiring_1304 Source #

d_'43''45'commutativeMonoid_1550 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_1550 :: T_SemiringWithoutOne_1458 -> T_CommutativeMonoid_582 Source #

d_commutativeMagma_1554 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_CommutativeMagma_148 Source #

du_commutativeMagma_1554 :: T_SemiringWithoutOne_1458 -> T_CommutativeMagma_148 Source #

d_commutativeSemigroup_1556 :: T_Level_14 -> T_Level_14 -> T_SemiringWithoutOne_1458 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_1556 :: T_SemiringWithoutOne_1458 -> T_CommutativeSemigroup_332 Source #

d_CommutativeSemiringWithoutOne_1562 :: p1 -> p2 -> () Source #

data T_CommutativeSemiringWithoutOne_1562 Source #

d_Carrier_1580 :: T_CommutativeSemiringWithoutOne_1562 -> () Source #

d__'8776'__1582 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> () Source #

d__'43'__1584 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'42'__1586 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_1588 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny Source #

d_isCommutativeSemiringWithoutOne_1590 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_'42''45'assoc_1594 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_1596 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1598 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1600 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1600 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1602 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1602 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1604 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1604 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeSemigroup_1606 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_1606 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_1608 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1608 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_1610 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1610 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsSemigroup_206 Source #

d_comm_1612 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1614 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1614 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1616 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1618 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1618 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsCommutativeSemigroup_282 Source #

d_isMonoid_1620 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsMonoid_370 Source #

d_distrib_1622 :: T_CommutativeSemiringWithoutOne_1562 -> T_Σ_14 Source #

d_isEquivalence_1624 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1626 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1626 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsNearSemiring_826 Source #

d_isSemiringWithoutOne_1628 :: T_CommutativeSemiringWithoutOne_1562 -> T_IsSemiringWithoutOne_906 Source #

d_zero_1630 :: T_CommutativeSemiringWithoutOne_1562 -> T_Σ_14 Source #

d_zero'691'_1632 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1632 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1634 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1634 :: T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny Source #

d_semiringWithoutOne_1636 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_SemiringWithoutOne_1458 Source #

du_semiringWithoutOne_1636 :: T_CommutativeSemiringWithoutOne_1562 -> T_SemiringWithoutOne_1458 Source #

d__'8777'__1640 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> AgdaAny -> AgdaAny -> () Source #

d_magma_1642 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_Magma_36 Source #

du_magma_1642 :: T_CommutativeSemiringWithoutOne_1562 -> T_Magma_36 Source #

d_rawMagma_1644 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_RawMagma_8 Source #

du_rawMagma_1644 :: T_CommutativeSemiringWithoutOne_1562 -> T_RawMagma_8 Source #

d_'42''45'semigroup_1646 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_Semigroup_206 Source #

du_'42''45'semigroup_1646 :: T_CommutativeSemiringWithoutOne_1562 -> T_Semigroup_206 Source #

d_'43''45'commutativeMonoid_1648 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_1648 :: T_CommutativeSemiringWithoutOne_1562 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_1650 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_1650 :: T_CommutativeSemiringWithoutOne_1562 -> T_CommutativeSemigroup_332 Source #

d_magma_1652 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_Magma_36 Source #

du_magma_1652 :: T_CommutativeSemiringWithoutOne_1562 -> T_Magma_36 Source #

d_'43''45'monoid_1654 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_Monoid_502 Source #

du_'43''45'monoid_1654 :: T_CommutativeSemiringWithoutOne_1562 -> T_Monoid_502 Source #

d_rawMagma_1656 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_RawMagma_8 Source #

du_rawMagma_1656 :: T_CommutativeSemiringWithoutOne_1562 -> T_RawMagma_8 Source #

d_rawMonoid_1658 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_RawMonoid_402 Source #

du_rawMonoid_1658 :: T_CommutativeSemiringWithoutOne_1562 -> T_RawMonoid_402 Source #

d_semigroup_1660 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_Semigroup_206 Source #

du_semigroup_1660 :: T_CommutativeSemiringWithoutOne_1562 -> T_Semigroup_206 Source #

d_unitalMagma_1662 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_UnitalMagma_434 Source #

du_unitalMagma_1662 :: T_CommutativeSemiringWithoutOne_1562 -> T_UnitalMagma_434 Source #

d_nearSemiring_1664 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_NearSemiring_1344 Source #

du_nearSemiring_1664 :: T_CommutativeSemiringWithoutOne_1562 -> T_NearSemiring_1344 Source #

d_rawNearSemiring_1666 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiringWithoutOne_1562 -> T_RawNearSemiring_1304 Source #