Safe Haskell	None

MAlonzo.Code.Algebra.Solver.Ring.AlmostCommutativeRing

Documentation

d_IsAlmostCommutativeRing_26 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsAlmostCommutativeRing_26 Source #

Constructors

C_IsAlmostCommutativeRing'46'constructor_587 T_IsCommutativeSemiring_1244 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)

d_isCommutativeSemiring_62 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemiring_1244 Source #

d_'45''8255'cong_64 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''42''45'distrib'737'_70 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''43''45'comm_76 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_80 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_82 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_84 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_86 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_86 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_88 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_88 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_90 :: T_IsAlmostCommutativeRing_26 -> T_Σ_14 Source #

d_identity'691'_92 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

du_identity'691'_92 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_identity'737'_94 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

du_identity'737'_94 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_96 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_96 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_98 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_98 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_100 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_100 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_102 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsMagma_98 Source #

du_'42''45'isMagma_102 :: T_IsAlmostCommutativeRing_26 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_104 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_104 :: T_IsAlmostCommutativeRing_26 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_106 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_106 :: T_IsAlmostCommutativeRing_26 -> T_IsSemigroup_206 Source #

d_assoc_108 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_110 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_112 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_114 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_114 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_116 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_116 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_118 :: T_IsAlmostCommutativeRing_26 -> T_Σ_14 Source #

d_identity'691'_120 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

du_identity'691'_120 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_identity'737'_122 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

du_identity'737'_122 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_124 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_124 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_126 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_128 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_128 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_130 :: T_IsAlmostCommutativeRing_26 -> T_IsMagma_98 Source #

d_isMonoid_132 :: T_IsAlmostCommutativeRing_26 -> T_IsMonoid_370 Source #

d_isSemigroup_134 :: T_IsAlmostCommutativeRing_26 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_136 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_136 :: T_IsAlmostCommutativeRing_26 -> T_IsUnitalMagma_326 Source #

d_distrib_138 :: T_IsAlmostCommutativeRing_26 -> T_Σ_14 Source #

d_distrib'691'_140 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_140 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_142 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_142 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiringWithoutOne_144 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_144 :: T_IsAlmostCommutativeRing_26 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_146 :: T_IsAlmostCommutativeRing_26 -> T_IsEquivalence_26 Source #

d_isNearSemiring_148 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_148 :: T_IsAlmostCommutativeRing_26 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_150 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_150 :: T_IsAlmostCommutativeRing_26 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_152 :: T_IsAlmostCommutativeRing_26 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_154 :: T_IsAlmostCommutativeRing_26 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_156 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_156 :: T_IsAlmostCommutativeRing_26 -> T_IsSemiringWithoutOne_906 Source #

d_refl_158 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_reflexive_160 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_160 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_162 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> T_Setoid_44 Source #

du_setoid_162 :: T_IsAlmostCommutativeRing_26 -> T_Setoid_44 Source #

d_sym_164 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_166 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_168 :: T_IsAlmostCommutativeRing_26 -> T_Σ_14 Source #

d_zero'691'_170 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

du_zero'691'_170 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_zero'737'_172 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

du_zero'737'_172 :: T_IsAlmostCommutativeRing_26 -> AgdaAny -> AgdaAny Source #

d_AlmostCommutativeRing_178 :: p1 -> p2 -> () Source #

data T_AlmostCommutativeRing_178 Source #

Constructors

C_AlmostCommutativeRing'46'constructor_5201 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsAlmostCommutativeRing_26

d_Carrier_200 :: T_AlmostCommutativeRing_178 -> () Source #

d__'8776'__202 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> () Source #

d__'43'__204 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'42'__206 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45'__208 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_0'35'_210 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_1'35'_212 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_isAlmostCommutativeRing_214 :: T_AlmostCommutativeRing_178 -> T_IsAlmostCommutativeRing_26 Source #

d_'42''45'assoc_218 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_220 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_222 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_224 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_224 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_226 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_226 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_228 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_230 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'691'_230 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_232 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'737'_232 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_234 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_234 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_236 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_236 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_238 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_238 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_240 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

du_'42''45'isMagma_240 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_242 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_242 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_244 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_244 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_assoc_246 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_248 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_250 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_252 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_252 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_254 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_254 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_256 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_258 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'691'_258 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_260 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'737'_260 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_262 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_262 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_264 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_266 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_266 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_268 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_isMonoid_270 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_isSemigroup_272 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_274 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_274 :: T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

