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_26 Source #

d_isPartialOrder_42 ∷ T_ProtoMetric_12 → T_IsPartialOrder_174 Source #

d_isPreorder_44 ∷ T_ProtoMetric_12 → T_IsPreorder_70 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_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'__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_96 ∷ p → p → () Source #

data T_PreMetric_96 Source #

d_Carrier_110 ∷ T_PreMetric_96 → () Source #

d__'8776'__112 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → () Source #

d_d_114 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → Integer Source #

d_isPreMetric_116 ∷ T_PreMetric_96 → T_IsPreMetric_102 Source #

d_antisym_120 ∷ T_PreMetric_96 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_122 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_124 ∷ T_PreMetric_96 → T_IsEquivalence_26 Source #

d_isPartialOrder_126 ∷ T_PreMetric_96 → T_IsPartialOrder_174 Source #

d_isPreorder_128 ∷ T_PreMetric_96 → T_IsPreorder_70 Source #

d_isProtoMetric_130 ∷ T_PreMetric_96 → T_IsProtoMetric_30 Source #

d_nonNegative_132 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_134 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → Integer → T__'8804'__22 Source #

du_refl_134 ∷ T_PreMetric_96 → Integer → T__'8804'__22 Source #

d_reflexive_136 ∷ T_PreMetric_96 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_trans_138 ∷ T_PreMetric_96 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_140 ∷ T_PreMetric_96 → T_IsEquivalence_26 Source #

d_'8776''8658'0_142 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_144 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_144 ∷ T_PreMetric_96 → T_Σ_14 Source #

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

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

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

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

d_'8818''45'resp'45''8776'_150 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_150 ∷ T_PreMetric_96 → T_Σ_14 Source #

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

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

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

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

d_isPartialEquivalence_158 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_158 ∷ T_PreMetric_96 → T_IsPartialEquivalence_16 Source #

d_refl_160 ∷ T_PreMetric_96 → AgdaAny → AgdaAny Source #

d_reflexive_162 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_162 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_164 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_166 ∷ T_PreMetric_96 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_170 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_170 ∷ T_PreMetric_96 → T_IsPartialEquivalence_16 Source #

d_refl_172 ∷ T_PreMetric_96 → Integer → T__'8801'__12 Source #

d_reflexive_174 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_176 ∷ T_PreMetric_96 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_178 ∷ T_PreMetric_96 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_protoMetric_180 ∷ T_Level_18 → T_Level_18 → T_PreMetric_96 → T_ProtoMetric_12 Source #

du_protoMetric_180 ∷ T_PreMetric_96 → T_ProtoMetric_12 Source #

d_QuasiSemiMetric_186 ∷ p → p → () Source #

data T_QuasiSemiMetric_186 Source #

d_Carrier_200 ∷ T_QuasiSemiMetric_186 → () Source #

d__'8776'__202 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → () Source #

d_d_204 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → Integer Source #

d_isQuasiSemiMetric_206 ∷ T_QuasiSemiMetric_186 → T_IsQuasiSemiMetric_174 Source #

d_0'8658''8776'_210 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_212 ∷ T_QuasiSemiMetric_186 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_214 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_216 ∷ T_QuasiSemiMetric_186 → T_IsEquivalence_26 Source #

d_isPartialOrder_218 ∷ T_QuasiSemiMetric_186 → T_IsPartialOrder_174 Source #

d_isPreMetric_220 ∷ T_QuasiSemiMetric_186 → T_IsPreMetric_102 Source #

d_isPreorder_222 ∷ T_QuasiSemiMetric_186 → T_IsPreorder_70 Source #

d_isProtoMetric_224 ∷ T_QuasiSemiMetric_186 → T_IsProtoMetric_30 Source #

d_nonNegative_226 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_228 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → Integer → T__'8804'__22 Source #

du_refl_228 ∷ T_QuasiSemiMetric_186 → Integer → T__'8804'__22 Source #

d_reflexive_230 ∷ T_QuasiSemiMetric_186 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_trans_232 ∷ T_QuasiSemiMetric_186 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_234 ∷ T_QuasiSemiMetric_186 → T_IsEquivalence_26 Source #

d_'8776''8658'0_236 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_238 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_238 ∷ T_QuasiSemiMetric_186 → T_Σ_14 Source #

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

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

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

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

d_'8818''45'resp'45''8776'_244 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_244 ∷ T_QuasiSemiMetric_186 → T_Σ_14 Source #

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

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

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

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

d_isPartialEquivalence_252 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_252 ∷ T_QuasiSemiMetric_186 → T_IsPartialEquivalence_16 Source #

d_refl_254 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny Source #

d_reflexive_256 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_256 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_258 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_260 ∷ T_QuasiSemiMetric_186 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_264 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_264 ∷ T_QuasiSemiMetric_186 → T_IsPartialEquivalence_16 Source #

d_refl_266 ∷ T_QuasiSemiMetric_186 → Integer → T__'8801'__12 Source #

d_reflexive_268 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_270 ∷ T_QuasiSemiMetric_186 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_272 ∷ T_QuasiSemiMetric_186 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_preMetric_274 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → T_PreMetric_96 Source #

