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_26 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_44 Source #

du_setoid_44 ∷ T_SuccessorSet_8 → T_Setoid_44 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_Carrier_58 ∷ T_Level_18 → T_Level_18 → T_SuccessorSet_8 → () Source #

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

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

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

du_zero'35'_62 ∷ T_SuccessorSet_8 → AgdaAny Source #

d_Magma_68 ∷ p → p → () Source #

data T_Magma_68 Source #

d_Carrier_82 ∷ T_Magma_68 → () Source #

d__'8776'__84 ∷ T_Magma_68 → AgdaAny → AgdaAny → () Source #

d__'8729'__86 ∷ T_Magma_68 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_88 ∷ T_Magma_68 → T_IsMagma_176 Source #

d_isEquivalence_92 ∷ T_Magma_68 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_94 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_94 ∷ T_Magma_68 → T_IsPartialEquivalence_16 Source #

d_refl_96 ∷ T_Magma_68 → AgdaAny → AgdaAny Source #

d_reflexive_98 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_98 ∷ T_Magma_68 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_100 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → T_Setoid_44 Source #

du_setoid_100 ∷ T_Magma_68 → T_Setoid_44 Source #

d_sym_102 ∷ T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_104 ∷ T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_106 ∷ T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_108 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_108 ∷ T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_110 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_110 ∷ T_Magma_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawMagma_112 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → T_RawMagma_36 Source #

du_rawMagma_112 ∷ T_Magma_68 → T_RawMagma_36 Source #

d__'8777'__116 ∷ T_Level_18 → T_Level_18 → T_Magma_68 → AgdaAny → AgdaAny → () Source #

d_SelectiveMagma_122 ∷ p → p → () Source #

data T_SelectiveMagma_122 Source #

d_Carrier_136 ∷ T_SelectiveMagma_122 → () Source #

d__'8776'__138 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → () Source #

d__'8729'__140 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSelectiveMagma_142 ∷ T_SelectiveMagma_122 → T_IsSelectiveMagma_436 Source #

d_isEquivalence_146 ∷ T_SelectiveMagma_122 → T_IsEquivalence_26 Source #

d_isMagma_148 ∷ T_SelectiveMagma_122 → T_IsMagma_176 Source #

d_isPartialEquivalence_150 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_150 ∷ T_SelectiveMagma_122 → T_IsPartialEquivalence_16 Source #

d_refl_152 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny Source #

d_reflexive_154 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_154 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sel_156 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_setoid_158 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → T_Setoid_44 Source #

du_setoid_158 ∷ T_SelectiveMagma_122 → T_Setoid_44 Source #

d_sym_160 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_162 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_164 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_166 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_166 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_168 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_168 ∷ T_SelectiveMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_170 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → T_Magma_68 Source #

du_magma_170 ∷ T_SelectiveMagma_122 → T_Magma_68 Source #

d_rawMagma_174 ∷ T_Level_18 → T_Level_18 → T_SelectiveMagma_122 → T_RawMagma_36 Source #

du_rawMagma_174 ∷ T_SelectiveMagma_122 → T_RawMagma_36 Source #

d_CommutativeMagma_180 ∷ p → p → () Source #

data T_CommutativeMagma_180 Source #

d_Carrier_194 ∷ T_CommutativeMagma_180 → () Source #

d__'8776'__196 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → () Source #

d__'8729'__198 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_200 ∷ T_CommutativeMagma_180 → T_IsCommutativeMagma_212 Source #

d_comm_204 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_206 ∷ T_CommutativeMagma_180 → T_IsEquivalence_26 Source #

d_isMagma_208 ∷ T_CommutativeMagma_180 → T_IsMagma_176 Source #

d_isPartialEquivalence_210 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_210 ∷ T_CommutativeMagma_180 → T_IsPartialEquivalence_16 Source #

d_refl_212 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny Source #

d_reflexive_214 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_214 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_216 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → T_Setoid_44 Source #

du_setoid_216 ∷ T_CommutativeMagma_180 → T_Setoid_44 Source #

d_sym_218 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_220 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_222 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_224 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_224 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_226 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_226 ∷ T_CommutativeMagma_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_228 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → T_Magma_68 Source #

du_magma_228 ∷ T_CommutativeMagma_180 → T_Magma_68 Source #

d_rawMagma_232 ∷ T_Level_18 → T_Level_18 → T_CommutativeMagma_180 → T_RawMagma_36 Source #

du_rawMagma_232 ∷ T_CommutativeMagma_180 → T_RawMagma_36 Source #

d_IdempotentMagma_238 ∷ p → p → () Source #

data T_IdempotentMagma_238 Source #

d_Carrier_252 ∷ T_IdempotentMagma_238 → () Source #

d__'8776'__254 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → () Source #

d__'8729'__256 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny Source #

d_isIdempotentMagma_258 ∷ T_IdempotentMagma_238 → T_IsIdempotentMagma_248 Source #

d_idem_262 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny Source #

d_isEquivalence_264 ∷ T_IdempotentMagma_238 → T_IsEquivalence_26 Source #

d_isMagma_266 ∷ T_IdempotentMagma_238 → T_IsMagma_176 Source #

d_isPartialEquivalence_268 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_268 ∷ T_IdempotentMagma_238 → T_IsPartialEquivalence_16 Source #

d_refl_270 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny Source #

d_reflexive_272 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_272 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_274 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → T_Setoid_44 Source #

du_setoid_274 ∷ T_IdempotentMagma_238 → T_Setoid_44 Source #

d_sym_276 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_278 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_280 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_282 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_282 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_284 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_284 ∷ T_IdempotentMagma_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_286 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → T_Magma_68 Source #

du_magma_286 ∷ T_IdempotentMagma_238 → T_Magma_68 Source #

d_rawMagma_290 ∷ T_Level_18 → T_Level_18 → T_IdempotentMagma_238 → T_RawMagma_36 Source #

du_rawMagma_290 ∷ T_IdempotentMagma_238 → T_RawMagma_36 Source #

d_AlternativeMagma_296 ∷ p → p → () Source #

data T_AlternativeMagma_296 Source #

d_Carrier_310 ∷ T_AlternativeMagma_296 → () Source #

d__'8776'__312 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → () Source #

d__'8729'__314 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny Source #

d_isAlternativeMagma_316 ∷ T_AlternativeMagma_296 → T_IsAlternativeMagma_284 Source #

d_alter_320 ∷ T_AlternativeMagma_296 → T_Σ_14 Source #

d_alternative'691'_322 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny Source #

du_alternative'691'_322 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny Source #

d_alternative'737'_324 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny Source #

du_alternative'737'_324 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_326 ∷ T_AlternativeMagma_296 → T_IsEquivalence_26 Source #

d_isMagma_328 ∷ T_AlternativeMagma_296 → T_IsMagma_176 Source #

d_isPartialEquivalence_330 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_330 ∷ T_AlternativeMagma_296 → T_IsPartialEquivalence_16 Source #

d_refl_332 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny Source #

d_reflexive_334 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_334 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_336 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → T_Setoid_44 Source #

du_setoid_336 ∷ T_AlternativeMagma_296 → T_Setoid_44 Source #

d_sym_338 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_340 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_342 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_344 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_344 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_346 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_346 ∷ T_AlternativeMagma_296 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_348 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → T_Magma_68 Source #

du_magma_348 ∷ T_AlternativeMagma_296 → T_Magma_68 Source #

d_rawMagma_352 ∷ T_Level_18 → T_Level_18 → T_AlternativeMagma_296 → T_RawMagma_36 Source #

du_rawMagma_352 ∷ T_AlternativeMagma_296 → T_RawMagma_36 Source #

d_FlexibleMagma_358 ∷ p → p → () Source #

data T_FlexibleMagma_358 Source #

d_Carrier_372 ∷ T_FlexibleMagma_358 → () Source #

d__'8776'__374 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → () Source #

d__'8729'__376 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny Source #

d_isFlexibleMagma_378 ∷ T_FlexibleMagma_358 → T_IsFlexibleMagma_324 Source #

d_flex_382 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_384 ∷ T_FlexibleMagma_358 → T_IsEquivalence_26 Source #

d_isMagma_386 ∷ T_FlexibleMagma_358 → T_IsMagma_176 Source #

d_isPartialEquivalence_388 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_388 ∷ T_FlexibleMagma_358 → T_IsPartialEquivalence_16 Source #

d_refl_390 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny Source #

d_reflexive_392 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_392 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_394 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → T_Setoid_44 Source #

du_setoid_394 ∷ T_FlexibleMagma_358 → T_Setoid_44 Source #

d_sym_396 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_398 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_400 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_402 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_402 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_404 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_404 ∷ T_FlexibleMagma_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_406 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → T_Magma_68 Source #

du_magma_406 ∷ T_FlexibleMagma_358 → T_Magma_68 Source #

d_rawMagma_410 ∷ T_Level_18 → T_Level_18 → T_FlexibleMagma_358 → T_RawMagma_36 Source #

du_rawMagma_410 ∷ T_FlexibleMagma_358 → T_RawMagma_36 Source #

d_MedialMagma_416 ∷ p → p → () Source #

data T_MedialMagma_416 Source #

d_Carrier_430 ∷ T_MedialMagma_416 → () Source #

d__'8776'__432 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → () Source #

d__'8729'__434 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMedialMagma_436 ∷ T_MedialMagma_416 → T_IsMedialMagma_360 Source #

d_isEquivalence_440 ∷ T_MedialMagma_416 → T_IsEquivalence_26 Source #

d_isMagma_442 ∷ T_MedialMagma_416 → T_IsMagma_176 Source #

d_isPartialEquivalence_444 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_444 ∷ T_MedialMagma_416 → T_IsPartialEquivalence_16 Source #

d_medial_446 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_448 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny Source #

d_reflexive_450 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_450 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_452 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → T_Setoid_44 Source #

du_setoid_452 ∷ T_MedialMagma_416 → T_Setoid_44 Source #

d_sym_454 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_456 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_458 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_460 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_460 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_462 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_462 ∷ T_MedialMagma_416 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_464 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → T_Magma_68 Source #

du_magma_464 ∷ T_MedialMagma_416 → T_Magma_68 Source #

d_rawMagma_468 ∷ T_Level_18 → T_Level_18 → T_MedialMagma_416 → T_RawMagma_36 Source #

du_rawMagma_468 ∷ T_MedialMagma_416 → T_RawMagma_36 Source #

d_SemimedialMagma_474 ∷ p → p → () Source #

data T_SemimedialMagma_474 Source #

d_Carrier_488 ∷ T_SemimedialMagma_474 → () Source #

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

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

d_isSemimedialMagma_494 ∷ T_SemimedialMagma_474 → T_IsSemimedialMagma_396 Source #

d_isEquivalence_498 ∷ T_SemimedialMagma_474 → T_IsEquivalence_26 Source #

d_isMagma_500 ∷ T_SemimedialMagma_474 → T_IsMagma_176 Source #

d_isPartialEquivalence_502 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_502 ∷ T_SemimedialMagma_474 → T_IsPartialEquivalence_16 Source #

d_refl_504 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny Source #

d_reflexive_506 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_506 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_semiMedial_508 ∷ T_SemimedialMagma_474 → T_Σ_14 Source #

d_semimedial'691'_510 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_semimedial'691'_510 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semimedial'737'_512 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_semimedial'737'_512 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_514 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → T_Setoid_44 Source #

du_setoid_514 ∷ T_SemimedialMagma_474 → T_Setoid_44 Source #

d_sym_516 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_518 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_520 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_522 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_522 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_524 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_524 ∷ T_SemimedialMagma_474 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_526 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → T_Magma_68 Source #

du_magma_526 ∷ T_SemimedialMagma_474 → T_Magma_68 Source #

d_rawMagma_530 ∷ T_Level_18 → T_Level_18 → T_SemimedialMagma_474 → T_RawMagma_36 Source #

du_rawMagma_530 ∷ T_SemimedialMagma_474 → T_RawMagma_36 Source #

d_Semigroup_536 ∷ p → p → () Source #

data T_Semigroup_536 Source #

d_Carrier_550 ∷ T_Semigroup_536 → () Source #

