Safe Haskell	None

MAlonzo.Code.Algebra.Structures

Documentation

d__DistributesOver__16 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver'691'__18 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver'737'__20 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_AlmostLeftCancellative_28 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Associative_32 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Commutative_36 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Congruent'8321'_38 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Congruent'8322'_40 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Idempotent_44 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Identity_48 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Inverse_52 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftCongruent_58 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftDivides_62 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftDivides'691'_64 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftDivides'737'_66 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftIdentity_68 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftInverse_70 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftZero_72 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightCongruent_76 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightDivides_80 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightDivides'691'_82 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightDivides'737'_84 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightIdentity_86 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightInverse_88 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightZero_90 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Selective_92 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Zero_94 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_IsMagma_98 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsMagma_98 Source #

Constructors

C_IsMagma'46'constructor_495 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isEquivalence_106 :: T_IsMagma_98 -> T_IsEquivalence_26 Source #

d_'8729''45'cong_108 :: T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_112 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_112 :: T_IsMagma_98 -> T_IsPartialEquivalence_16 Source #

d_refl_114 :: T_IsMagma_98 -> AgdaAny -> AgdaAny Source #

d_reflexive_116 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_116 :: T_IsMagma_98 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_118 :: T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_120 :: T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_122 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> T_Setoid_44 Source #

du_setoid_122 :: T_IsMagma_98 -> T_Setoid_44 Source #

d_'8729''45'cong'737'_124 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_124 :: T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_128 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_128 :: T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsCommutativeMagma_134 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsCommutativeMagma_134 Source #

Constructors

C_IsCommutativeMagma'46'constructor_2007 T_IsMagma_98 (AgdaAny -> AgdaAny -> AgdaAny)

d_isMagma_142 :: T_IsCommutativeMagma_134 -> T_IsMagma_98 Source #

d_comm_144 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_148 :: T_IsCommutativeMagma_134 -> T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_150 :: T_IsCommutativeMagma_134 -> T_IsPartialEquivalence_16 Source #

d_refl_152 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny Source #

d_reflexive_154 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_154 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_156 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMagma_134 -> T_Setoid_44 Source #

du_setoid_156 :: T_IsCommutativeMagma_134 -> T_Setoid_44 Source #

d_sym_158 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_160 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_162 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_164 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_164 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_166 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_166 :: T_IsCommutativeMagma_134 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsSelectiveMagma_170 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsSelectiveMagma_170 Source #

Constructors

C_IsSelectiveMagma'46'constructor_2741 T_IsMagma_98 (AgdaAny -> AgdaAny -> T__'8846'__30)

d_isMagma_178 :: T_IsSelectiveMagma_170 -> T_IsMagma_98 Source #

d_sel_180 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #

d_isEquivalence_184 :: T_IsSelectiveMagma_170 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_186 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_186 :: T_IsSelectiveMagma_170 -> T_IsPartialEquivalence_16 Source #

d_refl_188 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny Source #

d_reflexive_190 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_190 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_192 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> T_Setoid_44 Source #

du_setoid_192 :: T_IsSelectiveMagma_170 -> T_Setoid_44 Source #

d_sym_194 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_196 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_198 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_200 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_200 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_202 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_202 :: T_IsSelectiveMagma_170 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsSemigroup_206 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsSemigroup_206 Source #

Constructors

C_IsSemigroup'46'constructor_3475 T_IsMagma_98 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isMagma_214 :: T_IsSemigroup_206 -> T_IsMagma_98 Source #

d_assoc_216 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_220 :: T_IsSemigroup_206 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_222 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_222 :: T_IsSemigroup_206 -> T_IsPartialEquivalence_16 Source #

d_refl_224 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny Source #

d_reflexive_226 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_226 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_228 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> T_Setoid_44 Source #

du_setoid_228 :: T_IsSemigroup_206 -> T_Setoid_44 Source #

d_sym_230 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_232 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_234 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_236 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_236 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_238 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_238 :: T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBand_242 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsBand_242 Source #

Constructors

C_IsBand'46'constructor_4211 T_IsSemigroup_206 (AgdaAny -> AgdaAny)

d_isSemigroup_250 :: T_IsBand_242 -> T_IsSemigroup_206 Source #

d_idem_252 :: T_IsBand_242 -> AgdaAny -> AgdaAny Source #

d_assoc_256 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_258 :: T_IsBand_242 -> T_IsEquivalence_26 Source #

d_isMagma_260 :: T_IsBand_242 -> T_IsMagma_98 Source #

d_isPartialEquivalence_262 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_262 :: T_IsBand_242 -> T_IsPartialEquivalence_16 Source #

d_refl_264 :: T_IsBand_242 -> AgdaAny -> AgdaAny Source #

d_reflexive_266 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_266 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_268 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_Setoid_44 Source #

du_setoid_268 :: T_IsBand_242 -> T_Setoid_44 Source #

d_sym_270 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_272 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_274 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_276 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_276 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_278 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_278 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsCommutativeSemigroup_282 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsCommutativeSemigroup_282 Source #

Constructors

C_IsCommutativeSemigroup'46'constructor_5047 T_IsSemigroup_206 (AgdaAny -> AgdaAny -> AgdaAny)

d_isSemigroup_290 :: T_IsCommutativeSemigroup_282 -> T_IsSemigroup_206 Source #

d_comm_292 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_296 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_298 :: T_IsCommutativeSemigroup_282 -> T_IsEquivalence_26 Source #

d_isMagma_300 :: T_IsCommutativeSemigroup_282 -> T_IsMagma_98 Source #

d_isPartialEquivalence_302 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemigroup_282 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_302 :: T_IsCommutativeSemigroup_282 -> T_IsPartialEquivalence_16 Source #

d_refl_304 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny Source #

d_reflexive_306 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

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

d_setoid_308 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemigroup_282 -> T_Setoid_44 Source #

