Documentation

d_SuccessorSet_8 ∷ p → p → () Source #

data T_SuccessorSet_8 Source #

d_Carrier_24 ∷ T_SuccessorSet_8 → () Source #

d__'8776'__26 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny → () Source #

d_suc'35'_28 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny Source #

d_zero'35'_30 ∷ T_SuccessorSet_8 → AgdaAny Source #

d_isSuccessorSet_32 ∷ T_SuccessorSet_8 → T_IsSuccessorSet_146 Source #

d_isEquivalence_36 ∷ T_SuccessorSet_8 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_38 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_38 ∷ T_SuccessorSet_8 → T_IsPartialEquivalence_16 Source #

d_refl_40 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny Source #

d_reflexive_42 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_42 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_44 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → T_Setoid_46 Source #

du_setoid_44 ∷ T_SuccessorSet_8 → T_Setoid_46 Source #

d_suc'35''45'cong_46 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_sym_48 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_50 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawSuccessorSet_52 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → T_RawSuccessorSet_10 Source #

du_rawSuccessorSet_52 ∷ T_SuccessorSet_8 → T_RawSuccessorSet_10 Source #

d__'8776'__56 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → AgdaAny → AgdaAny → () Source #

d__'8777'__58 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → AgdaAny → AgdaAny → () Source #

d_Carrier_60 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → () Source #

d_rawSetoid_62 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → T_RawSetoid_12 Source #

d_suc'35'_64 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → AgdaAny → AgdaAny Source #

du_suc'35'_64 ∷ T_SuccessorSet_8 → AgdaAny → AgdaAny Source #

d_zero'35'_66 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → AgdaAny Source #

du_zero'35'_66 ∷ T_SuccessorSet_8 → AgdaAny Source #

d_Magma_74 ∷ p → p → () Source #

data T_Magma_74 Source #

d_Carrier_88 ∷ T_Magma_74 → () Source #

d__'8776'__90 ∷ T_Magma_74 → AgdaAny → AgdaAny → () Source #

d__'8729'__92 ∷ T_Magma_74 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_94 ∷ T_Magma_74 → T_IsMagma_178 Source #

d_isEquivalence_98 ∷ T_Magma_74 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_100 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_100 ∷ T_Magma_74 → T_IsPartialEquivalence_16 Source #

d_refl_102 ∷ T_Magma_74 → AgdaAny → AgdaAny Source #

d_reflexive_104 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_104 ∷ T_Magma_74 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_106 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → T_Setoid_46 Source #

du_setoid_106 ∷ T_Magma_74 → T_Setoid_46 Source #

d_sym_108 ∷ T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_110 ∷ T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_112 ∷ T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_114 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_114 ∷ T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_116 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_116 ∷ T_Magma_74 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawMagma_118 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → T_RawMagma_44 Source #

du_rawMagma_118 ∷ T_Magma_74 → T_RawMagma_44 Source #

d__'8777'__122 ∷ T_Level_18 → T_Level_18 → T_Magma_74 → AgdaAny → AgdaAny → () Source #

d_SelectiveMagma_130 ∷ p → p → () Source #

data T_SelectiveMagma_130 Source #

d_Carrier_144 ∷ T_SelectiveMagma_130 → () Source #

d__'8776'__146 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → () Source #

d__'8729'__148 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSelectiveMagma_150 ∷ T_SelectiveMagma_130 → T_IsSelectiveMagma_450 Source #

d_isEquivalence_154 ∷ T_SelectiveMagma_130 → T_IsEquivalence_28 Source #

d_isMagma_156 ∷ T_SelectiveMagma_130 → T_IsMagma_178 Source #

d_isPartialEquivalence_158 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_158 ∷ T_SelectiveMagma_130 → T_IsPartialEquivalence_16 Source #

d_refl_160 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny Source #

d_reflexive_162 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_162 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sel_164 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_setoid_166 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → T_Setoid_46 Source #

du_setoid_166 ∷ T_SelectiveMagma_130 → T_Setoid_46 Source #

d_sym_168 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_170 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_172 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_174 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_174 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_176 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_176 ∷ T_SelectiveMagma_130 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_178 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → T_Magma_74 Source #

du_magma_178 ∷ T_SelectiveMagma_130 → T_Magma_74 Source #

d_rawMagma_182 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_130 → T_RawMagma_44 Source #

du_rawMagma_182 ∷ T_SelectiveMagma_130 → T_RawMagma_44 Source #

d_CommutativeMagma_190 ∷ p → p → () Source #

data T_CommutativeMagma_190 Source #

d_Carrier_204 ∷ T_CommutativeMagma_190 → () Source #

d__'8776'__206 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → () Source #

d__'8729'__208 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_210 ∷ T_CommutativeMagma_190 → T_IsCommutativeMagma_214 Source #

d_comm_214 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_216 ∷ T_CommutativeMagma_190 → T_IsEquivalence_28 Source #

d_isMagma_218 ∷ T_CommutativeMagma_190 → T_IsMagma_178 Source #

d_isPartialEquivalence_220 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_220 ∷ T_CommutativeMagma_190 → T_IsPartialEquivalence_16 Source #

d_refl_222 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny Source #

d_reflexive_224 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_224 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_226 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → T_Setoid_46 Source #

du_setoid_226 ∷ T_CommutativeMagma_190 → T_Setoid_46 Source #

d_sym_228 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_230 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_232 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_234 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_234 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_236 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_236 ∷ T_CommutativeMagma_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_238 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → T_Magma_74 Source #

du_magma_238 ∷ T_CommutativeMagma_190 → T_Magma_74 Source #

d_rawMagma_242 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_190 → T_RawMagma_44 Source #

du_rawMagma_242 ∷ T_CommutativeMagma_190 → T_RawMagma_44 Source #

d_IdempotentMagma_250 ∷ p → p → () Source #

data T_IdempotentMagma_250 Source #

d_Carrier_264 ∷ T_IdempotentMagma_250 → () Source #

d__'8776'__266 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → () Source #

d__'8729'__268 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny Source #

d_isIdempotentMagma_270 ∷ T_IdempotentMagma_250 → T_IsIdempotentMagma_252 Source #