d__'8776'__552 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → () Source #

d__'8729'__554 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemigroup_556 ∷ T_Semigroup_536 → T_IsSemigroup_472 Source #

d_assoc_560 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_562 ∷ T_Semigroup_536 → T_IsEquivalence_26 Source #

d_isMagma_564 ∷ T_Semigroup_536 → T_IsMagma_176 Source #

d_isPartialEquivalence_566 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_566 ∷ T_Semigroup_536 → T_IsPartialEquivalence_16 Source #

d_refl_568 ∷ T_Semigroup_536 → AgdaAny → AgdaAny Source #

d_reflexive_570 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_570 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_572 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → T_Setoid_44 Source #

du_setoid_572 ∷ T_Semigroup_536 → T_Setoid_44 Source #

d_sym_574 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_576 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_578 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_580 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_580 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_582 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_582 ∷ T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_584 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → T_Magma_68 Source #

du_magma_584 ∷ T_Semigroup_536 → T_Magma_68 Source #

d__'8777'__588 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → AgdaAny → AgdaAny → () Source #

d_rawMagma_590 ∷ T_Level_18 → T_Level_18 → T_Semigroup_536 → T_RawMagma_36 Source #

du_rawMagma_590 ∷ T_Semigroup_536 → T_RawMagma_36 Source #

d_Band_596 ∷ p → p → () Source #

data T_Band_596 Source #

d_Carrier_610 ∷ T_Band_596 → () Source #

d__'8776'__612 ∷ T_Band_596 → AgdaAny → AgdaAny → () Source #

d__'8729'__614 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_616 ∷ T_Band_596 → T_IsBand_508 Source #

d_assoc_620 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_622 ∷ T_Band_596 → AgdaAny → AgdaAny Source #

d_isEquivalence_624 ∷ T_Band_596 → T_IsEquivalence_26 Source #

d_isMagma_626 ∷ T_Band_596 → T_IsMagma_176 Source #

d_isPartialEquivalence_628 ∷ T_Level_18 → T_Level_18 → T_Band_596 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_628 ∷ T_Band_596 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_630 ∷ T_Band_596 → T_IsSemigroup_472 Source #

d_refl_632 ∷ T_Band_596 → AgdaAny → AgdaAny Source #

d_reflexive_634 ∷ T_Level_18 → T_Level_18 → T_Band_596 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_634 ∷ T_Band_596 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_636 ∷ T_Level_18 → T_Level_18 → T_Band_596 → T_Setoid_44 Source #

du_setoid_636 ∷ T_Band_596 → T_Setoid_44 Source #

d_sym_638 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_640 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_642 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_644 ∷ T_Level_18 → T_Level_18 → T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_644 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_646 ∷ T_Level_18 → T_Level_18 → T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_646 ∷ T_Band_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_648 ∷ T_Level_18 → T_Level_18 → T_Band_596 → T_Semigroup_536 Source #

du_semigroup_648 ∷ T_Band_596 → T_Semigroup_536 Source #

d__'8777'__652 ∷ T_Level_18 → T_Level_18 → T_Band_596 → AgdaAny → AgdaAny → () Source #

d_magma_654 ∷ T_Level_18 → T_Level_18 → T_Band_596 → T_Magma_68 Source #

du_magma_654 ∷ T_Band_596 → T_Magma_68 Source #

d_rawMagma_656 ∷ T_Level_18 → T_Level_18 → T_Band_596 → T_RawMagma_36 Source #

du_rawMagma_656 ∷ T_Band_596 → T_RawMagma_36 Source #

d_CommutativeSemigroup_662 ∷ p → p → () Source #

data T_CommutativeSemigroup_662 Source #

d_Carrier_676 ∷ T_CommutativeSemigroup_662 → () Source #

d__'8776'__678 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → () Source #

d__'8729'__680 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeSemigroup_682 ∷ T_CommutativeSemigroup_662 → T_IsCommutativeSemigroup_548 Source #

d_assoc_686 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_688 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_690 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_690 ∷ T_CommutativeSemigroup_662 → T_IsCommutativeMagma_212 Source #

d_isEquivalence_692 ∷ T_CommutativeSemigroup_662 → T_IsEquivalence_26 Source #

d_isMagma_694 ∷ T_CommutativeSemigroup_662 → T_IsMagma_176 Source #

d_isPartialEquivalence_696 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_696 ∷ T_CommutativeSemigroup_662 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_698 ∷ T_CommutativeSemigroup_662 → T_IsSemigroup_472 Source #

d_refl_700 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny Source #

d_reflexive_702 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_702 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_704 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_Setoid_44 Source #

du_setoid_704 ∷ T_CommutativeSemigroup_662 → T_Setoid_44 Source #

d_sym_706 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_708 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_710 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_712 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_712 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_714 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_714 ∷ T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_716 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_Semigroup_536 Source #

du_semigroup_716 ∷ T_CommutativeSemigroup_662 → T_Semigroup_536 Source #

d__'8777'__720 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → AgdaAny → AgdaAny → () Source #

d_magma_722 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_Magma_68 Source #

du_magma_722 ∷ T_CommutativeSemigroup_662 → T_Magma_68 Source #

d_rawMagma_724 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_RawMagma_36 Source #

du_rawMagma_724 ∷ T_CommutativeSemigroup_662 → T_RawMagma_36 Source #

d_commutativeMagma_726 ∷ T_Level_18 → T_Level_18 → T_CommutativeSemigroup_662 → T_CommutativeMagma_180 Source #

du_commutativeMagma_726 ∷ T_CommutativeSemigroup_662 → T_CommutativeMagma_180 Source #

d_CommutativeBand_732 ∷ p → p → () Source #

data T_CommutativeBand_732 Source #

d_Carrier_746 ∷ T_CommutativeBand_732 → () Source #

d__'8776'__748 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → () Source #

d__'8729'__750 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeBand_752 ∷ T_CommutativeBand_732 → T_IsCommutativeBand_590 Source #

d_assoc_756 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_758 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_760 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny Source #

d_isBand_762 ∷ T_CommutativeBand_732 → T_IsBand_508 Source #