du_setoid_308 :: T_IsCommutativeSemigroup_282 -> T_Setoid_44 Source #

d_sym_310 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_312 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_314 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_316 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_316 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_318 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_318 :: T_IsCommutativeSemigroup_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_320 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemigroup_282 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_320 :: T_IsCommutativeSemigroup_282 -> T_IsCommutativeMagma_134 Source #

d_IsUnitalMagma_326 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsUnitalMagma_326 Source #

Constructors

C_IsUnitalMagma'46'constructor_6003 T_IsMagma_98 T_Σ_14

d_isMagma_336 :: T_IsUnitalMagma_326 -> T_IsMagma_98 Source #

d_identity_338 :: T_IsUnitalMagma_326 -> T_Σ_14 Source #

d_isEquivalence_342 :: T_IsUnitalMagma_326 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_344 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_344 :: T_IsUnitalMagma_326 -> T_IsPartialEquivalence_16 Source #

d_refl_346 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny Source #

d_reflexive_348 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_348 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_350 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> T_Setoid_44 Source #

du_setoid_350 :: T_IsUnitalMagma_326 -> T_Setoid_44 Source #

d_sym_352 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_354 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_356 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_358 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_358 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_360 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_360 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'737'_362 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny Source #

du_identity'737'_362 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny Source #

d_identity'691'_364 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny Source #

du_identity'691'_364 :: T_IsUnitalMagma_326 -> AgdaAny -> AgdaAny Source #

d_IsMonoid_370 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsMonoid_370 Source #

Constructors

C_IsMonoid'46'constructor_7357 T_IsSemigroup_206 T_Σ_14

d_isSemigroup_380 :: T_IsMonoid_370 -> T_IsSemigroup_206 Source #

d_identity_382 :: T_IsMonoid_370 -> T_Σ_14 Source #

d_assoc_386 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_388 :: T_IsMonoid_370 -> T_IsEquivalence_26 Source #

d_isMagma_390 :: T_IsMonoid_370 -> T_IsMagma_98 Source #

d_isPartialEquivalence_392 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_392 :: T_IsMonoid_370 -> T_IsPartialEquivalence_16 Source #

d_refl_394 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

d_reflexive_396 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_396 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_398 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_Setoid_44 Source #

du_setoid_398 :: T_IsMonoid_370 -> T_Setoid_44 Source #

d_sym_400 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_402 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_404 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_406 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_406 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_408 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_408 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'737'_410 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

du_identity'737'_410 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

d_identity'691'_412 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

du_identity'691'_412 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

d_isUnitalMagma_414 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_414 :: T_IsMonoid_370 -> T_IsUnitalMagma_326 Source #

d_IsCommutativeMonoid_420 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsCommutativeMonoid_420 Source #

Constructors

C_IsCommutativeMonoid'46'constructor_8965 T_IsMonoid_370 (AgdaAny -> AgdaAny -> AgdaAny)

d_isMonoid_430 :: T_IsCommutativeMonoid_420 -> T_IsMonoid_370 Source #

d_comm_432 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_436 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_438 :: T_IsCommutativeMonoid_420 -> T_Σ_14 Source #

d_identity'691'_440 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny Source #

du_identity'691'_440 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny Source #

d_identity'737'_442 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny Source #

du_identity'737'_442 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_444 :: T_IsCommutativeMonoid_420 -> T_IsEquivalence_26 Source #

d_isMagma_446 :: T_IsCommutativeMonoid_420 -> T_IsMagma_98 Source #

d_isPartialEquivalence_448 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_448 :: T_IsCommutativeMonoid_420 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_450 :: T_IsCommutativeMonoid_420 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_452 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_452 :: T_IsCommutativeMonoid_420 -> T_IsUnitalMagma_326 Source #

d_refl_454 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny Source #

d_reflexive_456 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_456 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_458 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_Setoid_44 Source #

du_setoid_458 :: T_IsCommutativeMonoid_420 -> T_Setoid_44 Source #

d_sym_460 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_462 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_464 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_466 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_466 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_468 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_468 :: T_IsCommutativeMonoid_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemigroup_470 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_470 :: T_IsCommutativeMonoid_420 -> T_IsCommutativeSemigroup_282 Source #

d_isCommutativeMagma_474 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_474 :: T_IsCommutativeMonoid_420 -> T_IsCommutativeMagma_134 Source #

d_IsIdempotentCommutativeMonoid_480 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsIdempotentCommutativeMonoid_480 Source #

Constructors

C_IsIdempotentCommutativeMonoid'46'constructor_10399 T_IsCommutativeMonoid_420 (AgdaAny -> AgdaAny)

d_isCommutativeMonoid_490 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMonoid_420 Source #

d_idem_492 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_assoc_496 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_498 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_500 :: T_IsIdempotentCommutativeMonoid_480 -> T_Σ_14 Source #

d_identity'691'_502 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'691'_502 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_identity'737'_504 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'737'_504 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_506 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_506 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeSemigroup_508 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_508 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_510 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsEquivalence_26 Source #

d_isMagma_512 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsMagma_98 Source #

d_isMonoid_514 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_516 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_516 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_518 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_520 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_520 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsUnitalMagma_326 Source #

d_refl_522 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_524 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_524 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_526 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

du_setoid_526 :: T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

d_sym_528 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_530 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_532 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_534 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_534 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_536 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_536 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isBand_538 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

du_isBand_538 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

d_IsInvertibleMagma_546 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsInvertibleMagma_546 Source #

Constructors

C_IsInvertibleMagma'46'constructor_11987 T_IsMagma_98 T_Σ_14

d_isMagma_558 :: T_IsInvertibleMagma_546 -> T_IsMagma_98 Source #

d_inverse_560 :: T_IsInvertibleMagma_546 -> T_Σ_14 Source #

d_isEquivalence_564 :: T_IsInvertibleMagma_546 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_566 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_566 :: T_IsInvertibleMagma_546 -> T_IsPartialEquivalence_16 Source #

