Documentation

d_RawMagma_8 ∷ p → p → () 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_18 → T_Level_18 → T_RawMagma_8 → AgdaAny → AgdaAny → () Source #

d_Magma_36 ∷ p → p → () 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_86 Source #

d_isEquivalence_60 ∷ T_Magma_36 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_62 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_Magma_36 → T_RawMagma_8 Source #

du_rawMagma_80 ∷ T_Magma_36 → T_RawMagma_8 Source #

d__'8777'__84 ∷ T_Level_18 → T_Level_18 → T_Magma_36 → AgdaAny → AgdaAny → () Source #

d_SelectiveMagma_90 ∷ p → p → () 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_158 Source #

d_isEquivalence_114 ∷ T_SelectiveMagma_90 → T_IsEquivalence_26 Source #

d_isMagma_116 ∷ T_SelectiveMagma_90 → T_IsMagma_86 Source #

d_isPartialEquivalence_118 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_SelectiveMagma_90 → T_Magma_36 Source #

du_magma_138 ∷ T_SelectiveMagma_90 → T_Magma_36 Source #

d_rawMagma_142 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_90 → T_RawMagma_8 Source #

du_rawMagma_142 ∷ T_SelectiveMagma_90 → T_RawMagma_8 Source #

d_CommutativeMagma_148 ∷ p → p → () 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_122 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_86 Source #

d_isPartialEquivalence_178 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_CommutativeMagma_148 → T_Magma_36 Source #

du_magma_196 ∷ T_CommutativeMagma_148 → T_Magma_36 Source #

d_rawMagma_200 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_148 → T_RawMagma_8 Source #

du_rawMagma_200 ∷ T_CommutativeMagma_148 → T_RawMagma_8 Source #

d_Semigroup_206 ∷ p → p → () 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_194 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_86 Source #

d_isPartialEquivalence_236 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_Semigroup_206 → T_Magma_36 Source #

du_magma_254 ∷ T_Semigroup_206 → T_Magma_36 Source #

d__'8777'__258 ∷ T_Level_18 → T_Level_18 → T_Semigroup_206 → AgdaAny → AgdaAny → () Source #

d_rawMagma_260 ∷ T_Level_18 → T_Level_18 → T_Semigroup_206 → T_RawMagma_8 Source #

du_rawMagma_260 ∷ T_Semigroup_206 → T_RawMagma_8 Source #

d_Band_266 ∷ p → p → () 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_230 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_86 Source #

d_isPartialEquivalence_298 ∷ T_Level_18 → T_Level_18 → 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_194 Source #

d_refl_302 ∷ T_Band_266 → AgdaAny → AgdaAny Source #

d_reflexive_304 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_Band_266 → T_Semigroup_206 Source #

du_semigroup_318 ∷ T_Band_266 → T_Semigroup_206 Source #

d__'8777'__322 ∷ T_Level_18 → T_Level_18 → T_Band_266 → AgdaAny → AgdaAny → () Source #

d_magma_324 ∷ T_Level_18 → T_Level_18 → T_Band_266 → T_Magma_36 Source #

du_magma_324 ∷ T_Band_266 → T_Magma_36 Source #

d_rawMagma_326 ∷ T_Level_18 → T_Level_18 → T_Band_266 → T_RawMagma_8 Source #

du_rawMagma_326 ∷ T_Band_266 → T_RawMagma_8 Source #

d_CommutativeSemigroup_332 ∷ p → p → () 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_270 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_18 → T_Level_18 → T_CommutativeSemigroup_332 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_360 ∷ T_CommutativeSemigroup_332 → T_IsCommutativeMagma_122 Source #

d_isEquivalence_362 ∷ T_CommutativeSemigroup_332 → T_IsEquivalence_26 Source #

d_isMagma_364 ∷ T_CommutativeSemigroup_332 → T_IsMagma_86 Source #

d_isPartialEquivalence_366 ∷ T_Level_18 → T_Level_18 → 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_194 Source #

d_refl_370 ∷ T_CommutativeSemigroup_332 → AgdaAny → AgdaAny Source #

d_reflexive_372 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_CommutativeSemigroup_332 → T_Semigroup_206 Source #

du_semigroup_386 ∷ T_CommutativeSemigroup_332 → T_Semigroup_206 Source #

d__'8777'__390 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_332 → AgdaAny → AgdaAny → () Source #

d_magma_392 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_332 → T_Magma_36 Source #

du_magma_392 ∷ T_CommutativeSemigroup_332 → T_Magma_36 Source #

d_rawMagma_394 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_332 → T_RawMagma_8 Source #

du_rawMagma_394 ∷ T_CommutativeSemigroup_332 → T_RawMagma_8 Source #

d_commutativeMagma_396 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_332 → T_CommutativeMagma_148 Source #

du_commutativeMagma_396 ∷ T_CommutativeSemigroup_332 → T_CommutativeMagma_148 Source #

d_Semilattice_402 ∷ p → p → () Source #

data T_Semilattice_402 Source #

d_Carrier_416 ∷ T_Semilattice_402 → () Source #

d__'8776'__418 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → () Source #

d__'8743'__420 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemilattice_422 ∷ T_Semilattice_402 → T_IsSemilattice_312 Source #

d_assoc_426 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_428 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_430 ∷ T_Semilattice_402 → AgdaAny → AgdaAny Source #

d_isBand_432 ∷ T_Semilattice_402 → T_IsBand_230 Source #

d_isEquivalence_434 ∷ T_Semilattice_402 → T_IsEquivalence_26 Source #

