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'__18 → T__'8804'__18 → 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_26 Source #

d_isPartialOrder_42 ∷ T_ProtoMetric_12 → T_IsPartialOrder_162 Source #

d_isPreorder_44 ∷ T_ProtoMetric_12 → T_IsPreorder_70 Source #

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

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

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

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

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

d_'8776''45'isEquivalence_54 ∷ T_ProtoMetric_12 → T_IsEquivalence_26 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'__18 → T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_58 ∷ T_ProtoMetric_12 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 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'__18 → T__'8804'__18 Source #

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

d_isPartialEquivalence_64 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_64 ∷ T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

d_refl_66 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny Source #

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

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

d_sym_70 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_72 ∷ T_ProtoMetric_12 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_76 ∷ T_Level_18 → T_Level_18 → T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_76 ∷ T_ProtoMetric_12 → T_IsPartialEquivalence_16 Source #

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

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

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

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

d_PreMetric_90 ∷ p → p → () Source #

data T_PreMetric_90 Source #

d_Carrier_104 ∷ T_PreMetric_90 → () Source #

d__'8776'__106 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → () Source #

d_d_108 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → Integer Source #

d_isPreMetric_110 ∷ T_PreMetric_90 → T_IsPreMetric_96 Source #

d_antisym_114 ∷ T_PreMetric_90 → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 Source #

d_cong_116 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_118 ∷ T_PreMetric_90 → T_IsEquivalence_26 Source #

d_isPartialOrder_120 ∷ T_PreMetric_90 → T_IsPartialOrder_162 Source #

d_isPreorder_122 ∷ T_PreMetric_90 → T_IsPreorder_70 Source #

d_isProtoMetric_124 ∷ T_PreMetric_90 → T_IsProtoMetric_30 Source #

d_nonNegative_126 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_refl_128 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → Integer → T__'8804'__18 Source #

du_refl_128 ∷ T_PreMetric_90 → Integer → T__'8804'__18 Source #

d_reflexive_130 ∷ T_PreMetric_90 → Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_trans_132 ∷ T_PreMetric_90 → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8776''45'isEquivalence_134 ∷ T_PreMetric_90 → T_IsEquivalence_26 Source #

d_'8776''8658'0_136 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_138 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_138 ∷ T_PreMetric_90 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_140 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_140 ∷ T_PreMetric_90 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_142 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_142 ∷ T_PreMetric_90 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_isPartialEquivalence_146 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_146 ∷ T_PreMetric_90 → T_IsPartialEquivalence_16 Source #

d_refl_148 ∷ T_PreMetric_90 → AgdaAny → AgdaAny Source #

d_reflexive_150 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_150 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_152 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_154 ∷ T_PreMetric_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_158 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_158 ∷ T_PreMetric_90 → T_IsPartialEquivalence_16 Source #

d_refl_160 ∷ T_PreMetric_90 → Integer → T__'8801'__12 Source #

d_reflexive_162 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_164 ∷ T_PreMetric_90 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_166 ∷ T_PreMetric_90 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_protoMetric_168 ∷ T_Level_18 → T_Level_18 → T_PreMetric_90 → T_ProtoMetric_12 Source #

du_protoMetric_168 ∷ T_PreMetric_90 → T_ProtoMetric_12 Source #

d_QuasiSemiMetric_174 ∷ p → p → () Source #

data T_QuasiSemiMetric_174 Source #

d_Carrier_188 ∷ T_QuasiSemiMetric_174 → () Source #

d__'8776'__190 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → () Source #

d_d_192 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → Integer Source #

d_isQuasiSemiMetric_194 ∷ T_QuasiSemiMetric_174 → T_IsQuasiSemiMetric_162 Source #

d_0'8658''8776'_198 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_200 ∷ T_QuasiSemiMetric_174 → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 Source #

d_cong_202 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_204 ∷ T_QuasiSemiMetric_174 → T_IsEquivalence_26 Source #