d_'45''8255''42''45'distrib'737'_276 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''43''45'comm_278 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'cong_280 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib_282 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_distrib'691'_284 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_284 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_286 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_286 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiring_288 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiring_1244 Source #

d_isCommutativeSemiringWithoutOne_290 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_290 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_292 :: T_AlmostCommutativeRing_178 -> T_IsEquivalence_26 Source #

d_isNearSemiring_294 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_294 :: T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_296 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_296 :: T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_298 :: T_AlmostCommutativeRing_178 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_300 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_302 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_302 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

d_refl_304 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_reflexive_306 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_306 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_308 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

du_setoid_308 :: T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

d_sym_310 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_312 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_314 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_zero'691'_316 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_zero'691'_316 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_zero'737'_318 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_zero'737'_318 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_commutativeSemiring_320 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

du_commutativeSemiring_320 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

d_'42''45'commutativeMonoid_324 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

du_'42''45'commutativeMonoid_324 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_326 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_326 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

d_magma_328 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

du_magma_328 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_'42''45'monoid_330 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

du_'42''45'monoid_330 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_332 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

du_semigroup_332 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_'43''45'commutativeMonoid_334 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_334 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_magma_336 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

du_magma_336 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_monoid_338 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

du_monoid_338 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_340 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

du_semigroup_340 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_semiring_342 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

du_semiring_342 :: T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

d_rawRing_344 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

du_rawRing_344 :: T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

d__'45'Raw'45'AlmostCommutative'10230'__358 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T__'45'Raw'45'AlmostCommutative'10230'__358 Source #

Constructors

C__'45'Raw'45'AlmostCommutative'10230'_'46'constructor_8311 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) AgdaAny AgdaAny

d__'42'__374 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'42'__374 :: T_RawRing_2558 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'43'__376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'43'__376 :: T_RawRing_2558 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45'__392 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_'45'__392 :: T_RawRing_2558 -> AgdaAny -> AgdaAny Source #

d_0'35'_394 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny Source #

du_0'35'_394 :: T_RawRing_2558 -> AgdaAny Source #

d_1'35'_396 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny Source #

du_1'35'_396 :: T_RawRing_2558 -> AgdaAny Source #

d_Carrier_398 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> () Source #

d__'42'__404 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'43'__406 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__408 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> () Source #

d_'42''45'assoc_410 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_412 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'commutativeMonoid_414 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

du_'42''45'commutativeMonoid_414 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_416 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_416 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

d_'42''45'cong_418 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_420 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_420 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_422 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_422 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_424 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_426 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'691'_426 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_428 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'737'_428 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_430 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_430 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_432 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_434 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_434 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_436 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

du_'42''45'isMagma_436 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_438 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_438 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_440 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_440 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_magma_442 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

du_magma_442 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_'42''45'monoid_444 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

du_'42''45'monoid_444 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_446 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

du_semigroup_446 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_assoc_448 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_450 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'commutativeMonoid_452 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_452 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_'8729''45'cong_454 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_456 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_456 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_458 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_458 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_460 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_462 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'691'_462 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_464 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'737'_464 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_466 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_466 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_468 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_470 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_470 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_472 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_isMonoid_474 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_isSemigroup_476 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_478 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_478 :: T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

d_magma_480 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

du_magma_480 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_monoid_482 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

du_monoid_482 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_484 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

du_semigroup_484 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_'45'__486 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_'45''8255''42''45'distrib'737'_488 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''43''45'comm_490 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'cong_492 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_494 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_1'35'_496 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_Carrier_498 :: T_AlmostCommutativeRing_178 -> () Source #

d_commutativeSemiring_500 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

du_commutativeSemiring_500 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

d_distrib_502 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_distrib'691'_504 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_504 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_506 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_506 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isAlmostCommutativeRing_508 :: T_AlmostCommutativeRing_178 -> T_IsAlmostCommutativeRing_26 Source #

d_isCommutativeSemiring_510 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiring_1244 Source #

d_isCommutativeSemiringWithoutOne_512 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_512 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_514 :: T_AlmostCommutativeRing_178 -> T_IsEquivalence_26 Source #

d_isNearSemiring_516 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_516 :: T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_518 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_518 :: T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_520 :: T_AlmostCommutativeRing_178 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_522 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_524 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_524 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

d_rawRing_526 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

du_rawRing_526 :: T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

d_refl_528 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_reflexive_530 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_530 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_semiring_532 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

du_semiring_532 :: T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

d_setoid_534 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