d_refl_568 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny Source #

d_reflexive_570 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_570 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_572 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> T_Setoid_44 Source #

du_setoid_572 :: T_IsInvertibleMagma_546 -> T_Setoid_44 Source #

d_sym_574 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_576 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_578 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_580 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_580 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_582 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_582 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'737'_584 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_584 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny Source #

d_inverse'691'_586 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_586 :: T_IsInvertibleMagma_546 -> AgdaAny -> AgdaAny Source #

d_IsInvertibleUnitalMagma_594 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsInvertibleUnitalMagma_594 Source #

Constructors

C_IsInvertibleUnitalMagma'46'constructor_13559 T_IsInvertibleMagma_546 T_Σ_14

d_isInvertibleMagma_606 :: T_IsInvertibleUnitalMagma_594 -> T_IsInvertibleMagma_546 Source #

d_identity_608 :: T_IsInvertibleUnitalMagma_594 -> T_Σ_14 Source #

d_inverse_612 :: T_IsInvertibleUnitalMagma_594 -> T_Σ_14 Source #

d_inverse'691'_614 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_614 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_616 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_616 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_618 :: T_IsInvertibleUnitalMagma_594 -> T_IsEquivalence_26 Source #

d_isMagma_620 :: T_IsInvertibleUnitalMagma_594 -> T_IsMagma_98 Source #

d_isPartialEquivalence_622 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_622 :: T_IsInvertibleUnitalMagma_594 -> T_IsPartialEquivalence_16 Source #

d_refl_624 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

d_reflexive_626 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_626 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_628 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> T_Setoid_44 Source #

du_setoid_628 :: T_IsInvertibleUnitalMagma_594 -> T_Setoid_44 Source #

d_sym_630 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_632 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_634 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_636 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_636 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_638 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_638 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'737'_640 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

du_identity'737'_640 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

d_identity'691'_642 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

du_identity'691'_642 :: T_IsInvertibleUnitalMagma_594 -> AgdaAny -> AgdaAny Source #

d_isUnitalMagma_644 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsInvertibleUnitalMagma_594 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_644 :: T_IsInvertibleUnitalMagma_594 -> T_IsUnitalMagma_326 Source #

d_IsGroup_652 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsGroup_652 Source #

Constructors

C_IsGroup'46'constructor_15567 T_IsMonoid_370 T_Σ_14 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isMonoid_666 :: T_IsGroup_652 -> T_IsMonoid_370 Source #

d_inverse_668 :: T_IsGroup_652 -> T_Σ_14 Source #

d_'8315''185''45'cong_670 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_674 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_676 :: T_IsGroup_652 -> T_Σ_14 Source #

d_identity'691'_678 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

du_identity'691'_678 :: T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

d_identity'737'_680 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

du_identity'737'_680 :: T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_682 :: T_IsGroup_652 -> T_IsEquivalence_26 Source #

d_isMagma_684 :: T_IsGroup_652 -> T_IsMagma_98 Source #

d_isPartialEquivalence_686 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_686 :: T_IsGroup_652 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_688 :: T_IsGroup_652 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_690 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_690 :: T_IsGroup_652 -> T_IsUnitalMagma_326 Source #

d_refl_692 :: T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

d_reflexive_694 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_694 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_696 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_Setoid_44 Source #

du_setoid_696 :: T_IsGroup_652 -> T_Setoid_44 Source #

d_sym_698 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_700 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_702 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_704 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_704 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_706 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_706 :: T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'45'__708 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__708 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'737'_714 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_714 :: T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

d_inverse'691'_716 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_716 :: T_IsGroup_652 -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_722 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_722 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_728 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_728 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isInvertibleMagma_730 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_730 :: T_IsGroup_652 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_732 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_732 :: T_IsGroup_652 -> T_IsInvertibleUnitalMagma_594 Source #

d_IsAbelianGroup_740 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsAbelianGroup_740 Source #

Constructors

C_IsAbelianGroup'46'constructor_19563 T_IsGroup_652 (AgdaAny -> AgdaAny -> AgdaAny)

d_isGroup_752 :: T_IsAbelianGroup_740 -> T_IsGroup_652 Source #

d_comm_754 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'45'__758 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__758 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_760 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_762 :: T_IsAbelianGroup_740 -> T_Σ_14 Source #

d_identity'691'_764 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_identity'691'_764 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_identity'737'_766 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_identity'737'_766 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_inverse_768 :: T_IsAbelianGroup_740 -> T_Σ_14 Source #

d_inverse'691'_770 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_770 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_772 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_772 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_774 :: T_IsAbelianGroup_740 -> T_IsEquivalence_26 Source #

d_isInvertibleMagma_776 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_776 :: T_IsAbelianGroup_740 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_778 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_778 :: T_IsAbelianGroup_740 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_780 :: T_IsAbelianGroup_740 -> T_IsMagma_98 Source #

d_isMonoid_782 :: T_IsAbelianGroup_740 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_784 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_784 :: T_IsAbelianGroup_740 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_786 :: T_IsAbelianGroup_740 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_788 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_788 :: T_IsAbelianGroup_740 -> T_IsUnitalMagma_326 Source #

d_refl_790 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_reflexive_792 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_792 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_794 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_Setoid_44 Source #

du_setoid_794 :: T_IsAbelianGroup_740 -> T_Setoid_44 Source #

d_sym_796 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_798 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_800 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_800 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_802 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_802 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8315''185''45'cong_804 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_806 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_808 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_808 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_810 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_810 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMonoid_812 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_812 :: T_IsAbelianGroup_740 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeMagma_816 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_816 :: T_IsAbelianGroup_740 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeSemigroup_818 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_818 :: T_IsAbelianGroup_740 -> T_IsCommutativeSemigroup_282 Source #

d_IsNearSemiring_826 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsNearSemiring_826 Source #

