Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Structures

Documentation

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

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_Absorptive_24 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_IsMagma_86 ∷ p → p → p → p → p → () Source #

data T_IsMagma_86 Source #

Constructors

C_IsMagma'46'constructor_553 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isEquivalence_94 ∷ T_IsMagma_86 → T_IsEquivalence_26 Source #

d_'8729''45'cong_96 ∷ T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_100 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_100 ∷ T_IsMagma_86 → T_IsPartialEquivalence_16 Source #

d_refl_102 ∷ T_IsMagma_86 → AgdaAny → AgdaAny Source #

d_reflexive_104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_sym_106 ∷ T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_108 ∷ T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_110 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → T_Setoid_44 Source #

du_setoid_110 ∷ T_IsMagma_86 → T_Setoid_44 Source #

d_'8729''45'cong'737'_112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_112 ∷ T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_116 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_116 ∷ T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsCommutativeMagma_122 ∷ p → p → p → p → p → () Source #

data T_IsCommutativeMagma_122 Source #

Constructors

C_IsCommutativeMagma'46'constructor_2433 T_IsMagma_86 (AgdaAny → AgdaAny → AgdaAny)

d_isMagma_130 ∷ T_IsCommutativeMagma_122 → T_IsMagma_86 Source #

d_comm_132 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_136 ∷ T_IsCommutativeMagma_122 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_138 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_138 ∷ T_IsCommutativeMagma_122 → T_IsPartialEquivalence_16 Source #

d_refl_140 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny Source #

d_reflexive_142 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_142 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_144 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → T_Setoid_44 Source #

du_setoid_144 ∷ T_IsCommutativeMagma_122 → T_Setoid_44 Source #

d_sym_146 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_148 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_150 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_152 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_152 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_154 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_154 ∷ T_IsCommutativeMagma_122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSelectiveMagma_158 ∷ p → p → p → p → p → () Source #

data T_IsSelectiveMagma_158 Source #

Constructors

C_IsSelectiveMagma'46'constructor_3217 T_IsMagma_86 (AgdaAny → AgdaAny → T__'8846'__30)

d_isMagma_166 ∷ T_IsSelectiveMagma_158 → T_IsMagma_86 Source #

d_sel_168 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_isEquivalence_172 ∷ T_IsSelectiveMagma_158 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_174 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_174 ∷ T_IsSelectiveMagma_158 → T_IsPartialEquivalence_16 Source #

d_refl_176 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny Source #

d_reflexive_178 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_178 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_180 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Setoid_44 Source #

du_setoid_180 ∷ T_IsSelectiveMagma_158 → T_Setoid_44 Source #

d_sym_182 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_184 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'691'_188 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_188 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_190 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_190 ∷ T_IsSelectiveMagma_158 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemigroup_194 ∷ p → p → p → p → p → () Source #

data T_IsSemigroup_194 Source #

Constructors

C_IsSemigroup'46'constructor_4001 T_IsMagma_86 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isMagma_202 ∷ T_IsSemigroup_194 → T_IsMagma_86 Source #

d_assoc_204 ∷ T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_208 ∷ T_IsSemigroup_194 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_210 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_210 ∷ T_IsSemigroup_194 → T_IsPartialEquivalence_16 Source #

d_refl_212 ∷ T_IsSemigroup_194 → AgdaAny → AgdaAny Source #

d_reflexive_214 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_216 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → T_Setoid_44 Source #

du_setoid_216 ∷ T_IsSemigroup_194 → T_Setoid_44 Source #

d_sym_218 ∷ T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_220 ∷ T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'691'_224 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'737'_226 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_IsBand_230 ∷ p → p → p → p → p → () Source #

data T_IsBand_230 Source #

Constructors

C_IsBand'46'constructor_4787 T_IsSemigroup_194 (AgdaAny → AgdaAny)

d_isSemigroup_238 ∷ T_IsBand_230 → T_IsSemigroup_194 Source #

d_idem_240 ∷ T_IsBand_230 → AgdaAny → AgdaAny Source #

d_assoc_244 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_246 ∷ T_IsBand_230 → T_IsEquivalence_26 Source #

d_isMagma_248 ∷ T_IsBand_230 → T_IsMagma_86 Source #

d_isPartialEquivalence_250 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_250 ∷ T_IsBand_230 → T_IsPartialEquivalence_16 Source #

d_refl_252 ∷ T_IsBand_230 → AgdaAny → AgdaAny Source #

d_reflexive_254 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_254 ∷ T_IsBand_230 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_256 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_Setoid_44 Source #

du_setoid_256 ∷ T_IsBand_230 → T_Setoid_44 Source #

d_sym_258 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_260 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_262 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_264 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_266 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_266 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsCommutativeSemigroup_270 ∷ p → p → p → p → p → () Source #

data T_IsCommutativeSemigroup_270 Source #

Constructors

C_IsCommutativeSemigroup'46'constructor_5673 T_IsSemigroup_194 (AgdaAny → AgdaAny → AgdaAny)

d_isSemigroup_278 ∷ T_IsCommutativeSemigroup_270 → T_IsSemigroup_194 Source #

d_comm_280 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_284 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_286 ∷ T_IsCommutativeSemigroup_270 → T_IsEquivalence_26 Source #

d_isMagma_288 ∷ T_IsCommutativeSemigroup_270 → T_IsMagma_86 Source #

d_isPartialEquivalence_290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_290 ∷ T_IsCommutativeSemigroup_270 → T_IsPartialEquivalence_16 Source #

d_refl_292 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny Source #

d_reflexive_294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_294 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → T_Setoid_44 Source #

du_setoid_296 ∷ T_IsCommutativeSemigroup_270 → T_Setoid_44 Source #

d_sym_298 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_300 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_302 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_304 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_304 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_306 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_306 ∷ T_IsCommutativeSemigroup_270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_308 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_308 ∷ T_IsCommutativeSemigroup_270 → T_IsCommutativeMagma_122 Source #

d_IsSemilattice_312 ∷ p → p → p → p → p → () Source #

data T_IsSemilattice_312 Source #

Constructors

C_IsSemilattice'46'constructor_6687 T_IsBand_230 (AgdaAny → AgdaAny → AgdaAny)

d_isBand_320 ∷ T_IsSemilattice_312 → T_IsBand_230 Source #

d_comm_322 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_326 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_328 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny Source #

d_isEquivalence_330 ∷ T_IsSemilattice_312 → T_IsEquivalence_26 Source #

d_isMagma_332 ∷ T_IsSemilattice_312 → T_IsMagma_86 Source #

d_isPartialEquivalence_334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_334 ∷ T_IsSemilattice_312 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_336 ∷ T_IsSemilattice_312 → T_IsSemigroup_194 Source #

d_refl_338 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny Source #

d_reflexive_340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_340 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_Setoid_44 Source #

du_setoid_342 ∷ T_IsSemilattice_312 → T_Setoid_44 Source #

d_sym_344 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_346 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_348 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_350 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_352 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_352 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoid_358 ∷ p → p → p → p → p → p → () Source #

data T_IsMonoid_358 Source #

Constructors

C_IsMonoid'46'constructor_7687 T_IsSemigroup_194 T_Σ_14

d_isSemigroup_368 ∷ T_IsMonoid_358 → T_IsSemigroup_194 Source #

d_identity_370 ∷ T_IsMonoid_358 → T_Σ_14 Source #

d_assoc_374 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_376 ∷ T_IsMonoid_358 → T_IsEquivalence_26 Source #

d_isMagma_378 ∷ T_IsMonoid_358 → T_IsMagma_86 Source #

d_isPartialEquivalence_380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_380 ∷ T_IsMonoid_358 → T_IsPartialEquivalence_16 Source #

d_refl_382 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny Source #

d_reflexive_384 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_384 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_386 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → T_Setoid_44 Source #

du_setoid_386 ∷ T_IsMonoid_358 → T_Setoid_44 Source #

d_sym_388 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_390 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_392 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_394 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_394 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_396 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'737'_398 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → AgdaAny → AgdaAny Source #

du_identity'737'_398 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny Source #

d_identity'691'_400 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → AgdaAny → AgdaAny Source #

du_identity'691'_400 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny Source #

d_IsCommutativeMonoid_406 ∷ p → p → p → p → p → p → () Source #

data T_IsCommutativeMonoid_406 Source #

Constructors

C_IsCommutativeMonoid'46'constructor_9361 T_IsMonoid_358 (AgdaAny → AgdaAny → AgdaAny)

d_isMonoid_416 ∷ T_IsCommutativeMonoid_406 → T_IsMonoid_358 Source #

d_comm_418 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_422 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_424 ∷ T_IsCommutativeMonoid_406 → T_Σ_14 Source #

d_identity'691'_426 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny Source #

du_identity'691'_426 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny Source #

d_identity'737'_428 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny Source #

du_identity'737'_428 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny Source #

d_isEquivalence_430 ∷ T_IsCommutativeMonoid_406 → T_IsEquivalence_26 Source #

d_isMagma_432 ∷ T_IsCommutativeMonoid_406 → T_IsMagma_86 Source #

d_isPartialEquivalence_434 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_434 ∷ T_IsCommutativeMonoid_406 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_436 ∷ T_IsCommutativeMonoid_406 → T_IsSemigroup_194 Source #

d_refl_438 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny Source #

d_reflexive_440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_440 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_442 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_Setoid_44 Source #

du_setoid_442 ∷ T_IsCommutativeMonoid_406 → T_Setoid_44 Source #

d_sym_444 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_446 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_448 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_450 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_450 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_452 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_452 ∷ T_IsCommutativeMonoid_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeSemigroup_454 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_454 ∷ T_IsCommutativeMonoid_406 → T_IsCommutativeSemigroup_270 Source #