du_setoid_534 :: T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

d_sym_536 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_538 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_540 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_zero'691'_542 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_zero'691'_542 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_zero'737'_544 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_zero'737'_544 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_Homomorphic'8320'_548 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_550 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_552 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_554 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> () Source #

d__'42'__600 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'42'__600 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'43'__602 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'43'__602 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__604 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> () Source #

d_'42''45'assoc_606 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'assoc_606 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_608 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'comm_608 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'commutativeMonoid_610 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_CommutativeMonoid_582 Source #

du_'42''45'commutativeMonoid_610 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_612 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_612 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

d_'42''45'cong_614 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'cong_614 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_616 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_616 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_618 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_618 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_620 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Σ_14 Source #

du_'42''45'identity_620 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_622 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_identity'691'_622 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_624 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_identity'737'_624 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_626 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_626 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_628 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_628 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_630 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_630 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_632 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsMagma_98 Source #

du_'42''45'isMagma_632 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_634 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_634 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_636 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_636 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_magma_638 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Magma_36 Source #

du_magma_638 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_'42''45'monoid_640 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Monoid_502 Source #

du_'42''45'monoid_640 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_642 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Semigroup_206 Source #

du_semigroup_642 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_assoc_644 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_assoc_644 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_646 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_comm_646 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'commutativeMonoid_648 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_648 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_'8729''45'cong_650 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong_650 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_652 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_652 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_654 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_654 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_656 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Σ_14 Source #

du_identity_656 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_658 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_identity'691'_658 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_660 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_identity'737'_660 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_662 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_662 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_664 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeMonoid_420 Source #

du_'43''45'isCommutativeMonoid_664 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_666 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_666 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_668 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsMagma_98 Source #

du_isMagma_668 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_isMonoid_670 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsMonoid_370 Source #

du_isMonoid_670 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_isSemigroup_672 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsSemigroup_206 Source #

du_isSemigroup_672 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_674 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_674 :: T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

d_magma_676 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Magma_36 Source #

du_magma_676 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_monoid_678 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Monoid_502 Source #

du_monoid_678 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_680 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Semigroup_206 Source #

du_semigroup_680 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_'45'__682 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_'45'__682 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_'45''8255''42''45'distrib'737'_684 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255''42''45'distrib'737'_684 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''43''45'comm_686 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255''43''45'comm_686 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'cong_688 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255'cong_688 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_690 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny Source #

du_0'35'_690 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_1'35'_692 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny Source #

du_1'35'_692 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_Carrier_694 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> () Source #

d_commutativeSemiring_696 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_CommutativeSemiring_2036 Source #

du_commutativeSemiring_696 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

d_distrib_698 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Σ_14 Source #

du_distrib_698 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_distrib'691'_700 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_700 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_702 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_702 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isAlmostCommutativeRing_704 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsAlmostCommutativeRing_26 Source #

du_isAlmostCommutativeRing_704 :: T_AlmostCommutativeRing_178 -> T_IsAlmostCommutativeRing_26 Source #

d_isCommutativeSemiring_706 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeSemiring_1244 Source #

du_isCommutativeSemiring_706 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiring_1244 Source #

d_isCommutativeSemiringWithoutOne_708 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_708 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_710 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsEquivalence_26 Source #

du_isEquivalence_710 :: T_AlmostCommutativeRing_178 -> T_IsEquivalence_26 Source #

d_isNearSemiring_712 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_712 :: T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_714 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_714 :: T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_716 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsSemiring_1136 Source #

du_isSemiring_716 :: T_AlmostCommutativeRing_178 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_718 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

du_isSemiringWithoutAnnihilatingZero_718 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_720 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_720 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

d_rawRing_722 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_RawRing_2558 Source #

du_rawRing_722 :: T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

d_refl_724 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_refl_724 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_reflexive_726 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_726 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_semiring_728 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Semiring_1870 Source #

du_semiring_728 :: T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

d_setoid_730 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Setoid_44 Source #

du_setoid_730 :: T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

d_sym_732 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_732 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_734 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_734 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_736 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Σ_14 Source #

du_zero_736 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_zero'691'_738 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_zero'691'_738 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_zero'737'_740 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

du_zero'737'_740 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_'10214'_'10215'_752 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

d_'43''45'homo_754 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_756 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'homo_758 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

d_0'45'homo_760 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny Source #

d_1'45'homo_762 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny Source #

d_'45'raw'45'almostCommutative'10230'_770 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 Source #

