Documentation

d__DistributesOver__16 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__18 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__20 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostLeftCancellative_30 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostRightCancellative_32 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Alternative_34 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_36 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_40 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8321'_42 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_44 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Flexible_48 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Idempotent_50 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identical_54 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_56 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_60 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftAlternative_66 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftBol_68 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftCongruent_72 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftDivides_76 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftDivides'691'_78 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftDivides'737'_80 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_82 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_84 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftSemimedial_88 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_90 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Medial_92 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_MiddleBol_94 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightAlternative_96 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightBol_98 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightCongruent_102 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightDivides_106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightDivides'691'_108 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightDivides'737'_110 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightSemimedial_118 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_120 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Selective_122 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Semimedial_126 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_StarDestructive_128 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarExpansive_130 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarLeftDestructive_132 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarLeftExpansive_134 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarRightDestructive_136 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarRightExpansive_138 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Zero_140 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsSuccessorSet_146 ∷ p → p → p → p → p → p → () Source #

data T_IsSuccessorSet_146 Source #

d_isEquivalence_156 ∷ T_IsSuccessorSet_146 → T_IsEquivalence_26 Source #

d_suc'35''45'cong_158 ∷ T_IsSuccessorSet_146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_162 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_IsSuccessorSet_146 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_162 ∷ T_IsSuccessorSet_146 → T_IsPartialEquivalence_16 Source #

d_refl_164 ∷ T_IsSuccessorSet_146 → AgdaAny → AgdaAny Source #

d_reflexive_166 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_IsSuccessorSet_146 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_166 ∷ T_IsSuccessorSet_146 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_168 ∷ T_IsSuccessorSet_146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_170 ∷ T_IsSuccessorSet_146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_172 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_IsSuccessorSet_146 → T_Setoid_44 Source #

du_setoid_172 ∷ T_IsSuccessorSet_146 → T_Setoid_44 Source #

d_IsMagma_176 ∷ p → p → p → p → p → () Source #

data T_IsMagma_176 Source #

d_isEquivalence_184 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

d_'8729''45'cong_186 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_190 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_190 ∷ T_IsMagma_176 → T_IsPartialEquivalence_16 Source #

d_refl_192 ∷ T_IsMagma_176 → AgdaAny → AgdaAny Source #

d_reflexive_194 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_194 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_196 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_198 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_200 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → T_Setoid_44 Source #

du_setoid_200 ∷ T_IsMagma_176 → T_Setoid_44 Source #

d_'8729''45'cong'737'_202 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_202 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_206 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_206 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsCommutativeMagma_212 ∷ p → p → p → p → p → () Source #

data T_IsCommutativeMagma_212 Source #

d_isMagma_220 ∷ T_IsCommutativeMagma_212 → T_IsMagma_176 Source #

d_comm_222 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_226 ∷ T_IsCommutativeMagma_212 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_228 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_212 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_228 ∷ T_IsCommutativeMagma_212 → T_IsPartialEquivalence_16 Source #

d_refl_230 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny Source #

d_reflexive_232 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_232 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_234 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_212 → T_Setoid_44 Source #

du_setoid_234 ∷ T_IsCommutativeMagma_212 → T_Setoid_44 Source #

d_sym_236 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_238 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_240 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_242 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_242 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_244 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_244 ∷ T_IsCommutativeMagma_212 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsIdempotentMagma_248 ∷ p → p → p → p → p → () Source #

data T_IsIdempotentMagma_248 Source #

d_isMagma_256 ∷ T_IsIdempotentMagma_248 → T_IsMagma_176 Source #

d_idem_258 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny Source #

d_isEquivalence_262 ∷ T_IsIdempotentMagma_248 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsIdempotentMagma_248 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_264 ∷ T_IsIdempotentMagma_248 → T_IsPartialEquivalence_16 Source #

d_refl_266 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny Source #

d_reflexive_268 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_268 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsIdempotentMagma_248 → T_Setoid_44 Source #

du_setoid_270 ∷ T_IsIdempotentMagma_248 → T_Setoid_44 Source #

d_sym_272 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_274 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_276 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_278 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_278 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_280 ∷ T_IsIdempotentMagma_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsAlternativeMagma_284 ∷ p → p → p → p → p → () Source #

data T_IsAlternativeMagma_284 Source #

d_isMagma_292 ∷ T_IsAlternativeMagma_284 → T_IsMagma_176 Source #

d_alter_294 ∷ T_IsAlternativeMagma_284 → T_Σ_14 Source #

d_isEquivalence_298 ∷ T_IsAlternativeMagma_284 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_300 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_300 ∷ T_IsAlternativeMagma_284 → T_IsPartialEquivalence_16 Source #

d_refl_302 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny Source #

d_reflexive_304 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_304 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_306 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → T_Setoid_44 Source #

du_setoid_306 ∷ T_IsAlternativeMagma_284 → T_Setoid_44 Source #

d_sym_308 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_310 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_312 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_314 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_314 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_316 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_316 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_alternative'737'_318 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny Source #

du_alternative'737'_318 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny Source #

d_alternative'691'_320 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny Source #

du_alternative'691'_320 ∷ T_IsAlternativeMagma_284 → AgdaAny → AgdaAny → AgdaAny Source #

d_IsFlexibleMagma_324 ∷ p → p → p → p → p → () Source #

data T_IsFlexibleMagma_324 Source #

d_isMagma_332 ∷ T_IsFlexibleMagma_324 → T_IsMagma_176 Source #

d_flex_334 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_338 ∷ T_IsFlexibleMagma_324 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsFlexibleMagma_324 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_340 ∷ T_IsFlexibleMagma_324 → T_IsPartialEquivalence_16 Source #

d_refl_342 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny Source #

d_reflexive_344 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_344 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_346 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsFlexibleMagma_324 → T_Setoid_44 Source #

du_setoid_346 ∷ T_IsFlexibleMagma_324 → T_Setoid_44 Source #

d_sym_348 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_350 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_352 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_354 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_354 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_356 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_356 ∷ T_IsFlexibleMagma_324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMedialMagma_360 ∷ p → p → p → p → p → () Source #

data T_IsMedialMagma_360 Source #

d_isMagma_368 ∷ T_IsMedialMagma_360 → T_IsMagma_176 Source #

d_medial_370 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_374 ∷ T_IsMedialMagma_360 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_376 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMedialMagma_360 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_376 ∷ T_IsMedialMagma_360 → T_IsPartialEquivalence_16 Source #

d_refl_378 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny Source #

d_reflexive_380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMedialMagma_360 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_380 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_382 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMedialMagma_360 → T_Setoid_44 Source #

du_setoid_382 ∷ T_IsMedialMagma_360 → T_Setoid_44 Source #

d_sym_384 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_386 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_388 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_390 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_390 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_392 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_392 ∷ T_IsMedialMagma_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemimedialMagma_396 ∷ p → p → p → p → p → () Source #

data T_IsSemimedialMagma_396 Source #

d_isMagma_404 ∷ T_IsSemimedialMagma_396 → T_IsMagma_176 Source #

d_semiMedial_406 ∷ T_IsSemimedialMagma_396 → T_Σ_14 Source #

d_isEquivalence_410 ∷ T_IsSemimedialMagma_396 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_412 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_412 ∷ T_IsSemimedialMagma_396 → T_IsPartialEquivalence_16 Source #

d_refl_414 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny Source #

d_reflexive_416 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_416 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_418 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → T_Setoid_44 Source #

du_setoid_418 ∷ T_IsSemimedialMagma_396 → T_Setoid_44 Source #

d_sym_420 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_422 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_424 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_426 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_426 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_428 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_428 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semimedial'737'_430 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_semimedial'737'_430 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semimedial'691'_432 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_semimedial'691'_432 ∷ T_IsSemimedialMagma_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSelectiveMagma_436 ∷ p → p → p → p → p → () Source #

data T_IsSelectiveMagma_436 Source #

d_isMagma_444 ∷ T_IsSelectiveMagma_436 → T_IsMagma_176 Source #

d_sel_446 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_isEquivalence_450 ∷ T_IsSelectiveMagma_436 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_452 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_452 ∷ T_IsSelectiveMagma_436 → T_IsPartialEquivalence_16 Source #

d_refl_454 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny Source #

d_reflexive_456 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_456 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_458 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Setoid_44 Source #

du_setoid_458 ∷ T_IsSelectiveMagma_436 → T_Setoid_44 Source #

d_sym_460 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_462 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_464 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_466 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_466 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_468 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_468 ∷ T_IsSelectiveMagma_436 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemigroup_472 ∷ p → p → p → p → p → () Source #