d_isPartialOrder_206 ∷ T_QuasiSemiMetric_174 → T_IsPartialOrder_162 Source #

d_isPreMetric_208 ∷ T_QuasiSemiMetric_174 → T_IsPreMetric_96 Source #

d_isPreorder_210 ∷ T_QuasiSemiMetric_174 → T_IsPreorder_70 Source #

d_isProtoMetric_212 ∷ T_QuasiSemiMetric_174 → T_IsProtoMetric_30 Source #

d_nonNegative_214 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_refl_216 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → Integer → T__'8804'__18 Source #

du_refl_216 ∷ T_QuasiSemiMetric_174 → Integer → T__'8804'__18 Source #

d_reflexive_218 ∷ T_QuasiSemiMetric_174 → Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_trans_220 ∷ T_QuasiSemiMetric_174 → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8776''45'isEquivalence_222 ∷ T_QuasiSemiMetric_174 → T_IsEquivalence_26 Source #

d_'8776''8658'0_224 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_226 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_226 ∷ T_QuasiSemiMetric_174 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_228 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_228 ∷ T_QuasiSemiMetric_174 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_230 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_230 ∷ T_QuasiSemiMetric_174 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_isPartialEquivalence_234 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_234 ∷ T_QuasiSemiMetric_174 → T_IsPartialEquivalence_16 Source #

d_refl_236 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny Source #

d_reflexive_238 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_238 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_240 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_242 ∷ T_QuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_246 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_246 ∷ T_QuasiSemiMetric_174 → T_IsPartialEquivalence_16 Source #

d_refl_248 ∷ T_QuasiSemiMetric_174 → Integer → T__'8801'__12 Source #

d_reflexive_250 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_252 ∷ T_QuasiSemiMetric_174 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_254 ∷ T_QuasiSemiMetric_174 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_preMetric_256 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → T_PreMetric_90 Source #

du_preMetric_256 ∷ T_QuasiSemiMetric_174 → T_PreMetric_90 Source #

d_protoMetric_260 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_174 → T_ProtoMetric_12 Source #

du_protoMetric_260 ∷ T_QuasiSemiMetric_174 → T_ProtoMetric_12 Source #

d_SemiMetric_266 ∷ p → p → () Source #

data T_SemiMetric_266 Source #

d_Carrier_280 ∷ T_SemiMetric_266 → () Source #

d__'8776'__282 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → () Source #

d_d_284 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → Integer Source #

d_isSemiMetric_286 ∷ T_SemiMetric_266 → T_IsSemiMetric_232 Source #

d_0'8658''8776'_290 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_292 ∷ T_SemiMetric_266 → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 Source #

d_cong_294 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_296 ∷ T_SemiMetric_266 → T_IsEquivalence_26 Source #

d_isPartialOrder_298 ∷ T_SemiMetric_266 → T_IsPartialOrder_162 Source #

d_isPreMetric_300 ∷ T_SemiMetric_266 → T_IsPreMetric_96 Source #

d_isPreorder_302 ∷ T_SemiMetric_266 → T_IsPreorder_70 Source #

d_isProtoMetric_304 ∷ T_SemiMetric_266 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_306 ∷ T_SemiMetric_266 → T_IsQuasiSemiMetric_162 Source #

d_nonNegative_308 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_refl_310 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → Integer → T__'8804'__18 Source #

du_refl_310 ∷ T_SemiMetric_266 → Integer → T__'8804'__18 Source #

d_reflexive_312 ∷ T_SemiMetric_266 → Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_sym_314 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_316 ∷ T_SemiMetric_266 → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8776''45'isEquivalence_318 ∷ T_SemiMetric_266 → T_IsEquivalence_26 Source #

d_'8776''8658'0_320 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_322 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_322 ∷ T_SemiMetric_266 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_324 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_324 ∷ T_SemiMetric_266 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_326 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_326 ∷ T_SemiMetric_266 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_isPartialEquivalence_330 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_330 ∷ T_SemiMetric_266 → T_IsPartialEquivalence_16 Source #