Constructors

C_IsNearSemiring'46'constructor_21939 T_IsMonoid_370 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_'43''45'isMonoid_844 :: T_IsNearSemiring_826 -> T_IsMonoid_370 Source #

d_'42''45'cong_846 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_848 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'691'_850 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'737'_852 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny Source #

d_assoc_856 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_858 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_860 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_860 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_862 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_862 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_864 :: T_IsNearSemiring_826 -> T_Σ_14 Source #

d_identity'691'_866 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny Source #

du_identity'691'_866 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny Source #

d_identity'737'_868 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny Source #

du_identity'737'_868 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny Source #

d_isMagma_870 :: T_IsNearSemiring_826 -> T_IsMagma_98 Source #

d_isSemigroup_872 :: T_IsNearSemiring_826 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_874 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_874 :: T_IsNearSemiring_826 -> T_IsUnitalMagma_326 Source #

d_isEquivalence_876 :: T_IsNearSemiring_826 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_878 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_878 :: T_IsNearSemiring_826 -> T_IsPartialEquivalence_16 Source #

d_refl_880 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny Source #

d_reflexive_882 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_882 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_884 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_Setoid_44 Source #

du_setoid_884 :: T_IsNearSemiring_826 -> T_Setoid_44 Source #

d_sym_886 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_888 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_890 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_IsMagma_98 Source #

du_'42''45'isMagma_890 :: T_IsNearSemiring_826 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_892 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_892 :: T_IsNearSemiring_826 -> T_IsSemigroup_206 Source #

d_'8729''45'cong'691'_896 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_896 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_898 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_898 :: T_IsNearSemiring_826 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsSemiringWithoutOne_906 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsSemiringWithoutOne_906 Source #

Constructors

C_IsSemiringWithoutOne'46'constructor_24235 T_IsCommutativeMonoid_420 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 T_Σ_14

d_'43''45'isCommutativeMonoid_924 :: T_IsSemiringWithoutOne_906 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'cong_926 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_928 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib_930 :: T_IsSemiringWithoutOne_906 -> T_Σ_14 Source #

d_zero_932 :: T_IsSemiringWithoutOne_906 -> T_Σ_14 Source #

d_comm_936 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_938 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_938 :: T_IsSemiringWithoutOne_906 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeSemigroup_940 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_940 :: T_IsSemiringWithoutOne_906 -> T_IsCommutativeSemigroup_282 Source #

d_isMonoid_942 :: T_IsSemiringWithoutOne_906 -> T_IsMonoid_370 Source #

d_isEquivalence_944 :: T_IsSemiringWithoutOne_906 -> T_IsEquivalence_26 Source #

d_'42''45'isMagma_946 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsMagma_98 Source #

du_'42''45'isMagma_946 :: T_IsSemiringWithoutOne_906 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_948 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_948 :: T_IsSemiringWithoutOne_906 -> T_IsSemigroup_206 Source #

d_'8729''45'cong'691'_952 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_952 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_954 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_954 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'737'_956 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny Source #

du_zero'737'_956 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny Source #

d_zero'691'_958 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny Source #

du_zero'691'_958 :: T_IsSemiringWithoutOne_906 -> AgdaAny -> AgdaAny Source #

d_isNearSemiring_960 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_960 :: T_IsSemiringWithoutOne_906 -> T_IsNearSemiring_826 Source #

d_IsCommutativeSemiringWithoutOne_968 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsCommutativeSemiringWithoutOne_968 Source #

Constructors

C_IsCommutativeSemiringWithoutOne'46'constructor_26859 T_IsSemiringWithoutOne_906 (AgdaAny -> AgdaAny -> AgdaAny)

d_isSemiringWithoutOne_980 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsSemiringWithoutOne_906 Source #

d_'42''45'comm_982 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_986 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_988 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_990 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_990 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_992 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_992 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_994 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsMagma_98 Source #

du_'42''45'isMagma_994 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_996 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsSemigroup_206 Source #

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

d_comm_998 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1000 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1000 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1002 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1004 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1004 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeSemigroup_282 Source #

d_isMonoid_1006 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsMonoid_370 Source #

d_distrib_1008 :: T_IsCommutativeSemiringWithoutOne_968 -> T_Σ_14 Source #

d_isEquivalence_1010 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1012 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1012 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsNearSemiring_826 Source #

d_zero_1014 :: T_IsCommutativeSemiringWithoutOne_968 -> T_Σ_14 Source #

d_zero'691'_1016 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1016 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1018 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1018 :: T_IsCommutativeSemiringWithoutOne_968 -> AgdaAny -> AgdaAny Source #

d_'42''45'isCommutativeSemigroup_1020 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_1020 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeSemigroup_282 Source #

d_isCommutativeMagma_1024 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1024 :: T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeMagma_134 Source #

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

data T_IsSemiringWithoutAnnihilatingZero_1034 Source #

Constructors

C_IsSemiringWithoutAnnihilatingZero'46'constructor_28479 T_IsCommutativeMonoid_420 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 T_Σ_14

d_'43''45'isCommutativeMonoid_1054 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'cong_1056 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_1058 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_1060 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_Σ_14 Source #

d_distrib_1062 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_Σ_14 Source #

d_distrib'737'_1064 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1064 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'691'_1066 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1066 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_1070 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1072 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1074 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1076 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1076 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1078 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1078 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1080 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_Σ_14 Source #

d_identity'691'_1082 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1082 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1084 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1084 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1086 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1086 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeSemigroup_1088 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1088 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_1090 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsMagma_98 Source #

d_isMonoid_1092 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsMonoid_370 Source #

d_isSemigroup_1094 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1096 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1096 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsUnitalMagma_326 Source #

d_isEquivalence_1098 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1100 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1100 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsPartialEquivalence_16 Source #

d_refl_1102 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

d_reflexive_1104 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1104 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1106 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_Setoid_44 Source #

