Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 #
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 #
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 #
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 #
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 #
d_isPartialEquivalence_138 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → T_IsPartialEquivalence_16 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 #
d_setoid_144 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeMagma_122 → T_Setoid_44 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 #
d_isPartialEquivalence_174 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_IsPartialEquivalence_16 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 #
d_setoid_180 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Setoid_44 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 #
d_assoc_204 ∷ T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_210 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → T_IsPartialEquivalence_16 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 #
d_setoid_216 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → T_Setoid_44 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 #
d_idem_240 ∷ T_IsBand_230 → AgdaAny → AgdaAny Source #
d_assoc_244 ∷ T_IsBand_230 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_250 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → 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 #
d_setoid_256 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_Setoid_44 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 #
d_isPartialEquivalence_290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemigroup_270 → T_IsPartialEquivalence_16 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 #
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 #
d_IsSemilattice_312 ∷ p → p → p → p → p → () Source #
data T_IsSemilattice_312 Source #
d_assoc_326 ∷ T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_IsPartialEquivalence_16 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 #
d_setoid_342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_Setoid_44 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 #
d_assoc_374 ∷ T_IsMonoid_358 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → T_IsPartialEquivalence_16 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 #
d_setoid_386 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → T_Setoid_44 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 #
d_identity'691'_400 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_358 → AgdaAny → AgdaAny Source #
d_IsCommutativeMonoid_406 ∷ p → p → p → p → p → p → () Source #
d_identity'691'_426 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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 #
d_isPartialEquivalence_434 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_IsPartialEquivalence_16 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 #
d_setoid_442 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_Setoid_44 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 #
d_isCommutativeMagma_458 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid_406 → T_IsCommutativeMagma_122 Source #
d_IsIdempotentCommutativeMonoid_464 ∷ p → p → p → p → p → p → () Source #
d_isCommutativeMonoid_474 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #
d_identity'691'_486 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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 #
d_isCommutativeMagma_490 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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_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_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 #
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_identity'691'_538 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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 #
d_isCommutativeMagma_542 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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_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_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 #
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 #
d_assoc_602 ∷ T_IsGroup_580 → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
d_identity'737'_608 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → AgdaAny → AgdaAny 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 #
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 #
d_setoid_622 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_580 → T_Setoid_44 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 #
d_inverse'691'_642 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → 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 #
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'691'_686 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → 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 #
d_inverse'691'_692 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → 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 #
d_isPartialEquivalence_702 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_IsPartialEquivalence_16 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 #
d_setoid_710 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_662 → T_Setoid_44 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_'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 #
d_isCommutativeMagma_732 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → 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 #
d_IsLattice_740 ∷ p → p → p → p → p → p → () Source #
data T_IsLattice_740 Source #
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_'8744''45'cong_768 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8743''45'cong_774 ∷ T_IsLattice_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
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 #
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 #
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 #
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 #
d_'8744''45'distrib'691''45''8743'_826 ∷ T_IsDistributiveLattice_814 → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
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_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'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'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 #
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'691'_912 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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 #
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 #
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 #
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 #
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_IsSemiringWithoutOne_952 ∷ p → p → p → p → p → p → p → () 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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
d_refl_1028 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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 #
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 #
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 #
d_isSemiringWithoutOne_1056 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemiringWithoutOne_952 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 #
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_'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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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'691'_1124 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → 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 #
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 #
d_'43''45'isCommutativeMonoid_1158 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeMonoid_406 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_'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'691'_1182 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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_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_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 #
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'691'_1222 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
d_IsSemiring_1238 ∷ p → p → p → p → p → p → p → p → () Source #
data T_IsSemiring_1238 Source #
d_isSemiringWithoutAnnihilatingZero_1252 ∷ T_IsSemiring_1238 → T_IsSemiringWithoutAnnihilatingZero_1142 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'691'_1268 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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'691'_1290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
d_IsCommutativeSemiring_1344 ∷ p → p → p → p → p → p → p → p → () 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'691'_1374 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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'691'_1396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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 #
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_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_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 #
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 #
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 #
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 #
d_trans_1436 ∷ T_IsCommutativeSemiring_1344 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
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 #
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 #
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 #
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'691'_1494 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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_assoc_1510 ∷ T_IsCancellativeCommutativeSemiring_1462 → AgdaAny → 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'691'_1522 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
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_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_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 #
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_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_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 #
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'691'_1570 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → 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 #
d_IsRing_1584 ∷ p → p → p → p → p → p → p → p → p → () Source #
data T_IsRing_1584 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'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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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'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 #
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 #
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 #
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 #
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 #
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 #
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 #
d_IsCommutativeRing_1720 ∷ p → p → p → p → p → p → p → p → p → () 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_'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'691'_1754 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny →