Documentation

d_ProtoMetric_16 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_ProtoMetric_16 Source #

d_Carrier_44 :: T_ProtoMetric_16 -> () Source #

d_Image_46 :: T_ProtoMetric_16 -> () Source #

d__'8776'__48 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> () Source #

d__'8776''7522'__50 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__52 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> () Source #

d_0'35'_54 :: T_ProtoMetric_16 -> AgdaAny Source #

d_d_56 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isProtoMetric_58 :: T_ProtoMetric_16 -> T_IsProtoMetric_30 Source #

d_antisym_62 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_64 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_66 :: T_ProtoMetric_16 -> T_IsEquivalence_26 Source #

d_isPartialOrder_68 :: T_ProtoMetric_16 -> T_IsPartialOrder_162 Source #

d_isPreorder_70 :: T_ProtoMetric_16 -> T_IsPreorder_70 Source #

d_nonNegative_72 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_74 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> AgdaAny -> AgdaAny Source #

du_refl_74 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny Source #

d_reflexive_76 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_78 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_80 :: T_ProtoMetric_16 -> T_IsEquivalence_26 Source #

d_'8764''45'resp'45''8776'_82 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_82 :: T_ProtoMetric_16 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_84 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_84 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_86 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_86 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_90 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_90 :: T_ProtoMetric_16 -> T_IsPartialEquivalence_16 Source #

d_refl_92 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny Source #

d_reflexive_94 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_94 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_96 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_98 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_102 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_102 :: T_ProtoMetric_16 -> T_IsPartialEquivalence_16 Source #

d_refl_104 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny Source #

d_reflexive_106 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_106 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_108 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_110 :: T_ProtoMetric_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_PreMetric_122 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_PreMetric_122 Source #

d_Carrier_150 :: T_PreMetric_122 -> () Source #

d_Image_152 :: T_PreMetric_122 -> () Source #

d__'8776'__154 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> () Source #

d__'8776''7522'__156 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__158 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> () Source #

d_0'35'_160 :: T_PreMetric_122 -> AgdaAny Source #

d_d_162 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPreMetric_164 :: T_PreMetric_122 -> T_IsPreMetric_96 Source #

d_antisym_168 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_170 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_172 :: T_PreMetric_122 -> T_IsEquivalence_26 Source #

d_isPartialOrder_174 :: T_PreMetric_122 -> T_IsPartialOrder_162 Source #

d_isPreorder_176 :: T_PreMetric_122 -> T_IsPreorder_70 Source #

d_isProtoMetric_178 :: T_PreMetric_122 -> T_IsProtoMetric_30 Source #

d_nonNegative_180 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_182 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> AgdaAny -> AgdaAny Source #

du_refl_182 :: T_PreMetric_122 -> AgdaAny -> AgdaAny Source #

d_reflexive_184 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_186 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_188 :: T_PreMetric_122 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_190 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_192 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_192 :: T_PreMetric_122 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_194 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_194 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_196 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_196 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_200 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_200 :: T_PreMetric_122 -> T_IsPartialEquivalence_16 Source #

d_refl_202 :: T_PreMetric_122 -> AgdaAny -> AgdaAny Source #

d_reflexive_204 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_204 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_206 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_208 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_212 :: T_PreMetric_122 -> T_IsPartialEquivalence_16 Source #

d_refl_214 :: T_PreMetric_122 -> AgdaAny -> AgdaAny Source #

d_reflexive_216 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_216 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_218 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_220 :: T_PreMetric_122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_protoMetric_222 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_PreMetric_122 -> T_ProtoMetric_16 Source #

du_protoMetric_222 :: T_PreMetric_122 -> T_ProtoMetric_16 Source #

d_QuasiSemiMetric_234 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_QuasiSemiMetric_234 Source #

d_Carrier_262 :: T_QuasiSemiMetric_234 -> () Source #

d_Image_264 :: T_QuasiSemiMetric_234 -> () Source #

d__'8776'__266 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> () Source #

d__'8776''7522'__268 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__270 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> () Source #

d_0'35'_272 :: T_QuasiSemiMetric_234 -> AgdaAny Source #

d_d_274 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isQuasiSemiMetric_276 :: T_QuasiSemiMetric_234 -> T_IsQuasiSemiMetric_162 Source #

d_0'8658''8776'_280 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_282 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_284 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_286 :: T_QuasiSemiMetric_234 -> T_IsEquivalence_26 Source #

d_isPartialOrder_288 :: T_QuasiSemiMetric_234 -> T_IsPartialOrder_162 Source #

d_isPreMetric_290 :: T_QuasiSemiMetric_234 -> T_IsPreMetric_96 Source #

d_isPreorder_292 :: T_QuasiSemiMetric_234 -> T_IsPreorder_70 Source #

d_isProtoMetric_294 :: T_QuasiSemiMetric_234 -> T_IsProtoMetric_30 Source #

d_nonNegative_296 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny Source #

du_refl_298 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny Source #

d_reflexive_300 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_302 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_304 :: T_QuasiSemiMetric_234 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_306 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_308 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_308 :: T_QuasiSemiMetric_234 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_310 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_310 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_312 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_312 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_316 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_316 :: T_QuasiSemiMetric_234 -> T_IsPartialEquivalence_16 Source #

d_refl_318 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny Source #

d_reflexive_320 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_320 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_322 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_324 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_328 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_328 :: T_QuasiSemiMetric_234 -> T_IsPartialEquivalence_16 Source #

d_refl_330 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny Source #

d_reflexive_332 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_332 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_334 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_336 :: T_QuasiSemiMetric_234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_preMetric_338 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> T_PreMetric_122 Source #

du_preMetric_338 :: T_QuasiSemiMetric_234 -> T_PreMetric_122 Source #

d_protoMetric_342 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_QuasiSemiMetric_234 -> T_ProtoMetric_16 Source #

du_protoMetric_342 :: T_QuasiSemiMetric_234 -> T_ProtoMetric_16 Source #

d_SemiMetric_354 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_SemiMetric_354 Source #

d_Carrier_382 :: T_SemiMetric_354 -> () Source #

d_Image_384 :: T_SemiMetric_354 -> () Source #

d__'8776'__386 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> () Source #

d__'8776''7522'__388 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__390 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> () Source #

d_0'35'_392 :: T_SemiMetric_354 -> AgdaAny Source #

d_d_394 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemiMetric_396 :: T_SemiMetric_354 -> T_IsSemiMetric_232 Source #

d_0'8658''8776'_400 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_402 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_404 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_406 :: T_SemiMetric_354 -> T_IsEquivalence_26 Source #

d_isPartialOrder_408 :: T_SemiMetric_354 -> T_IsPartialOrder_162 Source #

d_isPreMetric_410 :: T_SemiMetric_354 -> T_IsPreMetric_96 Source #

d_isPreorder_412 :: T_SemiMetric_354 -> T_IsPreorder_70 Source #

d_isProtoMetric_414 :: T_SemiMetric_354 -> T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_416 :: T_SemiMetric_354 -> T_IsQuasiSemiMetric_162 Source #

d_nonNegative_418 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_420 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> AgdaAny -> AgdaAny Source #

du_refl_420 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny Source #

d_reflexive_422 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_sym_424 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_426 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_428 :: T_SemiMetric_354 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_430 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_432 :: T_SemiMetric_354 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_434 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_434 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_436 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_436 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_440 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_440 :: T_SemiMetric_354 -> T_IsPartialEquivalence_16 Source #

d_refl_442 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny Source #

d_reflexive_444 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_444 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_446 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_448 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_452 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_452 :: T_SemiMetric_354 -> T_IsPartialEquivalence_16 Source #

d_refl_454 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny Source #

d_reflexive_456 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_456 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_458 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_460 :: T_SemiMetric_354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_quasiSemiMetric_462 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> T_QuasiSemiMetric_234 Source #

du_quasiSemiMetric_462 :: T_SemiMetric_354 -> T_QuasiSemiMetric_234 Source #

d_preMetric_466 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> T_PreMetric_122 Source #

du_preMetric_466 :: T_SemiMetric_354 -> T_PreMetric_122 Source #

d_protoMetric_468 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_SemiMetric_354 -> T_ProtoMetric_16 Source #

du_protoMetric_468 :: T_SemiMetric_354 -> T_ProtoMetric_16 Source #

d_GeneralMetric_480 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_GeneralMetric_480 Source #

d_Carrier_510 :: T_GeneralMetric_480 -> () Source #

d_Image_512 :: T_GeneralMetric_480 -> () Source #

d__'8776'__514 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> () Source #

d__'8776''7522'__516 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__518 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> () Source #

d_0'35'_520 :: T_GeneralMetric_480 -> AgdaAny Source #

d__'8729'__522 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_d_524 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isGeneralMetric_526 :: T_GeneralMetric_480 -> T_IsGeneralMetric_308 Source #

d_0'8658''8776'_530 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_532 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_534 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_536 :: T_GeneralMetric_480 -> T_IsEquivalence_26 Source #

d_isPartialOrder_538 :: T_GeneralMetric_480 -> T_IsPartialOrder_162 Source #

d_isPreMetric_540 :: T_GeneralMetric_480 -> T_IsPreMetric_96 Source #

d_isPreorder_542 :: T_GeneralMetric_480 -> T_IsPreorder_70 Source #

d_isProtoMetric_544 :: T_GeneralMetric_480 -> T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_546 :: T_GeneralMetric_480 -> T_IsQuasiSemiMetric_162 Source #

d_isSemiMetric_548 :: T_GeneralMetric_480 -> T_IsSemiMetric_232 Source #

d_nonNegative_550 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_552 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> AgdaAny -> AgdaAny Source #

du_refl_552 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_554 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_sym_556 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_558 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_triangle_560 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_562 :: T_GeneralMetric_480 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_564 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_566 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_566 :: T_GeneralMetric_480 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_568 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_568 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_570 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_570 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_574 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_574 :: T_GeneralMetric_480 -> T_IsPartialEquivalence_16 Source #

d_refl_576 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_578 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_578 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_580 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_582 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_586 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_586 :: T_GeneralMetric_480 -> T_IsPartialEquivalence_16 Source #

d_refl_588 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_590 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_590 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_592 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_594 :: T_GeneralMetric_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semiMetric_596 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_SemiMetric_354 Source #

du_semiMetric_596 :: T_GeneralMetric_480 -> T_SemiMetric_354 Source #

d_preMetric_600 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_PreMetric_122 Source #

du_preMetric_600 :: T_GeneralMetric_480 -> T_PreMetric_122 Source #

d_protoMetric_602 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_ProtoMetric_16 Source #

du_protoMetric_602 :: T_GeneralMetric_480 -> T_ProtoMetric_16 Source #

d_quasiSemiMetric_604 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_GeneralMetric_480 -> T_QuasiSemiMetric_234 Source #

du_quasiSemiMetric_604 :: T_GeneralMetric_480 -> T_QuasiSemiMetric_234 Source #