data T_IsSemigroup_472 Source #

d_isMagma_480 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_assoc_482 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_486 ∷ T_IsSemigroup_472 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_488 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_488 ∷ T_IsSemigroup_472 → T_IsPartialEquivalence_16 Source #

d_refl_490 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny Source #

d_reflexive_492 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_492 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_494 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → T_Setoid_44 Source #

du_setoid_494 ∷ T_IsSemigroup_472 → T_Setoid_44 Source #

d_sym_496 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_498 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_500 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_502 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_502 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_504 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_504 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBand_508 ∷ p → p → p → p → p → () Source #

data T_IsBand_508 Source #

d_isSemigroup_516 ∷ T_IsBand_508 → T_IsSemigroup_472 Source #

d_idem_518 ∷ T_IsBand_508 → AgdaAny → AgdaAny Source #

d_assoc_522 ∷ T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_524 ∷ T_IsBand_508 → T_IsEquivalence_26 Source #

d_isMagma_526 ∷ T_IsBand_508 → T_IsMagma_176 Source #

d_isPartialEquivalence_528 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_528 ∷ T_IsBand_508 → T_IsPartialEquivalence_16 Source #

d_refl_530 ∷ T_IsBand_508 → AgdaAny → AgdaAny Source #

d_reflexive_532 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_532 ∷ T_IsBand_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_534 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_Setoid_44 Source #

du_setoid_534 ∷ T_IsBand_508 → T_Setoid_44 Source #

d_sym_536 ∷ T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_538 ∷ T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'691'_542 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'737'_544 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_IsCommutativeSemigroup_548 ∷ p → p → p → p → p → () Source #

data T_IsCommutativeSemigroup_548 Source #

d_isSemigroup_556 ∷ T_IsCommutativeSemigroup_548 → T_IsSemigroup_472 Source #

d_comm_558 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_562 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_564 ∷ T_IsCommutativeSemigroup_548 → T_IsEquivalence_26 Source #

d_isMagma_566 ∷ T_IsCommutativeSemigroup_548 → T_IsMagma_176 Source #

d_isPartialEquivalence_568 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_548 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_568 ∷ T_IsCommutativeSemigroup_548 → T_IsPartialEquivalence_16 Source #

d_refl_570 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny Source #

d_reflexive_572 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_572 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_574 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_548 → T_Setoid_44 Source #

du_setoid_574 ∷ T_IsCommutativeSemigroup_548 → T_Setoid_44 Source #

d_sym_576 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_578 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_580 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_582 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_582 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_584 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_584 ∷ T_IsCommutativeSemigroup_548 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_586 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_548 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_586 ∷ T_IsCommutativeSemigroup_548 → T_IsCommutativeMagma_212 Source #

d_IsCommutativeBand_590 ∷ p → p → p → p → p → () Source #

data T_IsCommutativeBand_590 Source #

d_isBand_598 ∷ T_IsCommutativeBand_590 → T_IsBand_508 Source #

d_comm_600 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_604 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_606 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_isEquivalence_608 ∷ T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

d_isMagma_610 ∷ T_IsCommutativeBand_590 → T_IsMagma_176 Source #

d_isPartialEquivalence_612 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_612 ∷ T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_614 ∷ T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

d_refl_616 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_reflexive_618 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_618 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_620 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_Setoid_44 Source #

du_setoid_620 ∷ T_IsCommutativeBand_590 → T_Setoid_44 Source #

d_sym_622 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_624 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_626 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_628 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_628 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_630 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_630 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeSemigroup_632 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_632 ∷ T_IsCommutativeBand_590 → T_IsCommutativeSemigroup_548 Source #

d_isCommutativeMagma_636 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_636 ∷ T_IsCommutativeBand_590 → T_IsCommutativeMagma_212 Source #

d_IsUnitalMagma_642 ∷ p → p → p → p → p → p → () Source #

data T_IsUnitalMagma_642 Source #

d_isMagma_652 ∷ T_IsUnitalMagma_642 → T_IsMagma_176 Source #

d_identity_654 ∷ T_IsUnitalMagma_642 → T_Σ_14 Source #

d_isEquivalence_658 ∷ T_IsUnitalMagma_642 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_660 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_660 ∷ T_IsUnitalMagma_642 → T_IsPartialEquivalence_16 Source #

d_refl_662 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny Source #

d_reflexive_664 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_664 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_666 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → T_Setoid_44 Source #