du_'45'raw'45'almostCommutative'10230'_770 :: T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 Source #

d__'42'__780 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'43'__782 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__784 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> () Source #

d_'42''45'assoc_786 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_788 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'commutativeMonoid_790 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

du_'42''45'commutativeMonoid_790 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_792 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_792 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

d_'42''45'cong_794 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_796 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_796 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_798 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_798 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_800 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_802 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'691'_802 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_804 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'737'_804 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_806 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_806 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_808 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_808 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_810 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_810 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_812 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

du_'42''45'isMagma_812 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_814 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_814 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_816 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_816 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_magma_818 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

du_magma_818 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_'42''45'monoid_820 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

du_'42''45'monoid_820 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_822 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

du_semigroup_822 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_assoc_824 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_826 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'commutativeMonoid_828 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_828 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_'8729''45'cong_830 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_832 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_832 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_834 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_834 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_836 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_838 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'691'_838 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_840 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_identity'737'_840 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_842 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_842 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_844 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_846 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_846 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_848 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_isMonoid_850 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_isSemigroup_852 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_854 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_854 :: T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

d_magma_856 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

du_magma_856 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_monoid_858 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

du_monoid_858 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_860 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

du_semigroup_860 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_'45'__862 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_'45''8255''42''45'distrib'737'_864 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''43''45'comm_866 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'cong_868 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_870 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_1'35'_872 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_Carrier_874 :: T_AlmostCommutativeRing_178 -> () Source #

d_commutativeSemiring_876 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

du_commutativeSemiring_876 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

d_distrib_878 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_distrib'691'_880 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_880 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_882 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_882 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isAlmostCommutativeRing_884 :: T_AlmostCommutativeRing_178 -> T_IsAlmostCommutativeRing_26 Source #

d_isCommutativeSemiring_886 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiring_1244 Source #

d_isCommutativeSemiringWithoutOne_888 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_888 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_890 :: T_AlmostCommutativeRing_178 -> T_IsEquivalence_26 Source #

d_isNearSemiring_892 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_892 :: T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_894 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_894 :: T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_896 :: T_AlmostCommutativeRing_178 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_898 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_900 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_900 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

d_rawRing_902 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

du_rawRing_902 :: T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

d_refl_904 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_reflexive_906 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_906 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_semiring_908 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

du_semiring_908 :: T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

d_setoid_910 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

du_setoid_910 :: T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

d_sym_912 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_914 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_916 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_zero'691'_918 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_zero'691'_918 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_zero'737'_920 :: T_Level_14 -> T_Level_14 -> T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

du_zero'737'_920 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_Induced'45'equivalence_944 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> () Source #

d__'42'__960 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'42'__960 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'43'__962 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'43'__962 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__964 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () Source #

d_'42''45'assoc_966 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'assoc_966 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_968 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'comm_968 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'commutativeMonoid_970 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_582 Source #

du_'42''45'commutativeMonoid_970 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_commutativeSemigroup_972 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_CommutativeSemigroup_332 Source #

du_commutativeSemigroup_972 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemigroup_332 Source #

d_'42''45'cong_974 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'cong_974 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_976 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_976 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_978 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_978 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_980 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_'42''45'identity_980 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_982 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_identity'691'_982 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_984 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_identity'737'_984 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_986 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_986 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_988 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_988 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_990 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_990 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_992 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsMagma_98 Source #

du_'42''45'isMagma_992 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_994 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_994 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_996 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_996 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_magma_998 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Magma_36 Source #

du_magma_998 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_'42''45'monoid_1000 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Monoid_502 Source #

du_'42''45'monoid_1000 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_1002 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Semigroup_206 Source #

du_semigroup_1002 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_assoc_1004 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_assoc_1004 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1006 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_comm_1006 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'commutativeMonoid_1008 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_582 Source #

du_'43''45'commutativeMonoid_1008 :: T_AlmostCommutativeRing_178 -> T_CommutativeMonoid_582 Source #

d_'8729''45'cong_1010 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong_1010 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1012 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1012 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1014 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1014 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1016 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_identity_1016 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_identity'691'_1018 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_identity'691'_1018 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1020 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_identity'737'_1020 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1022 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1022 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1024 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_420 Source #

du_'43''45'isCommutativeMonoid_1024 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1026 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1026 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_1028 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsMagma_98 Source #

du_isMagma_1028 :: T_AlmostCommutativeRing_178 -> T_IsMagma_98 Source #

d_isMonoid_1030 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsMonoid_370 Source #

