Documentation

d_ProtoMetric_12 ∷ p → p → () Source #

data T_ProtoMetric_12 Source #

d_Carrier_26 ∷ T_ProtoMetric_12 → () Source #

d__'8776'__28 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → () Source #

d_d_30 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → Integer Source #

d_isProtoMetric_32 ∷ T_ProtoMetric_12 → T_IsProtoMetric_30 Source #

d_antisym_36 ∷ T_ProtoMetric_12 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_38 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_40 ∷ T_ProtoMetric_12 → T_IsEquivalence_28 Source #

d_isPartialOrder_42 ∷ T_ProtoMetric_12 → T_IsPartialOrder_248 Source #

d_isPreorder_44 ∷ T_ProtoMetric_12 → T_IsPreorder_76 Source #

d_nonNegative_46 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_48 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → Integer → T__'8804'__22 Source #

du_refl_48 ∷ T_ProtoMetric_12 → Integer → T__'8804'__22 Source #

d_reflexive_50 ∷ T_ProtoMetric_12 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_trans_52 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_54 ∷ T_ProtoMetric_12 → T_IsEquivalence_28 Source #

d_'8764''45'resp'45''8776'_56 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_56 ∷ T_ProtoMetric_12 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_58 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'691''45''8776'_58 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8764''45'resp'737''45''8776'_60 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'737''45''8776'_60 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'45''8776'_62 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_62 ∷ T_ProtoMetric_12 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_64 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'691''45''8776'_64 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'737''45''8776'_66 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'737''45''8776'_66 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_isPartialEquivalence_70 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_70 ∷ T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

d_refl_72 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny Source #

d_reflexive_74 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_74 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_76 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_78 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_82 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_82 ∷ T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

d_refl_84 ∷ T_ProtoMetric_12 → Integer → T__'8801'__12 Source #

d_reflexive_86 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_88 ∷ T_ProtoMetric_12 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_90 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_PreMetric_98 ∷ p → p → () Source #

data T_PreMetric_98 Source #

d_Carrier_112 ∷ T_PreMetric_98 → () Source #

d__'8776'__114 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → () Source #

d_d_116 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → Integer Source #

d_isPreMetric_118 ∷ T_PreMetric_98 → T_IsPreMetric_104 Source #

d_antisym_122 ∷ T_PreMetric_98 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_124 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_126 ∷ T_PreMetric_98 → T_IsEquivalence_28 Source #

d_isPartialOrder_128 ∷ T_PreMetric_98 → T_IsPartialOrder_248 Source #

d_isPreorder_130 ∷ T_PreMetric_98 → T_IsPreorder_76 Source #

d_isProtoMetric_132 ∷ T_PreMetric_98 → T_IsProtoMetric_30 Source #

d_nonNegative_134 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_136 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → Integer → T__'8804'__22 Source #

du_refl_136 ∷ T_PreMetric_98 → Integer → T__'8804'__22 Source #

d_reflexive_138 ∷ T_PreMetric_98 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_trans_140 ∷ T_PreMetric_98 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_142 ∷ T_PreMetric_98 → T_IsEquivalence_28 Source #

d_'8776''8658'0_144 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_146 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_146 ∷ T_PreMetric_98 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_148 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'691''45''8776'_148 ∷ T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8764''45'resp'737''45''8776'_150 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'737''45''8776'_150 ∷ T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'45''8776'_152 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_152 ∷ T_PreMetric_98 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_154 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'691''45''8776'_154 ∷ T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'737''45''8776'_156 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'737''45''8776'_156 ∷ T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_isPartialEquivalence_160 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_160 ∷ T_PreMetric_98 → T_IsPartialEquivalence_16 Source #

d_refl_162 ∷ T_PreMetric_98 → AgdaAny → AgdaAny Source #

d_reflexive_164 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_164 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_166 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_168 ∷ T_PreMetric_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_172 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_172 ∷ T_PreMetric_98 → T_IsPartialEquivalence_16 Source #

d_refl_174 ∷ T_PreMetric_98 → Integer → T__'8801'__12 Source #

d_reflexive_176 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_178 ∷ T_PreMetric_98 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_180 ∷ T_PreMetric_98 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_protoMetric_182 ∷ T_Level_18 → T_Level_18 → T_PreMetric_98 → T_ProtoMetric_12 Source #