du_setoid_666 ∷ T_IsUnitalMagma_642 → T_Setoid_44 Source #

d_sym_668 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_670 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_672 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_674 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_674 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_676 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_676 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'737'_678 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → AgdaAny → AgdaAny Source #

du_identity'737'_678 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny Source #

d_identity'691'_680 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsUnitalMagma_642 → AgdaAny → AgdaAny Source #

du_identity'691'_680 ∷ T_IsUnitalMagma_642 → AgdaAny → AgdaAny Source #

d_IsMonoid_686 ∷ p → p → p → p → p → p → () Source #

data T_IsMonoid_686 Source #

d_isSemigroup_696 ∷ T_IsMonoid_686 → T_IsSemigroup_472 Source #

d_identity_698 ∷ T_IsMonoid_686 → T_Σ_14 Source #

d_assoc_702 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_704 ∷ T_IsMonoid_686 → T_IsEquivalence_26 Source #

d_isMagma_706 ∷ T_IsMonoid_686 → T_IsMagma_176 Source #

d_isPartialEquivalence_708 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_708 ∷ T_IsMonoid_686 → T_IsPartialEquivalence_16 Source #

d_refl_710 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny Source #

d_reflexive_712 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_712 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_714 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_Setoid_44 Source #

du_setoid_714 ∷ T_IsMonoid_686 → T_Setoid_44 Source #

d_sym_716 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_718 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_720 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_722 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_722 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_724 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_724 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'737'_726 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny Source #

du_identity'737'_726 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny Source #

d_identity'691'_728 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny Source #

du_identity'691'_728 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny Source #

d_isUnitalMagma_730 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_730 ∷ T_IsMonoid_686 → T_IsUnitalMagma_642 Source #

d_IsCommutativeMonoid_736 ∷ p → p → p → p → p → p → () Source #

data T_IsCommutativeMonoid_736 Source #

d_isMonoid_746 ∷ T_IsCommutativeMonoid_736 → T_IsMonoid_686 Source #

d_comm_748 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_752 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_754 ∷ T_IsCommutativeMonoid_736 → T_Σ_14 Source #

d_identity'691'_756 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny Source #

du_identity'691'_756 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny Source #

d_identity'737'_758 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny Source #

du_identity'737'_758 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny Source #

d_isEquivalence_760 ∷ T_IsCommutativeMonoid_736 → T_IsEquivalence_26 Source #

d_isMagma_762 ∷ T_IsCommutativeMonoid_736 → T_IsMagma_176 Source #

d_isPartialEquivalence_764 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_764 ∷ T_IsCommutativeMonoid_736 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_766 ∷ T_IsCommutativeMonoid_736 → T_IsSemigroup_472 Source #

d_isUnitalMagma_768 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_768 ∷ T_IsCommutativeMonoid_736 → T_IsUnitalMagma_642 Source #

d_refl_770 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny Source #

d_reflexive_772 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_772 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_774 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → T_Setoid_44 Source #

du_setoid_774 ∷ T_IsCommutativeMonoid_736 → T_Setoid_44 Source #

d_sym_776 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_778 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_780 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_782 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_782 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_784 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_784 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeSemigroup_786 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_786 ∷ T_IsCommutativeMonoid_736 → T_IsCommutativeSemigroup_548 Source #

d_isCommutativeMagma_790 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_736 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_790 ∷ T_IsCommutativeMonoid_736 → T_IsCommutativeMagma_212 Source #

d_IsIdempotentMonoid_796 ∷ p → p → p → p → p → p → () Source #

data T_IsIdempotentMonoid_796 Source #

d_isMonoid_806 ∷ T_IsIdempotentMonoid_796 → T_IsMonoid_686 Source #

d_idem_808 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny Source #

d_assoc_812 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_814 ∷ T_IsIdempotentMonoid_796 → T_Σ_14 Source #

d_identity'691'_816 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny Source #

du_identity'691'_816 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny Source #

d_identity'737'_818 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny Source #

du_identity'737'_818 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny Source #

d_isEquivalence_820 ∷ T_IsIdempotentMonoid_796 → T_IsEquivalence_26 Source #

d_isMagma_822 ∷ T_IsIdempotentMonoid_796 → T_IsMagma_176 Source #

d_isPartialEquivalence_824 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_824 ∷ T_IsIdempotentMonoid_796 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_826 ∷ T_IsIdempotentMonoid_796 → T_IsSemigroup_472 Source #