du_setoid_1106 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_Setoid_44 Source #

d_sym_1108 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1110 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1112 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1112 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_1114 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1114 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsSemigroup_206 Source #

d_'42''45'isMonoid_1116 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_1116 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> T_IsMonoid_370 Source #

d_'8729''45'cong'691'_1120 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1120 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1122 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1122 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'691'_1124 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1124 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1126 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1126 :: T_IsSemiringWithoutAnnihilatingZero_1034 -> AgdaAny -> AgdaAny Source #

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

data T_IsSemiring_1136 Source #

Constructors

C_IsSemiring'46'constructor_32267 T_IsSemiringWithoutAnnihilatingZero_1034 T_Σ_14

d_isSemiringWithoutAnnihilatingZero_1150 :: T_IsSemiring_1136 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_zero_1152 :: T_IsSemiring_1136 -> T_Σ_14 Source #

d_'42''45'assoc_1156 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1158 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1160 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1160 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1162 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1162 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_1164 :: T_IsSemiring_1136 -> T_Σ_14 Source #

d_identity'691'_1166 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1166 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1168 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1168 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1170 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1170 :: T_IsSemiring_1136 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_1172 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_1172 :: T_IsSemiring_1136 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_1174 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1174 :: T_IsSemiring_1136 -> T_IsSemigroup_206 Source #

d_assoc_1176 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1178 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1180 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1182 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1182 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1184 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1184 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1186 :: T_IsSemiring_1136 -> T_Σ_14 Source #

d_identity'691'_1188 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1188 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1190 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1190 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1192 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1192 :: T_IsSemiring_1136 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1194 :: T_IsSemiring_1136 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1196 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1196 :: T_IsSemiring_1136 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_1198 :: T_IsSemiring_1136 -> T_IsMagma_98 Source #

d_isMonoid_1200 :: T_IsSemiring_1136 -> T_IsMonoid_370 Source #

d_isSemigroup_1202 :: T_IsSemiring_1136 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1204 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1204 :: T_IsSemiring_1136 -> T_IsUnitalMagma_326 Source #

d_distrib_1206 :: T_IsSemiring_1136 -> T_Σ_14 Source #

d_distrib'691'_1208 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1208 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1210 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1210 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1212 :: T_IsSemiring_1136 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1214 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1214 :: T_IsSemiring_1136 -> T_IsPartialEquivalence_16 Source #

d_refl_1216 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

d_reflexive_1218 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1218 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1220 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_Setoid_44 Source #

du_setoid_1220 :: T_IsSemiring_1136 -> T_Setoid_44 Source #

d_sym_1222 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1224 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemiringWithoutOne_1226 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1226 :: T_IsSemiring_1136 -> T_IsSemiringWithoutOne_906 Source #

d_isNearSemiring_1230 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1230 :: T_IsSemiring_1136 -> T_IsNearSemiring_826 Source #

d_zero'691'_1232 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1232 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1234 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1234 :: T_IsSemiring_1136 -> AgdaAny -> AgdaAny Source #

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

data T_IsCommutativeSemiring_1244 Source #

Constructors

C_IsCommutativeSemiring'46'constructor_35797 T_IsSemiring_1136 (AgdaAny -> AgdaAny -> AgdaAny)

d_isSemiring_1258 :: T_IsCommutativeSemiring_1244 -> T_IsSemiring_1136 Source #

d_'42''45'comm_1260 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_1264 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1266 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1268 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1268 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1270 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1270 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_1272 :: T_IsCommutativeSemiring_1244 -> T_Σ_14 Source #

d_identity'691'_1274 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1274 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1276 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1276 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1278 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1278 :: T_IsCommutativeSemiring_1244 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_1280 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_1280 :: T_IsCommutativeSemiring_1244 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_1282 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1282 :: T_IsCommutativeSemiring_1244 -> T_IsSemigroup_206 Source #

d_assoc_1284 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1286 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1288 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1290 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1290 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1292 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1292 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1294 :: T_IsCommutativeSemiring_1244 -> T_Σ_14 Source #

d_identity'691'_1296 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1296 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1298 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1298 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1300 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1300 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1302 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1304 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1304 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_1306 :: T_IsCommutativeSemiring_1244 -> T_IsMagma_98 Source #

d_isMonoid_1308 :: T_IsCommutativeSemiring_1244 -> T_IsMonoid_370 Source #

d_isSemigroup_1310 :: T_IsCommutativeSemiring_1244 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1312 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1312 :: T_IsCommutativeSemiring_1244 -> T_IsUnitalMagma_326 Source #

d_distrib_1314 :: T_IsCommutativeSemiring_1244 -> T_Σ_14 Source #

d_distrib'691'_1316 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1316 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1318 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1318 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1320 :: T_IsCommutativeSemiring_1244 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1322 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1322 :: T_IsCommutativeSemiring_1244 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_1324 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1324 :: T_IsCommutativeSemiring_1244 -> T_IsPartialEquivalence_16 Source #

d_isSemiringWithoutAnnihilatingZero_1326 :: T_IsCommutativeSemiring_1244 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_1328 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1328 :: T_IsCommutativeSemiring_1244 -> T_IsSemiringWithoutOne_906 Source #

d_refl_1330 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_reflexive_1332 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1332 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1334 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_Setoid_44 Source #

du_setoid_1334 :: T_IsCommutativeSemiring_1244 -> T_Setoid_44 Source #

d_sym_1336 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1338 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_1340 :: T_IsCommutativeSemiring_1244 -> T_Σ_14 Source #

d_zero'691'_1342 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1342 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1344 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1344 :: T_IsCommutativeSemiring_1244 -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiringWithoutOne_1346 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_1346 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isCommutativeMagma_1350 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1350 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeSemigroup_1352 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_1352 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isCommutativeMonoid_1354 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1244 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_1354 :: T_IsCommutativeSemiring_1244 -> T_IsCommutativeMonoid_420 Source #

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