d_isMagma_436 ∷ T_Semilattice_402 → T_IsMagma_86 Source #

d_isPartialEquivalence_438 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_438 ∷ T_Semilattice_402 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_440 ∷ T_Semilattice_402 → T_IsSemigroup_194 Source #

d_refl_442 ∷ T_Semilattice_402 → AgdaAny → AgdaAny Source #

d_reflexive_444 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_444 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_446 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → T_Setoid_44 Source #

du_setoid_446 ∷ T_Semilattice_402 → T_Setoid_44 Source #

d_sym_448 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_450 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_452 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_454 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_454 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_456 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_456 ∷ T_Semilattice_402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_band_458 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → T_Band_266 Source #

du_band_458 ∷ T_Semilattice_402 → T_Band_266 Source #

d__'8777'__462 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → AgdaAny → AgdaAny → () Source #

d_magma_464 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → T_Magma_36 Source #

du_magma_464 ∷ T_Semilattice_402 → T_Magma_36 Source #

d_rawMagma_466 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → T_RawMagma_8 Source #

du_rawMagma_466 ∷ T_Semilattice_402 → T_RawMagma_8 Source #

d_semigroup_468 ∷ T_Level_18 → T_Level_18 → T_Semilattice_402 → T_Semigroup_206 Source #

du_semigroup_468 ∷ T_Semilattice_402 → T_Semigroup_206 Source #

d_RawMonoid_474 ∷ p → p → () Source #

data T_RawMonoid_474 Source #

d_Carrier_488 ∷ T_RawMonoid_474 → () Source #

d__'8776'__490 ∷ T_RawMonoid_474 → AgdaAny → AgdaAny → () Source #

d__'8729'__492 ∷ T_RawMonoid_474 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_494 ∷ T_RawMonoid_474 → AgdaAny Source #

d_rawMagma_496 ∷ T_Level_18 → T_Level_18 → T_RawMonoid_474 → T_RawMagma_8 Source #

du_rawMagma_496 ∷ T_RawMonoid_474 → T_RawMagma_8 Source #

d__'8777'__500 ∷ T_Level_18 → T_Level_18 → T_RawMonoid_474 → AgdaAny → AgdaAny → () Source #

d_Monoid_506 ∷ p → p → () Source #

data T_Monoid_506 Source #

d_Carrier_522 ∷ T_Monoid_506 → () Source #

d__'8776'__524 ∷ T_Monoid_506 → AgdaAny → AgdaAny → () Source #

d__'8729'__526 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_528 ∷ T_Monoid_506 → AgdaAny Source #

d_isMonoid_530 ∷ T_Monoid_506 → T_IsMonoid_358 Source #

d_assoc_534 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_536 ∷ T_Monoid_506 → T_Σ_14 Source #

d_identity'691'_538 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → AgdaAny → AgdaAny Source #

du_identity'691'_538 ∷ T_Monoid_506 → AgdaAny → AgdaAny Source #

d_identity'737'_540 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → AgdaAny → AgdaAny Source #

du_identity'737'_540 ∷ T_Monoid_506 → AgdaAny → AgdaAny Source #

d_isEquivalence_542 ∷ T_Monoid_506 → T_IsEquivalence_26 Source #

d_isMagma_544 ∷ T_Monoid_506 → T_IsMagma_86 Source #

d_isPartialEquivalence_546 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_546 ∷ T_Monoid_506 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_548 ∷ T_Monoid_506 → T_IsSemigroup_194 Source #

d_refl_550 ∷ T_Monoid_506 → AgdaAny → AgdaAny Source #

d_reflexive_552 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_552 ∷ T_Monoid_506 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_554 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → T_Setoid_44 Source #

du_setoid_554 ∷ T_Monoid_506 → T_Setoid_44 Source #

d_sym_556 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_558 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_560 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_562 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_562 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_564 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_564 ∷ T_Monoid_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_566 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → T_Semigroup_206 Source #

du_semigroup_566 ∷ T_Monoid_506 → T_Semigroup_206 Source #

d__'8777'__570 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → AgdaAny → AgdaAny → () Source #

d_magma_572 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → T_Magma_36 Source #

du_magma_572 ∷ T_Monoid_506 → T_Magma_36 Source #

d_rawMagma_574 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → T_RawMagma_8 Source #

du_rawMagma_574 ∷ T_Monoid_506 → T_RawMagma_8 Source #

d_rawMonoid_576 ∷ T_Level_18 → T_Level_18 → T_Monoid_506 → T_RawMonoid_474 Source #

du_rawMonoid_576 ∷ T_Monoid_506 → T_RawMonoid_474 Source #

d_CommutativeMonoid_582 ∷ p → p → () 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_406 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_18 → T_Level_18 → T_CommutativeMonoid_582 → AgdaAny → AgdaAny Source #

du_identity'691'_616 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny Source #

d_identity'737'_618 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → AgdaAny → AgdaAny Source #

du_identity'737'_618 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_620 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_620 ∷ T_CommutativeMonoid_582 → T_IsCommutativeMagma_122 Source #

d_isCommutativeSemigroup_622 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_622 ∷ T_CommutativeMonoid_582 → T_IsCommutativeSemigroup_270 Source #

d_isEquivalence_624 ∷ T_CommutativeMonoid_582 → T_IsEquivalence_26 Source #

d_isMagma_626 ∷ T_CommutativeMonoid_582 → T_IsMagma_86 Source #

d_isMonoid_628 ∷ T_CommutativeMonoid_582 → T_IsMonoid_358 Source #

