Safe Haskell	None

MAlonzo.Code.Function.Metric.Structures

Documentation

d_IsProtoMetric_30 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> () Source #

data T_IsProtoMetric_30 Source #

Constructors

C_IsProtoMetric'46'constructor_1309 T_IsPartialOrder_162 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)

d_isPartialOrder_42 :: T_IsProtoMetric_30 -> T_IsPartialOrder_162 Source #

d_'8776''45'isEquivalence_44 :: T_IsProtoMetric_30 -> T_IsEquivalence_26 Source #

d_cong_46 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_nonNegative_48 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_52 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_54 :: T_IsProtoMetric_30 -> T_IsEquivalence_26 Source #

d_isPreorder_56 :: T_IsProtoMetric_30 -> T_IsPreorder_70 Source #

d_refl_58 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> AgdaAny -> AgdaAny Source #

du_refl_58 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny Source #

d_reflexive_60 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_62 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_64 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_64 :: T_IsProtoMetric_30 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_66 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_66 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_68 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_68 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_72 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_72 :: T_IsProtoMetric_30 -> T_IsPartialEquivalence_16 Source #

d_refl_74 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny Source #

d_reflexive_76 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_76 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_78 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_80 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_84 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_84 :: T_IsProtoMetric_30 -> T_IsPartialEquivalence_16 Source #

d_refl_86 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny Source #

d_reflexive_88 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_88 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_90 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_92 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsPreMetric_96 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> () Source #

data T_IsPreMetric_96 Source #

Constructors

C_IsPreMetric'46'constructor_4743 T_IsProtoMetric_30 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isProtoMetric_104 :: T_IsPreMetric_96 -> T_IsProtoMetric_30 Source #

d_'8776''8658'0_106 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_110 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_112 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_114 :: T_IsPreMetric_96 -> T_IsEquivalence_26 Source #

d_isPartialOrder_116 :: T_IsPreMetric_96 -> T_IsPartialOrder_162 Source #

d_isPreorder_118 :: T_IsPreMetric_96 -> T_IsPreorder_70 Source #

d_nonNegative_120 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_122 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> AgdaAny -> AgdaAny Source #

du_refl_122 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny Source #

d_reflexive_124 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_126 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_128 :: T_IsPreMetric_96 -> T_IsEquivalence_26 Source #

d_'8764''45'resp'45''8776'_130 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_130 :: T_IsPreMetric_96 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_132 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_134 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_134 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_138 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_138 :: T_IsPreMetric_96 -> T_IsPartialEquivalence_16 Source #

d_refl_140 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny Source #

d_reflexive_142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_142 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_144 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_146 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_150 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_150 :: T_IsPreMetric_96 -> T_IsPartialEquivalence_16 Source #

d_refl_152 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny Source #

d_reflexive_154 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_154 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_156 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_158 :: T_IsPreMetric_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsQuasiSemiMetric_162 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> () Source #

data T_IsQuasiSemiMetric_162 Source #

Constructors

C_IsQuasiSemiMetric'46'constructor_7947 T_IsPreMetric_96 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isPreMetric_170 :: T_IsQuasiSemiMetric_162 -> T_IsPreMetric_96 Source #

d_0'8658''8776'_172 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_176 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_178 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_180 :: T_IsQuasiSemiMetric_162 -> T_IsEquivalence_26 Source #

d_isPartialOrder_182 :: T_IsQuasiSemiMetric_162 -> T_IsPartialOrder_162 Source #

d_isPreorder_184 :: T_IsQuasiSemiMetric_162 -> T_IsPreorder_70 Source #

d_isProtoMetric_186 :: T_IsQuasiSemiMetric_162 -> T_IsProtoMetric_30 Source #

d_nonNegative_188 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_190 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny Source #

du_refl_190 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny Source #