data T_IsCancellativeCommutativeSemiring_1364 Source #

Constructors

C_IsCancellativeCommutativeSemiring'46'constructor_39561 T_IsCommutativeSemiring_1244 (AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> T_'8869'_4) -> AgdaAny -> AgdaAny)

d_isCommutativeSemiring_1378 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemiring_1244 Source #

d_'42''45'cancel'737''45'nonZero_1380 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> T_'8869'_4) -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_1384 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'comm_1386 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1388 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1390 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1390 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1392 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1392 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_1394 :: T_IsCancellativeCommutativeSemiring_1364 -> T_Σ_14 Source #

d_identity'691'_1396 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1396 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1398 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1398 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1400 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1400 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_1402 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_1402 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_1404 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_1404 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemigroup_282 Source #

d_'42''45'isMagma_1406 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1406 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_1408 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_1408 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_1410 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1410 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemigroup_206 Source #

d_assoc_1412 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1414 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1416 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1418 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1418 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1420 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1420 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1422 :: T_IsCancellativeCommutativeSemiring_1364 -> T_Σ_14 Source #

d_identity'691'_1424 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1424 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1426 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1426 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1428 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1428 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMagma_134 Source #

d_'43''45'isCommutativeMonoid_1430 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1432 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1432 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemigroup_282 Source #

d_isMagma_1434 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsMagma_98 Source #

d_isMonoid_1436 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsMonoid_370 Source #

d_isSemigroup_1438 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1440 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1440 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsUnitalMagma_326 Source #

d_distrib_1442 :: T_IsCancellativeCommutativeSemiring_1364 -> T_Σ_14 Source #

d_distrib'691'_1444 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1444 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1446 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1446 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiringWithoutOne_1448 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_1448 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_isEquivalence_1450 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1452 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1452 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_1454 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1454 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_1456 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_1458 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_1460 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1460 :: T_IsCancellativeCommutativeSemiring_1364 -> T_IsSemiringWithoutOne_906 Source #

d_refl_1462 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

d_reflexive_1464 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1464 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1466 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> T_Setoid_44 Source #

du_setoid_1466 :: T_IsCancellativeCommutativeSemiring_1364 -> T_Setoid_44 Source #

d_sym_1468 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1470 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_1472 :: T_IsCancellativeCommutativeSemiring_1364 -> T_Σ_14 Source #

d_zero'691'_1474 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1474 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1476 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1476 :: T_IsCancellativeCommutativeSemiring_1364 -> AgdaAny -> AgdaAny Source #

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

data T_IsRingWithoutOne_1486 Source #

Constructors

C_IsRingWithoutOne'46'constructor_43147 T_IsAbelianGroup_740 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 T_Σ_14

d_'43''45'isAbelianGroup_1506 :: T_IsRingWithoutOne_1486 -> T_IsAbelianGroup_740 Source #

d_'42''45'cong_1508 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_1510 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib_1512 :: T_IsRingWithoutOne_1486 -> T_Σ_14 Source #

d_zero_1514 :: T_IsRingWithoutOne_1486 -> T_Σ_14 Source #

d__'45'__1518 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__1518 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_1520 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1522 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1524 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1526 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1526 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1528 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1528 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1530 :: T_IsRingWithoutOne_1486 -> T_Σ_14 Source #

d_identity'691'_1532 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1532 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1534 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1534 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1536 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1536 :: T_IsRingWithoutOne_1486 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_1538 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_1538 :: T_IsRingWithoutOne_1486 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1540 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1540 :: T_IsRingWithoutOne_1486 -> T_IsCommutativeSemigroup_282 Source #

d_isGroup_1542 :: T_IsRingWithoutOne_1486 -> T_IsGroup_652 Source #

d_isInvertibleMagma_1544 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_1544 :: T_IsRingWithoutOne_1486 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_1546 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_1546 :: T_IsRingWithoutOne_1486 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_1548 :: T_IsRingWithoutOne_1486 -> T_IsMagma_98 Source #

d_isMonoid_1550 :: T_IsRingWithoutOne_1486 -> T_IsMonoid_370 Source #

d_isSemigroup_1552 :: T_IsRingWithoutOne_1486 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1554 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1554 :: T_IsRingWithoutOne_1486 -> T_IsUnitalMagma_326 Source #

d_'8315''185''45'cong_1556 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse_1558 :: T_IsRingWithoutOne_1486 -> T_Σ_14 Source #

d_inverse'691'_1560 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1560 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1562 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1562 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1564 :: T_IsRingWithoutOne_1486 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1566 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1566 :: T_IsRingWithoutOne_1486 -> T_IsPartialEquivalence_16 Source #

d_refl_1568 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_reflexive_1570 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1570 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1572 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_Setoid_44 Source #

du_setoid_1572 :: T_IsRingWithoutOne_1486 -> T_Setoid_44 Source #

d_sym_1574 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1576 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_1578 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_1578 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_1580 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_1580 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1582 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1582 :: T_IsRingWithoutOne_1486 -> T_IsMagma_98 Source #

d_zero'737'_1584 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1584 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_zero'691'_1586 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1586 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1588 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1588 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'691'_1590 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1590 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isSemigroup_1592 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1592 :: T_IsRingWithoutOne_1486 -> T_IsSemigroup_206 Source #

d_'8729''45'cong'691'_1596 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1596 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1598 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1598 :: T_IsRingWithoutOne_1486 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

data T_IsRing_1610 Source #

Constructors

C_IsRing'46'constructor_48103 T_IsAbelianGroup_740 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 T_Σ_14 T_Σ_14

d_'43''45'isAbelianGroup_1634 :: T_IsRing_1610 -> T_IsAbelianGroup_740 Source #

d_'42''45'cong_1636 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_1638 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_1640 :: T_IsRing_1610 -> T_Σ_14 Source #

d_distrib_1642 :: T_IsRing_1610 -> T_Σ_14 Source #