d_isCommutativeMagma_764 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_764 ∷ T_CommutativeBand_732 → T_IsCommutativeMagma_212 Source #

d_isCommutativeSemigroup_766 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_766 ∷ T_CommutativeBand_732 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_768 ∷ T_CommutativeBand_732 → T_IsEquivalence_26 Source #

d_isMagma_770 ∷ T_CommutativeBand_732 → T_IsMagma_176 Source #

d_isPartialEquivalence_772 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_772 ∷ T_CommutativeBand_732 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_774 ∷ T_CommutativeBand_732 → T_IsSemigroup_472 Source #

d_refl_776 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny Source #

d_reflexive_778 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_778 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_780 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_Setoid_44 Source #

du_setoid_780 ∷ T_CommutativeBand_732 → T_Setoid_44 Source #

d_sym_782 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_784 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_786 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_788 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_788 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_790 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_790 ∷ T_CommutativeBand_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_band_792 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_Band_596 Source #

du_band_792 ∷ T_CommutativeBand_732 → T_Band_596 Source #

d__'8777'__796 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → AgdaAny → AgdaAny → () Source #

d_magma_798 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_Magma_68 Source #

du_magma_798 ∷ T_CommutativeBand_732 → T_Magma_68 Source #

d_rawMagma_800 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_RawMagma_36 Source #

du_rawMagma_800 ∷ T_CommutativeBand_732 → T_RawMagma_36 Source #

d_semigroup_802 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_Semigroup_536 Source #

du_semigroup_802 ∷ T_CommutativeBand_732 → T_Semigroup_536 Source #

d_commutativeSemigroup_804 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_CommutativeSemigroup_662 Source #

du_commutativeSemigroup_804 ∷ T_CommutativeBand_732 → T_CommutativeSemigroup_662 Source #

d_commutativeMagma_808 ∷ T_Level_18 → T_Level_18 → T_CommutativeBand_732 → T_CommutativeMagma_180 Source #

du_commutativeMagma_808 ∷ T_CommutativeBand_732 → T_CommutativeMagma_180 Source #

d_UnitalMagma_814 ∷ p → p → () Source #

data T_UnitalMagma_814 Source #

d_Carrier_830 ∷ T_UnitalMagma_814 → () Source #

d__'8776'__832 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → () Source #

d__'8729'__834 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_836 ∷ T_UnitalMagma_814 → AgdaAny Source #

d_isUnitalMagma_838 ∷ T_UnitalMagma_814 → T_IsUnitalMagma_642 Source #

d_identity_842 ∷ T_UnitalMagma_814 → T_Σ_14 Source #

d_identity'691'_844 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → AgdaAny → AgdaAny Source #

du_identity'691'_844 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny Source #

d_identity'737'_846 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → AgdaAny → AgdaAny Source #

du_identity'737'_846 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny Source #

d_isEquivalence_848 ∷ T_UnitalMagma_814 → T_IsEquivalence_26 Source #

d_isMagma_850 ∷ T_UnitalMagma_814 → T_IsMagma_176 Source #

d_isPartialEquivalence_852 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_852 ∷ T_UnitalMagma_814 → T_IsPartialEquivalence_16 Source #

d_refl_854 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny Source #

d_reflexive_856 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_856 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_858 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → T_Setoid_44 Source #

du_setoid_858 ∷ T_UnitalMagma_814 → T_Setoid_44 Source #

d_sym_860 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_862 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_864 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_866 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_866 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_868 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_868 ∷ T_UnitalMagma_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_870 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → T_Magma_68 Source #

du_magma_870 ∷ T_UnitalMagma_814 → T_Magma_68 Source #

d__'8777'__874 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → AgdaAny → AgdaAny → () Source #

d_rawMagma_876 ∷ T_Level_18 → T_Level_18 → T_UnitalMagma_814 → T_RawMagma_36 Source #

du_rawMagma_876 ∷ T_UnitalMagma_814 → T_RawMagma_36 Source #

d_Monoid_882 ∷ p → p → () Source #

data T_Monoid_882 Source #

d_Carrier_898 ∷ T_Monoid_882 → () Source #

d__'8776'__900 ∷ T_Monoid_882 → AgdaAny → AgdaAny → () Source #

d__'8729'__902 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_904 ∷ T_Monoid_882 → AgdaAny Source #

d_isMonoid_906 ∷ T_Monoid_882 → T_IsMonoid_686 Source #

d_assoc_910 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_912 ∷ T_Monoid_882 → T_Σ_14 Source #

d_identity'691'_914 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → AgdaAny → AgdaAny Source #

du_identity'691'_914 ∷ T_Monoid_882 → AgdaAny → AgdaAny Source #

d_identity'737'_916 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → AgdaAny → AgdaAny Source #

du_identity'737'_916 ∷ T_Monoid_882 → AgdaAny → AgdaAny Source #

d_isEquivalence_918 ∷ T_Monoid_882 → T_IsEquivalence_26 Source #

d_isMagma_920 ∷ T_Monoid_882 → T_IsMagma_176 Source #

d_isPartialEquivalence_922 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_922 ∷ T_Monoid_882 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_924 ∷ T_Monoid_882 → T_IsSemigroup_472 Source #

d_isUnitalMagma_926 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_926 ∷ T_Monoid_882 → T_IsUnitalMagma_642 Source #

d_refl_928 ∷ T_Monoid_882 → AgdaAny → AgdaAny Source #

d_reflexive_930 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_930 ∷ T_Monoid_882 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_932 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_Setoid_44 Source #

du_setoid_932 ∷ T_Monoid_882 → T_Setoid_44 Source #

d_sym_934 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_936 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_938 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_940 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_940 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_942 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_942 ∷ T_Monoid_882 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semigroup_944 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_Semigroup_536 Source #

du_semigroup_944 ∷ T_Monoid_882 → T_Semigroup_536 Source #

d__'8777'__948 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → AgdaAny → AgdaAny → () Source #

d_magma_950 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_Magma_68 Source #

du_magma_950 ∷ T_Monoid_882 → T_Magma_68 Source #

d_rawMagma_952 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_RawMagma_36 Source #

du_rawMagma_952 ∷ T_Monoid_882 → T_RawMagma_36 Source #