du_preMetric_274 ∷ T_QuasiSemiMetric_186 → T_PreMetric_96 Source #

d_protoMetric_278 ∷ T_Level_18 → T_Level_18 → T_QuasiSemiMetric_186 → T_ProtoMetric_12 Source #

du_protoMetric_278 ∷ T_QuasiSemiMetric_186 → T_ProtoMetric_12 Source #

d_SemiMetric_284 ∷ p → p → () Source #

data T_SemiMetric_284 Source #

d_Carrier_298 ∷ T_SemiMetric_284 → () Source #

d__'8776'__300 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → () Source #

d_d_302 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → Integer Source #

d_isSemiMetric_304 ∷ T_SemiMetric_284 → T_IsSemiMetric_250 Source #

d_0'8658''8776'_308 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_310 ∷ T_SemiMetric_284 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_312 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_314 ∷ T_SemiMetric_284 → T_IsEquivalence_26 Source #

d_isPartialOrder_316 ∷ T_SemiMetric_284 → T_IsPartialOrder_174 Source #

d_isPreMetric_318 ∷ T_SemiMetric_284 → T_IsPreMetric_102 Source #

d_isPreorder_320 ∷ T_SemiMetric_284 → T_IsPreorder_70 Source #

d_isProtoMetric_322 ∷ T_SemiMetric_284 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_324 ∷ T_SemiMetric_284 → T_IsQuasiSemiMetric_174 Source #

d_nonNegative_326 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_328 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → Integer → T__'8804'__22 Source #

du_refl_328 ∷ T_SemiMetric_284 → Integer → T__'8804'__22 Source #

d_reflexive_330 ∷ T_SemiMetric_284 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_sym_332 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_334 ∷ T_SemiMetric_284 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8776''45'isEquivalence_336 ∷ T_SemiMetric_284 → T_IsEquivalence_26 Source #

d_'8776''8658'0_338 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_340 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_340 ∷ T_SemiMetric_284 → T_Σ_14 Source #

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

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

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

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

d_'8818''45'resp'45''8776'_346 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_346 ∷ T_SemiMetric_284 → T_Σ_14 Source #

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

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

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

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

d_isPartialEquivalence_354 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_354 ∷ T_SemiMetric_284 → T_IsPartialEquivalence_16 Source #

d_refl_356 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny Source #

d_reflexive_358 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_358 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_360 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_362 ∷ T_SemiMetric_284 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_366 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_366 ∷ T_SemiMetric_284 → T_IsPartialEquivalence_16 Source #

d_refl_368 ∷ T_SemiMetric_284 → Integer → T__'8801'__12 Source #

d_reflexive_370 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_372 ∷ T_SemiMetric_284 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_374 ∷ T_SemiMetric_284 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_quasiSemiMetric_376 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_QuasiSemiMetric_186 Source #

du_quasiSemiMetric_376 ∷ T_SemiMetric_284 → T_QuasiSemiMetric_186 Source #

d_preMetric_380 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_PreMetric_96 Source #

du_preMetric_380 ∷ T_SemiMetric_284 → T_PreMetric_96 Source #

d_protoMetric_382 ∷ T_Level_18 → T_Level_18 → T_SemiMetric_284 → T_ProtoMetric_12 Source #

du_protoMetric_382 ∷ T_SemiMetric_284 → T_ProtoMetric_12 Source #

d_Metric_388 ∷ p → p → () Source #

data T_Metric_388 Source #

d_Carrier_402 ∷ T_Metric_388 → () Source #

d__'8776'__404 ∷ T_Metric_388 → AgdaAny → AgdaAny → () Source #

d_d_406 ∷ T_Metric_388 → AgdaAny → AgdaAny → Integer Source #

d_isMetric_408 ∷ T_Metric_388 → T_IsGeneralMetric_332 Source #

d_0'8658''8776'_412 ∷ T_Metric_388 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_414 ∷ T_Metric_388 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_416 ∷ T_Metric_388 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_418 ∷ T_Metric_388 → T_IsEquivalence_26 Source #

d_isPartialOrder_420 ∷ T_Metric_388 → T_IsPartialOrder_174 Source #

d_isPreMetric_422 ∷ T_Metric_388 → T_IsPreMetric_102 Source #

d_isPreorder_424 ∷ T_Metric_388 → T_IsPreorder_70 Source #

d_isProtoMetric_426 ∷ T_Metric_388 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_428 ∷ T_Metric_388 → T_IsQuasiSemiMetric_174 Source #

d_isSemiMetric_430 ∷ T_Metric_388 → T_IsSemiMetric_250 Source #

d_nonNegative_432 ∷ T_Metric_388 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_434 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → Integer → T__'8804'__22 Source #

du_refl_434 ∷ T_Metric_388 → Integer → T__'8804'__22 Source #

d_reflexive_436 ∷ T_Metric_388 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_sym_438 ∷ T_Metric_388 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_440 ∷ T_Metric_388 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_triangle_442 ∷ T_Metric_388 → AgdaAny → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_'8776''45'isEquivalence_444 ∷ T_Metric_388 → T_IsEquivalence_26 Source #