d_zero_1644 :: T_IsRing_1610 -> T_Σ_14 Source #

d__'45'__1648 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__1648 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_1650 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1652 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1654 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1656 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1656 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1658 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1658 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1660 :: T_IsRing_1610 -> T_Σ_14 Source #

d_identity'691'_1662 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1662 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1664 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1664 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_1666 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1666 :: T_IsRing_1610 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_1668 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_1668 :: T_IsRing_1610 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1670 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1670 :: T_IsRing_1610 -> T_IsCommutativeSemigroup_282 Source #

d_isGroup_1672 :: T_IsRing_1610 -> T_IsGroup_652 Source #

d_isInvertibleMagma_1674 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_1674 :: T_IsRing_1610 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_1676 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_1676 :: T_IsRing_1610 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_1678 :: T_IsRing_1610 -> T_IsMagma_98 Source #

d_isMonoid_1680 :: T_IsRing_1610 -> T_IsMonoid_370 Source #

d_isSemigroup_1682 :: T_IsRing_1610 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1684 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1684 :: T_IsRing_1610 -> T_IsUnitalMagma_326 Source #

d_'8315''185''45'cong_1686 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse_1688 :: T_IsRing_1610 -> T_Σ_14 Source #

d_inverse'691'_1690 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1690 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1692 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1692 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1694 :: T_IsRing_1610 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1696 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1696 :: T_IsRing_1610 -> T_IsPartialEquivalence_16 Source #

d_refl_1698 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_reflexive_1700 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1700 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1702 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_Setoid_44 Source #

du_setoid_1702 :: T_IsRing_1610 -> T_Setoid_44 Source #

d_sym_1704 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1706 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_1708 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_1708 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_1710 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_1710 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1712 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1712 :: T_IsRing_1610 -> T_IsMagma_98 Source #

d_'42''45'isSemigroup_1714 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1714 :: T_IsRing_1610 -> T_IsSemigroup_206 Source #

d_'42''45'isMonoid_1716 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_1716 :: T_IsRing_1610 -> T_IsMonoid_370 Source #

d_'8729''45'cong'691'_1720 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1720 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1722 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1722 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'691'_1724 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1724 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1726 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1726 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1728 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1728 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_zero'691'_1730 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1730 :: T_IsRing_1610 -> AgdaAny -> AgdaAny Source #

d_isSemiringWithoutAnnihilatingZero_1732 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

du_isSemiringWithoutAnnihilatingZero_1732 :: T_IsRing_1610 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiring_1734 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsSemiring_1136 Source #

du_isSemiring_1734 :: T_IsRing_1610 -> T_IsSemiring_1136 Source #

d_distrib'691'_1738 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1738 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1740 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1740 :: T_IsRing_1610 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiring_1742 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1742 :: T_IsRing_1610 -> T_IsNearSemiring_826 Source #

d_isSemiringWithoutOne_1744 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing_1610 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1744 :: T_IsRing_1610 -> T_IsSemiringWithoutOne_906 Source #

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

data T_IsCommutativeRing_1756 Source #

Constructors

C_IsCommutativeRing'46'constructor_54323 T_IsRing_1610 (AgdaAny -> AgdaAny -> AgdaAny)

d_isRing_1772 :: T_IsCommutativeRing_1756 -> T_IsRing_1610 Source #

d_'42''45'comm_1774 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'45'__1778 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__1778 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'assoc_1780 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'cong_1782 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1784 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1784 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1786 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1786 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'identity_1788 :: T_IsCommutativeRing_1756 -> T_Σ_14 Source #

d_identity'691'_1790 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1790 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1792 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1792 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagma_1794 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsMagma_98 Source #

du_'42''45'isMagma_1794 :: T_IsCommutativeRing_1756 -> T_IsMagma_98 Source #

d_'42''45'isMonoid_1796 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsMonoid_370 Source #

du_'42''45'isMonoid_1796 :: T_IsCommutativeRing_1756 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_1798 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsSemigroup_206 Source #

du_'42''45'isSemigroup_1798 :: T_IsCommutativeRing_1756 -> T_IsSemigroup_206 Source #

d_assoc_1800 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1802 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1804 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1806 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1806 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1808 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1808 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_1810 :: T_IsCommutativeRing_1756 -> T_Σ_14 Source #

d_identity'691'_1812 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1812 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1814 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1814 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_'43''45'isAbelianGroup_1816 :: T_IsCommutativeRing_1756 -> T_IsAbelianGroup_740 Source #

d_isCommutativeMagma_1818 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1818 :: T_IsCommutativeRing_1756 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_1820 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_1820 :: T_IsCommutativeRing_1756 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1822 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1822 :: T_IsCommutativeRing_1756 -> T_IsCommutativeSemigroup_282 Source #

d_isGroup_1824 :: T_IsCommutativeRing_1756 -> T_IsGroup_652 Source #

d_isInvertibleMagma_1826 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_1826 :: T_IsCommutativeRing_1756 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_1828 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_1828 :: T_IsCommutativeRing_1756 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_1830 :: T_IsCommutativeRing_1756 -> T_IsMagma_98 Source #

d_isMonoid_1832 :: T_IsCommutativeRing_1756 -> T_IsMonoid_370 Source #

d_isSemigroup_1834 :: T_IsCommutativeRing_1756 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1836 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1836 :: T_IsCommutativeRing_1756 -> T_IsUnitalMagma_326 Source #

d_'8315''185''45'cong_1838 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse_1840 :: T_IsCommutativeRing_1756 -> T_Σ_14 Source #

d_inverse'691'_1842 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1842 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1844 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1844 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_distrib_1846 :: T_IsCommutativeRing_1756 -> T_Σ_14 Source #

d_distrib'691'_1848 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'691'_1848 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distrib'737'_1850 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_distrib'737'_1850 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1852 :: T_IsCommutativeRing_1756 -> T_IsEquivalence_26 Source #