d_isCommutativeMagma_458 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_458 ∷ T_IsCommutativeMonoid_406 → T_IsCommutativeMagma_122 Source #

d_IsIdempotentCommutativeMonoid_464 ∷ p → p → p → p → p → p → () Source #

data T_IsIdempotentCommutativeMonoid_464 Source #

Constructors

C_IsIdempotentCommutativeMonoid'46'constructor_10859 T_IsCommutativeMonoid_406 (AgdaAny → AgdaAny)

d_isCommutativeMonoid_474 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_idem_476 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

d_assoc_480 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_482 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_484 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_identity'691'_486 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

du_identity'691'_486 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

d_identity'737'_488 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

du_identity'737'_488 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_490 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_490 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMagma_122 Source #

d_isCommutativeSemigroup_492 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_492 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeSemigroup_270 Source #

d_isEquivalence_494 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_496 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_498 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isPartialEquivalence_500 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_500 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_502 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

d_refl_504 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

d_reflexive_506 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_508 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_Setoid_44 Source #

du_setoid_508 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Setoid_44 Source #

d_sym_510 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_512 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_514 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_516 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_516 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_518 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_530 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_532 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_534 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

d_identity_536 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_identity'691'_538 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

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

d_identity'737'_540 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

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

d_isCommutativeMagma_542 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_542 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMagma_122 Source #

d_isCommutativeMonoid_544 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_546 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_546 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeSemigroup_270 Source #

d_isEquivalence_548 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_550 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_552 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isPartialEquivalence_554 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_554 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_556 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

d_refl_558 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny Source #

d_reflexive_560 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_560 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_562 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → T_Setoid_44 Source #

du_setoid_562 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Setoid_44 Source #

d_sym_564 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_566 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_568 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_570 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_570 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_572 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_572 ∷ T_IsIdempotentCommutativeMonoid_464 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGroup_580 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroup_580 Source #

Constructors

C_IsGroup'46'constructor_12945 T_IsMonoid_358 T_Σ_14 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isMonoid_594 ∷ T_IsGroup_580 → T_IsMonoid_358 Source #

d_inverse_596 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_'8315''185''45'cong_598 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_602 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_604 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_identity'691'_606 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny Source #

du_identity'691'_606 ∷ T_IsGroup_580 → AgdaAny → AgdaAny Source #

d_identity'737'_608 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny Source #

du_identity'737'_608 ∷ T_IsGroup_580 → AgdaAny → AgdaAny Source #

d_isEquivalence_610 ∷ T_IsGroup_580 → T_IsEquivalence_26 Source #

d_isMagma_612 ∷ T_IsGroup_580 → T_IsMagma_86 Source #

d_isPartialEquivalence_614 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_614 ∷ T_IsGroup_580 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_616 ∷ T_IsGroup_580 → T_IsSemigroup_194 Source #

d_refl_618 ∷ T_IsGroup_580 → AgdaAny → AgdaAny Source #

d_reflexive_620 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_620 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_622 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → T_Setoid_44 Source #

du_setoid_622 ∷ T_IsGroup_580 → T_Setoid_44 Source #

d_sym_624 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_626 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_628 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_630 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_630 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_632 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_632 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'45'__634 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny Source #

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

d_inverse'737'_640 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny Source #

du_inverse'737'_640 ∷ T_IsGroup_580 → AgdaAny → AgdaAny Source #

d_inverse'691'_642 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny Source #

du_inverse'691'_642 ∷ T_IsGroup_580 → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_648 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_648 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_654 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_654 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsAbelianGroup_662 ∷ p → p → p → p → p → p → p → () Source #

data T_IsAbelianGroup_662 Source #

Constructors

C_IsAbelianGroup'46'constructor_17421 T_IsGroup_580 (AgdaAny → AgdaAny → AgdaAny)

d_isGroup_674 ∷ T_IsAbelianGroup_662 → T_IsGroup_580 Source #

d_comm_676 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny Source #

d__'45'__680 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_682 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_684 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_identity'691'_686 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

du_identity'691'_686 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

d_identity'737'_688 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

du_identity'737'_688 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

d_inverse_690 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_inverse'691'_692 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

du_inverse'691'_692 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

d_inverse'737'_694 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

du_inverse'737'_694 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

d_isEquivalence_696 ∷ T_IsAbelianGroup_662 → T_IsEquivalence_26 Source #

d_isMagma_698 ∷ T_IsAbelianGroup_662 → T_IsMagma_86 Source #

d_isMonoid_700 ∷ T_IsAbelianGroup_662 → T_IsMonoid_358 Source #

d_isPartialEquivalence_702 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_702 ∷ T_IsAbelianGroup_662 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_704 ∷ T_IsAbelianGroup_662 → T_IsSemigroup_194 Source #

d_refl_706 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny Source #

d_reflexive_708 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_708 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_710 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_Setoid_44 Source #