d_refl_332 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny Source #

d_reflexive_334 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_334 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_336 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_338 ∷ T_SemiMetric_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_342 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_342 ∷ T_SemiMetric_266 → T_IsPartialEquivalence_16 Source #

d_refl_344 ∷ T_SemiMetric_266 → Integer → T__'8801'__12 Source #

d_reflexive_346 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_348 ∷ T_SemiMetric_266 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_350 ∷ T_SemiMetric_266 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_quasiSemiMetric_352 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → T_QuasiSemiMetric_174 Source #

du_quasiSemiMetric_352 ∷ T_SemiMetric_266 → T_QuasiSemiMetric_174 Source #

d_preMetric_356 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → T_PreMetric_90 Source #

du_preMetric_356 ∷ T_SemiMetric_266 → T_PreMetric_90 Source #

d_protoMetric_358 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_266 → T_ProtoMetric_12 Source #

du_protoMetric_358 ∷ T_SemiMetric_266 → T_ProtoMetric_12 Source #

d_Metric_364 ∷ p → p → () Source #

data T_Metric_364 Source #

d_Carrier_378 ∷ T_Metric_364 → () Source #

d__'8776'__380 ∷ T_Metric_364 → AgdaAny → AgdaAny → () Source #

d_d_382 ∷ T_Metric_364 → AgdaAny → AgdaAny → Integer Source #

d_isMetric_384 ∷ T_Metric_364 → T_IsGeneralMetric_308 Source #

d_0'8658''8776'_388 ∷ T_Metric_364 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_390 ∷ T_Metric_364 → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 Source #

d_cong_392 ∷ T_Metric_364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_394 ∷ T_Metric_364 → T_IsEquivalence_26 Source #

d_isPartialOrder_396 ∷ T_Metric_364 → T_IsPartialOrder_162 Source #

d_isPreMetric_398 ∷ T_Metric_364 → T_IsPreMetric_96 Source #

d_isPreorder_400 ∷ T_Metric_364 → T_IsPreorder_70 Source #

d_isProtoMetric_402 ∷ T_Metric_364 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_404 ∷ T_Metric_364 → T_IsQuasiSemiMetric_162 Source #

d_isSemiMetric_406 ∷ T_Metric_364 → T_IsSemiMetric_232 Source #

d_nonNegative_408 ∷ T_Metric_364 → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_refl_410 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → Integer → T__'8804'__18 Source #

du_refl_410 ∷ T_Metric_364 → Integer → T__'8804'__18 Source #

d_reflexive_412 ∷ T_Metric_364 → Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_sym_414 ∷ T_Metric_364 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_416 ∷ T_Metric_364 → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_triangle_418 ∷ T_Metric_364 → AgdaAny → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_'8776''45'isEquivalence_420 ∷ T_Metric_364 → T_IsEquivalence_26 Source #

d_'8776''8658'0_422 ∷ T_Metric_364 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_424 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_424 ∷ T_Metric_364 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_426 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_426 ∷ T_Metric_364 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_428 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_428 ∷ T_Metric_364 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_isPartialEquivalence_432 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_432 ∷ T_Metric_364 → T_IsPartialEquivalence_16 Source #

d_refl_434 ∷ T_Metric_364 → AgdaAny → AgdaAny Source #

d_reflexive_436 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_436 ∷ T_Metric_364 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_438 ∷ T_Metric_364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_440 ∷ T_Metric_364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_444 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_444 ∷ T_Metric_364 → T_IsPartialEquivalence_16 Source #

d_refl_446 ∷ T_Metric_364 → Integer → T__'8801'__12 Source #

d_reflexive_448 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_450 ∷ T_Metric_364 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_452 ∷ T_Metric_364 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_semiMetric_454 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_SemiMetric_266 Source #

du_semiMetric_454 ∷ T_Metric_364 → T_SemiMetric_266 Source #