d_isUnitalMagma_828 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_828 ∷ T_IsIdempotentMonoid_796 → T_IsUnitalMagma_642 Source #

d_refl_830 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny Source #

d_reflexive_832 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_832 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_834 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → T_Setoid_44 Source #

du_setoid_834 ∷ T_IsIdempotentMonoid_796 → T_Setoid_44 Source #

d_sym_836 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_838 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_840 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_842 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_842 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_844 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_844 ∷ T_IsIdempotentMonoid_796 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_846 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentMonoid_796 → T_IsBand_508 Source #

du_isBand_846 ∷ T_IsIdempotentMonoid_796 → T_IsBand_508 Source #

d_IsIdempotentCommutativeMonoid_852 ∷ p → p → p → p → p → p → () Source #

data T_IsIdempotentCommutativeMonoid_852 Source #

d_isCommutativeMonoid_862 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMonoid_736 Source #

d_idem_864 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_assoc_868 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_870 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_872 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Σ_14 Source #

d_identity'691'_874 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

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

d_identity'737'_876 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

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

d_isCommutativeMagma_878 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_878 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMagma_212 Source #

d_isCommutativeSemigroup_880 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_880 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_882 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsEquivalence_26 Source #

d_isMagma_884 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsMagma_176 Source #

d_isMonoid_886 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsMonoid_686 Source #

d_isPartialEquivalence_888 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_888 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_890 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsSemigroup_472 Source #

d_isUnitalMagma_892 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_892 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsUnitalMagma_642 Source #

d_refl_894 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_reflexive_896 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_896 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_898 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

du_setoid_898 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

d_sym_900 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_902 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_904 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_906 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_906 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_908 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_908 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isIdempotentMonoid_910 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsIdempotentMonoid_796 Source #

du_isIdempotentMonoid_910 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsIdempotentMonoid_796 Source #

d_isBand_914 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

du_isBand_914 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

d_isCommutativeBand_916 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_916 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

d_IsInvertibleMagma_924 ∷ p → p → p → p → p → p → p → () Source #

data T_IsInvertibleMagma_924 Source #

d_isMagma_938 ∷ T_IsInvertibleMagma_924 → T_IsMagma_176 Source #

d_inverse_940 ∷ T_IsInvertibleMagma_924 → T_Σ_14 Source #

d_'8315''185''45'cong_942 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_946 ∷ T_IsInvertibleMagma_924 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_948 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_948 ∷ T_IsInvertibleMagma_924 → T_IsPartialEquivalence_16 Source #

d_refl_950 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny Source #

d_reflexive_952 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_952 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_954 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → T_Setoid_44 Source #

du_setoid_954 ∷ T_IsInvertibleMagma_924 → T_Setoid_44 Source #

d_sym_956 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_958 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_960 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_962 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_962 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_964 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_964 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_966 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → AgdaAny → AgdaAny Source #

du_inverse'737'_966 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny Source #

d_inverse'691'_968 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleMagma_924 → AgdaAny → AgdaAny Source #

du_inverse'691'_968 ∷ T_IsInvertibleMagma_924 → AgdaAny → AgdaAny Source #

d_IsInvertibleUnitalMagma_976 ∷ p → p → p → p → p → p → p → () Source #

data T_IsInvertibleUnitalMagma_976 Source #

d_isInvertibleMagma_988 ∷ T_IsInvertibleUnitalMagma_976 → T_IsInvertibleMagma_924 Source #

d_identity_990 ∷ T_IsInvertibleUnitalMagma_976 → T_Σ_14 Source #

d_inverse_994 ∷ T_IsInvertibleUnitalMagma_976 → T_Σ_14 Source #

d_inverse'691'_996 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

du_inverse'691'_996 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

d_inverse'737'_998 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

du_inverse'737'_998 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

d_isEquivalence_1000 ∷ T_IsInvertibleUnitalMagma_976 → T_IsEquivalence_26 Source #

d_isMagma_1002 ∷ T_IsInvertibleUnitalMagma_976 → T_IsMagma_176 Source #

d_isPartialEquivalence_1004 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1004 ∷ T_IsInvertibleUnitalMagma_976 → T_IsPartialEquivalence_16 Source #

d_refl_1006 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

d_reflexive_1008 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1008 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1010 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → T_Setoid_44 Source #

du_setoid_1010 ∷ T_IsInvertibleUnitalMagma_976 → T_Setoid_44 Source #

d_sym_1012 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1014 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1016 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1018 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1020 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1020 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1022 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1022 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'737'_1024 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

du_identity'737'_1024 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

d_identity'691'_1026 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

du_identity'691'_1026 ∷ T_IsInvertibleUnitalMagma_976 → AgdaAny → AgdaAny Source #

d_isUnitalMagma_1028 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsInvertibleUnitalMagma_976 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1028 ∷ T_IsInvertibleUnitalMagma_976 → T_IsUnitalMagma_642 Source #

d_IsGroup_1036 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroup_1036 Source #

d_isMonoid_1050 ∷ T_IsGroup_1036 → T_IsMonoid_686 Source #

d_inverse_1052 ∷ T_IsGroup_1036 → T_Σ_14 Source #

d_'8315''185''45'cong_1054 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1058 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1060 ∷ T_IsGroup_1036 → T_Σ_14 Source #

d_identity'691'_1062 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny Source #

du_identity'691'_1062 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny Source #

d_identity'737'_1064 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny Source #

du_identity'737'_1064 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny Source #

d_isEquivalence_1066 ∷ T_IsGroup_1036 → T_IsEquivalence_26 Source #

d_isMagma_1068 ∷ T_IsGroup_1036 → T_IsMagma_176 Source #

d_isPartialEquivalence_1070 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1070 ∷ T_IsGroup_1036 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1072 ∷ T_IsGroup_1036 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1074 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1074 ∷ T_IsGroup_1036 → T_IsUnitalMagma_642 Source #

d_refl_1076 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny Source #

d_reflexive_1078 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1078 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1080 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → T_Setoid_44 Source #

du_setoid_1080 ∷ T_IsGroup_1036 → T_Setoid_44 Source #

d_sym_1082 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1084 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1086 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1088 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1088 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1090 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1090 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'92''92'__1092 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny Source #

du__'92''92'__1092 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d__'47''47'__1098 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__1098 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d__'45'__1104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny Source #

du__'45'__1104 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny Source #

du_inverse'737'_1106 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny Source #

d_inverse'691'_1108 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny Source #

du_inverse'691'_1108 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1114 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1120 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1120 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isInvertibleMagma_1122 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → T_IsInvertibleMagma_924 Source #

du_isInvertibleMagma_1122 ∷ T_IsGroup_1036 → T_IsInvertibleMagma_924 Source #

d_isInvertibleUnitalMagma_1124 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1036 → T_IsInvertibleUnitalMagma_976 Source #

du_isInvertibleUnitalMagma_1124 ∷ T_IsGroup_1036 → T_IsInvertibleUnitalMagma_976 Source #

d_IsAbelianGroup_1132 ∷ p → p → p → p → p → p → p → () Source #

data T_IsAbelianGroup_1132 Source #

d_isGroup_1144 ∷ T_IsAbelianGroup_1132 → T_IsGroup_1036 Source #

d_comm_1146 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny Source #

d__'47''47'__1150 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__1150 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1152 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1154 ∷ T_IsAbelianGroup_1132 → T_Σ_14 Source #

d_identity'691'_1156 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

du_identity'691'_1156 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

d_identity'737'_1158 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

du_identity'737'_1158 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

d_inverse_1160 ∷ T_IsAbelianGroup_1132 → T_Σ_14 Source #

d_inverse'691'_1162 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

du_inverse'691'_1162 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

d_inverse'737'_1164 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

du_inverse'737'_1164 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

d_isEquivalence_1166 ∷ T_IsAbelianGroup_1132 → T_IsEquivalence_26 Source #

d_isInvertibleMagma_1168 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsInvertibleMagma_924 Source #

du_isInvertibleMagma_1168 ∷ T_IsAbelianGroup_1132 → T_IsInvertibleMagma_924 Source #

d_isInvertibleUnitalMagma_1170 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsInvertibleUnitalMagma_976 Source #

du_isInvertibleUnitalMagma_1170 ∷ T_IsAbelianGroup_1132 → T_IsInvertibleUnitalMagma_976 Source #

d_isMagma_1172 ∷ T_IsAbelianGroup_1132 → T_IsMagma_176 Source #

d_isMonoid_1174 ∷ T_IsAbelianGroup_1132 → T_IsMonoid_686 Source #

d_isPartialEquivalence_1176 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1176 ∷ T_IsAbelianGroup_1132 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1178 ∷ T_IsAbelianGroup_1132 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1180 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1180 ∷ T_IsAbelianGroup_1132 → T_IsUnitalMagma_642 Source #

d_refl_1182 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #

d_reflexive_1184 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1184 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1186 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_Setoid_44 Source #

du_setoid_1186 ∷ T_IsAbelianGroup_1132 → T_Setoid_44 Source #

d_sym_1188 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1190 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1192 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1192 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1194 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1194 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_1196 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1198 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1200 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1200 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1202 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1202 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMonoid_1204 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeMonoid_736 Source #

du_isCommutativeMonoid_1204 ∷ T_IsAbelianGroup_1132 → T_IsCommutativeMonoid_736 Source #

d_isCommutativeMagma_1208 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_1208 ∷ T_IsAbelianGroup_1132 → T_IsCommutativeMagma_212 Source #

d_isCommutativeSemigroup_1210 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_1210 ∷ T_IsAbelianGroup_1132 → T_IsCommutativeSemigroup_548 Source #

d_IsNearSemiring_1218 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiring_1218 Source #

d_'43''45'isMonoid_1236 ∷ T_IsNearSemiring_1218 → T_IsMonoid_686 Source #

d_'42''45'cong_1238 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'assoc_1240 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'691'_1242 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_1244 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny Source #

d_assoc_1248 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1250 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1252 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1252 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1254 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1254 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1256 ∷ T_IsNearSemiring_1218 → T_Σ_14 Source #

d_identity'691'_1258 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny Source #

du_identity'691'_1258 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny Source #

d_identity'737'_1260 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny Source #

du_identity'737'_1260 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny Source #

d_isMagma_1262 ∷ T_IsNearSemiring_1218 → T_IsMagma_176 Source #

d_isSemigroup_1264 ∷ T_IsNearSemiring_1218 → T_IsSemigroup_472 Source #

d_isUnitalMagma_1266 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1266 ∷ T_IsNearSemiring_1218 → T_IsUnitalMagma_642 Source #

d_isEquivalence_1268 ∷ T_IsNearSemiring_1218 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1270 ∷ T_IsNearSemiring_1218 → T_IsPartialEquivalence_16 Source #

d_refl_1272 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny Source #

d_reflexive_1274 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1274 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1276 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → T_Setoid_44 Source #

du_setoid_1276 ∷ T_IsNearSemiring_1218 → T_Setoid_44 Source #

d_sym_1278 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1280 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagma_1282 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → T_IsMagma_176 Source #

du_'42''45'isMagma_1282 ∷ T_IsNearSemiring_1218 → T_IsMagma_176 Source #

d_'42''45'isSemigroup_1284 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → T_IsSemigroup_472 Source #

du_'42''45'isSemigroup_1284 ∷ T_IsNearSemiring_1218 → T_IsSemigroup_472 Source #

d_'8729''45'cong'691'_1288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1288 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1290 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemiringWithoutOne_1298 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringWithoutOne_1298 Source #

d_'43''45'isCommutativeMonoid_1316 ∷ T_IsSemiringWithoutOne_1298 → T_IsCommutativeMonoid_736 Source #

d_'42''45'cong_1318 ∷ T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'assoc_1320 ∷ T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib_1322 ∷ T_IsSemiringWithoutOne_1298 → T_Σ_14 Source #

d_zero_1324 ∷ T_IsSemiringWithoutOne_1298 → T_Σ_14 Source #

d_comm_1328 ∷ T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1330 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_1330 ∷ T_IsSemiringWithoutOne_1298 → T_IsCommutativeMagma_212 Source #

d_isCommutativeSemigroup_1332 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_1332 ∷ T_IsSemiringWithoutOne_1298 → T_IsCommutativeSemigroup_548 Source #

d_isMonoid_1334 ∷ T_IsSemiringWithoutOne_1298 → T_IsMonoid_686 Source #

d_setoid_1336 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → T_Setoid_44 Source #

du_setoid_1336 ∷ T_IsSemiringWithoutOne_1298 → T_Setoid_44 Source #

d__'8776'__1340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → () Source #

d__'8777'__1342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → () Source #

d_Carrier_1344 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → () Source #

d_isEquivalence_1346 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_1298 → T_IsEquivalence_26 Source #