du_setoid_710 ∷ T_IsAbelianGroup_662 → T_Setoid_44 Source #

d_sym_712 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_714 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_716 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_716 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_718 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_718 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_720 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_722 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_724 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_724 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_726 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_726 ∷ T_IsAbelianGroup_662 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMonoid_728 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_IsCommutativeMonoid_406 Source #

du_isCommutativeMonoid_728 ∷ T_IsAbelianGroup_662 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeMagma_732 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_732 ∷ T_IsAbelianGroup_662 → T_IsCommutativeMagma_122 Source #

d_isCommutativeSemigroup_734 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_734 ∷ T_IsAbelianGroup_662 → T_IsCommutativeSemigroup_270 Source #

d_IsLattice_740 ∷ p → p → p → p → p → p → () Source #

data T_IsLattice_740 Source #

Constructors

C_IsLattice'46'constructor_20027 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) T_Σ_14

d_isEquivalence_762 ∷ T_IsLattice_740 → T_IsEquivalence_26 Source #

d_'8744''45'comm_764 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_766 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_768 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_770 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_772 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_774 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_776 ∷ T_IsLattice_740 → T_Σ_14 Source #

d_isPartialEquivalence_780 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_780 ∷ T_IsLattice_740 → T_IsPartialEquivalence_16 Source #

d_refl_782 ∷ T_IsLattice_740 → AgdaAny → AgdaAny Source #

d_reflexive_784 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_784 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_786 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_788 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_790 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_790 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_792 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_792 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_794 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_794 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_798 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_798 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_802 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_802 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_806 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_806 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_814 ∷ p → p → p → p → p → p → () Source #

data T_IsDistributiveLattice_814 Source #

Constructors

C_IsDistributiveLattice'46'constructor_24097 T_IsLattice_740 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isLattice_824 ∷ T_IsDistributiveLattice_814 → T_IsLattice_740 Source #

d_'8744''45'distrib'691''45''8743'_826 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_830 ∷ T_IsDistributiveLattice_814 → T_Σ_14 Source #

d_isEquivalence_832 ∷ T_IsDistributiveLattice_814 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_834 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_834 ∷ T_IsDistributiveLattice_814 → T_IsPartialEquivalence_16 Source #

d_refl_836 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny Source #

d_reflexive_838 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_838 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_840 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_842 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_844 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_844 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_846 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_848 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_850 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_852 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_852 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_854 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_854 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_856 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_856 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_858 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_860 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_862 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_864 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_864 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_866 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_866 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45''8743''45'distrib'691'_868 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45''8743''45'distrib'691'_868 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsNearSemiring_876 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiring_876 Source #

Constructors

C_IsNearSemiring'46'constructor_25785 T_IsMonoid_358 T_IsSemigroup_194 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

d_'43''45'isMonoid_892 ∷ T_IsNearSemiring_876 → T_IsMonoid_358 Source #

d_'42''45'isSemigroup_894 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

d_distrib'691'_896 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_898 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny Source #

d_assoc_902 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_904 ∷ T_IsNearSemiring_876 → 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 → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

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

d_identity_910 ∷ T_IsNearSemiring_876 → T_Σ_14 Source #

d_identity'691'_912 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → AgdaAny → AgdaAny Source #

du_identity'691'_912 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny Source #

d_identity'737'_914 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → AgdaAny → AgdaAny Source #

du_identity'737'_914 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny Source #

d_isMagma_916 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

d_isSemigroup_918 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

d_isEquivalence_920 ∷ T_IsNearSemiring_876 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_922 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_922 ∷ T_IsNearSemiring_876 → T_IsPartialEquivalence_16 Source #

d_refl_924 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny Source #

d_reflexive_926 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_926 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_928 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → T_Setoid_44 Source #

du_setoid_928 ∷ T_IsNearSemiring_876 → T_Setoid_44 Source #

d_sym_930 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_932 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_936 ∷ T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'691'_940 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'737'_942 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring_876 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_isMagma_944 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

d_IsSemiringWithoutOne_952 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringWithoutOne_952 Source #

Constructors

C_IsSemiringWithoutOne'46'constructor_27777 T_IsCommutativeMonoid_406 T_IsSemigroup_194 T_Σ_14 T_Σ_14

d_'43''45'isCommutativeMonoid_968 ∷ T_IsSemiringWithoutOne_952 → T_IsCommutativeMonoid_406 Source #

d_'42''45'isSemigroup_970 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_distrib_972 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_zero_974 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_comm_978 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_980 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_980 ∷ T_IsSemiringWithoutOne_952 → T_IsCommutativeMagma_122 Source #

d_isCommutativeSemigroup_982 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_982 ∷ T_IsSemiringWithoutOne_952 → T_IsCommutativeSemigroup_270 Source #

d_isMonoid_984 ∷ T_IsSemiringWithoutOne_952 → T_IsMonoid_358 Source #

d_zero'737'_986 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

du_zero'737'_986 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