d_preMetric_458 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_PreMetric_90 Source #

du_preMetric_458 ∷ T_Metric_364 → T_PreMetric_90 Source #

d_protoMetric_460 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_ProtoMetric_12 Source #

du_protoMetric_460 ∷ T_Metric_364 → T_ProtoMetric_12 Source #

d_quasiSemiMetric_462 ∷ T_Level_18 → T_Level_18 → T_Metric_364 → T_QuasiSemiMetric_174 Source #

du_quasiSemiMetric_462 ∷ T_Metric_364 → T_QuasiSemiMetric_174 Source #

d_UltraMetric_468 ∷ p → p → () Source #

data T_UltraMetric_468 Source #

d_Carrier_482 ∷ T_UltraMetric_468 → () Source #

d__'8776'__484 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → () Source #

d_d_486 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → Integer Source #

d_isUltraMetric_488 ∷ T_UltraMetric_468 → T_IsGeneralMetric_308 Source #

d_0'8658''8776'_492 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_494 ∷ T_UltraMetric_468 → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 Source #

d_cong_496 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_498 ∷ T_UltraMetric_468 → T_IsEquivalence_26 Source #

d_isPartialOrder_500 ∷ T_UltraMetric_468 → T_IsPartialOrder_162 Source #

d_isPreMetric_502 ∷ T_UltraMetric_468 → T_IsPreMetric_96 Source #

d_isPreorder_504 ∷ T_UltraMetric_468 → T_IsPreorder_70 Source #

d_isProtoMetric_506 ∷ T_UltraMetric_468 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_508 ∷ T_UltraMetric_468 → T_IsQuasiSemiMetric_162 Source #

d_isSemiMetric_510 ∷ T_UltraMetric_468 → T_IsSemiMetric_232 Source #

d_nonNegative_512 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_refl_514 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → Integer → T__'8804'__18 Source #

du_refl_514 ∷ T_UltraMetric_468 → Integer → T__'8804'__18 Source #

d_reflexive_516 ∷ T_UltraMetric_468 → Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_sym_518 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_520 ∷ T_UltraMetric_468 → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_triangle_522 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → AgdaAny → T__'8804'__18 Source #

d_'8776''45'isEquivalence_524 ∷ T_UltraMetric_468 → T_IsEquivalence_26 Source #

d_'8776''8658'0_526 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_528 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_528 ∷ T_UltraMetric_468 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_530 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_530 ∷ T_UltraMetric_468 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_532 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_532 ∷ T_UltraMetric_468 → Integer → Integer → Integer → T__'8801'__12 → T__'8804'__18 → T__'8804'__18 Source #

d_isPartialEquivalence_536 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_536 ∷ T_UltraMetric_468 → T_IsPartialEquivalence_16 Source #

d_refl_538 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny Source #

d_reflexive_540 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_540 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_542 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_544 ∷ T_UltraMetric_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_548 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_548 ∷ T_UltraMetric_468 → T_IsPartialEquivalence_16 Source #

d_refl_550 ∷ T_UltraMetric_468 → Integer → T__'8801'__12 Source #

d_reflexive_552 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_554 ∷ T_UltraMetric_468 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_556 ∷ T_UltraMetric_468 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_semiMetric_558 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_SemiMetric_266 Source #

du_semiMetric_558 ∷ T_UltraMetric_468 → T_SemiMetric_266 Source #

d_preMetric_562 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_PreMetric_90 Source #

du_preMetric_562 ∷ T_UltraMetric_468 → T_PreMetric_90 Source #

d_protoMetric_564 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_ProtoMetric_12 Source #

du_protoMetric_564 ∷ T_UltraMetric_468 → T_ProtoMetric_12 Source #

d_quasiSemiMetric_566 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_468 → T_QuasiSemiMetric_174 Source #

du_quasiSemiMetric_566 ∷ T_UltraMetric_468 → T_QuasiSemiMetric_174 Source #