d_isNearSemiring_1854 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1854 :: T_IsCommutativeRing_1756 -> T_IsNearSemiring_826 Source #

d_isPartialEquivalence_1856 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1856 :: T_IsCommutativeRing_1756 -> T_IsPartialEquivalence_16 Source #

d_isSemiring_1858 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsSemiring_1136 Source #

du_isSemiring_1858 :: T_IsCommutativeRing_1756 -> T_IsSemiring_1136 Source #

d_isSemiringWithoutAnnihilatingZero_1860 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

du_isSemiringWithoutAnnihilatingZero_1860 :: T_IsCommutativeRing_1756 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_isSemiringWithoutOne_1862 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1862 :: T_IsCommutativeRing_1756 -> T_IsSemiringWithoutOne_906 Source #

d_refl_1864 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_reflexive_1866 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1866 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1868 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_Setoid_44 Source #

du_setoid_1868 :: T_IsCommutativeRing_1756 -> T_Setoid_44 Source #

d_sym_1870 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1872 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_1874 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_1874 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_1876 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_1876 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero_1878 :: T_IsCommutativeRing_1756 -> T_Σ_14 Source #

d_zero'691'_1880 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_zero'691'_1880 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_zero'737'_1882 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

du_zero'737'_1882 :: T_IsCommutativeRing_1756 -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiring_1884 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeSemiring_1244 Source #

du_isCommutativeSemiring_1884 :: T_IsCommutativeRing_1756 -> T_IsCommutativeSemiring_1244 Source #

d_isCommutativeMagma_1888 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1888 :: T_IsCommutativeRing_1756 -> T_IsCommutativeMagma_134 Source #

d_'42''45'isCommutativeMonoid_1890 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeMonoid_420 Source #

du_'42''45'isCommutativeMonoid_1890 :: T_IsCommutativeRing_1756 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeSemigroup_1892 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeSemigroup_282 Source #

du_'42''45'isCommutativeSemigroup_1892 :: T_IsCommutativeRing_1756 -> T_IsCommutativeSemigroup_282 Source #

d_isCommutativeSemiringWithoutOne_1894 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeRing_1756 -> T_IsCommutativeSemiringWithoutOne_968 Source #

du_isCommutativeSemiringWithoutOne_1894 :: T_IsCommutativeRing_1756 -> T_IsCommutativeSemiringWithoutOne_968 Source #

d_IsQuasigroup_1902 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsQuasigroup_1902 Source #

Constructors

C_IsQuasigroup'46'constructor_59443 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 T_Σ_14

d_isEquivalence_1922 :: T_IsQuasigroup_1902 -> T_IsEquivalence_26 Source #

d_'8729''45'cong_1924 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'cong_1926 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'cong_1928 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_leftDivides_1930 :: T_IsQuasigroup_1902 -> T_Σ_14 Source #

d_rightDivides_1932 :: T_IsQuasigroup_1902 -> T_Σ_14 Source #

d_isPartialEquivalence_1936 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1936 :: T_IsQuasigroup_1902 -> T_IsPartialEquivalence_16 Source #

d_refl_1938 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny Source #

d_reflexive_1940 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1940 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_1942 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1944 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_1946 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> T_Setoid_44 Source #

du_setoid_1946 :: T_IsQuasigroup_1902 -> T_Setoid_44 Source #

d_'8729''45'cong'737'_1948 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1948 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1952 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1952 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'cong'737'_1956 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'92''92''45'cong'737'_1956 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'cong'691'_1960 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'92''92''45'cong'691'_1960 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'cong'737'_1964 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'47''47''45'cong'737'_1964 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'cong'691'_1968 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'47''47''45'cong'691'_1968 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_leftDivides'737'_1972 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_leftDivides'737'_1972 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_leftDivides'691'_1974 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_leftDivides'691'_1974 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_rightDivides'737'_1976 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_rightDivides'737'_1976 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_rightDivides'691'_1978 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_rightDivides'691'_1978 :: T_IsQuasigroup_1902 -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

data T_IsLoop_1988 Source #

Constructors

C_IsLoop'46'constructor_64685 T_IsQuasigroup_1902 T_Σ_14

d_isQuasigroup_2002 :: T_IsLoop_1988 -> T_IsQuasigroup_1902 Source #

d_identity_2004 :: T_IsLoop_1988 -> T_Σ_14 Source #

d_'47''47''45'cong_2008 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'cong'691'_2010 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'47''47''45'cong'691'_2010 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'cong'737'_2012 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'47''47''45'cong'737'_2012 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'cong_2014 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'cong'691'_2016 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'92''92''45'cong'691'_2016 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'cong'737'_2018 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'92''92''45'cong'737'_2018 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_2020 :: T_IsLoop_1988 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_2022 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2022 :: T_IsLoop_1988 -> T_IsPartialEquivalence_16 Source #

d_leftDivides_2024 :: T_IsLoop_1988 -> T_Σ_14 Source #

d_leftDivides'691'_2026 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_leftDivides'691'_2026 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_leftDivides'737'_2028 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_leftDivides'737'_2028 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_2030 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny Source #

d_reflexive_2032 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_2032 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_rightDivides_2034 :: T_IsLoop_1988 -> T_Σ_14 Source #

d_rightDivides'691'_2036 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_rightDivides'691'_2036 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_rightDivides'737'_2038 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_rightDivides'737'_2038 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_2040 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> T_Setoid_44 Source #

du_setoid_2040 :: T_IsLoop_1988 -> T_Setoid_44 Source #

d_sym_2042 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_2044 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_2046 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_2048 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_2048 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_2050 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_2050 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'737'_2052 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny Source #

du_identity'737'_2052 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny Source #

d_identity'691'_2054 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsLoop_1988 -> AgdaAny -> AgdaAny Source #

du_identity'691'_2054 :: T_IsLoop_1988 -> AgdaAny -> AgdaAny Source #