d_rawMonoid_954 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_RawMonoid_64 Source #

du_rawMonoid_954 ∷ T_Monoid_882 → T_RawMonoid_64 Source #

d_unitalMagma_956 ∷ T_Level_18 → T_Level_18 → T_Monoid_882 → T_UnitalMagma_814 Source #

du_unitalMagma_956 ∷ T_Monoid_882 → T_UnitalMagma_814 Source #

d_CommutativeMonoid_962 ∷ p → p → () Source #

data T_CommutativeMonoid_962 Source #

d_Carrier_978 ∷ T_CommutativeMonoid_962 → () Source #

d__'8776'__980 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → () Source #

d__'8729'__982 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_984 ∷ T_CommutativeMonoid_962 → AgdaAny Source #

d_isCommutativeMonoid_986 ∷ T_CommutativeMonoid_962 → T_IsCommutativeMonoid_736 Source #

d_assoc_990 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_992 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_994 ∷ T_CommutativeMonoid_962 → T_Σ_14 Source #

d_identity'691'_996 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → AgdaAny → AgdaAny Source #

du_identity'691'_996 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny Source #

d_identity'737'_998 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → AgdaAny → AgdaAny Source #

du_identity'737'_998 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1000 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_1000 ∷ T_CommutativeMonoid_962 → T_IsCommutativeMagma_212 Source #

d_isCommutativeSemigroup_1002 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_1002 ∷ T_CommutativeMonoid_962 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_1004 ∷ T_CommutativeMonoid_962 → T_IsEquivalence_26 Source #

d_isMagma_1006 ∷ T_CommutativeMonoid_962 → T_IsMagma_176 Source #

d_isMonoid_1008 ∷ T_CommutativeMonoid_962 → T_IsMonoid_686 Source #

d_isPartialEquivalence_1010 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1010 ∷ T_CommutativeMonoid_962 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1012 ∷ T_CommutativeMonoid_962 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1014 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1014 ∷ T_CommutativeMonoid_962 → T_IsUnitalMagma_642 Source #

d_refl_1016 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny Source #

d_reflexive_1018 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1018 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1020 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_Setoid_44 Source #

du_setoid_1020 ∷ T_CommutativeMonoid_962 → T_Setoid_44 Source #

d_sym_1022 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1024 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1026 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1028 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1028 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1030 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1030 ∷ T_CommutativeMonoid_962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_monoid_1032 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_Monoid_882 Source #

du_monoid_1032 ∷ T_CommutativeMonoid_962 → T_Monoid_882 Source #

d__'8777'__1036 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → AgdaAny → AgdaAny → () Source #

d_magma_1038 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_Magma_68 Source #

du_magma_1038 ∷ T_CommutativeMonoid_962 → T_Magma_68 Source #

d_rawMagma_1040 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_RawMagma_36 Source #

du_rawMagma_1040 ∷ T_CommutativeMonoid_962 → T_RawMagma_36 Source #

d_rawMonoid_1042 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_RawMonoid_64 Source #

du_rawMonoid_1042 ∷ T_CommutativeMonoid_962 → T_RawMonoid_64 Source #

d_semigroup_1044 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_Semigroup_536 Source #

du_semigroup_1044 ∷ T_CommutativeMonoid_962 → T_Semigroup_536 Source #

d_unitalMagma_1046 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_UnitalMagma_814 Source #

du_unitalMagma_1046 ∷ T_CommutativeMonoid_962 → T_UnitalMagma_814 Source #

d_commutativeSemigroup_1048 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_CommutativeSemigroup_662 Source #

du_commutativeSemigroup_1048 ∷ T_CommutativeMonoid_962 → T_CommutativeSemigroup_662 Source #

d_commutativeMagma_1052 ∷ T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_CommutativeMagma_180 Source #

du_commutativeMagma_1052 ∷ T_CommutativeMonoid_962 → T_CommutativeMagma_180 Source #

d_IdempotentMonoid_1058 ∷ p → p → () Source #

data T_IdempotentMonoid_1058 Source #

d_Carrier_1074 ∷ T_IdempotentMonoid_1058 → () Source #

d__'8776'__1076 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → () Source #

d__'8729'__1078 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1080 ∷ T_IdempotentMonoid_1058 → AgdaAny Source #

d_isIdempotentMonoid_1082 ∷ T_IdempotentMonoid_1058 → T_IsIdempotentMonoid_796 Source #

d_assoc_1086 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_1088 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny Source #

d_identity_1090 ∷ T_IdempotentMonoid_1058 → T_Σ_14 Source #

d_identity'691'_1092 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → AgdaAny → AgdaAny Source #

du_identity'691'_1092 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny Source #

d_identity'737'_1094 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → AgdaAny → AgdaAny Source #

du_identity'737'_1094 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny Source #

d_isBand_1096 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_IsBand_508 Source #

du_isBand_1096 ∷ T_IdempotentMonoid_1058 → T_IsBand_508 Source #

d_isEquivalence_1098 ∷ T_IdempotentMonoid_1058 → T_IsEquivalence_26 Source #

d_isMagma_1100 ∷ T_IdempotentMonoid_1058 → T_IsMagma_176 Source #

d_isMonoid_1102 ∷ T_IdempotentMonoid_1058 → T_IsMonoid_686 Source #

d_isPartialEquivalence_1104 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1104 ∷ T_IdempotentMonoid_1058 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1106 ∷ T_IdempotentMonoid_1058 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1108 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1108 ∷ T_IdempotentMonoid_1058 → T_IsUnitalMagma_642 Source #

d_refl_1110 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny Source #

d_reflexive_1112 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1112 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1114 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_Setoid_44 Source #

du_setoid_1114 ∷ T_IdempotentMonoid_1058 → T_Setoid_44 Source #

d_sym_1116 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1118 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1120 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1122 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1122 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1124 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1124 ∷ T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_monoid_1126 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_Monoid_882 Source #

du_monoid_1126 ∷ T_IdempotentMonoid_1058 → T_Monoid_882 Source #

d__'8777'__1130 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → AgdaAny → AgdaAny → () Source #

d_magma_1132 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_Magma_68 Source #

