Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Function.Metric.Structures

Documentation

d_IsProtoMetric_30 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsProtoMetric_30 Source #

Constructors

C_IsProtoMetric'46'constructor_2109 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsPreMetric_96 Source #

Constructors

C_IsPreMetric'46'constructor_6061 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsQuasiSemiMetric_162 Source #

Constructors

C_IsQuasiSemiMetric'46'constructor_9549 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsSemiMetric_232 Source #

Constructors

C_IsSemiMetric'46'constructor_13167 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsGeneralMetric_308 Source #

Constructors

C_IsGeneralMetric'46'constructor_17141 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (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 #