du_protoMetric_182 ∷ T_PreMetric_98 → T_ProtoMetric_12 Source #

d_QuasiSemiMetric_190 ∷ p → p → () Source #

data T_QuasiSemiMetric_190 Source #

d_Carrier_204 ∷ T_QuasiSemiMetric_190 → () Source #

d__'8776'__206 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → () Source #

d_d_208 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → Integer Source #

d_isQuasiSemiMetric_210 ∷ T_QuasiSemiMetric_190 → T_IsQuasiSemiMetric_178 Source #

d_0'8658''8776'_214 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_216 ∷ T_QuasiSemiMetric_190 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_218 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_220 ∷ T_QuasiSemiMetric_190 → T_IsEquivalence_28 Source #

d_isPartialOrder_222 ∷ T_QuasiSemiMetric_190 → T_IsPartialOrder_248 Source #

d_isPreMetric_224 ∷ T_QuasiSemiMetric_190 → T_IsPreMetric_104 Source #

d_isPreorder_226 ∷ T_QuasiSemiMetric_190 → T_IsPreorder_76 Source #

d_isProtoMetric_228 ∷ T_QuasiSemiMetric_190 → T_IsProtoMetric_30 Source #

d_nonNegative_230 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_232 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → Integer → T__'8804'__22 Source #

du_refl_232 ∷ T_QuasiSemiMetric_190 → Integer → T__'8804'__22 Source #

d_reflexive_234 ∷ T_QuasiSemiMetric_190 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_trans_236 ∷ T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_238 ∷ T_QuasiSemiMetric_190 → T_IsEquivalence_28 Source #

d_'8776''8658'0_240 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_242 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_242 ∷ T_QuasiSemiMetric_190 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_244 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'691''45''8776'_244 ∷ T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8764''45'resp'737''45''8776'_246 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'737''45''8776'_246 ∷ T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'45''8776'_248 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_248 ∷ T_QuasiSemiMetric_190 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_250 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'691''45''8776'_250 ∷ T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'737''45''8776'_252 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'737''45''8776'_252 ∷ T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_isPartialEquivalence_256 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_256 ∷ T_QuasiSemiMetric_190 → T_IsPartialEquivalence_16 Source #

d_refl_258 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny Source #

d_reflexive_260 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_260 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_262 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_264 ∷ T_QuasiSemiMetric_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_268 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_268 ∷ T_QuasiSemiMetric_190 → T_IsPartialEquivalence_16 Source #

d_refl_270 ∷ T_QuasiSemiMetric_190 → Integer → T__'8801'__12 Source #

d_reflexive_272 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_274 ∷ T_QuasiSemiMetric_190 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_276 ∷ T_QuasiSemiMetric_190 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_preMetric_278 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → T_PreMetric_98 Source #

du_preMetric_278 ∷ T_QuasiSemiMetric_190 → T_PreMetric_98 Source #

d_protoMetric_282 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_190 → T_ProtoMetric_12 Source #

du_protoMetric_282 ∷ T_QuasiSemiMetric_190 → T_ProtoMetric_12 Source #

d_SemiMetric_290 ∷ p → p → () Source #

data T_SemiMetric_290 Source #

d_Carrier_304 ∷ T_SemiMetric_290 → () Source #

d__'8776'__306 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → () Source #

d_d_308 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → Integer Source #

d_isSemiMetric_310 ∷ T_SemiMetric_290 → T_IsSemiMetric_256 Source #

d_0'8658''8776'_314 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_316 ∷ T_SemiMetric_290 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_318 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_320 ∷ T_SemiMetric_290 → T_IsEquivalence_28 Source #

d_isPartialOrder_322 ∷ T_SemiMetric_290 → T_IsPartialOrder_248 Source #

d_isPreMetric_324 ∷ T_SemiMetric_290 → T_IsPreMetric_104 Source #

d_isPreorder_326 ∷ T_SemiMetric_290 → T_IsPreorder_76 Source #

d_isProtoMetric_328 ∷ T_SemiMetric_290 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_330 ∷ T_SemiMetric_290 → T_IsQuasiSemiMetric_178 Source #

d_nonNegative_332 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_334 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → Integer → T__'8804'__22 Source #

du_refl_334 ∷ T_SemiMetric_290 → Integer → T__'8804'__22 Source #

d_reflexive_336 ∷ T_SemiMetric_290 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_sym_338 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_340 ∷ T_SemiMetric_290 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_342 ∷ T_SemiMetric_290 → T_IsEquivalence_28 Source #

d_'8776''8658'0_344 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_346 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_346 ∷ T_SemiMetric_290 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_348 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'691''45''8776'_348 ∷ T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8764''45'resp'737''45''8776'_350 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'737''45''8776'_350 ∷ T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'45''8776'_352 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_352 ∷ T_SemiMetric_290 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_354 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'691''45''8776'_354 ∷ T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'737''45''8776'_356 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'737''45''8776'_356 ∷ T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_isPartialEquivalence_360 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_360 ∷ T_SemiMetric_290 → T_IsPartialEquivalence_16 Source #

d_refl_362 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny Source #

d_reflexive_364 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_364 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_366 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_368 ∷ T_SemiMetric_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_372 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_372 ∷ T_SemiMetric_290 → T_IsPartialEquivalence_16 Source #

d_refl_374 ∷ T_SemiMetric_290 → Integer → T__'8801'__12 Source #

d_reflexive_376 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_378 ∷ T_SemiMetric_290 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_380 ∷ T_SemiMetric_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_quasiSemiMetric_382 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_QuasiSemiMetric_190 Source #

du_quasiSemiMetric_382 ∷ T_SemiMetric_290 → T_QuasiSemiMetric_190 Source #

d_preMetric_386 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_PreMetric_98 Source #

du_preMetric_386 ∷ T_SemiMetric_290 → T_PreMetric_98 Source #

d_protoMetric_388 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_290 → T_ProtoMetric_12 Source #

du_protoMetric_388 ∷ T_SemiMetric_290 → T_ProtoMetric_12 Source #

d_Metric_396 ∷ p → p → () Source #

data T_Metric_396 Source #

d_Carrier_410 ∷ T_Metric_396 → () Source #

d__'8776'__412 ∷ T_Metric_396 → AgdaAny → AgdaAny → () Source #

d_d_414 ∷ T_Metric_396 → AgdaAny → AgdaAny → Integer Source #

d_isMetric_416 ∷ T_Metric_396 → T_IsGeneralMetric_340 Source #

d_0'8658''8776'_420 ∷ T_Metric_396 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_422 ∷ T_Metric_396 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_424 ∷ T_Metric_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_426 ∷ T_Metric_396 → T_IsEquivalence_28 Source #

d_isPartialOrder_428 ∷ T_Metric_396 → T_IsPartialOrder_248 Source #

d_isPreMetric_430 ∷ T_Metric_396 → T_IsPreMetric_104 Source #

d_isPreorder_432 ∷ T_Metric_396 → T_IsPreorder_76 Source #

d_isProtoMetric_434 ∷ T_Metric_396 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_436 ∷ T_Metric_396 → T_IsQuasiSemiMetric_178 Source #

d_isSemiMetric_438 ∷ T_Metric_396 → T_IsSemiMetric_256 Source #

d_nonNegative_440 ∷ T_Metric_396 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_442 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → Integer → T__'8804'__22 Source #

du_refl_442 ∷ T_Metric_396 → Integer → T__'8804'__22 Source #

d_reflexive_444 ∷ T_Metric_396 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_sym_446 ∷ T_Metric_396 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_448 ∷ T_Metric_396 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_triangle_450 ∷ T_Metric_396 → AgdaAny → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_'8776''45'isEquivalence_452 ∷ T_Metric_396 → T_IsEquivalence_28 Source #

d_'8776''8658'0_454 ∷ T_Metric_396 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_456 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_456 ∷ T_Metric_396 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_458 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'691''45''8776'_458 ∷ T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8764''45'resp'737''45''8776'_460 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'737''45''8776'_460 ∷ T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'45''8776'_462 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_462 ∷ T_Metric_396 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_464 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'691''45''8776'_464 ∷ T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'737''45''8776'_466 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'737''45''8776'_466 ∷ T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_isPartialEquivalence_470 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_470 ∷ T_Metric_396 → T_IsPartialEquivalence_16 Source #

d_refl_472 ∷ T_Metric_396 → AgdaAny → AgdaAny Source #

d_reflexive_474 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_474 ∷ T_Metric_396 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_476 ∷ T_Metric_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_478 ∷ T_Metric_396 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_482 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_482 ∷ T_Metric_396 → T_IsPartialEquivalence_16 Source #

d_refl_484 ∷ T_Metric_396 → Integer → T__'8801'__12 Source #

d_reflexive_486 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_488 ∷ T_Metric_396 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_490 ∷ T_Metric_396 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_semiMetric_492 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_SemiMetric_290 Source #

du_semiMetric_492 ∷ T_Metric_396 → T_SemiMetric_290 Source #

d_preMetric_496 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_PreMetric_98 Source #

du_preMetric_496 ∷ T_Metric_396 → T_PreMetric_98 Source #

d_protoMetric_498 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_ProtoMetric_12 Source #

du_protoMetric_498 ∷ T_Metric_396 → T_ProtoMetric_12 Source #

d_quasiSemiMetric_500 ∷ T_Level_18 → T_Level_18 → T_Metric_396 → T_QuasiSemiMetric_190 Source #

du_quasiSemiMetric_500 ∷ T_Metric_396 → T_QuasiSemiMetric_190 Source #

d_UltraMetric_508 ∷ p → p → () Source #

data T_UltraMetric_508 Source #

d_Carrier_522 ∷ T_UltraMetric_508 → () Source #

d__'8776'__524 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → () Source #

d_d_526 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → Integer Source #

d_isUltraMetric_528 ∷ T_UltraMetric_508 → T_IsGeneralMetric_340 Source #

d_0'8658''8776'_532 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_534 ∷ T_UltraMetric_508 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_536 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_538 ∷ T_UltraMetric_508 → T_IsEquivalence_28 Source #

d_isPartialOrder_540 ∷ T_UltraMetric_508 → T_IsPartialOrder_248 Source #

d_isPreMetric_542 ∷ T_UltraMetric_508 → T_IsPreMetric_104 Source #

d_isPreorder_544 ∷ T_UltraMetric_508 → T_IsPreorder_76 Source #

d_isProtoMetric_546 ∷ T_UltraMetric_508 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_548 ∷ T_UltraMetric_508 → T_IsQuasiSemiMetric_178 Source #

d_isSemiMetric_550 ∷ T_UltraMetric_508 → T_IsSemiMetric_256 Source #

d_nonNegative_552 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_554 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → Integer → T__'8804'__22 Source #

du_refl_554 ∷ T_UltraMetric_508 → Integer → T__'8804'__22 Source #

d_reflexive_556 ∷ T_UltraMetric_508 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_sym_558 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_560 ∷ T_UltraMetric_508 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_triangle_562 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_'8776''45'isEquivalence_564 ∷ T_UltraMetric_508 → T_IsEquivalence_28 Source #

d_'8776''8658'0_566 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_568 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_568 ∷ T_UltraMetric_508 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_570 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'691''45''8776'_570 ∷ T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8764''45'resp'737''45''8776'_572 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8764''45'resp'737''45''8776'_572 ∷ T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'45''8776'_574 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_574 ∷ T_UltraMetric_508 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_576 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'691''45''8776'_576 ∷ T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_'8818''45'resp'737''45''8776'_578 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'8818''45'resp'737''45''8776'_578 ∷ T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

d_isPartialEquivalence_582 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_582 ∷ T_UltraMetric_508 → T_IsPartialEquivalence_16 Source #

d_refl_584 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny Source #

d_reflexive_586 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_586 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_588 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_590 ∷ T_UltraMetric_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_594 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_594 ∷ T_UltraMetric_508 → T_IsPartialEquivalence_16 Source #

d_refl_596 ∷ T_UltraMetric_508 → Integer → T__'8801'__12 Source #

d_reflexive_598 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_600 ∷ T_UltraMetric_508 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_602 ∷ T_UltraMetric_508 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_semiMetric_604 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_SemiMetric_290 Source #

du_semiMetric_604 ∷ T_UltraMetric_508 → T_SemiMetric_290 Source #

d_preMetric_608 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_PreMetric_98 Source #

du_preMetric_608 ∷ T_UltraMetric_508 → T_PreMetric_98 Source #

d_protoMetric_610 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_ProtoMetric_12 Source #

du_protoMetric_610 ∷ T_UltraMetric_508 → T_ProtoMetric_12 Source #

d_quasiSemiMetric_612 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_508 → T_QuasiSemiMetric_190 Source #

du_quasiSemiMetric_612 ∷ T_UltraMetric_508 → T_QuasiSemiMetric_190 Source #