du_magma_1132 ∷ T_IdempotentMonoid_1058 → T_Magma_68 Source #

d_rawMagma_1134 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_RawMagma_36 Source #

du_rawMagma_1134 ∷ T_IdempotentMonoid_1058 → T_RawMagma_36 Source #

d_rawMonoid_1136 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_RawMonoid_64 Source #

du_rawMonoid_1136 ∷ T_IdempotentMonoid_1058 → T_RawMonoid_64 Source #

d_semigroup_1138 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_Semigroup_536 Source #

du_semigroup_1138 ∷ T_IdempotentMonoid_1058 → T_Semigroup_536 Source #

d_unitalMagma_1140 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_UnitalMagma_814 Source #

du_unitalMagma_1140 ∷ T_IdempotentMonoid_1058 → T_UnitalMagma_814 Source #

d_band_1142 ∷ T_Level_18 → T_Level_18 → T_IdempotentMonoid_1058 → T_Band_596 Source #

du_band_1142 ∷ T_IdempotentMonoid_1058 → T_Band_596 Source #

d_IdempotentCommutativeMonoid_1148 ∷ p → p → () Source #

data T_IdempotentCommutativeMonoid_1148 Source #

d_Carrier_1164 ∷ T_IdempotentCommutativeMonoid_1148 → () Source #

d__'8776'__1166 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → () Source #

d__'8729'__1168 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1170 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny Source #

d_isIdempotentCommutativeMonoid_1172 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsIdempotentCommutativeMonoid_852 Source #

d_assoc_1176 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1178 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_1180 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_identity_1182 ∷ T_IdempotentCommutativeMonoid_1148 → T_Σ_14 Source #

d_identity'691'_1184 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

du_identity'691'_1184 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_identity'737'_1186 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

du_identity'737'_1186 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_isBand_1188 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsBand_508 Source #

du_isBand_1188 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsBand_508 Source #

d_isCommutativeBand_1190 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_1190 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeBand_590 Source #

d_isCommutativeMagma_1192 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_1192 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeMagma_212 Source #

d_isCommutativeMonoid_1194 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeMonoid_736 Source #

d_isCommutativeSemigroup_1196 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_1196 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_1198 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsEquivalence_26 Source #

d_isIdempotentMonoid_1200 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsIdempotentMonoid_796 Source #

du_isIdempotentMonoid_1200 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsIdempotentMonoid_796 Source #

d_isMagma_1202 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsMagma_176 Source #

d_isMonoid_1204 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsMonoid_686 Source #

d_isPartialEquivalence_1206 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1206 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1208 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1210 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1210 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsUnitalMagma_642 Source #

d_refl_1212 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_reflexive_1214 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1214 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1216 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Setoid_44 Source #

du_setoid_1216 ∷ T_IdempotentCommutativeMonoid_1148 → T_Setoid_44 Source #

d_sym_1218 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1220 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1222 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1224 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1224 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1226 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1226 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeMonoid_1228 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

du_commutativeMonoid_1228 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

d_idempotentMonoid_1230 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentMonoid_1058 Source #

du_idempotentMonoid_1230 ∷ T_IdempotentCommutativeMonoid_1148 → T_IdempotentMonoid_1058 Source #

d_commutativeBand_1232 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeBand_732 Source #

du_commutativeBand_1232 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeBand_732 Source #

d__'8777'__1236 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → () Source #

d_commutativeMagma_1238 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeMagma_180 Source #

du_commutativeMagma_1238 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeMagma_180 Source #

d_commutativeSemigroup_1240 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeSemigroup_662 Source #

du_commutativeSemigroup_1240 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeSemigroup_662 Source #

d_magma_1242 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Magma_68 Source #

du_magma_1242 ∷ T_IdempotentCommutativeMonoid_1148 → T_Magma_68 Source #

d_monoid_1244 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

du_monoid_1244 ∷ T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

d_rawMagma_1246 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_RawMagma_36 Source #

du_rawMagma_1246 ∷ T_IdempotentCommutativeMonoid_1148 → T_RawMagma_36 Source #

d_rawMonoid_1248 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_RawMonoid_64 Source #

du_rawMonoid_1248 ∷ T_IdempotentCommutativeMonoid_1148 → T_RawMonoid_64 Source #

d_semigroup_1250 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Semigroup_536 Source #

du_semigroup_1250 ∷ T_IdempotentCommutativeMonoid_1148 → T_Semigroup_536 Source #

d_unitalMagma_1252 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_UnitalMagma_814 Source #

du_unitalMagma_1252 ∷ T_IdempotentCommutativeMonoid_1148 → T_UnitalMagma_814 Source #

d_band_1256 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Band_596 Source #

du_band_1256 ∷ T_IdempotentCommutativeMonoid_1148 → T_Band_596 Source #

d_BoundedLattice_1258 ∷ T_Level_18 → T_Level_18 → () Source #

d__'8729'__1268 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1270 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → () Source #

d__'8777'__1272 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → () Source #

d_Carrier_1274 ∷ T_IdempotentCommutativeMonoid_1148 → () Source #

d_assoc_1276 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_band_1278 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Band_596 Source #

du_band_1278 ∷ T_IdempotentCommutativeMonoid_1148 → T_Band_596 Source #

d_comm_1280 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeBand_1282 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeBand_732 Source #

du_commutativeBand_1282 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeBand_732 Source #

d_commutativeMagma_1284 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeMagma_180 Source #

du_commutativeMagma_1284 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeMagma_180 Source #

d_commutativeMonoid_1286 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

du_commutativeMonoid_1286 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

d_commutativeSemigroup_1288 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeSemigroup_662 Source #

du_commutativeSemigroup_1288 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeSemigroup_662 Source #

d_idem_1290 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_idempotentMonoid_1292 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentMonoid_1058 Source #

du_idempotentMonoid_1292 ∷ T_IdempotentCommutativeMonoid_1148 → T_IdempotentMonoid_1058 Source #

d_identity_1294 ∷ T_IdempotentCommutativeMonoid_1148 → T_Σ_14 Source #

d_identity'691'_1296 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

du_identity'691'_1296 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_identity'737'_1298 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

du_identity'737'_1298 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_isBand_1300 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsBand_508 Source #