du_isMonoid_1030 :: T_AlmostCommutativeRing_178 -> T_IsMonoid_370 Source #

d_isSemigroup_1032 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsSemigroup_206 Source #

du_isSemigroup_1032 :: T_AlmostCommutativeRing_178 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1034 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1034 :: T_AlmostCommutativeRing_178 -> T_IsUnitalMagma_326 Source #

d_magma_1036 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Magma_36 Source #

du_magma_1036 :: T_AlmostCommutativeRing_178 -> T_Magma_36 Source #

d_monoid_1038 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Monoid_502 Source #

du_monoid_1038 :: T_AlmostCommutativeRing_178 -> T_Monoid_502 Source #

d_semigroup_1040 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Semigroup_206 Source #

du_semigroup_1040 :: T_AlmostCommutativeRing_178 -> T_Semigroup_206 Source #

d_'45'__1042 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45'__1042 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_'45''8255''42''45'distrib'737'_1044 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255''42''45'distrib'737'_1044 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255''43''45'comm_1046 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255''43''45'comm_1046 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'cong_1048 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255'cong_1048 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'35'_1050 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_0'35'_1050 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_1'35'_1052 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_1'35'_1052 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_Carrier_1054 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> () Source #

d_commutativeSemiring_1056 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_CommutativeSemiring_2036 Source #

du_commutativeSemiring_1056 :: T_AlmostCommutativeRing_178 -> T_CommutativeSemiring_2036 Source #

d_distrib_1058 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_distrib_1058 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_distrib'691'_1060 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1060 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1062 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1062 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isAlmostCommutativeRing_1064 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsAlmostCommutativeRing_26 Source #

du_isAlmostCommutativeRing_1064 :: T_AlmostCommutativeRing_178 -> T_IsAlmostCommutativeRing_26 Source #

d_isCommutativeSemiring_1066 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 Source #

du_isCommutativeSemiring_1066 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiring_1244 Source #

d_isCommutativeSemiringWithoutOne_1068 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_1068 :: T_AlmostCommutativeRing_178 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_1070 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsEquivalence_26 Source #

du_isEquivalence_1070 :: T_AlmostCommutativeRing_178 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1072 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1072 :: T_AlmostCommutativeRing_178 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_1074 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1074 :: T_AlmostCommutativeRing_178 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_1076 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 Source #

du_isSemiring_1076 :: T_AlmostCommutativeRing_178 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_1078 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

du_isSemiringWithoutAnnihilatingZero_1078 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_1080 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1080 :: T_AlmostCommutativeRing_178 -> T_IsSemiringWithoutOne_906 Source #

d_rawRing_1082 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_RawRing_2558 Source #

du_rawRing_1082 :: T_AlmostCommutativeRing_178 -> T_RawRing_2558 Source #

d_refl_1084 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_refl_1084 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_reflexive_1086 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1086 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_semiring_1088 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Semiring_1870 Source #

du_semiring_1088 :: T_AlmostCommutativeRing_178 -> T_Semiring_1870 Source #

d_setoid_1090 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Setoid_44 Source #

du_setoid_1090 :: T_AlmostCommutativeRing_178 -> T_Setoid_44 Source #

d_sym_1092 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_1092 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1094 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_1094 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_1096 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_zero_1096 :: T_AlmostCommutativeRing_178 -> T_Σ_14 Source #

d_zero'691'_1098 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_zero'691'_1098 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1100 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_zero'737'_1100 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1104 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'42''45'homo_1104 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'homo_1106 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'43''45'homo_1106 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'45''8255'homo_1108 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'45''8255'homo_1108 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

d_0'45'homo_1110 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_0'45'homo_1110 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny Source #

d_1'45'homo_1112 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_1'45'homo_1112 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny Source #

d_'10214'_'10215'_1114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'10214'_'10215'_1114 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

d_fromCommutativeRing_1120 :: T_Level_14 -> T_Level_14 -> T_CommutativeRing_2814 -> T_AlmostCommutativeRing_178 Source #

du_fromCommutativeRing_1120 :: T_CommutativeRing_2814 -> T_AlmostCommutativeRing_178 Source #

d_fromCommutativeSemiring_1414 :: T_Level_14 -> T_Level_14 -> T_CommutativeSemiring_2036 -> T_AlmostCommutativeRing_178 Source #

du_fromCommutativeSemiring_1414 :: T_CommutativeSemiring_2036 -> T_AlmostCommutativeRing_178 Source #