d_isPartialEquivalence_630 ∷ T_Level_18 → T_Level_18 → 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_194 Source #

d_refl_634 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny Source #

d_reflexive_636 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_636 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_638 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_Setoid_44 Source #

du_setoid_638 ∷ T_CommutativeMonoid_582 → T_Setoid_44 Source #

d_sym_640 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_642 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_644 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_646 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_646 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_648 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_648 ∷ T_CommutativeMonoid_582 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_monoid_650 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_Monoid_506 Source #

du_monoid_650 ∷ T_CommutativeMonoid_582 → T_Monoid_506 Source #

d__'8777'__654 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → AgdaAny → AgdaAny → () Source #

d_magma_656 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_Magma_36 Source #

du_magma_656 ∷ T_CommutativeMonoid_582 → T_Magma_36 Source #

d_rawMagma_658 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_RawMagma_8 Source #

du_rawMagma_658 ∷ T_CommutativeMonoid_582 → T_RawMagma_8 Source #

d_rawMonoid_660 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_RawMonoid_474 Source #

du_rawMonoid_660 ∷ T_CommutativeMonoid_582 → T_RawMonoid_474 Source #

d_semigroup_662 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_Semigroup_206 Source #

du_semigroup_662 ∷ T_CommutativeMonoid_582 → T_Semigroup_206 Source #

d_commutativeSemigroup_664 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_664 ∷ T_CommutativeMonoid_582 → T_CommutativeSemigroup_332 Source #

d_commutativeMagma_668 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMagma_148 Source #

du_commutativeMagma_668 ∷ T_CommutativeMonoid_582 → T_CommutativeMagma_148 Source #

d_IdempotentCommutativeMonoid_674 ∷ p → p → () Source #

data T_IdempotentCommutativeMonoid_674 Source #

d_Carrier_690 ∷ T_IdempotentCommutativeMonoid_674 → () Source #

d__'8776'__692 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → () Source #

d__'8729'__694 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_696 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny Source #

d_isIdempotentCommutativeMonoid_698 ∷ T_IdempotentCommutativeMonoid_674 → T_IsIdempotentCommutativeMonoid_464 Source #

d_assoc_702 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_704 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_706 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_identity_708 ∷ T_IdempotentCommutativeMonoid_674 → T_Σ_14 Source #

d_identity'691'_710 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

du_identity'691'_710 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_identity'737'_712 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

du_identity'737'_712 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_714 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_714 ∷ T_IdempotentCommutativeMonoid_674 → T_IsCommutativeMagma_122 Source #

d_isCommutativeMonoid_716 ∷ T_IdempotentCommutativeMonoid_674 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_718 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_718 ∷ T_IdempotentCommutativeMonoid_674 → T_IsCommutativeSemigroup_270 Source #

d_isEquivalence_720 ∷ T_IdempotentCommutativeMonoid_674 → T_IsEquivalence_26 Source #

d_isMagma_722 ∷ T_IdempotentCommutativeMonoid_674 → T_IsMagma_86 Source #

d_isMonoid_724 ∷ T_IdempotentCommutativeMonoid_674 → T_IsMonoid_358 Source #

d_isPartialEquivalence_726 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_726 ∷ T_IdempotentCommutativeMonoid_674 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_728 ∷ T_IdempotentCommutativeMonoid_674 → T_IsSemigroup_194 Source #

d_refl_730 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_reflexive_732 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_732 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_734 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Setoid_44 Source #

du_setoid_734 ∷ T_IdempotentCommutativeMonoid_674 → T_Setoid_44 Source #

d_sym_736 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_738 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_740 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_742 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_742 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_744 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_744 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeMonoid_746 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

du_commutativeMonoid_746 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

d__'8777'__750 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → () Source #

d_commutativeMagma_752 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_CommutativeMagma_148 Source #

du_commutativeMagma_752 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeMagma_148 Source #

d_commutativeSemigroup_754 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_754 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeSemigroup_332 Source #

d_magma_756 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Magma_36 Source #

du_magma_756 ∷ T_IdempotentCommutativeMonoid_674 → T_Magma_36 Source #

d_monoid_758 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

du_monoid_758 ∷ T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

d_rawMagma_760 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_RawMagma_8 Source #

du_rawMagma_760 ∷ T_IdempotentCommutativeMonoid_674 → T_RawMagma_8 Source #

d_rawMonoid_762 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_RawMonoid_474 Source #

du_rawMonoid_762 ∷ T_IdempotentCommutativeMonoid_674 → T_RawMonoid_474 Source #

d_semigroup_764 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Semigroup_206 Source #

du_semigroup_764 ∷ T_IdempotentCommutativeMonoid_674 → T_Semigroup_206 Source #

d_BoundedLattice_766 ∷ T_Level_18 → T_Level_18 → () Source #

d__'8729'__776 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__778 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → () Source #

d__'8777'__780 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → () Source #

d_Carrier_782 ∷ T_IdempotentCommutativeMonoid_674 → () Source #

d_assoc_784 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_786 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeMagma_788 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_CommutativeMagma_148 Source #

du_commutativeMagma_788 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeMagma_148 Source #

d_commutativeMonoid_790 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

du_commutativeMonoid_790 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_792 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_792 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeSemigroup_332 Source #

d_idem_794 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_identity_796 ∷ T_IdempotentCommutativeMonoid_674 → T_Σ_14 Source #

d_identity'691'_798 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

du_identity'691'_798 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_identity'737'_800 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

du_identity'737'_800 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_802 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_802 ∷ T_IdempotentCommutativeMonoid_674 → T_IsCommutativeMagma_122 Source #

d_isCommutativeMonoid_804 ∷ T_IdempotentCommutativeMonoid_674 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_806 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_806 ∷ T_IdempotentCommutativeMonoid_674 → T_IsCommutativeSemigroup_270 Source #

d_isEquivalence_808 ∷ T_IdempotentCommutativeMonoid_674 → T_IsEquivalence_26 Source #

d_isIdempotentCommutativeMonoid_810 ∷ T_IdempotentCommutativeMonoid_674 → T_IsIdempotentCommutativeMonoid_464 Source #

d_isMagma_812 ∷ T_IdempotentCommutativeMonoid_674 → T_IsMagma_86 Source #

d_isMonoid_814 ∷ T_IdempotentCommutativeMonoid_674 → T_IsMonoid_358 Source #

d_isPartialEquivalence_816 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_816 ∷ T_IdempotentCommutativeMonoid_674 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_818 ∷ T_IdempotentCommutativeMonoid_674 → T_IsSemigroup_194 Source #

d_magma_820 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Magma_36 Source #

du_magma_820 ∷ T_IdempotentCommutativeMonoid_674 → T_Magma_36 Source #

d_monoid_822 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

du_monoid_822 ∷ T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

d_rawMagma_824 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_RawMagma_8 Source #

du_rawMagma_824 ∷ T_IdempotentCommutativeMonoid_674 → T_RawMagma_8 Source #

d_rawMonoid_826 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_RawMonoid_474 Source #

du_rawMonoid_826 ∷ T_IdempotentCommutativeMonoid_674 → T_RawMonoid_474 Source #

d_refl_828 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny Source #

d_reflexive_830 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_830 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_semigroup_832 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Semigroup_206 Source #

du_semigroup_832 ∷ T_IdempotentCommutativeMonoid_674 → T_Semigroup_206 Source #

d_setoid_834 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_Setoid_44 Source #

du_setoid_834 ∷ T_IdempotentCommutativeMonoid_674 → T_Setoid_44 Source #

d_sym_836 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_838 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_840 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny Source #

d_'8729''45'cong_842 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_844 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_844 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_846 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_846 ∷ T_IdempotentCommutativeMonoid_674 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_RawGroup_852 ∷ p → p → () Source #

data T_RawGroup_852 Source #

d_Carrier_868 ∷ T_RawGroup_852 → () Source #

d__'8776'__870 ∷ T_RawGroup_852 → AgdaAny → AgdaAny → () Source #

d__'8729'__872 ∷ T_RawGroup_852 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_874 ∷ T_RawGroup_852 → AgdaAny Source #

d__'8315''185'_876 ∷ T_RawGroup_852 → AgdaAny → AgdaAny Source #

d_rawMonoid_878 ∷ T_Level_18 → T_Level_18 → T_RawGroup_852 → T_RawMonoid_474 Source #

du_rawMonoid_878 ∷ T_RawGroup_852 → T_RawMonoid_474 Source #

d__'8777'__882 ∷ T_Level_18 → T_Level_18 → T_RawGroup_852 → AgdaAny → AgdaAny → () Source #

d_rawMagma_884 ∷ T_Level_18 → T_Level_18 → T_RawGroup_852 → T_RawMagma_8 Source #

du_rawMagma_884 ∷ T_RawGroup_852 → T_RawMagma_8 Source #

d_Group_890 ∷ p → p → () Source #

data T_Group_890 Source #

d_Carrier_908 ∷ T_Group_890 → () Source #

d__'8776'__910 ∷ T_Group_890 → AgdaAny → AgdaAny → () Source #

d__'8729'__912 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_914 ∷ T_Group_890 → AgdaAny Source #

d__'8315''185'_916 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_isGroup_918 ∷ T_Group_890 → T_IsGroup_580 Source #

d__'45'__922 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → AgdaAny Source #

du__'45'__922 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_924 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_926 ∷ T_Group_890 → T_Σ_14 Source #

d_identity'691'_928 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny Source #

du_identity'691'_928 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_identity'737'_930 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny Source #

du_identity'737'_930 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_inverse_932 ∷ T_Group_890 → T_Σ_14 Source #

d_inverse'691'_934 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny Source #

du_inverse'691'_934 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_inverse'737'_936 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny Source #

du_inverse'737'_936 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_isEquivalence_938 ∷ T_Group_890 → T_IsEquivalence_26 Source #

d_isMagma_940 ∷ T_Group_890 → T_IsMagma_86 Source #

d_isMonoid_942 ∷ T_Group_890 → T_IsMonoid_358 Source #

d_isPartialEquivalence_944 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_944 ∷ T_Group_890 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_946 ∷ T_Group_890 → T_IsSemigroup_194 Source #

d_refl_948 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_reflexive_950 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_950 ∷ T_Group_890 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_952 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_Setoid_44 Source #

du_setoid_952 ∷ T_Group_890 → T_Setoid_44 Source #

d_sym_954 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_956 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_958 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_958 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_960 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_960 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_962 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_964 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_966 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_966 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_968 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_968 ∷ T_Group_890 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawGroup_970 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_RawGroup_852 Source #

du_rawGroup_970 ∷ T_Group_890 → T_RawGroup_852 Source #

d_monoid_972 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_Monoid_506 Source #

du_monoid_972 ∷ T_Group_890 → T_Monoid_506 Source #

d__'8777'__976 ∷ T_Level_18 → T_Level_18 → T_Group_890 → AgdaAny → AgdaAny → () Source #

d_magma_978 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_Magma_36 Source #

du_magma_978 ∷ T_Group_890 → T_Magma_36 Source #

d_rawMagma_980 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_RawMagma_8 Source #

du_rawMagma_980 ∷ T_Group_890 → T_RawMagma_8 Source #

d_rawMonoid_982 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_RawMonoid_474 Source #

du_rawMonoid_982 ∷ T_Group_890 → T_RawMonoid_474 Source #

d_semigroup_984 ∷ T_Level_18 → T_Level_18 → T_Group_890 → T_Semigroup_206 Source #

du_semigroup_984 ∷ T_Group_890 → T_Semigroup_206 Source #

d_AbelianGroup_990 ∷ p → p → () Source #

data T_AbelianGroup_990 Source #

d_Carrier_1008 ∷ T_AbelianGroup_990 → () Source #

d__'8776'__1010 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → () Source #

d__'8729'__1012 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1014 ∷ T_AbelianGroup_990 → AgdaAny Source #

d__'8315''185'_1016 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

d_isAbelianGroup_1018 ∷ T_AbelianGroup_990 → T_IsAbelianGroup_662 Source #

d__'45'__1022 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny Source #

du__'45'__1022 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1024 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1026 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1028 ∷ T_AbelianGroup_990 → T_Σ_14 Source #

d_identity'691'_1030 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

du_identity'691'_1030 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

d_identity'737'_1032 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

du_identity'737'_1032 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

d_inverse_1034 ∷ T_AbelianGroup_990 → T_Σ_14 Source #

d_inverse'691'_1036 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

du_inverse'691'_1036 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

d_inverse'737'_1038 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

du_inverse'737'_1038 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1040 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1040 ∷ T_AbelianGroup_990 → T_IsCommutativeMagma_122 Source #

d_isCommutativeMonoid_1042 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_IsCommutativeMonoid_406 Source #

du_isCommutativeMonoid_1042 ∷ T_AbelianGroup_990 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1044 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1044 ∷ T_AbelianGroup_990 → T_IsCommutativeSemigroup_270 Source #

d_isEquivalence_1046 ∷ T_AbelianGroup_990 → T_IsEquivalence_26 Source #

d_isGroup_1048 ∷ T_AbelianGroup_990 → T_IsGroup_580 Source #

d_isMagma_1050 ∷ T_AbelianGroup_990 → T_IsMagma_86 Source #

d_isMonoid_1052 ∷ T_AbelianGroup_990 → T_IsMonoid_358 Source #

d_isPartialEquivalence_1054 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1054 ∷ T_AbelianGroup_990 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1056 ∷ T_AbelianGroup_990 → T_IsSemigroup_194 Source #

d_refl_1058 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny Source #

d_reflexive_1060 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1060 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1062 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_Setoid_44 Source #

du_setoid_1062 ∷ T_AbelianGroup_990 → T_Setoid_44 Source #

d_sym_1064 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1066 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1068 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1068 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1070 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1070 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1072 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1074 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1076 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1076 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1078 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1078 ∷ T_AbelianGroup_990 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_group_1080 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_Group_890 Source #

du_group_1080 ∷ T_AbelianGroup_990 → T_Group_890 Source #

d__'8777'__1084 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → AgdaAny → AgdaAny → () Source #

d_magma_1086 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_Magma_36 Source #

du_magma_1086 ∷ T_AbelianGroup_990 → T_Magma_36 Source #

d_monoid_1088 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_Monoid_506 Source #

du_monoid_1088 ∷ T_AbelianGroup_990 → T_Monoid_506 Source #

d_rawGroup_1090 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_RawGroup_852 Source #

du_rawGroup_1090 ∷ T_AbelianGroup_990 → T_RawGroup_852 Source #

d_rawMagma_1092 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_RawMagma_8 Source #

du_rawMagma_1092 ∷ T_AbelianGroup_990 → T_RawMagma_8 Source #

d_rawMonoid_1094 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_RawMonoid_474 Source #

du_rawMonoid_1094 ∷ T_AbelianGroup_990 → T_RawMonoid_474 Source #

d_semigroup_1096 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_Semigroup_206 Source #

du_semigroup_1096 ∷ T_AbelianGroup_990 → T_Semigroup_206 Source #

d_commutativeMonoid_1098 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_CommutativeMonoid_582 Source #

du_commutativeMonoid_1098 ∷ T_AbelianGroup_990 → T_CommutativeMonoid_582 Source #

d_commutativeMagma_1102 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_CommutativeMagma_148 Source #

du_commutativeMagma_1102 ∷ T_AbelianGroup_990 → T_CommutativeMagma_148 Source #

d_commutativeSemigroup_1104 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_1104 ∷ T_AbelianGroup_990 → T_CommutativeSemigroup_332 Source #

d_RawLattice_1110 ∷ p → p → () Source #

data T_RawLattice_1110 Source #

d_Carrier_1124 ∷ T_RawLattice_1110 → () Source #

d__'8776'__1126 ∷ T_RawLattice_1110 → AgdaAny → AgdaAny → () Source #

d__'8743'__1128 ∷ T_RawLattice_1110 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8744'__1130 ∷ T_RawLattice_1110 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'rawMagma_1132 ∷ T_Level_18 → T_Level_18 → T_RawLattice_1110 → T_RawMagma_8 Source #

du_'8744''45'rawMagma_1132 ∷ T_RawLattice_1110 → T_RawMagma_8 Source #

d_'8743''45'rawMagma_1134 ∷ T_Level_18 → T_Level_18 → T_RawLattice_1110 → T_RawMagma_8 Source #

du_'8743''45'rawMagma_1134 ∷ T_RawLattice_1110 → T_RawMagma_8 Source #

d__'8777'__1138 ∷ T_Level_18 → T_Level_18 → T_RawLattice_1110 → AgdaAny → AgdaAny → () Source #

d_Lattice_1144 ∷ p → p → () Source #

data T_Lattice_1144 Source #

d_Carrier_1160 ∷ T_Lattice_1144 → () Source #

d__'8776'__1162 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → () Source #

d__'8744'__1164 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__1166 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_1168 ∷ T_Lattice_1144 → T_IsLattice_740 Source #

d_absorptive_1172 ∷ T_Lattice_1144 → T_Σ_14 Source #

d_isEquivalence_1174 ∷ T_Lattice_1144 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1176 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1176 ∷ T_Lattice_1144 → T_IsPartialEquivalence_16 Source #

d_refl_1178 ∷ T_Lattice_1144 → AgdaAny → AgdaAny Source #

d_reflexive_1180 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1180 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1182 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1184 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_1186 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_1186 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_1188 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_1190 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_1192 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_1194 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_1194 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_1196 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_1196 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_1198 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_1198 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_1200 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_1202 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_1204 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_1206 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_1206 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_1208 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_1208 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawLattice_1210 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_RawLattice_1110 Source #

du_rawLattice_1210 ∷ T_Lattice_1144 → T_RawLattice_1110 Source #

d_'8743''45'rawMagma_1214 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_RawMagma_8 Source #

du_'8743''45'rawMagma_1214 ∷ T_Lattice_1144 → T_RawMagma_8 Source #

d_'8744''45'rawMagma_1216 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_RawMagma_8 Source #

du_'8744''45'rawMagma_1216 ∷ T_Lattice_1144 → T_RawMagma_8 Source #

d_setoid_1218 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Setoid_44 Source #

du_setoid_1218 ∷ T_Lattice_1144 → T_Setoid_44 Source #

d__'8777'__1222 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → () Source #

d_DistributiveLattice_1228 ∷ p → p → () Source #

data T_DistributiveLattice_1228 Source #

d_Carrier_1244 ∷ T_DistributiveLattice_1228 → () Source #

d__'8776'__1246 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → () Source #

d__'8744'__1248 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__1250 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

d_isDistributiveLattice_1252 ∷ T_DistributiveLattice_1228 → T_IsDistributiveLattice_814 Source #

d_absorptive_1256 ∷ T_DistributiveLattice_1228 → T_Σ_14 Source #

d_isEquivalence_1258 ∷ T_DistributiveLattice_1228 → T_IsEquivalence_26 Source #

d_isLattice_1260 ∷ T_DistributiveLattice_1228 → T_IsLattice_740 Source #

d_isPartialEquivalence_1262 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1262 ∷ T_DistributiveLattice_1228 → T_IsPartialEquivalence_16 Source #

d_refl_1264 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

d_reflexive_1266 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1266 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1268 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1270 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_1272 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_1272 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_1274 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_1276 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_1278 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_1280 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_1280 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_1282 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_1282 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_1284 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_1284 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_1286 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_1288 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_1290 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_1292 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_1292 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_1294 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_1294 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'691''45''8743'_1296 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45''8743''45'distrib'691'_1298 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45''8743''45'distrib'691'_1298 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lattice_1300 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Lattice_1144 Source #

du_lattice_1300 ∷ T_DistributiveLattice_1228 → T_Lattice_1144 Source #

d__'8777'__1304 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → () Source #

d_rawLattice_1306 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_RawLattice_1110 Source #

du_rawLattice_1306 ∷ T_DistributiveLattice_1228 → T_RawLattice_1110 Source #

d_setoid_1308 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Setoid_44 Source #

du_setoid_1308 ∷ T_DistributiveLattice_1228 → T_Setoid_44 Source #

d_RawNearSemiring_1314 ∷ p → p → () Source #

data T_RawNearSemiring_1314 Source #

d_Carrier_1330 ∷ T_RawNearSemiring_1314 → () Source #

d__'8776'__1332 ∷ T_RawNearSemiring_1314 → AgdaAny → AgdaAny → () Source #

d__'43'__1334 ∷ T_RawNearSemiring_1314 → AgdaAny → AgdaAny → AgdaAny Source #

d__'42'__1336 ∷ T_RawNearSemiring_1314 → AgdaAny → AgdaAny → AgdaAny Source #

d_0'35'_1338 ∷ T_RawNearSemiring_1314 → AgdaAny Source #

d_'43''45'rawMonoid_1340 ∷ T_Level_18 → T_Level_18 → T_RawNearSemiring_1314 → T_RawMonoid_474 Source #

du_'43''45'rawMonoid_1340 ∷ T_RawNearSemiring_1314 → T_RawMonoid_474 Source #

d__'8777'__1344 ∷ T_Level_18 → T_Level_18 → T_RawNearSemiring_1314 → AgdaAny → AgdaAny → () Source #

d_rawMagma_1346 ∷ T_Level_18 → T_Level_18 → T_RawNearSemiring_1314 → T_RawMagma_8 Source #

du_rawMagma_1346 ∷ T_RawNearSemiring_1314 → T_RawMagma_8 Source #

d_'42''45'rawMagma_1348 ∷ T_Level_18 → T_Level_18 → T_RawNearSemiring_1314 → T_RawMagma_8 Source #

du_'42''45'rawMagma_1348 ∷ T_RawNearSemiring_1314 → T_RawMagma_8 Source #

d_NearSemiring_1354 ∷ p → p → () Source #

data T_NearSemiring_1354 Source #

d_Carrier_1372 ∷ T_NearSemiring_1354 → () Source #

d__'8776'__1374 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → () Source #

d__'43'__1376 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny Source #

d__'42'__1378 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny Source #

d_0'35'_1380 ∷ T_NearSemiring_1354 → AgdaAny Source #

d_isNearSemiring_1382 ∷ T_NearSemiring_1354 → T_IsNearSemiring_876 Source #

d_assoc_1386 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1388 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1390 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1390 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1392 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1392 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_1394 ∷ T_NearSemiring_1354 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1396 ∷ T_NearSemiring_1354 → T_IsSemigroup_194 Source #

d_assoc_1398 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1400 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1402 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1402 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1404 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1404 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1406 ∷ T_NearSemiring_1354 → T_Σ_14 Source #

d_identity'691'_1408 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny Source #

du_identity'691'_1408 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny Source #

d_identity'737'_1410 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny Source #

du_identity'737'_1410 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny Source #

d_isMagma_1412 ∷ T_NearSemiring_1354 → T_IsMagma_86 Source #

d_'43''45'isMonoid_1414 ∷ T_NearSemiring_1354 → T_IsMonoid_358 Source #

d_isSemigroup_1416 ∷ T_NearSemiring_1354 → T_IsSemigroup_194 Source #

d_distrib'691'_1418 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1420 ∷ T_NearSemiring_1354 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1422 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1422 ∷ T_NearSemiring_1354 → T_IsPartialEquivalence_16 Source #

d_refl_1424 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny Source #

d_reflexive_1426 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1426 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1428 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_Setoid_44 Source #

du_setoid_1428 ∷ T_NearSemiring_1354 → T_Setoid_44 Source #

d_sym_1430 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1432 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_1434 ∷ T_NearSemiring_1354 → AgdaAny → AgdaAny Source #

d_rawNearSemiring_1436 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_RawNearSemiring_1314 Source #

du_rawNearSemiring_1436 ∷ T_NearSemiring_1354 → T_RawNearSemiring_1314 Source #

d_'43''45'monoid_1438 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_Monoid_506 Source #

du_'43''45'monoid_1438 ∷ T_NearSemiring_1354 → T_Monoid_506 Source #

d__'8777'__1442 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → AgdaAny → AgdaAny → () Source #

d_magma_1444 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_Magma_36 Source #

du_magma_1444 ∷ T_NearSemiring_1354 → T_Magma_36 Source #

d_rawMagma_1446 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_RawMagma_8 Source #

du_rawMagma_1446 ∷ T_NearSemiring_1354 → T_RawMagma_8 Source #

d_rawMonoid_1448 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_RawMonoid_474 Source #

du_rawMonoid_1448 ∷ T_NearSemiring_1354 → T_RawMonoid_474 Source #

d_semigroup_1450 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_Semigroup_206 Source #

du_semigroup_1450 ∷ T_NearSemiring_1354 → T_Semigroup_206 Source #

d_'42''45'semigroup_1452 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_Semigroup_206 Source #

du_'42''45'semigroup_1452 ∷ T_NearSemiring_1354 → T_Semigroup_206 Source #

d_magma_1456 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_Magma_36 Source #

du_magma_1456 ∷ T_NearSemiring_1354 → T_Magma_36 Source #

d_rawMagma_1458 ∷ T_Level_18 → T_Level_18 → T_NearSemiring_1354 → T_RawMagma_8 Source #

du_rawMagma_1458 ∷ T_NearSemiring_1354 → T_RawMagma_8 Source #

d_SemiringWithoutOne_1464 ∷ p → p → () Source #

data T_SemiringWithoutOne_1464 Source #

d_Carrier_1482 ∷ T_SemiringWithoutOne_1464 → () Source #

d__'8776'__1484 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → () Source #

d__'43'__1486 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny Source #

d__'42'__1488 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny Source #

d_0'35'_1490 ∷ T_SemiringWithoutOne_1464 → AgdaAny Source #

d_isSemiringWithoutOne_1492 ∷ T_SemiringWithoutOne_1464 → T_IsSemiringWithoutOne_952 Source #

d_assoc_1496 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1496 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1498 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1498 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1500 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1500 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1502 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1502 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_1504 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsMagma_86 Source #

du_isMagma_1504 ∷ T_SemiringWithoutOne_1464 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1506 ∷ T_SemiringWithoutOne_1464 → T_IsSemigroup_194 Source #

d_assoc_1508 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1508 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1510 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1512 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1512 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1514 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1514 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1516 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1516 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1518 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Σ_14 Source #

du_identity_1518 ∷ T_SemiringWithoutOne_1464 → T_Σ_14 Source #

d_identity'691'_1520 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

du_identity'691'_1520 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

d_identity'737'_1522 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

du_identity'737'_1522 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1524 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1524 ∷ T_SemiringWithoutOne_1464 → T_IsCommutativeMagma_122 Source #

d_'43''45'isCommutativeMonoid_1526 ∷ T_SemiringWithoutOne_1464 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1528 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1528 ∷ T_SemiringWithoutOne_1464 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1530 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsMagma_86 Source #

du_isMagma_1530 ∷ T_SemiringWithoutOne_1464 → T_IsMagma_86 Source #

d_isMonoid_1532 ∷ T_SemiringWithoutOne_1464 → T_IsMonoid_358 Source #