d_zero'691'_988 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

du_zero'691'_988 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

d_isNearSemiring_990 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsNearSemiring_876 Source #

du_isNearSemiring_990 ∷ T_IsSemiringWithoutOne_952 → T_IsNearSemiring_876 Source #

d_assoc_994 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_994 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_996 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_996 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_998 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_998 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1000 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1000 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_1002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1002 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_assoc_1004 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1004 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1006 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1008 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1008 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1010 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1010 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1012 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

du_identity_1012 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_identity'691'_1014 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

du_identity'691'_1014 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

d_identity'737'_1016 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

du_identity'737'_1016 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

d_isMagma_1018 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1018 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_isSemigroup_1020 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

du_isSemigroup_1020 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_distrib'691'_1022 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1022 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1024 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

du_isEquivalence_1024 ∷ T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1026 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1026 ∷ T_IsSemiringWithoutOne_952 → T_IsPartialEquivalence_16 Source #

d_refl_1028 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

du_refl_1028 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny Source #

d_reflexive_1030 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1030 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1032 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → T_Setoid_44 Source #

du_setoid_1032 ∷ T_IsSemiringWithoutOne_952 → T_Setoid_44 Source #

d_sym_1034 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1034 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1036 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1036 ∷ T_IsSemiringWithoutOne_952 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsCommutativeSemiringWithoutOne_1044 ∷ p → p → p → p → p → p → p → () Source #

data T_IsCommutativeSemiringWithoutOne_1044 Source #

Constructors

C_IsCommutativeSemiringWithoutOne'46'constructor_31059 T_IsSemiringWithoutOne_952 (AgdaAny → AgdaAny → AgdaAny)

d_isSemiringWithoutOne_1056 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemiringWithoutOne_952 Source #

d_'42''45'comm_1058 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1062 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1062 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1064 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1064 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1066 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1066 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1068 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1068 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_1070 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_1070 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1072 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_assoc_1074 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_1074 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1076 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1078 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_1078 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1080 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1080 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1082 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1082 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1084 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

du_identity_1084 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_identity'691'_1086 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

du_identity'691'_1086 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

d_identity'737'_1088 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

du_identity'737'_1088 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1090 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1090 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMagma_122 Source #

d_'43''45'isCommutativeMonoid_1092 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1094 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1094 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1096 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_1096 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_isMonoid_1098 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMonoid_358 Source #

d_isSemigroup_1100 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

du_isSemigroup_1100 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_distrib_1102 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_distrib'691'_1104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1104 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

du_isEquivalence_1106 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

d_isNearSemiring_1108 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1108 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

d_isPartialEquivalence_1110 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1110 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsPartialEquivalence_16 Source #

d_refl_1112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

du_refl_1112 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

d_reflexive_1114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1114 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1116 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_Setoid_44 Source #

du_setoid_1116 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Setoid_44 Source #

d_sym_1118 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1118 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1120 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1120 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_1122 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_zero'691'_1124 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

du_zero'691'_1124 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

d_zero'737'_1126 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

du_zero'737'_1126 ∷ T_IsCommutativeSemiringWithoutOne_1044 → AgdaAny → AgdaAny Source #

d_'42''45'isCommutativeSemigroup_1128 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeSemigroup_270 Source #

du_'42''45'isCommutativeSemigroup_1128 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeSemigroup_270 Source #

d_isCommutativeMagma_1132 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1132 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMagma_122 Source #

d_IsSemiringWithoutAnnihilatingZero_1142 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsSemiringWithoutAnnihilatingZero_1142 Source #

Constructors

C_IsSemiringWithoutAnnihilatingZero'46'constructor_33703 T_IsCommutativeMonoid_406 T_IsMonoid_358 T_Σ_14

d_'43''45'isCommutativeMonoid_1158 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeMonoid_406 Source #

d_'42''45'isMonoid_1160 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_distrib_1162 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_distrib'737'_1164 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1164 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'691'_1166 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1166 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1170 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1172 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1174 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1176 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1176 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1178 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1178 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1180 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_identity'691'_1182 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

du_identity'691'_1182 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

d_identity'737'_1184 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

du_identity'737'_1184 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1186 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1186 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeMagma_122 Source #

d_isCommutativeSemigroup_1188 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1188 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1190 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_isMonoid_1192 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_isSemigroup_1194 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_isEquivalence_1196 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1198 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1198 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsPartialEquivalence_16 Source #

d_refl_1200 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

d_reflexive_1202 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1202 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1204 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → T_Setoid_44 Source #

du_setoid_1204 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Setoid_44 Source #

d_sym_1206 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1208 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1212 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1214 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1216 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1216 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1218 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1218 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1220 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_identity'691'_1222 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

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

d_identity'737'_1224 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero_1142 → AgdaAny → AgdaAny Source #

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

d_isMagma_1226 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_isSemigroup_1228 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_IsSemiring_1238 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsSemiring_1238 Source #

Constructors