d_'8776''8658'0_446 ∷ T_Metric_388 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_448 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_448 ∷ T_Metric_388 → T_Σ_14 Source #

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

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

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

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

d_'8818''45'resp'45''8776'_454 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_454 ∷ T_Metric_388 → T_Σ_14 Source #

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

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

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

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

d_isPartialEquivalence_462 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_462 ∷ T_Metric_388 → T_IsPartialEquivalence_16 Source #

d_refl_464 ∷ T_Metric_388 → AgdaAny → AgdaAny Source #

d_reflexive_466 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_466 ∷ T_Metric_388 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_468 ∷ T_Metric_388 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_470 ∷ T_Metric_388 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_474 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_474 ∷ T_Metric_388 → T_IsPartialEquivalence_16 Source #

d_refl_476 ∷ T_Metric_388 → Integer → T__'8801'__12 Source #

d_reflexive_478 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_480 ∷ T_Metric_388 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_482 ∷ T_Metric_388 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_semiMetric_484 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_SemiMetric_284 Source #

du_semiMetric_484 ∷ T_Metric_388 → T_SemiMetric_284 Source #

d_preMetric_488 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_PreMetric_96 Source #

du_preMetric_488 ∷ T_Metric_388 → T_PreMetric_96 Source #

d_protoMetric_490 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_ProtoMetric_12 Source #

du_protoMetric_490 ∷ T_Metric_388 → T_ProtoMetric_12 Source #

d_quasiSemiMetric_492 ∷ T_Level_18 → T_Level_18 → T_Metric_388 → T_QuasiSemiMetric_186 Source #

du_quasiSemiMetric_492 ∷ T_Metric_388 → T_QuasiSemiMetric_186 Source #

d_UltraMetric_498 ∷ p → p → () Source #

data T_UltraMetric_498 Source #

d_Carrier_512 ∷ T_UltraMetric_498 → () Source #

d__'8776'__514 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → () Source #

d_d_516 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → Integer Source #

d_isUltraMetric_518 ∷ T_UltraMetric_498 → T_IsGeneralMetric_332 Source #

d_0'8658''8776'_522 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_antisym_524 ∷ T_UltraMetric_498 → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_cong_526 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_isEquivalence_528 ∷ T_UltraMetric_498 → T_IsEquivalence_26 Source #

d_isPartialOrder_530 ∷ T_UltraMetric_498 → T_IsPartialOrder_174 Source #

d_isPreMetric_532 ∷ T_UltraMetric_498 → T_IsPreMetric_102 Source #

d_isPreorder_534 ∷ T_UltraMetric_498 → T_IsPreorder_70 Source #

d_isProtoMetric_536 ∷ T_UltraMetric_498 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_538 ∷ T_UltraMetric_498 → T_IsQuasiSemiMetric_174 Source #

d_isSemiMetric_540 ∷ T_UltraMetric_498 → T_IsSemiMetric_250 Source #

d_nonNegative_542 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_refl_544 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → Integer → T__'8804'__22 Source #

du_refl_544 ∷ T_UltraMetric_498 → Integer → T__'8804'__22 Source #

d_reflexive_546 ∷ T_UltraMetric_498 → Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_sym_548 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_trans_550 ∷ T_UltraMetric_498 → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_triangle_552 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → AgdaAny → T__'8804'__22 Source #

d_'8776''45'isEquivalence_554 ∷ T_UltraMetric_498 → T_IsEquivalence_26 Source #

d_'8776''8658'0_556 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_558 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_558 ∷ T_UltraMetric_498 → T_Σ_14 Source #

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

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

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

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

d_'8818''45'resp'45''8776'_564 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_564 ∷ T_UltraMetric_498 → T_Σ_14 Source #

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

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

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

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

d_isPartialEquivalence_572 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_572 ∷ T_UltraMetric_498 → T_IsPartialEquivalence_16 Source #

d_refl_574 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny Source #

d_reflexive_576 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_576 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_578 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_580 ∷ T_UltraMetric_498 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_584 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_584 ∷ T_UltraMetric_498 → T_IsPartialEquivalence_16 Source #

d_refl_586 ∷ T_UltraMetric_498 → Integer → T__'8801'__12 Source #

d_reflexive_588 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_sym_590 ∷ T_UltraMetric_498 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_592 ∷ T_UltraMetric_498 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_semiMetric_594 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_SemiMetric_284 Source #

du_semiMetric_594 ∷ T_UltraMetric_498 → T_SemiMetric_284 Source #

d_preMetric_598 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_PreMetric_96 Source #

du_preMetric_598 ∷ T_UltraMetric_498 → T_PreMetric_96 Source #

d_protoMetric_600 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_ProtoMetric_12 Source #

du_protoMetric_600 ∷ T_UltraMetric_498 → T_ProtoMetric_12 Source #

d_quasiSemiMetric_602 ∷ T_Level_18 → T_Level_18 → T_UltraMetric_498 → T_QuasiSemiMetric_186 Source #

du_quasiSemiMetric_602 ∷ T_UltraMetric_498 → T_QuasiSemiMetric_186 Source #