d_isSemigroup_1534 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsSemigroup_194 Source #

du_isSemigroup_1534 ∷ T_SemiringWithoutOne_1464 → T_IsSemigroup_194 Source #

d_distrib_1536 ∷ T_SemiringWithoutOne_1464 → T_Σ_14 Source #

d_distrib'691'_1538 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1538 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1540 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsEquivalence_26 Source #

du_isEquivalence_1540 ∷ T_SemiringWithoutOne_1464 → T_IsEquivalence_26 Source #

d_isNearSemiring_1542 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1542 ∷ T_SemiringWithoutOne_1464 → T_IsNearSemiring_876 Source #

d_isPartialEquivalence_1544 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1544 ∷ T_SemiringWithoutOne_1464 → T_IsPartialEquivalence_16 Source #

d_refl_1546 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

du_refl_1546 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

d_reflexive_1548 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1548 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1550 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Setoid_44 Source #

du_setoid_1550 ∷ T_SemiringWithoutOne_1464 → T_Setoid_44 Source #

d_sym_1552 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1552 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1554 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1554 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_1556 ∷ T_SemiringWithoutOne_1464 → T_Σ_14 Source #

d_zero'691'_1558 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

du_zero'691'_1558 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

d_zero'737'_1560 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

du_zero'737'_1560 ∷ T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny Source #

d_nearSemiring_1562 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_NearSemiring_1354 Source #

du_nearSemiring_1562 ∷ T_SemiringWithoutOne_1464 → T_NearSemiring_1354 Source #

d__'8777'__1566 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → AgdaAny → AgdaAny → () Source #

d_magma_1568 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Magma_36 Source #

du_magma_1568 ∷ T_SemiringWithoutOne_1464 → T_Magma_36 Source #

d_rawMagma_1570 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_RawMagma_8 Source #

du_rawMagma_1570 ∷ T_SemiringWithoutOne_1464 → T_RawMagma_8 Source #

d_'42''45'semigroup_1572 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Semigroup_206 Source #

du_'42''45'semigroup_1572 ∷ T_SemiringWithoutOne_1464 → T_Semigroup_206 Source #

d_magma_1574 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Magma_36 Source #

du_magma_1574 ∷ T_SemiringWithoutOne_1464 → T_Magma_36 Source #

d_'43''45'monoid_1576 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Monoid_506 Source #

du_'43''45'monoid_1576 ∷ T_SemiringWithoutOne_1464 → T_Monoid_506 Source #

d_rawMagma_1578 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_RawMagma_8 Source #

du_rawMagma_1578 ∷ T_SemiringWithoutOne_1464 → T_RawMagma_8 Source #

d_rawMonoid_1580 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_RawMonoid_474 Source #

du_rawMonoid_1580 ∷ T_SemiringWithoutOne_1464 → T_RawMonoid_474 Source #

d_semigroup_1582 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_Semigroup_206 Source #

du_semigroup_1582 ∷ T_SemiringWithoutOne_1464 → T_Semigroup_206 Source #

d_rawNearSemiring_1584 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_RawNearSemiring_1314 Source #

du_rawNearSemiring_1584 ∷ T_SemiringWithoutOne_1464 → T_RawNearSemiring_1314 Source #

d_'43''45'commutativeMonoid_1586 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_1586 ∷ T_SemiringWithoutOne_1464 → T_CommutativeMonoid_582 Source #

d_commutativeMagma_1590 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_CommutativeMagma_148 Source #

du_commutativeMagma_1590 ∷ T_SemiringWithoutOne_1464 → T_CommutativeMagma_148 Source #

d_commutativeSemigroup_1592 ∷ T_Level_18 → T_Level_18 → T_SemiringWithoutOne_1464 → T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_1592 ∷ T_SemiringWithoutOne_1464 → T_CommutativeSemigroup_332 Source #

d_CommutativeSemiringWithoutOne_1598 ∷ p → p → () Source #

data T_CommutativeSemiringWithoutOne_1598 Source #

d_Carrier_1616 ∷ T_CommutativeSemiringWithoutOne_1598 → () Source #

d__'8776'__1618 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → () Source #

d__'43'__1620 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny Source #

d__'42'__1622 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny Source #

d_0'35'_1624 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny Source #

d_isCommutativeSemiringWithoutOne_1626 ∷ T_CommutativeSemiringWithoutOne_1598 → T_IsCommutativeSemiringWithoutOne_1044 Source #

d_assoc_1630 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1630 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'comm_1632 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1634 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1634 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1636 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1636 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1638 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1638 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1640 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1640 ∷ T_CommutativeSemiringWithoutOne_1598 → T_IsCommutativeMagma_122 Source #

d_'42''45'isCommutativeSemigroup_1642 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → T_IsCommutativeSemigroup_270 Source #

du_'42''45'isCommutativeSemigroup_1642 ∷ T_CommutativeSemiringWithoutOne_1598 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1644 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → T_IsMagma_86 Source #

du_isMagma_1644 ∷ T_CommutativeSemiringWithoutOne_1598 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1646 ∷ T_CommutativeSemiringWithoutOne_1598 → T_IsSemigroup_194 Source #

d_assoc_1648 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1648 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1650 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1652 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1652 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1654 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1654 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1656 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1656 ∷ T_CommutativeSemiringWithoutOne_1598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1658 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemiringWithoutOne_1598 → T_Σ_14 Source #

du_identity_1658 ∷ T_CommutativeSemiringWithoutOne_1598 → T_Σ_14 Source #