Documentation

d_ProtoMetric_12 :: p -> p -> () #

data T_ProtoMetric_12 #

d_Carrier_26 :: T_ProtoMetric_12 -> () #

d__'8776'__28 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> () #

d_d_30 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> Integer #

d_isProtoMetric_32 :: T_ProtoMetric_12 -> T_IsProtoMetric_30 #

d_antisym_36 :: T_ProtoMetric_12 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_cong_38 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_isEquivalence_40 :: T_ProtoMetric_12 -> T_IsEquivalence_26 #

d_isPartialOrder_42 :: T_ProtoMetric_12 -> T_IsPartialOrder_174 #

d_isPreorder_44 :: T_ProtoMetric_12 -> T_IsPreorder_70 #

d_nonNegative_46 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_refl_48 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> Integer -> T__'8804'__22 #

du_refl_48 :: T_ProtoMetric_12 -> Integer -> T__'8804'__22 #

d_reflexive_50 :: T_ProtoMetric_12 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_trans_52 :: T_ProtoMetric_12 -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8776''45'isEquivalence_54 :: T_ProtoMetric_12 -> T_IsEquivalence_26 #

d_'8764''45'resp'45''8776'_56 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_56 :: T_ProtoMetric_12 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_58 :: T_ProtoMetric_12 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8764''45'resp'737''45''8776'_60 :: T_ProtoMetric_12 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_'8818''45'resp'45''8776'_62 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_62 :: T_ProtoMetric_12 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_64 :: T_ProtoMetric_12 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8818''45'resp'737''45''8776'_66 :: T_ProtoMetric_12 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_isPartialEquivalence_70 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_70 :: T_ProtoMetric_12 -> T_IsPartialEquivalence_16 #

d_refl_72 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny #

d_reflexive_74 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_74 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_76 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_78 :: T_ProtoMetric_12 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_82 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_82 :: T_ProtoMetric_12 -> T_IsPartialEquivalence_16 #

d_refl_84 :: T_ProtoMetric_12 -> Integer -> T__'8801'__12 #

d_reflexive_86 :: T_Level_18 -> T_Level_18 -> T_ProtoMetric_12 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_sym_88 :: T_ProtoMetric_12 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_trans_90 :: T_ProtoMetric_12 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_PreMetric_96 :: p -> p -> () #

data T_PreMetric_96 #

d_Carrier_110 :: T_PreMetric_96 -> () #

d__'8776'__112 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> () #

d_d_114 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> Integer #

d_isPreMetric_116 :: T_PreMetric_96 -> T_IsPreMetric_102 #

d_antisym_120 :: T_PreMetric_96 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_cong_122 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_isEquivalence_124 :: T_PreMetric_96 -> T_IsEquivalence_26 #

d_isPartialOrder_126 :: T_PreMetric_96 -> T_IsPartialOrder_174 #

d_isPreorder_128 :: T_PreMetric_96 -> T_IsPreorder_70 #

d_isProtoMetric_130 :: T_PreMetric_96 -> T_IsProtoMetric_30 #

d_nonNegative_132 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_refl_134 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> Integer -> T__'8804'__22 #

du_refl_134 :: T_PreMetric_96 -> Integer -> T__'8804'__22 #

d_reflexive_136 :: T_PreMetric_96 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_trans_138 :: T_PreMetric_96 -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8776''45'isEquivalence_140 :: T_PreMetric_96 -> T_IsEquivalence_26 #

d_'8776''8658'0_142 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_'8764''45'resp'45''8776'_144 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_144 :: T_PreMetric_96 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_146 :: T_PreMetric_96 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8764''45'resp'737''45''8776'_148 :: T_PreMetric_96 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_'8818''45'resp'45''8776'_150 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_150 :: T_PreMetric_96 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_152 :: T_PreMetric_96 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8818''45'resp'737''45''8776'_154 :: T_PreMetric_96 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_isPartialEquivalence_158 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_158 :: T_PreMetric_96 -> T_IsPartialEquivalence_16 #

d_refl_160 :: T_PreMetric_96 -> AgdaAny -> AgdaAny #

d_reflexive_162 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_162 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_164 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_166 :: T_PreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_170 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_170 :: T_PreMetric_96 -> T_IsPartialEquivalence_16 #

d_refl_172 :: T_PreMetric_96 -> Integer -> T__'8801'__12 #