d_idem_274 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny Source #

d_isEquivalence_276 ∷ T_IdempotentMagma_250 → T_IsEquivalence_28 Source #

d_isMagma_278 ∷ T_IdempotentMagma_250 → T_IsMagma_178 Source #

d_isPartialEquivalence_280 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_280 ∷ T_IdempotentMagma_250 → T_IsPartialEquivalence_16 Source #

d_refl_282 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny Source #

d_reflexive_284 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_284 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_286 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → T_Setoid_46 Source #

du_setoid_286 ∷ T_IdempotentMagma_250 → T_Setoid_46 Source #

d_sym_288 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_290 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_292 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_294 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_294 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_296 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_296 ∷ T_IdempotentMagma_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_298 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → T_Magma_74 Source #

du_magma_298 ∷ T_IdempotentMagma_250 → T_Magma_74 Source #

d_rawMagma_302 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_250 → T_RawMagma_44 Source #

du_rawMagma_302 ∷ T_IdempotentMagma_250 → T_RawMagma_44 Source #

d_AlternativeMagma_310 ∷ p → p → () Source #

data T_AlternativeMagma_310 Source #

d_Carrier_324 ∷ T_AlternativeMagma_310 → () Source #

d__'8776'__326 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → () Source #

d__'8729'__328 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny Source #

d_isAlternativeMagma_330 ∷ T_AlternativeMagma_310 → T_IsAlternativeMagma_290 Source #

d_alter_334 ∷ T_AlternativeMagma_310 → T_Σ_14 Source #

d_alternative'691'_336 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny Source #

du_alternative'691'_336 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny Source #

d_alternative'737'_338 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny Source #

du_alternative'737'_338 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_340 ∷ T_AlternativeMagma_310 → T_IsEquivalence_28 Source #

d_isMagma_342 ∷ T_AlternativeMagma_310 → T_IsMagma_178 Source #

d_isPartialEquivalence_344 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_344 ∷ T_AlternativeMagma_310 → T_IsPartialEquivalence_16 Source #

d_refl_346 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny Source #

d_reflexive_348 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_348 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_350 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → T_Setoid_46 Source #

du_setoid_350 ∷ T_AlternativeMagma_310 → T_Setoid_46 Source #

d_sym_352 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_354 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_356 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_358 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_358 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_360 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_360 ∷ T_AlternativeMagma_310 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_362 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → T_Magma_74 Source #

du_magma_362 ∷ T_AlternativeMagma_310 → T_Magma_74 Source #

d_rawMagma_366 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_310 → T_RawMagma_44 Source #

du_rawMagma_366 ∷ T_AlternativeMagma_310 → T_RawMagma_44 Source #

d_FlexibleMagma_374 ∷ p → p → () Source #

data T_FlexibleMagma_374 Source #

d_Carrier_388 ∷ T_FlexibleMagma_374 → () Source #

d__'8776'__390 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → () Source #

d__'8729'__392 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny Source #

d_isFlexibleMagma_394 ∷ T_FlexibleMagma_374 → T_IsFlexibleMagma_332 Source #

d_flex_398 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_400 ∷ T_FlexibleMagma_374 → T_IsEquivalence_28 Source #

d_isMagma_402 ∷ T_FlexibleMagma_374 → T_IsMagma_178 Source #

d_isPartialEquivalence_404 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_404 ∷ T_FlexibleMagma_374 → T_IsPartialEquivalence_16 Source #

d_refl_406 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny Source #

d_reflexive_408 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_408 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_410 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → T_Setoid_46 Source #

du_setoid_410 ∷ T_FlexibleMagma_374 → T_Setoid_46 Source #

d_sym_412 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_414 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_416 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_418 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_418 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_420 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_420 ∷ T_FlexibleMagma_374 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_422 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → T_Magma_74 Source #

du_magma_422 ∷ T_FlexibleMagma_374 → T_Magma_74 Source #

d_rawMagma_426 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_374 → T_RawMagma_44 Source #

du_rawMagma_426 ∷ T_FlexibleMagma_374 → T_RawMagma_44 Source #

d_MedialMagma_434 ∷ p → p → () Source #

data T_MedialMagma_434 Source #

d_Carrier_448 ∷ T_MedialMagma_434 → () Source #

d__'8776'__450 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → () Source #

d__'8729'__452 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMedialMagma_454 ∷ T_MedialMagma_434 → T_IsMedialMagma_370 Source #

d_isEquivalence_458 ∷ T_MedialMagma_434 → T_IsEquivalence_28 Source #

d_isMagma_460 ∷ T_MedialMagma_434 → T_IsMagma_178 Source #

d_isPartialEquivalence_462 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_462 ∷ T_MedialMagma_434 → T_IsPartialEquivalence_16 Source #

d_medial_464 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_466 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny Source #

d_reflexive_468 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_468 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_470 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → T_Setoid_46 Source #

du_setoid_470 ∷ T_MedialMagma_434 → T_Setoid_46 Source #

d_sym_472 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_474 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_476 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_478 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_478 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_480 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_480 ∷ T_MedialMagma_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_482 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → T_Magma_74 Source #

du_magma_482 ∷ T_MedialMagma_434 → T_Magma_74 Source #

d_rawMagma_486 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_434 → T_RawMagma_44 Source #

du_rawMagma_486 ∷ T_MedialMagma_434 → T_RawMagma_44 Source #

d_SemimedialMagma_494 ∷ p → p → () Source #

data T_SemimedialMagma_494 Source #

d_Carrier_508 ∷ T_SemimedialMagma_494 → () Source #

d__'8776'__510 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → () Source #

d__'8729'__512 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemimedialMagma_514 ∷ T_SemimedialMagma_494 → T_IsSemimedialMagma_408 Source #

d_isEquivalence_518 ∷ T_SemimedialMagma_494 → T_IsEquivalence_28 Source #

d_isMagma_520 ∷ T_SemimedialMagma_494 → T_IsMagma_178 Source #

d_isPartialEquivalence_522 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_522 ∷ T_SemimedialMagma_494 → T_IsPartialEquivalence_16 Source #