C_IsSemiring'46'constructor_37213 T_IsSemiringWithoutAnnihilatingZero_1142 T_Σ_14

d_isSemiringWithoutAnnihilatingZero_1252 ∷ T_IsSemiring_1238 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_zero_1254 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_assoc_1258 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'691'_1262 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'737'_1264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_identity_1266 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_identity'691'_1268 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

du_identity'691'_1268 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_identity'737'_1270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

du_identity'737'_1270 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_isMagma_1272 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1274 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1276 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_assoc_1278 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1280 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1282 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1284 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1284 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1286 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1286 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1288 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_identity'691'_1290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

du_identity'691'_1290 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_identity'737'_1292 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

du_identity'737'_1292 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1294 ∷ T_IsSemiring_1238 → T_IsCommutativeMagma_122 Source #

d_'43''45'isCommutativeMonoid_1296 ∷ T_IsSemiring_1238 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1298 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1298 ∷ T_IsSemiring_1238 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1300 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_isMonoid_1302 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1304 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_distrib_1306 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_distrib'691'_1308 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1308 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_1310 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1310 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1312 ∷ T_IsSemiring_1238 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1314 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1314 ∷ T_IsSemiring_1238 → T_IsPartialEquivalence_16 Source #

d_refl_1316 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_reflexive_1318 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1318 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1320 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → T_Setoid_44 Source #

du_setoid_1320 ∷ T_IsSemiring_1238 → T_Setoid_44 Source #

d_sym_1322 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1324 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemiringWithoutOne_1326 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1326 ∷ T_IsSemiring_1238 → T_IsSemiringWithoutOne_952 Source #

d_isNearSemiring_1330 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1330 ∷ T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

d_zero'691'_1332 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

du_zero'691'_1332 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_zero'737'_1334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

du_zero'737'_1334 ∷ T_IsSemiring_1238 → AgdaAny → AgdaAny Source #

d_IsCommutativeSemiring_1344 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsCommutativeSemiring_1344 Source #

Constructors

C_IsCommutativeSemiring'46'constructor_40675 T_IsSemiring_1238 (AgdaAny → AgdaAny → AgdaAny)

d_isSemiring_1358 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiring_1238 Source #

d_'42''45'comm_1360 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1364 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1366 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1368 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1368 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1370 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1370 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1372 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_identity'691'_1374 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

du_identity'691'_1374 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_identity'737'_1376 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

du_identity'737'_1376 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_isMagma_1378 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1380 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_1382 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_assoc_1384 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1386 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'691'_1390 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_'8729''45'cong'737'_1392 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_identity_1394 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_identity'691'_1396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

du_identity'691'_1396 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_identity'737'_1398 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

du_identity'737'_1398 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1400 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1400 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeMagma_122 Source #

d_'43''45'isCommutativeMonoid_1402 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1404 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1404 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1406 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_isMonoid_1408 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_1410 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_distrib_1412 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_distrib'691'_1414 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1414 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_1416 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1416 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1418 ∷ T_IsCommutativeSemiring_1344 → T_IsEquivalence_26 Source #

d_isNearSemiring_1420 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1420 ∷ T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

d_isPartialEquivalence_1422 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1422 ∷ T_IsCommutativeSemiring_1344 → T_IsPartialEquivalence_16 Source #

d_isSemiringWithoutAnnihilatingZero_1424 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_1426 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1426 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

d_refl_1428 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_reflexive_1430 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1430 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1432 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_Setoid_44 Source #

du_setoid_1432 ∷ T_IsCommutativeSemiring_1344 → T_Setoid_44 Source #

d_sym_1434 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1436 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_1438 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_zero'691'_1440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

du_zero'691'_1440 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_zero'737'_1442 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

du_zero'737'_1442 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny Source #

d_isCommutativeSemiringWithoutOne_1444 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsCommutativeSemiringWithoutOne_1044 Source #

du_isCommutativeSemiringWithoutOne_1444 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeSemiringWithoutOne_1044 Source #

d_isCommutativeMagma_1448 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1448 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeMagma_122 Source #

d_'42''45'isCommutativeSemigroup_1450 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsCommutativeSemigroup_270 Source #

du_'42''45'isCommutativeSemigroup_1450 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeSemigroup_270 Source #

d_'42''45'isCommutativeMonoid_1452 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring_1344 → T_IsCommutativeMonoid_406 Source #

du_'42''45'isCommutativeMonoid_1452 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeMonoid_406 Source #

d_IsCancellativeCommutativeSemiring_1462 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsCancellativeCommutativeSemiring_1462 Source #

Constructors

C_IsCancellativeCommutativeSemiring'46'constructor_44635 T_IsCommutativeSemiring_1344 (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny)

d_isCommutativeSemiring_1476 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemiring_1344 Source #

d_'42''45'cancel'737''45'nonZero_1478 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny Source #

d_assoc_1482 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'comm_1484 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1486 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1488 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1488 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1490 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1490 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1492 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_identity'691'_1494 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

du_identity'691'_1494 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_identity'737'_1496 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

du_identity'737'_1496 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1498 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1498 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMagma_122 Source #

d_'42''45'isCommutativeMonoid_1500 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMonoid_406 Source #

du_'42''45'isCommutativeMonoid_1500 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMonoid_406 Source #

d_'42''45'isCommutativeSemigroup_1502 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemigroup_270 Source #

du_'42''45'isCommutativeSemigroup_1502 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1504 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1506 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_1508 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_assoc_1510 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1512 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1514 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1516 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1516 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1518 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1520 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_identity'691'_1522 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

du_identity'691'_1522 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_identity'737'_1524 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

du_identity'737'_1524 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1526 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1526 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMagma_122 Source #

d_'43''45'isCommutativeMonoid_1528 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1530 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1530 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemigroup_270 Source #

d_isMagma_1532 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_isMonoid_1534 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_1536 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_distrib_1538 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_distrib'691'_1540 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1540 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_1542 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1542 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeSemiringWithoutOne_1544 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemiringWithoutOne_1044 Source #

du_isCommutativeSemiringWithoutOne_1544 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemiringWithoutOne_1044 Source #

d_isEquivalence_1546 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsEquivalence_26 Source #

d_isNearSemiring_1548 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1548 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

d_isPartialEquivalence_1550 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1550 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsPartialEquivalence_16 Source #

d_isSemiring_1552 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_1554 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_1556 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1556 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

d_refl_1558 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_reflexive_1560 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1560 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1562 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → T_Setoid_44 Source #

du_setoid_1562 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Setoid_44 Source #

d_sym_1564 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1566 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_1568 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_zero'691'_1570 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

du_zero'691'_1570 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_zero'737'_1572 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

du_zero'737'_1572 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → AgdaAny Source #

d_IsRing_1584 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRing_1584 Source #

Constructors

C_IsRing'46'constructor_48413 T_IsAbelianGroup_662 T_IsMonoid_358 T_Σ_14 T_Σ_14

d_'43''45'isAbelianGroup_1604 ∷ T_IsRing_1584 → T_IsAbelianGroup_662 Source #

d_'42''45'isMonoid_1606 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_distrib_1608 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_zero_1610 ∷ T_IsRing_1584 → T_Σ_14 Source #

d__'45'__1614 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_1616 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1618 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1620 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1622 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1622 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1624 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1624 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1626 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_identity'691'_1628 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_identity'691'_1628 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_identity'737'_1630 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_identity'737'_1630 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_1632 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1632 ∷ T_IsRing_1584 → T_IsCommutativeMagma_122 Source #

d_isCommutativeMonoid_1634 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsCommutativeMonoid_406 Source #

du_isCommutativeMonoid_1634 ∷ T_IsRing_1584 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1636 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1636 ∷ T_IsRing_1584 → T_IsCommutativeSemigroup_270 Source #

d_isGroup_1638 ∷ T_IsRing_1584 → T_IsGroup_580 Source #

d_isMagma_1640 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_isMonoid_1642 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_isSemigroup_1644 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

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

d_inverse_1648 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_inverse'691'_1650 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_inverse'691'_1650 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_inverse'737'_1652 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_inverse'737'_1652 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_isEquivalence_1654 ∷ T_IsRing_1584 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1656 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1656 ∷ T_IsRing_1584 → T_IsPartialEquivalence_16 Source #

d_refl_1658 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_reflexive_1660 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1660 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1662 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_Setoid_44 Source #

du_setoid_1662 ∷ T_IsRing_1584 → T_Setoid_44 Source #

d_sym_1664 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1666 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1668 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1668 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1670 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1670 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_1674 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1676 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1678 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1678 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1680 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1680 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1682 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_identity'691'_1684 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_identity'691'_1684 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_identity'737'_1686 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_identity'737'_1686 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_isMagma_1688 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_isSemigroup_1690 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

d_zero'737'_1692 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_zero'737'_1692 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_zero'691'_1694 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny Source #

du_zero'691'_1694 ∷ T_IsRing_1584 → AgdaAny → AgdaAny Source #

d_isSemiringWithoutAnnihilatingZero_1696 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

du_isSemiringWithoutAnnihilatingZero_1696 ∷ T_IsRing_1584 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiring_1698 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsSemiring_1238 Source #

du_isSemiring_1698 ∷ T_IsRing_1584 → T_IsSemiring_1238 Source #

d_distrib'691'_1702 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1702 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_1704 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1704 ∷ T_IsRing_1584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiring_1706 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1706 ∷ T_IsRing_1584 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutOne_1708 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1708 ∷ T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

d_IsCommutativeRing_1720 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsCommutativeRing_1720 Source #

Constructors

C_IsCommutativeRing'46'constructor_54081 T_IsRing_1584 (AgdaAny → AgdaAny → AgdaAny)

