Documentation

d_IsProtoMetric_14 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_IsPreMetric_18 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_IsQuasiSemiMetric_22 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_IsSemiMetric_26 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_IsMetric_30 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_0'8658''8776'_48 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_antisym_50 :: T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_cong_52 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_isEquivalence_54 :: T_IsGeneralMetric_308 -> T_IsEquivalence_26 Source #

d_isPartialOrder_56 :: T_IsGeneralMetric_308 -> T_IsPartialOrder_162 Source #

d_isPreMetric_58 :: T_IsGeneralMetric_308 -> T_IsPreMetric_96 Source #

d_isPreorder_60 :: T_IsGeneralMetric_308 -> T_IsPreorder_70 Source #

d_isProtoMetric_62 :: T_IsGeneralMetric_308 -> T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_64 :: T_IsGeneralMetric_308 -> T_IsQuasiSemiMetric_162 Source #

d_isSemiMetric_66 :: T_IsGeneralMetric_308 -> T_IsSemiMetric_232 Source #

d_nonNegative_68 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8804'__18 Source #

d_refl_70 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> T__'8804'__18 Source #

du_refl_70 :: T_IsGeneralMetric_308 -> Integer -> T__'8804'__18 Source #

d_reflexive_72 :: T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 Source #

d_sym_74 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_trans_76 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 Source #

d_triangle_78 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8804'__18 Source #

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

d_'8776''8658'0_82 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_84 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_84 :: T_IsGeneralMetric_308 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_86 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_86 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_88 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_88 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

d_isPartialEquivalence_92 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_92 :: T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

d_refl_94 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny Source #

d_reflexive_96 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_96 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_98 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_100 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_104 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_104 :: T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

d_refl_106 :: T_IsGeneralMetric_308 -> Integer -> T__'8801'__12 Source #

d_reflexive_108 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 Source #

d_sym_110 :: T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 Source #

d_trans_112 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 Source #

d_IsUltraMetric_114 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_0'8658''8776'_132 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_antisym_134 :: T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_cong_136 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_isEquivalence_138 :: T_IsGeneralMetric_308 -> T_IsEquivalence_26 Source #

d_isPartialOrder_140 :: T_IsGeneralMetric_308 -> T_IsPartialOrder_162 Source #

d_isPreMetric_142 :: T_IsGeneralMetric_308 -> T_IsPreMetric_96 Source #

d_isPreorder_144 :: T_IsGeneralMetric_308 -> T_IsPreorder_70 Source #

d_isProtoMetric_146 :: T_IsGeneralMetric_308 -> T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_148 :: T_IsGeneralMetric_308 -> T_IsQuasiSemiMetric_162 Source #

d_isSemiMetric_150 :: T_IsGeneralMetric_308 -> T_IsSemiMetric_232 Source #

d_nonNegative_152 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8804'__18 Source #

d_refl_154 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> T__'8804'__18 Source #

du_refl_154 :: T_IsGeneralMetric_308 -> Integer -> T__'8804'__18 Source #

d_reflexive_156 :: T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 Source #

d_sym_158 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_trans_160 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 Source #

d_triangle_162 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8804'__18 Source #

d_'8776''45'isEquivalence_164 :: T_IsGeneralMetric_308 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_166 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_'8764''45'resp'45''8776'_168 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_168 :: T_IsGeneralMetric_308 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_170 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'8764''45'resp'691''45''8776'_170 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

d_'8764''45'resp'737''45''8776'_172 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'8764''45'resp'737''45''8776'_172 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

d_isPartialEquivalence_176 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_176 :: T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

d_refl_178 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny Source #

d_reflexive_180 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_180 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_182 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_184 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_188 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_188 :: T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

d_refl_190 :: T_IsGeneralMetric_308 -> Integer -> T__'8801'__12 Source #

d_reflexive_192 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 Source #

d_sym_194 :: T_IsGeneralMetric_308 -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 Source #

d_trans_196 :: T_IsGeneralMetric_308 -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 Source #