d_refl_524 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny Source #

d_reflexive_526 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_526 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_semiMedial_528 ∷ T_SemimedialMagma_494 → T_Σ_14 Source #

d_semimedial'691'_530 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_semimedial'691'_530 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semimedial'737'_532 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_semimedial'737'_532 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_534 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → T_Setoid_46 Source #

du_setoid_534 ∷ T_SemimedialMagma_494 → T_Setoid_46 Source #

d_sym_536 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_538 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_540 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_542 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_542 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_544 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_544 ∷ T_SemimedialMagma_494 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_546 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → T_Magma_74 Source #

du_magma_546 ∷ T_SemimedialMagma_494 → T_Magma_74 Source #

d_rawMagma_550 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_494 → T_RawMagma_44 Source #

du_rawMagma_550 ∷ T_SemimedialMagma_494 → T_RawMagma_44 Source #

d_Semigroup_558 ∷ p → p → () Source #

data T_Semigroup_558 Source #

d_Carrier_572 ∷ T_Semigroup_558 → () Source #

d__'8776'__574 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → () Source #

d__'8729'__576 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemigroup_578 ∷ T_Semigroup_558 → T_IsSemigroup_488 Source #

d_assoc_582 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_584 ∷ T_Semigroup_558 → T_IsEquivalence_28 Source #

d_isMagma_586 ∷ T_Semigroup_558 → T_IsMagma_178 Source #

d_isPartialEquivalence_588 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_588 ∷ T_Semigroup_558 → T_IsPartialEquivalence_16 Source #

d_refl_590 ∷ T_Semigroup_558 → AgdaAny → AgdaAny Source #

d_reflexive_592 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_592 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_594 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Setoid_46 Source #

du_setoid_594 ∷ T_Semigroup_558 → T_Setoid_46 Source #

d_sym_596 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_598 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_600 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_602 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_602 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_604 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_604 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_606 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Magma_74 Source #

du_magma_606 ∷ T_Semigroup_558 → T_Magma_74 Source #

d__'8777'__610 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → AgdaAny → AgdaAny → () Source #

d_rawMagma_612 ∷ T_Level_18 → T_Level_18 → T_Semigroup_558 → T_RawMagma_44 Source #

du_rawMagma_612 ∷ T_Semigroup_558 → T_RawMagma_44 Source #

d_Band_620 ∷ p → p → () Source #

data T_Band_620 Source #

d_Carrier_634 ∷ T_Band_620 → () Source #

d__'8776'__636 ∷ T_Band_620 → AgdaAny → AgdaAny → () Source #

d__'8729'__638 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_640 ∷ T_Band_620 → T_IsBand_526 Source #

d_assoc_644 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_646 ∷ T_Band_620 → AgdaAny → AgdaAny Source #

d_isEquivalence_648 ∷ T_Band_620 → T_IsEquivalence_28 Source #

d_isMagma_650 ∷ T_Band_620 → T_IsMagma_178 Source #

d_isPartialEquivalence_652 ∷ T_Level_18 → T_Level_18 → T_Band_620 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_652 ∷ T_Band_620 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_654 ∷ T_Band_620 → T_IsSemigroup_488 Source #

d_refl_656 ∷ T_Band_620 → AgdaAny → AgdaAny Source #

d_reflexive_658 ∷ T_Level_18 → T_Level_18 → T_Band_620 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_658 ∷ T_Band_620 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_660 ∷ T_Level_18 → T_Level_18 → T_Band_620 → T_Setoid_46 Source #

du_setoid_660 ∷ T_Band_620 → T_Setoid_46 Source #

d_sym_662 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_664 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_666 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_668 ∷ T_Level_18 → T_Level_18 → T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_668 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_670 ∷ T_Level_18 → T_Level_18 → T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_670 ∷ T_Band_620 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_672 ∷ T_Level_18 → T_Level_18 → T_Band_620 → T_Semigroup_558 Source #

du_semigroup_672 ∷ T_Band_620 → T_Semigroup_558 Source #

d__'8777'__676 ∷ T_Level_18 → T_Level_18 → T_Band_620 → AgdaAny → AgdaAny → () Source #

d_magma_678 ∷ T_Level_18 → T_Level_18 → T_Band_620 → T_Magma_74 Source #

du_magma_678 ∷ T_Band_620 → T_Magma_74 Source #

d_rawMagma_680 ∷ T_Level_18 → T_Level_18 → T_Band_620 → T_RawMagma_44 Source #

du_rawMagma_680 ∷ T_Band_620 → T_RawMagma_44 Source #

d_CommutativeSemigroup_688 ∷ p → p → () Source #

data T_CommutativeSemigroup_688 Source #

d_Carrier_702 ∷ T_CommutativeSemigroup_688 → () Source #

d__'8776'__704 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → () Source #

d__'8729'__706 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeSemigroup_708 ∷ T_CommutativeSemigroup_688 → T_IsCommutativeSemigroup_568 Source #

d_assoc_712 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_714 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_716 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_716 ∷ T_CommutativeSemigroup_688 → T_IsCommutativeMagma_214 Source #

d_isEquivalence_718 ∷ T_CommutativeSemigroup_688 → T_IsEquivalence_28 Source #

d_isMagma_720 ∷ T_CommutativeSemigroup_688 → T_IsMagma_178 Source #

d_isPartialEquivalence_722 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_722 ∷ T_CommutativeSemigroup_688 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_724 ∷ T_CommutativeSemigroup_688 → T_IsSemigroup_488 Source #

d_refl_726 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny Source #

d_reflexive_728 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_728 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_730 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_Setoid_46 Source #

du_setoid_730 ∷ T_CommutativeSemigroup_688 → T_Setoid_46 Source #

d_sym_732 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_734 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_736 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_738 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_738 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_740 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_740 ∷ T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_742 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_Semigroup_558 Source #

du_semigroup_742 ∷ T_CommutativeSemigroup_688 → T_Semigroup_558 Source #

d__'8777'__746 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → AgdaAny → AgdaAny → () Source #

d_magma_748 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_Magma_74 Source #

du_magma_748 ∷ T_CommutativeSemigroup_688 → T_Magma_74 Source #

d_rawMagma_750 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_RawMagma_44 Source #

du_rawMagma_750 ∷ T_CommutativeSemigroup_688 → T_RawMagma_44 Source #

d_commutativeMagma_752 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_688 → T_CommutativeMagma_190 Source #

du_commutativeMagma_752 ∷ T_CommutativeSemigroup_688 → T_CommutativeMagma_190 Source #

d_CommutativeBand_760 ∷ p → p → () Source #

data T_CommutativeBand_760 Source #

d_Carrier_774 ∷ T_CommutativeBand_760 → () Source #

d__'8776'__776 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → () Source #

d__'8729'__778 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeBand_780 ∷ T_CommutativeBand_760 → T_IsCommutativeBand_612 Source #

d_assoc_784 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_786 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_788 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny Source #

d_isBand_790 ∷ T_CommutativeBand_760 → T_IsBand_526 Source #

d_isCommutativeMagma_792 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_792 ∷ T_CommutativeBand_760 → T_IsCommutativeMagma_214 Source #

d_isCommutativeSemigroup_794 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_794 ∷ T_CommutativeBand_760 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_796 ∷ T_CommutativeBand_760 → T_IsEquivalence_28 Source #

d_isMagma_798 ∷ T_CommutativeBand_760 → T_IsMagma_178 Source #

d_isPartialEquivalence_800 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_800 ∷ T_CommutativeBand_760 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_802 ∷ T_CommutativeBand_760 → T_IsSemigroup_488 Source #

d_refl_804 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny Source #

d_reflexive_806 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_806 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_808 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_Setoid_46 Source #

du_setoid_808 ∷ T_CommutativeBand_760 → T_Setoid_46 Source #

d_sym_810 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_812 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_814 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_816 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_816 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_818 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_818 ∷ T_CommutativeBand_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_band_820 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_Band_620 Source #

du_band_820 ∷ T_CommutativeBand_760 → T_Band_620 Source #

d__'8777'__824 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → AgdaAny → AgdaAny → () Source #

d_magma_826 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_Magma_74 Source #

du_magma_826 ∷ T_CommutativeBand_760 → T_Magma_74 Source #

d_rawMagma_828 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_RawMagma_44 Source #

du_rawMagma_828 ∷ T_CommutativeBand_760 → T_RawMagma_44 Source #

d_semigroup_830 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_Semigroup_558 Source #

du_semigroup_830 ∷ T_CommutativeBand_760 → T_Semigroup_558 Source #

d_commutativeSemigroup_832 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_CommutativeSemigroup_688 Source #

du_commutativeSemigroup_832 ∷ T_CommutativeBand_760 → T_CommutativeSemigroup_688 Source #

d_commutativeMagma_836 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_760 → T_CommutativeMagma_190 Source #

du_commutativeMagma_836 ∷ T_CommutativeBand_760 → T_CommutativeMagma_190 Source #

d_UnitalMagma_844 ∷ p → p → () Source #

data T_UnitalMagma_844 Source #

d_Carrier_860 ∷ T_UnitalMagma_844 → () Source #

d__'8776'__862 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → () Source #

d__'8729'__864 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_866 ∷ T_UnitalMagma_844 → AgdaAny Source #

d_isUnitalMagma_868 ∷ T_UnitalMagma_844 → T_IsUnitalMagma_666 Source #

d_identity_872 ∷ T_UnitalMagma_844 → T_Σ_14 Source #

d_identity'691'_874 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → AgdaAny → AgdaAny Source #

du_identity'691'_874 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny Source #

d_identity'737'_876 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → AgdaAny → AgdaAny Source #

du_identity'737'_876 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny Source #

d_isEquivalence_878 ∷ T_UnitalMagma_844 → T_IsEquivalence_28 Source #

d_isMagma_880 ∷ T_UnitalMagma_844 → T_IsMagma_178 Source #

d_isPartialEquivalence_882 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_882 ∷ T_UnitalMagma_844 → T_IsPartialEquivalence_16 Source #

d_refl_884 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny Source #

d_reflexive_886 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_886 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_888 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → T_Setoid_46 Source #

du_setoid_888 ∷ T_UnitalMagma_844 → T_Setoid_46 Source #

d_sym_890 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_892 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_894 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_896 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_896 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_898 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_898 ∷ T_UnitalMagma_844 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_900 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → T_Magma_74 Source #

du_magma_900 ∷ T_UnitalMagma_844 → T_Magma_74 Source #

d__'8777'__904 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → AgdaAny → AgdaAny → () Source #

d_rawMagma_906 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_844 → T_RawMagma_44 Source #

du_rawMagma_906 ∷ T_UnitalMagma_844 → T_RawMagma_44 Source #

d_Monoid_914 ∷ p → p → () Source #

data T_Monoid_914 Source #

d_Carrier_930 ∷ T_Monoid_914 → () Source #

d__'8776'__932 ∷ T_Monoid_914 → AgdaAny → AgdaAny → () Source #

d__'8729'__934 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_936 ∷ T_Monoid_914 → AgdaAny Source #

d_isMonoid_938 ∷ T_Monoid_914 → T_IsMonoid_712 Source #

d_assoc_942 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_944 ∷ T_Monoid_914 → T_Σ_14 Source #

d_identity'691'_946 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → AgdaAny → AgdaAny Source #

du_identity'691'_946 ∷ T_Monoid_914 → AgdaAny → AgdaAny Source #

d_identity'737'_948 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → AgdaAny → AgdaAny Source #

du_identity'737'_948 ∷ T_Monoid_914 → AgdaAny → AgdaAny Source #

d_isEquivalence_950 ∷ T_Monoid_914 → T_IsEquivalence_28 Source #

d_isMagma_952 ∷ T_Monoid_914 → T_IsMagma_178 Source #

d_isPartialEquivalence_954 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_954 ∷ T_Monoid_914 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_956 ∷ T_Monoid_914 → T_IsSemigroup_488 Source #

d_isUnitalMagma_958 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_958 ∷ T_Monoid_914 → T_IsUnitalMagma_666 Source #