d_isRing_1736 ∷ T_IsCommutativeRing_1720 → T_IsRing_1584 Source #

d_'42''45'comm_1738 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny Source #

d__'45'__1742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_1744 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1746 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1748 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1748 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1750 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1750 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1752 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_identity'691'_1754 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_identity'691'_1754 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_identity'737'_1756 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_identity'737'_1756 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_isMagma_1758 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1760 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_1762 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

d_assoc_1764 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_1766 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_1768 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_1770 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1770 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1772 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1772 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1774 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_identity'691'_1776 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_identity'691'_1776 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_identity'737'_1778 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_identity'737'_1778 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_'43''45'isAbelianGroup_1780 ∷ T_IsCommutativeRing_1720 → T_IsAbelianGroup_662 Source #

d_isCommutativeMagma_1782 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1782 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeMagma_122 Source #

d_isCommutativeMonoid_1784 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeMonoid_406 Source #

du_isCommutativeMonoid_1784 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeMonoid_406 Source #

d_isCommutativeSemigroup_1786 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeSemigroup_270 Source #

du_isCommutativeSemigroup_1786 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeSemigroup_270 Source #

d_isGroup_1788 ∷ T_IsCommutativeRing_1720 → T_IsGroup_580 Source #

d_isMagma_1790 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_isMonoid_1792 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_1794 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_1796 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse_1798 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_inverse'691'_1800 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_inverse'691'_1800 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_inverse'737'_1802 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_inverse'737'_1802 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_distrib_1804 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_distrib'691'_1806 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1806 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_1808 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1808 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1810 ∷ T_IsCommutativeRing_1720 → T_IsEquivalence_26 Source #

d_isNearSemiring_1812 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1812 ∷ T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

d_isPartialEquivalence_1814 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1814 ∷ T_IsCommutativeRing_1720 → T_IsPartialEquivalence_16 Source #

d_isSemiring_1816 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

du_isSemiring_1816 ∷ T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_1818 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

du_isSemiringWithoutAnnihilatingZero_1818 ∷ T_IsCommutativeRing_1720 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_1820 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1820 ∷ T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

d_refl_1822 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_reflexive_1824 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1824 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1826 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_Setoid_44 Source #

du_setoid_1826 ∷ T_IsCommutativeRing_1720 → T_Setoid_44 Source #

d_sym_1828 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1830 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_1832 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_1832 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_1834 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_1834 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_1836 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_zero'691'_1838 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_zero'691'_1838 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_zero'737'_1840 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

du_zero'737'_1840 ∷ T_IsCommutativeRing_1720 → AgdaAny → AgdaAny Source #

d_isCommutativeSemiring_1842 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeSemiring_1344 Source #

du_isCommutativeSemiring_1842 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeSemiring_1344 Source #

d_isCommutativeMagma_1846 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeMagma_122 Source #

du_isCommutativeMagma_1846 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeMagma_122 Source #

d_'42''45'isCommutativeMonoid_1848 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeMonoid_406 Source #

du_'42''45'isCommutativeMonoid_1848 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeMonoid_406 Source #

d_'42''45'isCommutativeSemigroup_1850 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeSemigroup_270 Source #

du_'42''45'isCommutativeSemigroup_1850 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeSemigroup_270 Source #

d_isCommutativeSemiringWithoutOne_1852 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_1720 → T_IsCommutativeSemiringWithoutOne_1044 Source #

du_isCommutativeSemiringWithoutOne_1852 ∷ T_IsCommutativeRing_1720 → T_IsCommutativeSemiringWithoutOne_1044 Source #

d_IsBooleanAlgebra_1864 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsBooleanAlgebra_1864 Source #

Constructors

C_IsBooleanAlgebra'46'constructor_59337 T_IsDistributiveLattice_814 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isDistributiveLattice_1884 ∷ T_IsBooleanAlgebra_1864 → T_IsDistributiveLattice_814 Source #

d_'8744''45'complement'691'_1886 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'691'_1888 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny Source #

d_'172''45'cong_1890 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_1894 ∷ T_IsBooleanAlgebra_1864 → T_Σ_14 Source #

d_isEquivalence_1896 ∷ T_IsBooleanAlgebra_1864 → T_IsEquivalence_26 Source #

d_isLattice_1898 ∷ T_IsBooleanAlgebra_1864 → T_IsLattice_740 Source #

d_isPartialEquivalence_1900 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1900 ∷ T_IsBooleanAlgebra_1864 → T_IsPartialEquivalence_16 Source #

d_refl_1902 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny Source #

d_reflexive_1904 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1904 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1906 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1908 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_1910 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_1910 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_1912 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_1914 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_1916 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_1918 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_1918 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_1920 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_1920 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_1922 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_1922 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_1924 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_1926 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_1928 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_1930 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_1930 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_1932 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_1932 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'691''45''8743'_1934 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45''8743''45'distrib'691'_1936 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45''8743''45'distrib'691'_1936 ∷ T_IsBooleanAlgebra_1864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #