Documentation

d_ProtoMetric_12 :: p1 -> p2 -> () 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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 :: p1 -> p2 -> () 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_PreMetric_90 -> T_ProtoMetric_12 Source #

du_protoMetric_168 :: T_PreMetric_90 -> T_ProtoMetric_12 Source #

d_QuasiSemiMetric_174 :: p1 -> p2 -> () 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_QuasiSemiMetric_174 -> T_PreMetric_90 Source #

du_preMetric_256 :: T_QuasiSemiMetric_174 -> T_PreMetric_90 Source #

d_protoMetric_260 :: T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_174 -> T_ProtoMetric_12 Source #

du_protoMetric_260 :: T_QuasiSemiMetric_174 -> T_ProtoMetric_12 Source #

d_SemiMetric_266 :: p1 -> p2 -> () 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_SemiMetric_266 -> T_QuasiSemiMetric_174 Source #

du_quasiSemiMetric_352 :: T_SemiMetric_266 -> T_QuasiSemiMetric_174 Source #

d_preMetric_356 :: T_Level_14 -> T_Level_14 -> T_SemiMetric_266 -> T_PreMetric_90 Source #

du_preMetric_356 :: T_SemiMetric_266 -> T_PreMetric_90 Source #

d_protoMetric_358 :: T_Level_14 -> T_Level_14 -> T_SemiMetric_266 -> T_ProtoMetric_12 Source #

du_protoMetric_358 :: T_SemiMetric_266 -> T_ProtoMetric_12 Source #

d_Metric_364 :: p1 -> p2 -> () 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Metric_364 -> T_SemiMetric_266 Source #

du_semiMetric_454 :: T_Metric_364 -> T_SemiMetric_266 Source #

d_preMetric_458 :: T_Level_14 -> T_Level_14 -> T_Metric_364 -> T_PreMetric_90 Source #

du_preMetric_458 :: T_Metric_364 -> T_PreMetric_90 Source #

d_protoMetric_460 :: T_Level_14 -> T_Level_14 -> T_Metric_364 -> T_ProtoMetric_12 Source #

du_protoMetric_460 :: T_Metric_364 -> T_ProtoMetric_12 Source #

d_quasiSemiMetric_462 :: T_Level_14 -> T_Level_14 -> T_Metric_364 -> T_QuasiSemiMetric_174 Source #

du_quasiSemiMetric_462 :: T_Metric_364 -> T_QuasiSemiMetric_174 Source #

d_UltraMetric_468 :: p1 -> p2 -> () 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_UltraMetric_468 -> T_SemiMetric_266 Source #

du_semiMetric_558 :: T_UltraMetric_468 -> T_SemiMetric_266 Source #

d_preMetric_562 :: T_Level_14 -> T_Level_14 -> T_UltraMetric_468 -> T_PreMetric_90 Source #

du_preMetric_562 :: T_UltraMetric_468 -> T_PreMetric_90 Source #

d_protoMetric_564 :: T_Level_14 -> T_Level_14 -> T_UltraMetric_468 -> T_ProtoMetric_12 Source #

du_protoMetric_564 :: T_UltraMetric_468 -> T_ProtoMetric_12 Source #

d_quasiSemiMetric_566 :: T_Level_14 -> T_Level_14 -> T_UltraMetric_468 -> T_QuasiSemiMetric_174 Source #

du_quasiSemiMetric_566 :: T_UltraMetric_468 -> T_QuasiSemiMetric_174 Source #