du_isBand_1300 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsBand_508 Source #

d_isCommutativeBand_1302 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_1302 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeBand_590 Source #

d_isCommutativeMagma_1304 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_1304 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeMagma_212 Source #

d_isCommutativeMonoid_1306 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeMonoid_736 Source #

d_isCommutativeSemigroup_1308 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_1308 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_1310 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsEquivalence_26 Source #

d_isIdempotentCommutativeMonoid_1312 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsIdempotentCommutativeMonoid_852 Source #

d_isIdempotentMonoid_1314 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsIdempotentMonoid_796 Source #

du_isIdempotentMonoid_1314 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsIdempotentMonoid_796 Source #

d_isMagma_1316 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsMagma_176 Source #

d_isMonoid_1318 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsMonoid_686 Source #

d_isPartialEquivalence_1320 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1320 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1322 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1324 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1324 ∷ T_IdempotentCommutativeMonoid_1148 → T_IsUnitalMagma_642 Source #

d_magma_1326 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Magma_68 Source #

du_magma_1326 ∷ T_IdempotentCommutativeMonoid_1148 → T_Magma_68 Source #

d_monoid_1328 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

du_monoid_1328 ∷ T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

d_rawMagma_1330 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_RawMagma_36 Source #

du_rawMagma_1330 ∷ T_IdempotentCommutativeMonoid_1148 → T_RawMagma_36 Source #

d_rawMonoid_1332 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_RawMonoid_64 Source #

du_rawMonoid_1332 ∷ T_IdempotentCommutativeMonoid_1148 → T_RawMonoid_64 Source #

d_refl_1334 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny Source #

d_reflexive_1336 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1336 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_semigroup_1338 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Semigroup_536 Source #

du_semigroup_1338 ∷ T_IdempotentCommutativeMonoid_1148 → T_Semigroup_536 Source #

d_setoid_1340 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_Setoid_44 Source #

du_setoid_1340 ∷ T_IdempotentCommutativeMonoid_1148 → T_Setoid_44 Source #

d_sym_1342 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1344 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unitalMagma_1346 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_UnitalMagma_814 Source #

du_unitalMagma_1346 ∷ T_IdempotentCommutativeMonoid_1148 → T_UnitalMagma_814 Source #

d_ε_1348 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny Source #

d_'8729''45'cong_1350 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1352 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1352 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1354 ∷ T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1354 ∷ T_IdempotentCommutativeMonoid_1148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_InvertibleMagma_1360 ∷ p → p → () Source #

data T_InvertibleMagma_1360 Source #

d_Carrier_1378 ∷ T_InvertibleMagma_1360 → () Source #

d__'8776'__1380 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → () Source #

d__'8729'__1382 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1384 ∷ T_InvertibleMagma_1360 → AgdaAny Source #

d__'8315''185'_1386 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny Source #

d_isInvertibleMagma_1388 ∷ T_InvertibleMagma_1360 → T_IsInvertibleMagma_924 Source #

d_inverse_1392 ∷ T_InvertibleMagma_1360 → T_Σ_14 Source #

d_inverse'691'_1394 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → AgdaAny → AgdaAny Source #

du_inverse'691'_1394 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny Source #

d_inverse'737'_1396 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → AgdaAny → AgdaAny Source #

du_inverse'737'_1396 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny Source #

d_isEquivalence_1398 ∷ T_InvertibleMagma_1360 → T_IsEquivalence_26 Source #

d_isMagma_1400 ∷ T_InvertibleMagma_1360 → T_IsMagma_176 Source #

d_isPartialEquivalence_1402 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1402 ∷ T_InvertibleMagma_1360 → T_IsPartialEquivalence_16 Source #

d_refl_1404 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny Source #

d_reflexive_1406 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1406 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1408 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → T_Setoid_44 Source #

du_setoid_1408 ∷ T_InvertibleMagma_1360 → T_Setoid_44 Source #

d_sym_1410 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1412 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1414 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1416 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1418 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1418 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1420 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1420 ∷ T_InvertibleMagma_1360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_magma_1422 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → T_Magma_68 Source #

du_magma_1422 ∷ T_InvertibleMagma_1360 → T_Magma_68 Source #

d__'8777'__1426 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → AgdaAny → AgdaAny → () Source #

d_rawMagma_1428 ∷ T_Level_18 → T_Level_18 → T_InvertibleMagma_1360 → T_RawMagma_36 Source #

du_rawMagma_1428 ∷ T_InvertibleMagma_1360 → T_RawMagma_36 Source #

d_InvertibleUnitalMagma_1434 ∷ p → p → () Source #

data T_InvertibleUnitalMagma_1434 Source #

d_Carrier_1452 ∷ T_InvertibleUnitalMagma_1434 → () Source #

d__'8776'__1454 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → () Source #

d__'8729'__1456 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1458 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny Source #

d__'8315''185'_1460 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

d_isInvertibleUnitalMagma_1462 ∷ T_InvertibleUnitalMagma_1434 → T_IsInvertibleUnitalMagma_976 Source #

d_identity_1466 ∷ T_InvertibleUnitalMagma_1434 → T_Σ_14 Source #

d_identity'691'_1468 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

du_identity'691'_1468 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

d_identity'737'_1470 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

du_identity'737'_1470 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

d_inverse_1472 ∷ T_InvertibleUnitalMagma_1434 → T_Σ_14 Source #

d_inverse'691'_1474 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

du_inverse'691'_1474 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

d_inverse'737'_1476 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

du_inverse'737'_1476 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

d_isEquivalence_1478 ∷ T_InvertibleUnitalMagma_1434 → T_IsEquivalence_26 Source #

d_isInvertibleMagma_1480 ∷ T_InvertibleUnitalMagma_1434 → T_IsInvertibleMagma_924 Source #

d_isMagma_1482 ∷ T_InvertibleUnitalMagma_1434 → T_IsMagma_176 Source #

d_isPartialEquivalence_1484 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1484 ∷ T_InvertibleUnitalMagma_1434 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1486 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1486 ∷ T_InvertibleUnitalMagma_1434 → T_IsUnitalMagma_642 Source #

d_refl_1488 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny Source #

d_reflexive_1490 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1490 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1492 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → T_Setoid_44 Source #

du_setoid_1492 ∷ T_InvertibleUnitalMagma_1434 → T_Setoid_44 Source #

d_sym_1494 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1496 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1498 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1500 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1502 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1502 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1504 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1504 ∷ T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_invertibleMagma_1506 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → T_InvertibleMagma_1360 Source #

du_invertibleMagma_1506 ∷ T_InvertibleUnitalMagma_1434 → T_InvertibleMagma_1360 Source #

d__'8777'__1510 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → AgdaAny → AgdaAny → () Source #

d_magma_1512 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → T_Magma_68 Source #

du_magma_1512 ∷ T_InvertibleUnitalMagma_1434 → T_Magma_68 Source #

d_rawMagma_1514 ∷ T_Level_18 → T_Level_18 → T_InvertibleUnitalMagma_1434 → T_RawMagma_36 Source #

du_rawMagma_1514 ∷ T_InvertibleUnitalMagma_1434 → T_RawMagma_36 Source #

d_Group_1520 ∷ p → p → () Source #

data T_Group_1520 Source #

d_Carrier_1538 ∷ T_Group_1520 → () Source #

d__'8776'__1540 ∷ T_Group_1520 → AgdaAny → AgdaAny → () Source #

d__'8729'__1542 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1544 ∷ T_Group_1520 → AgdaAny Source #

d__'8315''185'_1546 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_isGroup_1548 ∷ T_Group_1520 → T_IsGroup_1036 Source #

d__'45'__1552 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

du__'45'__1552 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

d__'47''47'__1554 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__1554 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

d__'92''92'__1556 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

du__'92''92'__1556 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1558 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1560 ∷ T_Group_1520 → T_Σ_14 Source #

d_identity'691'_1562 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny Source #

du_identity'691'_1562 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_identity'737'_1564 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny Source #

du_identity'737'_1564 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_inverse_1566 ∷ T_Group_1520 → T_Σ_14 Source #

d_inverse'691'_1568 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny Source #

du_inverse'691'_1568 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_inverse'737'_1570 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny Source #

du_inverse'737'_1570 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_isEquivalence_1572 ∷ T_Group_1520 → T_IsEquivalence_26 Source #

d_isInvertibleMagma_1574 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_IsInvertibleMagma_924 Source #

du_isInvertibleMagma_1574 ∷ T_Group_1520 → T_IsInvertibleMagma_924 Source #

d_isInvertibleUnitalMagma_1576 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_IsInvertibleUnitalMagma_976 Source #

du_isInvertibleUnitalMagma_1576 ∷ T_Group_1520 → T_IsInvertibleUnitalMagma_976 Source #

d_isMagma_1578 ∷ T_Group_1520 → T_IsMagma_176 Source #

d_isMonoid_1580 ∷ T_Group_1520 → T_IsMonoid_686 Source #

d_isPartialEquivalence_1582 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1582 ∷ T_Group_1520 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1584 ∷ T_Group_1520 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1586 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1586 ∷ T_Group_1520 → T_IsUnitalMagma_642 Source #

d_refl_1588 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_reflexive_1590 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1590 ∷ T_Group_1520 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1592 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_Setoid_44 Source #

du_setoid_1592 ∷ T_Group_1520 → T_Setoid_44 Source #

d_sym_1594 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1596 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1598 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1598 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1600 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1600 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1602 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1604 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1606 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1606 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1608 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1608 ∷ T_Group_1520 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawGroup_1610 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_RawGroup_96 Source #

du_rawGroup_1610 ∷ T_Group_1520 → T_RawGroup_96 Source #

d_monoid_1612 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_Monoid_882 Source #

du_monoid_1612 ∷ T_Group_1520 → T_Monoid_882 Source #

d__'8777'__1616 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → AgdaAny → AgdaAny → () Source #

d_magma_1618 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_Magma_68 Source #

du_magma_1618 ∷ T_Group_1520 → T_Magma_68 Source #

d_rawMagma_1620 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_RawMagma_36 Source #

du_rawMagma_1620 ∷ T_Group_1520 → T_RawMagma_36 Source #

d_rawMonoid_1622 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_RawMonoid_64 Source #

du_rawMonoid_1622 ∷ T_Group_1520 → T_RawMonoid_64 Source #

d_semigroup_1624 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_Semigroup_536 Source #

du_semigroup_1624 ∷ T_Group_1520 → T_Semigroup_536 Source #

d_unitalMagma_1626 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_UnitalMagma_814 Source #

du_unitalMagma_1626 ∷ T_Group_1520 → T_UnitalMagma_814 Source #

d_invertibleMagma_1628 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_InvertibleMagma_1360 Source #

du_invertibleMagma_1628 ∷ T_Group_1520 → T_InvertibleMagma_1360 Source #

d_invertibleUnitalMagma_1630 ∷ T_Level_18 → T_Level_18 → T_Group_1520 → T_InvertibleUnitalMagma_1434 Source #

du_invertibleUnitalMagma_1630 ∷ T_Group_1520 → T_InvertibleUnitalMagma_1434 Source #

d_AbelianGroup_1636 ∷ p → p → () Source #

data T_AbelianGroup_1636 Source #

d_Carrier_1654 ∷ T_AbelianGroup_1636 → () Source #

d__'8776'__1656 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny → () Source #

d__'8729'__1658 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_1660 ∷ T_AbelianGroup_1636 → AgdaAny Source #

d__'8315''185'_1662 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #

d_isAbelianGroup_1664 ∷ T_AbelianGroup_1636 → T_IsAbelianGroup_1132 Source #

d__'47''47'__1668 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__1668 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1670 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1672 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1674 ∷ T_AbelianGroup_1636 → T_Σ_14 Source #

d_identity'691'_1676 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #

du_identity'691'_1676 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #

d_identity'737'_1678 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #

du_identity'737'_1678 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #

d_inverse_1680 ∷ T_AbelianGroup_1636 → T_Σ_14 Source #

d_inverse'691'_1682 ∷ T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #

du_inverse'691'_1682 ∷ T_AbelianGroup_1636 → AgdaAny → AgdaAny Source #