d_reflexive_174 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_sym_176 :: T_PreMetric_96 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_trans_178 :: T_PreMetric_96 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_protoMetric_180 :: T_Level_18 -> T_Level_18 -> T_PreMetric_96 -> T_ProtoMetric_12 #

du_protoMetric_180 :: T_PreMetric_96 -> T_ProtoMetric_12 #

d_QuasiSemiMetric_186 :: p -> p -> () #

data T_QuasiSemiMetric_186 #

d_Carrier_200 :: T_QuasiSemiMetric_186 -> () #

d__'8776'__202 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> () #

d_d_204 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> Integer #

d_isQuasiSemiMetric_206 :: T_QuasiSemiMetric_186 -> T_IsQuasiSemiMetric_174 #

d_0'8658''8776'_210 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_antisym_212 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_cong_214 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_isEquivalence_216 :: T_QuasiSemiMetric_186 -> T_IsEquivalence_26 #

d_isPartialOrder_218 :: T_QuasiSemiMetric_186 -> T_IsPartialOrder_174 #

d_isPreMetric_220 :: T_QuasiSemiMetric_186 -> T_IsPreMetric_102 #

d_isPreorder_222 :: T_QuasiSemiMetric_186 -> T_IsPreorder_70 #

d_isProtoMetric_224 :: T_QuasiSemiMetric_186 -> T_IsProtoMetric_30 #

d_nonNegative_226 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_refl_228 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> Integer -> T__'8804'__22 #

du_refl_228 :: T_QuasiSemiMetric_186 -> Integer -> T__'8804'__22 #

d_reflexive_230 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_trans_232 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8776''45'isEquivalence_234 :: T_QuasiSemiMetric_186 -> T_IsEquivalence_26 #

d_'8776''8658'0_236 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_'8764''45'resp'45''8776'_238 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_238 :: T_QuasiSemiMetric_186 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_240 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8764''45'resp'737''45''8776'_242 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_'8818''45'resp'45''8776'_244 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_244 :: T_QuasiSemiMetric_186 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_246 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8818''45'resp'737''45''8776'_248 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_isPartialEquivalence_252 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_252 :: T_QuasiSemiMetric_186 -> T_IsPartialEquivalence_16 #

d_refl_254 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny #

d_reflexive_256 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_256 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_258 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_260 :: T_QuasiSemiMetric_186 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_264 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_264 :: T_QuasiSemiMetric_186 -> T_IsPartialEquivalence_16 #

d_refl_266 :: T_QuasiSemiMetric_186 -> Integer -> T__'8801'__12 #

d_reflexive_268 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_sym_270 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_trans_272 :: T_QuasiSemiMetric_186 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_preMetric_274 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> T_PreMetric_96 #

du_preMetric_274 :: T_QuasiSemiMetric_186 -> T_PreMetric_96 #

d_protoMetric_278 :: T_Level_18 -> T_Level_18 -> T_QuasiSemiMetric_186 -> T_ProtoMetric_12 #

du_protoMetric_278 :: T_QuasiSemiMetric_186 -> T_ProtoMetric_12 #

d_SemiMetric_284 :: p -> p -> () #

data T_SemiMetric_284 #

d_Carrier_298 :: T_SemiMetric_284 -> () #

d__'8776'__300 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> () #

d_d_302 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> Integer #

d_isSemiMetric_304 :: T_SemiMetric_284 -> T_IsSemiMetric_250 #

d_0'8658''8776'_308 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_antisym_310 :: T_SemiMetric_284 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_cong_312 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_isEquivalence_314 :: T_SemiMetric_284 -> T_IsEquivalence_26 #

d_isPartialOrder_316 :: T_SemiMetric_284 -> T_IsPartialOrder_174 #

d_isPreMetric_318 :: T_SemiMetric_284 -> T_IsPreMetric_102 #

d_isPreorder_320 :: T_SemiMetric_284 -> T_IsPreorder_70 #

d_isProtoMetric_322 :: T_SemiMetric_284 -> T_IsProtoMetric_30 #

d_isQuasiSemiMetric_324 :: T_SemiMetric_284 -> T_IsQuasiSemiMetric_174 #

d_nonNegative_326 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_refl_328 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> Integer -> T__'8804'__22 #

du_refl_328 :: T_SemiMetric_284 -> Integer -> T__'8804'__22 #

d_reflexive_330 :: T_SemiMetric_284 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_sym_332 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_trans_334 :: T_SemiMetric_284 -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8776''45'isEquivalence_336 :: T_SemiMetric_284 -> T_IsEquivalence_26 #

d_'8776''8658'0_338 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_'8764''45'resp'45''8776'_340 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_340 :: T_SemiMetric_284 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_342 :: T_SemiMetric_284 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8764''45'resp'737''45''8776'_344 :: T_SemiMetric_284 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_'8818''45'resp'45''8776'_346 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_346 :: T_SemiMetric_284 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_348 :: T_SemiMetric_284 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8818''45'resp'737''45''8776'_350 :: T_SemiMetric_284 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_isPartialEquivalence_354 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_354 :: T_SemiMetric_284 -> T_IsPartialEquivalence_16 #

d_refl_356 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny #

d_reflexive_358 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_358 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_360 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_362 :: T_SemiMetric_284 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_366 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_366 :: T_SemiMetric_284 -> T_IsPartialEquivalence_16 #

d_refl_368 :: T_SemiMetric_284 -> Integer -> T__'8801'__12 #

d_reflexive_370 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_sym_372 :: T_SemiMetric_284 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_trans_374 :: T_SemiMetric_284 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_quasiSemiMetric_376 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_QuasiSemiMetric_186 #

du_quasiSemiMetric_376 :: T_SemiMetric_284 -> T_QuasiSemiMetric_186 #

d_preMetric_380 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_PreMetric_96 #

du_preMetric_380 :: T_SemiMetric_284 -> T_PreMetric_96 #

d_protoMetric_382 :: T_Level_18 -> T_Level_18 -> T_SemiMetric_284 -> T_ProtoMetric_12 #

du_protoMetric_382 :: T_SemiMetric_284 -> T_ProtoMetric_12 #

d_Metric_388 :: p -> p -> () #

data T_Metric_388 #

d_Carrier_402 :: T_Metric_388 -> () #

d__'8776'__404 :: T_Metric_388 -> AgdaAny -> AgdaAny -> () #

d_d_406 :: T_Metric_388 -> AgdaAny -> AgdaAny -> Integer #

d_isMetric_408 :: T_Metric_388 -> T_IsGeneralMetric_332 #

d_0'8658''8776'_412 :: T_Metric_388 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_antisym_414 :: T_Metric_388 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_cong_416 :: T_Metric_388 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_isEquivalence_418 :: T_Metric_388 -> T_IsEquivalence_26 #

d_isPartialOrder_420 :: T_Metric_388 -> T_IsPartialOrder_174 #

d_isPreMetric_422 :: T_Metric_388 -> T_IsPreMetric_102 #

d_isPreorder_424 :: T_Metric_388 -> T_IsPreorder_70 #

d_isProtoMetric_426 :: T_Metric_388 -> T_IsProtoMetric_30 #

d_isQuasiSemiMetric_428 :: T_Metric_388 -> T_IsQuasiSemiMetric_174 #

d_isSemiMetric_430 :: T_Metric_388 -> T_IsSemiMetric_250 #

d_nonNegative_432 :: T_Metric_388 -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_refl_434 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> Integer -> T__'8804'__22 #

du_refl_434 :: T_Metric_388 -> Integer -> T__'8804'__22 #

d_reflexive_436 :: T_Metric_388 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_sym_438 :: T_Metric_388 -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_trans_440 :: T_Metric_388 -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_triangle_442 :: T_Metric_388 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_'8776''45'isEquivalence_444 :: T_Metric_388 -> T_IsEquivalence_26 #

d_'8776''8658'0_446 :: T_Metric_388 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_'8764''45'resp'45''8776'_448 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_448 :: T_Metric_388 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_450 :: T_Metric_388 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8764''45'resp'737''45''8776'_452 :: T_Metric_388 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_'8818''45'resp'45''8776'_454 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_454 :: T_Metric_388 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_456 :: T_Metric_388 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8818''45'resp'737''45''8776'_458 :: T_Metric_388 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_isPartialEquivalence_462 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_462 :: T_Metric_388 -> T_IsPartialEquivalence_16 #

d_refl_464 :: T_Metric_388 -> AgdaAny -> AgdaAny #

d_reflexive_466 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_466 :: T_Metric_388 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_468 :: T_Metric_388 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_470 :: T_Metric_388 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_474 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_474 :: T_Metric_388 -> T_IsPartialEquivalence_16 #

d_refl_476 :: T_Metric_388 -> Integer -> T__'8801'__12 #

d_reflexive_478 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_sym_480 :: T_Metric_388 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_trans_482 :: T_Metric_388 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_semiMetric_484 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_SemiMetric_284 #

du_semiMetric_484 :: T_Metric_388 -> T_SemiMetric_284 #

d_preMetric_488 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_PreMetric_96 #

du_preMetric_488 :: T_Metric_388 -> T_PreMetric_96 #

d_protoMetric_490 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_ProtoMetric_12 #

du_protoMetric_490 :: T_Metric_388 -> T_ProtoMetric_12 #

d_quasiSemiMetric_492 :: T_Level_18 -> T_Level_18 -> T_Metric_388 -> T_QuasiSemiMetric_186 #

du_quasiSemiMetric_492 :: T_Metric_388 -> T_QuasiSemiMetric_186 #

d_UltraMetric_498 :: p -> p -> () #

data T_UltraMetric_498 #

d_Carrier_512 :: T_UltraMetric_498 -> () #

d__'8776'__514 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> () #

d_d_516 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> Integer #

d_isUltraMetric_518 :: T_UltraMetric_498 -> T_IsGeneralMetric_332 #

d_0'8658''8776'_522 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_antisym_524 :: T_UltraMetric_498 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_cong_526 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_isEquivalence_528 :: T_UltraMetric_498 -> T_IsEquivalence_26 #

d_isPartialOrder_530 :: T_UltraMetric_498 -> T_IsPartialOrder_174 #

d_isPreMetric_532 :: T_UltraMetric_498 -> T_IsPreMetric_102 #

d_isPreorder_534 :: T_UltraMetric_498 -> T_IsPreorder_70 #

d_isProtoMetric_536 :: T_UltraMetric_498 -> T_IsProtoMetric_30 #

d_isQuasiSemiMetric_538 :: T_UltraMetric_498 -> T_IsQuasiSemiMetric_174 #

d_isSemiMetric_540 :: T_UltraMetric_498 -> T_IsSemiMetric_250 #

d_nonNegative_542 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_refl_544 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> Integer -> T__'8804'__22 #

du_refl_544 :: T_UltraMetric_498 -> Integer -> T__'8804'__22 #

d_reflexive_546 :: T_UltraMetric_498 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_sym_548 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_trans_550 :: T_UltraMetric_498 -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_triangle_552 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8804'__22 #

d_'8776''45'isEquivalence_554 :: T_UltraMetric_498 -> T_IsEquivalence_26 #

d_'8776''8658'0_556 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_'8764''45'resp'45''8776'_558 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_558 :: T_UltraMetric_498 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_560 :: T_UltraMetric_498 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8764''45'resp'737''45''8776'_562 :: T_UltraMetric_498 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_'8818''45'resp'45''8776'_564 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_564 :: T_UltraMetric_498 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_566 :: T_UltraMetric_498 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8818''45'resp'737''45''8776'_568 :: T_UltraMetric_498 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 #

d_isPartialEquivalence_572 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_572 :: T_UltraMetric_498 -> T_IsPartialEquivalence_16 #

d_refl_574 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny #

d_reflexive_576 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_576 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_578 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_580 :: T_UltraMetric_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_584 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_584 :: T_UltraMetric_498 -> T_IsPartialEquivalence_16 #

d_refl_586 :: T_UltraMetric_498 -> Integer -> T__'8801'__12 #

d_reflexive_588 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_sym_590 :: T_UltraMetric_498 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_trans_592 :: T_UltraMetric_498 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_semiMetric_594 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_SemiMetric_284 #

du_semiMetric_594 :: T_UltraMetric_498 -> T_SemiMetric_284 #

d_preMetric_598 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_PreMetric_96 #

du_preMetric_598 :: T_UltraMetric_498 -> T_PreMetric_96 #

d_protoMetric_600 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_ProtoMetric_12 #

du_protoMetric_600 :: T_UltraMetric_498 -> T_ProtoMetric_12 #

d_quasiSemiMetric_602 :: T_Level_18 -> T_Level_18 -> T_UltraMetric_498 -> T_QuasiSemiMetric_186 #

du_quasiSemiMetric_602 :: T_UltraMetric_498 -> T_QuasiSemiMetric_186 #