d_refl_960 ∷ T_Monoid_914 → AgdaAny → AgdaAny Source #

d_reflexive_962 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_962 ∷ T_Monoid_914 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_964 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_Setoid_46 Source #

du_setoid_964 ∷ T_Monoid_914 → T_Setoid_46 Source #

d_sym_966 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_968 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_970 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_972 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_972 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_974 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_974 ∷ T_Monoid_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_976 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_Semigroup_558 Source #

du_semigroup_976 ∷ T_Monoid_914 → T_Semigroup_558 Source #

d__'8777'__980 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → AgdaAny → AgdaAny → () Source #

d_magma_982 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_Magma_74 Source #

du_magma_982 ∷ T_Monoid_914 → T_Magma_74 Source #

d_rawMagma_984 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_RawMagma_44 Source #

du_rawMagma_984 ∷ T_Monoid_914 → T_RawMagma_44 Source #

d_rawMonoid_986 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_RawMonoid_74 Source #

du_rawMonoid_986 ∷ T_Monoid_914 → T_RawMonoid_74 Source #

d_unitalMagma_988 ∷ T_Level_18 → T_Level_18 → T_Monoid_914 → T_UnitalMagma_844 Source #

du_unitalMagma_988 ∷ T_Monoid_914 → T_UnitalMagma_844 Source #

d_CommutativeMonoid_996 ∷ p → p → () Source #

data T_CommutativeMonoid_996 Source #

d_Carrier_1012 ∷ T_CommutativeMonoid_996 → () Source #

d__'8776'__1014 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → () Source #

d__'8729'__1016 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1018 ∷ T_CommutativeMonoid_996 → AgdaAny Source #

d_isCommutativeMonoid_1020 ∷ T_CommutativeMonoid_996 → T_IsCommutativeMonoid_764 Source #

d_assoc_1024 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1026 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1028 ∷ T_CommutativeMonoid_996 → T_Σ_14 Source #

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

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

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

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

d_isCommutativeMagma_1034 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_1034 ∷ T_CommutativeMonoid_996 → T_IsCommutativeMagma_214 Source #

d_isCommutativeSemigroup_1036 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_1036 ∷ T_CommutativeMonoid_996 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_1038 ∷ T_CommutativeMonoid_996 → T_IsEquivalence_28 Source #

d_isMagma_1040 ∷ T_CommutativeMonoid_996 → T_IsMagma_178 Source #

d_isMonoid_1042 ∷ T_CommutativeMonoid_996 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1044 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1044 ∷ T_CommutativeMonoid_996 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1046 ∷ T_CommutativeMonoid_996 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1048 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1048 ∷ T_CommutativeMonoid_996 → T_IsUnitalMagma_666 Source #

d_refl_1050 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny Source #

d_reflexive_1052 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1052 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1054 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_Setoid_46 Source #

du_setoid_1054 ∷ T_CommutativeMonoid_996 → T_Setoid_46 Source #

d_sym_1056 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1058 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1060 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1062 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1062 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1064 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1064 ∷ T_CommutativeMonoid_996 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_monoid_1066 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_Monoid_914 Source #

du_monoid_1066 ∷ T_CommutativeMonoid_996 → T_Monoid_914 Source #

d__'8777'__1070 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → AgdaAny → AgdaAny → () Source #

d_magma_1072 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_Magma_74 Source #

du_magma_1072 ∷ T_CommutativeMonoid_996 → T_Magma_74 Source #

d_rawMagma_1074 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_RawMagma_44 Source #

du_rawMagma_1074 ∷ T_CommutativeMonoid_996 → T_RawMagma_44 Source #

d_rawMonoid_1076 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_RawMonoid_74 Source #

du_rawMonoid_1076 ∷ T_CommutativeMonoid_996 → T_RawMonoid_74 Source #

d_semigroup_1078 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_Semigroup_558 Source #

du_semigroup_1078 ∷ T_CommutativeMonoid_996 → T_Semigroup_558 Source #

d_unitalMagma_1080 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_UnitalMagma_844 Source #

du_unitalMagma_1080 ∷ T_CommutativeMonoid_996 → T_UnitalMagma_844 Source #

d_commutativeSemigroup_1082 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeSemigroup_688 Source #

du_commutativeSemigroup_1082 ∷ T_CommutativeMonoid_996 → T_CommutativeSemigroup_688 Source #

d_commutativeMagma_1086 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMagma_190 Source #

du_commutativeMagma_1086 ∷ T_CommutativeMonoid_996 → T_CommutativeMagma_190 Source #

d_IdempotentMonoid_1094 ∷ p → p → () Source #

data T_IdempotentMonoid_1094 Source #

d_Carrier_1110 ∷ T_IdempotentMonoid_1094 → () Source #

d__'8776'__1112 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → () Source #

d__'8729'__1114 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1116 ∷ T_IdempotentMonoid_1094 → AgdaAny Source #

d_isIdempotentMonoid_1118 ∷ T_IdempotentMonoid_1094 → T_IsIdempotentMonoid_826 Source #

d_assoc_1122 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_1124 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny Source #

d_identity_1126 ∷ T_IdempotentMonoid_1094 → T_Σ_14 Source #

d_identity'691'_1128 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → AgdaAny → AgdaAny Source #

du_identity'691'_1128 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny Source #

d_identity'737'_1130 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → AgdaAny → AgdaAny Source #

du_identity'737'_1130 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny Source #

d_isBand_1132 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_IsBand_526 Source #

du_isBand_1132 ∷ T_IdempotentMonoid_1094 → T_IsBand_526 Source #

d_isEquivalence_1134 ∷ T_IdempotentMonoid_1094 → T_IsEquivalence_28 Source #

d_isMagma_1136 ∷ T_IdempotentMonoid_1094 → T_IsMagma_178 Source #

d_isMonoid_1138 ∷ T_IdempotentMonoid_1094 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1140 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1140 ∷ T_IdempotentMonoid_1094 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1142 ∷ T_IdempotentMonoid_1094 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1144 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1144 ∷ T_IdempotentMonoid_1094 → T_IsUnitalMagma_666 Source #

d_refl_1146 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny Source #

d_reflexive_1148 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1148 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1150 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_Setoid_46 Source #

du_setoid_1150 ∷ T_IdempotentMonoid_1094 → T_Setoid_46 Source #

d_sym_1152 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1154 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1156 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1158 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1158 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1160 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1160 ∷ T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_monoid_1162 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_Monoid_914 Source #

du_monoid_1162 ∷ T_IdempotentMonoid_1094 → T_Monoid_914 Source #

d__'8777'__1166 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → AgdaAny → AgdaAny → () Source #

d_magma_1168 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_Magma_74 Source #

du_magma_1168 ∷ T_IdempotentMonoid_1094 → T_Magma_74 Source #

d_rawMagma_1170 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_RawMagma_44 Source #

du_rawMagma_1170 ∷ T_IdempotentMonoid_1094 → T_RawMagma_44 Source #

d_rawMonoid_1172 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_RawMonoid_74 Source #

du_rawMonoid_1172 ∷ T_IdempotentMonoid_1094 → T_RawMonoid_74 Source #

d_semigroup_1174 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_Semigroup_558 Source #

du_semigroup_1174 ∷ T_IdempotentMonoid_1094 → T_Semigroup_558 Source #

d_unitalMagma_1176 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_UnitalMagma_844 Source #

du_unitalMagma_1176 ∷ T_IdempotentMonoid_1094 → T_UnitalMagma_844 Source #

d_band_1178 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1094 → T_Band_620 Source #

du_band_1178 ∷ T_IdempotentMonoid_1094 → T_Band_620 Source #

d_IdempotentCommutativeMonoid_1186 ∷ p → p → () Source #

data T_IdempotentCommutativeMonoid_1186 Source #

d_Carrier_1202 ∷ T_IdempotentCommutativeMonoid_1186 → () Source #

d__'8776'__1204 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → () Source #

d__'8729'__1206 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1208 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny Source #

d_isIdempotentCommutativeMonoid_1210 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsIdempotentCommutativeMonoid_884 Source #

d_assoc_1214 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1216 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_1218 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_identity_1220 ∷ T_IdempotentCommutativeMonoid_1186 → T_Σ_14 Source #

d_identity'691'_1222 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

du_identity'691'_1222 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_identity'737'_1224 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

du_identity'737'_1224 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_isBand_1226 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsBand_526 Source #

du_isBand_1226 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsBand_526 Source #

d_isCommutativeBand_1228 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_1228 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeBand_612 Source #

d_isCommutativeMagma_1230 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_1230 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_1232 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_1234 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_1234 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_1236 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsEquivalence_28 Source #

d_isIdempotentMonoid_1238 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsIdempotentMonoid_826 Source #

du_isIdempotentMonoid_1238 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsIdempotentMonoid_826 Source #

d_isMagma_1240 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsMagma_178 Source #

d_isMonoid_1242 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1244 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1244 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1246 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1248 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1248 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsUnitalMagma_666 Source #

d_refl_1250 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_reflexive_1252 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1252 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1254 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Setoid_46 Source #

du_setoid_1254 ∷ T_IdempotentCommutativeMonoid_1186 → T_Setoid_46 Source #

d_sym_1256 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1258 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1260 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1262 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1262 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1264 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1264 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeMonoid_1266 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

du_commutativeMonoid_1266 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

d_idempotentMonoid_1268 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentMonoid_1094 Source #

du_idempotentMonoid_1268 ∷ T_IdempotentCommutativeMonoid_1186 → T_IdempotentMonoid_1094 Source #

d_commutativeBand_1270 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeBand_760 Source #

du_commutativeBand_1270 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeBand_760 Source #

d__'8777'__1274 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → () Source #

d_commutativeMagma_1276 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeMagma_190 Source #

du_commutativeMagma_1276 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeMagma_190 Source #

d_commutativeSemigroup_1278 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeSemigroup_688 Source #

du_commutativeSemigroup_1278 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeSemigroup_688 Source #

d_magma_1280 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Magma_74 Source #

du_magma_1280 ∷ T_IdempotentCommutativeMonoid_1186 → T_Magma_74 Source #

d_monoid_1282 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

du_monoid_1282 ∷ T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

d_rawMagma_1284 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_RawMagma_44 Source #

du_rawMagma_1284 ∷ T_IdempotentCommutativeMonoid_1186 → T_RawMagma_44 Source #

d_rawMonoid_1286 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_RawMonoid_74 Source #

du_rawMonoid_1286 ∷ T_IdempotentCommutativeMonoid_1186 → T_RawMonoid_74 Source #

d_semigroup_1288 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Semigroup_558 Source #

du_semigroup_1288 ∷ T_IdempotentCommutativeMonoid_1186 → T_Semigroup_558 Source #

d_unitalMagma_1290 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_UnitalMagma_844 Source #

du_unitalMagma_1290 ∷ T_IdempotentCommutativeMonoid_1186 → T_UnitalMagma_844 Source #

d_band_1294 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Band_620 Source #

du_band_1294 ∷ T_IdempotentCommutativeMonoid_1186 → T_Band_620 Source #

d_BoundedLattice_1298 ∷ T_Level_18 → T_Level_18 → () Source #

d__'8729'__1308 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1310 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → () Source #

d__'8777'__1312 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → () Source #

d_Carrier_1314 ∷ T_IdempotentCommutativeMonoid_1186 → () Source #

d_assoc_1316 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_band_1318 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Band_620 Source #

du_band_1318 ∷ T_IdempotentCommutativeMonoid_1186 → T_Band_620 Source #

d_comm_1320 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeBand_1322 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeBand_760 Source #

du_commutativeBand_1322 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeBand_760 Source #

d_commutativeMagma_1324 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeMagma_190 Source #

du_commutativeMagma_1324 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeMagma_190 Source #

d_commutativeMonoid_1326 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

du_commutativeMonoid_1326 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

d_commutativeSemigroup_1328 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeSemigroup_688 Source #

du_commutativeSemigroup_1328 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeSemigroup_688 Source #

d_idem_1330 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_idempotentMonoid_1332 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentMonoid_1094 Source #

du_idempotentMonoid_1332 ∷ T_IdempotentCommutativeMonoid_1186 → T_IdempotentMonoid_1094 Source #

d_identity_1334 ∷ T_IdempotentCommutativeMonoid_1186 → T_Σ_14 Source #

d_identity'691'_1336 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

du_identity'691'_1336 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_identity'737'_1338 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

du_identity'737'_1338 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_isBand_1340 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsBand_526 Source #

du_isBand_1340 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsBand_526 Source #

d_isCommutativeBand_1342 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_1342 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeBand_612 Source #

d_isCommutativeMagma_1344 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_1344 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_1346 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_1348 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_1348 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_1350 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsEquivalence_28 Source #

d_isIdempotentCommutativeMonoid_1352 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsIdempotentCommutativeMonoid_884 Source #

d_isIdempotentMonoid_1354 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsIdempotentMonoid_826 Source #

du_isIdempotentMonoid_1354 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsIdempotentMonoid_826 Source #

d_isMagma_1356 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsMagma_178 Source #

d_isMonoid_1358 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1360 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1360 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1362 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1364 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1364 ∷ T_IdempotentCommutativeMonoid_1186 → T_IsUnitalMagma_666 Source #

d_magma_1366 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Magma_74 Source #

du_magma_1366 ∷ T_IdempotentCommutativeMonoid_1186 → T_Magma_74 Source #

d_monoid_1368 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

du_monoid_1368 ∷ T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

d_rawMagma_1370 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_RawMagma_44 Source #

du_rawMagma_1370 ∷ T_IdempotentCommutativeMonoid_1186 → T_RawMagma_44 Source #

d_rawMonoid_1372 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_RawMonoid_74 Source #

du_rawMonoid_1372 ∷ T_IdempotentCommutativeMonoid_1186 → T_RawMonoid_74 Source #

d_refl_1374 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny Source #

d_reflexive_1376 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1376 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_semigroup_1378 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Semigroup_558 Source #

du_semigroup_1378 ∷ T_IdempotentCommutativeMonoid_1186 → T_Semigroup_558 Source #

d_setoid_1380 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_Setoid_46 Source #

du_setoid_1380 ∷ T_IdempotentCommutativeMonoid_1186 → T_Setoid_46 Source #

d_sym_1382 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1384 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unitalMagma_1386 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_UnitalMagma_844 Source #

du_unitalMagma_1386 ∷ T_IdempotentCommutativeMonoid_1186 → T_UnitalMagma_844 Source #

d_ε_1388 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny Source #

d_'8729''45'cong_1390 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1392 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1392 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1394 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1394 ∷ T_IdempotentCommutativeMonoid_1186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_InvertibleMagma_1400 ∷ p → p → () Source #

data T_InvertibleMagma_1400 Source #

d_Carrier_1418 ∷ T_InvertibleMagma_1400 → () Source #

d__'8776'__1420 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → () Source #

d__'8729'__1422 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1424 ∷ T_InvertibleMagma_1400 → AgdaAny Source #

d__'8315''185'_1426 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny Source #

d_isInvertibleMagma_1428 ∷ T_InvertibleMagma_1400 → T_IsInvertibleMagma_958 Source #

d_inverse_1432 ∷ T_InvertibleMagma_1400 → T_Σ_14 Source #

d_inverse'691'_1434 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → AgdaAny → AgdaAny Source #

du_inverse'691'_1434 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny Source #

d_inverse'737'_1436 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → AgdaAny → AgdaAny Source #

du_inverse'737'_1436 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny Source #

d_isEquivalence_1438 ∷ T_InvertibleMagma_1400 → T_IsEquivalence_28 Source #

d_isMagma_1440 ∷ T_InvertibleMagma_1400 → T_IsMagma_178 Source #

d_isPartialEquivalence_1442 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1442 ∷ T_InvertibleMagma_1400 → T_IsPartialEquivalence_16 Source #

d_refl_1444 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny Source #

d_reflexive_1446 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1446 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1448 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → T_Setoid_46 Source #

du_setoid_1448 ∷ T_InvertibleMagma_1400 → T_Setoid_46 Source #

d_sym_1450 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1452 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1454 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1456 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1458 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1458 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1460 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1460 ∷ T_InvertibleMagma_1400 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_1462 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → T_Magma_74 Source #

du_magma_1462 ∷ T_InvertibleMagma_1400 → T_Magma_74 Source #

d__'8777'__1466 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → AgdaAny → AgdaAny → () Source #

d_rawMagma_1468 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1400 → T_RawMagma_44 Source #

du_rawMagma_1468 ∷ T_InvertibleMagma_1400 → T_RawMagma_44 Source #

d_InvertibleUnitalMagma_1476 ∷ p → p → () Source #

data T_InvertibleUnitalMagma_1476 Source #

d_Carrier_1494 ∷ T_InvertibleUnitalMagma_1476 → () Source #

d__'8776'__1496 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → () Source #

d__'8729'__1498 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1500 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny Source #

d__'8315''185'_1502 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

d_isInvertibleUnitalMagma_1504 ∷ T_InvertibleUnitalMagma_1476 → T_IsInvertibleUnitalMagma_1012 Source #

d_identity_1508 ∷ T_InvertibleUnitalMagma_1476 → T_Σ_14 Source #

d_identity'691'_1510 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

du_identity'691'_1510 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

d_identity'737'_1512 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

du_identity'737'_1512 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

d_inverse_1514 ∷ T_InvertibleUnitalMagma_1476 → T_Σ_14 Source #

d_inverse'691'_1516 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

du_inverse'691'_1516 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

d_inverse'737'_1518 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

du_inverse'737'_1518 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

d_isEquivalence_1520 ∷ T_InvertibleUnitalMagma_1476 → T_IsEquivalence_28 Source #

d_isInvertibleMagma_1522 ∷ T_InvertibleUnitalMagma_1476 → T_IsInvertibleMagma_958 Source #

d_isMagma_1524 ∷ T_InvertibleUnitalMagma_1476 → T_IsMagma_178 Source #

d_isPartialEquivalence_1526 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1526 ∷ T_InvertibleUnitalMagma_1476 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1528 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1528 ∷ T_InvertibleUnitalMagma_1476 → T_IsUnitalMagma_666 Source #

d_refl_1530 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny Source #

d_reflexive_1532 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1532 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1534 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → T_Setoid_46 Source #

du_setoid_1534 ∷ T_InvertibleUnitalMagma_1476 → T_Setoid_46 Source #

d_sym_1536 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1538 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1540 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1542 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1544 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1544 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1546 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1546 ∷ T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_invertibleMagma_1548 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → T_InvertibleMagma_1400 Source #

du_invertibleMagma_1548 ∷ T_InvertibleUnitalMagma_1476 → T_InvertibleMagma_1400 Source #

d__'8777'__1552 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → AgdaAny → AgdaAny → () Source #

d_magma_1554 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → T_Magma_74 Source #

du_magma_1554 ∷ T_InvertibleUnitalMagma_1476 → T_Magma_74 Source #

d_rawMagma_1556 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1476 → T_RawMagma_44 Source #

du_rawMagma_1556 ∷ T_InvertibleUnitalMagma_1476 → T_RawMagma_44 Source #

d_Group_1564 ∷ p → p → () Source #

data T_Group_1564 Source #

d_Carrier_1582 ∷ T_Group_1564 → () Source #

d__'8776'__1584 ∷ T_Group_1564 → AgdaAny → AgdaAny → () Source #

d__'8729'__1586 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1588 ∷ T_Group_1564 → AgdaAny Source #

d__'8315''185'_1590 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_isGroup_1592 ∷ T_Group_1564 → T_IsGroup_1074 Source #

d__'45'__1596 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

du__'45'__1596 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

d__'47''47'__1598 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__1598 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

d__'92''92'__1600 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

du__'92''92'__1600 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1602 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1604 ∷ T_Group_1564 → T_Σ_14 Source #

d_identity'691'_1606 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny Source #

du_identity'691'_1606 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_identity'737'_1608 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny Source #

du_identity'737'_1608 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_inverse_1610 ∷ T_Group_1564 → T_Σ_14 Source #

d_inverse'691'_1612 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny Source #

du_inverse'691'_1612 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_inverse'737'_1614 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny Source #

du_inverse'737'_1614 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_isEquivalence_1616 ∷ T_Group_1564 → T_IsEquivalence_28 Source #

d_isInvertibleMagma_1618 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_IsInvertibleMagma_958 Source #

du_isInvertibleMagma_1618 ∷ T_Group_1564 → T_IsInvertibleMagma_958 Source #

d_isInvertibleUnitalMagma_1620 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_IsInvertibleUnitalMagma_1012 Source #

du_isInvertibleUnitalMagma_1620 ∷ T_Group_1564 → T_IsInvertibleUnitalMagma_1012 Source #

d_isMagma_1622 ∷ T_Group_1564 → T_IsMagma_178 Source #

d_isMonoid_1624 ∷ T_Group_1564 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1626 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1626 ∷ T_Group_1564 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1628 ∷ T_Group_1564 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1630 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1630 ∷ T_Group_1564 → T_IsUnitalMagma_666 Source #

d_refl_1632 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_reflexive_1634 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1634 ∷ T_Group_1564 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1636 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_Setoid_46 Source #

du_setoid_1636 ∷ T_Group_1564 → T_Setoid_46 Source #

d_sym_1638 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1640 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1642 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1642 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1644 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1644 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1646 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1648 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1650 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1650 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1652 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1652 ∷ T_Group_1564 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawGroup_1654 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_RawGroup_108 Source #

du_rawGroup_1654 ∷ T_Group_1564 → T_RawGroup_108 Source #

d_monoid_1656 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_Monoid_914 Source #

du_monoid_1656 ∷ T_Group_1564 → T_Monoid_914 Source #

d__'8777'__1660 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → AgdaAny → AgdaAny → () Source #

d_magma_1662 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_Magma_74 Source #

du_magma_1662 ∷ T_Group_1564 → T_Magma_74 Source #

d_rawMagma_1664 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_RawMagma_44 Source #

du_rawMagma_1664 ∷ T_Group_1564 → T_RawMagma_44 Source #

d_rawMonoid_1666 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_RawMonoid_74 Source #

du_rawMonoid_1666 ∷ T_Group_1564 → T_RawMonoid_74 Source #

d_semigroup_1668 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_Semigroup_558 Source #

du_semigroup_1668 ∷ T_Group_1564 → T_Semigroup_558 Source #

d_unitalMagma_1670 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_UnitalMagma_844 Source #

du_unitalMagma_1670 ∷ T_Group_1564 → T_UnitalMagma_844 Source #

d_invertibleMagma_1672 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_InvertibleMagma_1400 Source #

du_invertibleMagma_1672 ∷ T_Group_1564 → T_InvertibleMagma_1400 Source #

d_invertibleUnitalMagma_1674 ∷ T_Level_18 → T_Level_18 → T_Group_1564 → T_InvertibleUnitalMagma_1476 Source #

du_invertibleUnitalMagma_1674 ∷ T_Group_1564 → T_InvertibleUnitalMagma_1476 Source #

d_AbelianGroup_1682 ∷ p → p → () Source #

data T_AbelianGroup_1682 Source #

d_Carrier_1700 ∷ T_AbelianGroup_1682 → () Source #

d__'8776'__1702 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny → () Source #

d__'8729'__1704 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1706 ∷ T_AbelianGroup_1682 → AgdaAny Source #

d__'8315''185'_1708 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny Source #

d_isAbelianGroup_1710 ∷ T_AbelianGroup_1682 → T_IsAbelianGroup_1172 Source #

d__'47''47'__1714 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__1714 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1716 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1718 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1720 ∷ T_AbelianGroup_1682 → T_Σ_14 Source #

d_identity'691'_1722 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → AgdaAny → AgdaAny Source #

du_identity'691'_1722 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny Source #

d_identity'737'_1724 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → AgdaAny → AgdaAny Source #

du_identity'737'_1724 ∷ T_AbelianGroup_1682 → AgdaAny → AgdaAny Source #

d_inverse_1726 ∷ T_AbelianGroup_1682 → T_Σ_14 Source #