d_reflexive_192 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_194 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_196 :: T_IsQuasiSemiMetric_162 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_198 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_200 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_200 :: T_IsQuasiSemiMetric_162 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_202 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_202 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_204 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_204 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_208 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_208 :: T_IsQuasiSemiMetric_162 -> T_IsPartialEquivalence_16 Source #

d_refl_210 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny Source #

d_reflexive_212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_212 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_214 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_216 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_220 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_220 :: T_IsQuasiSemiMetric_162 -> T_IsPartialEquivalence_16 Source #

d_refl_222 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny Source #

d_reflexive_224 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_224 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_226 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_228 :: T_IsQuasiSemiMetric_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsSemiMetric_232 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> () Source #

data T_IsSemiMetric_232 Source #

Constructors

C_IsSemiMetric'46'constructor_11297 T_IsQuasiSemiMetric_162 (AgdaAny -> AgdaAny -> AgdaAny)

d_isQuasiSemiMetric_240 :: T_IsSemiMetric_232 -> T_IsQuasiSemiMetric_162 Source #

d_sym_242 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'8658''8776'_246 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_248 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_250 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_252 :: T_IsSemiMetric_232 -> T_IsEquivalence_26 Source #

d_isPartialOrder_254 :: T_IsSemiMetric_232 -> T_IsPartialOrder_162 Source #

d_isPreMetric_256 :: T_IsSemiMetric_232 -> T_IsPreMetric_96 Source #

d_isPreorder_258 :: T_IsSemiMetric_232 -> T_IsPreorder_70 Source #

d_isProtoMetric_260 :: T_IsSemiMetric_232 -> T_IsProtoMetric_30 Source #

d_nonNegative_262 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_264 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> AgdaAny -> AgdaAny Source #

du_refl_264 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny Source #

d_reflexive_266 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_268 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8776''45'isEquivalence_270 :: T_IsSemiMetric_232 -> T_IsEquivalence_26 Source #

d_'8776''8658'0_272 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_274 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_274 :: T_IsSemiMetric_232 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_276 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_276 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_278 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_278 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_282 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_282 :: T_IsSemiMetric_232 -> T_IsPartialEquivalence_16 Source #

d_refl_284 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny Source #

d_reflexive_286 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_286 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_288 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_290 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_294 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_294 :: T_IsSemiMetric_232 -> T_IsPartialEquivalence_16 Source #

d_refl_296 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny Source #

d_reflexive_298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_298 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_300 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_302 :: T_IsSemiMetric_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsGeneralMetric_308 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> p13 -> () Source #

data T_IsGeneralMetric_308 Source #

Constructors

C_IsGeneralMetric'46'constructor_14943 T_IsSemiMetric_232 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isSemiMetric_318 :: T_IsGeneralMetric_308 -> T_IsSemiMetric_232 Source #

d_triangle_320 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_0'8658''8776'_324 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_326 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_328 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_330 :: T_IsGeneralMetric_308 -> T_IsEquivalence_26 Source #

d_isPartialOrder_332 :: T_IsGeneralMetric_308 -> T_IsPartialOrder_162 Source #

d_isPreMetric_334 :: T_IsGeneralMetric_308 -> T_IsPreMetric_96 Source #

d_isPreorder_336 :: T_IsGeneralMetric_308 -> T_IsPreorder_70 Source #

d_isProtoMetric_338 :: T_IsGeneralMetric_308 -> T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_340 :: T_IsGeneralMetric_308 -> T_IsQuasiSemiMetric_162 Source #

d_nonNegative_342 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_344 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny Source #

du_refl_344 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny Source #

d_reflexive_346 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_sym_348 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_350 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

d_'8776''8658'0_354 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

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

d_'8764''45'resp'691''45''8776'_358 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_358 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_360 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_360 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_364 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_364 :: T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

d_refl_366 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny Source #

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

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

d_sym_370 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_372 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_376 :: T_IsGeneralMetric_308 -> T_IsPartialEquivalence_16 Source #

d_refl_378 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny Source #

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

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

d_sym_382 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_384 :: T_IsGeneralMetric_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #