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_174 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

d_isPartialOrder_42 ∷ T_IsProtoMetric_30 → T_IsPartialOrder_174 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_'8818''45'resp'45''8776'_70 ∷ 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_'8818''45'resp'45''8776'_70 ∷ T_IsProtoMetric_30 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_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 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_72 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_74 ∷ 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_'8818''45'resp'737''45''8776'_74 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_78 ∷ 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_78 ∷ T_IsProtoMetric_30 → T_IsPartialEquivalence_16 Source #

d_refl_80 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny Source #

d_reflexive_82 ∷ 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_82 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_84 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_86 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_90 ∷ 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_90 ∷ T_IsProtoMetric_30 → T_IsPartialEquivalence_16 Source #

d_refl_92 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny Source #

d_reflexive_94 ∷ 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_94 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_96 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_98 ∷ T_IsProtoMetric_30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsPreMetric_102 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsPreMetric_102 Source #

Constructors

C_IsPreMetric'46'constructor_6347 T_IsProtoMetric_30 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isProtoMetric_110 ∷ T_IsPreMetric_102 → T_IsProtoMetric_30 Source #

d_'8776''8658'0_112 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_116 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_118 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_120 ∷ T_IsPreMetric_102 → T_IsEquivalence_26 Source #

d_isPartialOrder_122 ∷ T_IsPreMetric_102 → T_IsPartialOrder_174 Source #

d_isPreorder_124 ∷ T_IsPreMetric_102 → T_IsPreorder_70 Source #

d_nonNegative_126 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_128 ∷ 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_102 → AgdaAny → AgdaAny Source #

du_refl_128 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny Source #

d_reflexive_130 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_132 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_134 ∷ T_IsPreMetric_102 → T_IsEquivalence_26 Source #

d_'8764''45'resp'45''8776'_136 ∷ 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_102 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_136 ∷ T_IsPreMetric_102 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_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_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_138 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_140 ∷ 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_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_140 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_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_102 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_142 ∷ T_IsPreMetric_102 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_144 ∷ 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_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_144 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_146 ∷ 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_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_146 ∷ T_IsPreMetric_102 → 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_102 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_150 ∷ T_IsPreMetric_102 → T_IsPartialEquivalence_16 Source #

d_refl_152 ∷ T_IsPreMetric_102 → 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_102 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_154 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_156 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_158 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_162 ∷ 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_102 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_162 ∷ T_IsPreMetric_102 → T_IsPartialEquivalence_16 Source #

d_refl_164 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny Source #

d_reflexive_166 ∷ 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_102 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_166 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_168 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_170 ∷ T_IsPreMetric_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsQuasiSemiMetric_174 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsQuasiSemiMetric_174 Source #

Constructors

C_IsQuasiSemiMetric'46'constructor_10111 T_IsPreMetric_102 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isPreMetric_182 ∷ T_IsQuasiSemiMetric_174 → T_IsPreMetric_102 Source #

d_0'8658''8776'_184 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_188 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_190 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_192 ∷ T_IsQuasiSemiMetric_174 → T_IsEquivalence_26 Source #

d_isPartialOrder_194 ∷ T_IsQuasiSemiMetric_174 → T_IsPartialOrder_174 Source #

d_isPreorder_196 ∷ T_IsQuasiSemiMetric_174 → T_IsPreorder_70 Source #

d_isProtoMetric_198 ∷ T_IsQuasiSemiMetric_174 → T_IsProtoMetric_30 Source #

d_nonNegative_200 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_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_174 → AgdaAny → AgdaAny Source #

du_refl_202 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny Source #

d_reflexive_204 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_206 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_208 ∷ T_IsQuasiSemiMetric_174 → T_IsEquivalence_26 Source #

d_'8776''8658'0_210 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_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_174 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_212 ∷ T_IsQuasiSemiMetric_174 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_214 ∷ 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_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_214 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_216 ∷ 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_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_216 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_218 ∷ 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_174 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_218 ∷ T_IsQuasiSemiMetric_174 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_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_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_220 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_222 ∷ 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_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_222 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_226 ∷ 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_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_226 ∷ T_IsQuasiSemiMetric_174 → T_IsPartialEquivalence_16 Source #

d_refl_228 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny Source #

d_reflexive_230 ∷ 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_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_230 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_232 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_234 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_238 ∷ 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_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_238 ∷ T_IsQuasiSemiMetric_174 → T_IsPartialEquivalence_16 Source #

d_refl_240 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny Source #

d_reflexive_242 ∷ 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_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_242 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_244 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_246 ∷ T_IsQuasiSemiMetric_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemiMetric_250 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsSemiMetric_250 Source #

Constructors

C_IsSemiMetric'46'constructor_14005 T_IsQuasiSemiMetric_174 (AgdaAny → AgdaAny → AgdaAny)

d_isQuasiSemiMetric_258 ∷ T_IsSemiMetric_250 → T_IsQuasiSemiMetric_174 Source #

d_sym_260 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny Source #

d_0'8658''8776'_264 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_266 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_268 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_270 ∷ T_IsSemiMetric_250 → T_IsEquivalence_26 Source #

d_isPartialOrder_272 ∷ T_IsSemiMetric_250 → T_IsPartialOrder_174 Source #

d_isPreMetric_274 ∷ T_IsSemiMetric_250 → T_IsPreMetric_102 Source #

d_isPreorder_276 ∷ T_IsSemiMetric_250 → T_IsPreorder_70 Source #

d_isProtoMetric_278 ∷ T_IsSemiMetric_250 → T_IsProtoMetric_30 Source #

d_nonNegative_280 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_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_250 → AgdaAny → AgdaAny Source #

du_refl_282 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny Source #

d_reflexive_284 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_286 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_288 ∷ T_IsSemiMetric_250 → T_IsEquivalence_26 Source #

d_'8776''8658'0_290 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_292 ∷ 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_250 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_292 ∷ T_IsSemiMetric_250 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_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_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_294 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_296 ∷ 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_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_296 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_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_250 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_298 ∷ T_IsSemiMetric_250 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_300 ∷ 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_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_300 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_302 ∷ 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_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_302 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_306 ∷ 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_250 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_306 ∷ T_IsSemiMetric_250 → T_IsPartialEquivalence_16 Source #

d_refl_308 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny Source #

d_reflexive_310 ∷ 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_250 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_310 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_312 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_314 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_318 ∷ 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_250 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_318 ∷ T_IsSemiMetric_250 → T_IsPartialEquivalence_16 Source #

d_refl_320 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny Source #

d_reflexive_322 ∷ 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_250 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_322 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_324 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_326 ∷ T_IsSemiMetric_250 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGeneralMetric_332 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsGeneralMetric_332 Source #

Constructors

C_IsGeneralMetric'46'constructor_18255 T_IsSemiMetric_250 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isSemiMetric_342 ∷ T_IsGeneralMetric_332 → T_IsSemiMetric_250 Source #

d_triangle_344 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_0'8658''8776'_348 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_350 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_352 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_354 ∷ T_IsGeneralMetric_332 → T_IsEquivalence_26 Source #

d_isPartialOrder_356 ∷ T_IsGeneralMetric_332 → T_IsPartialOrder_174 Source #

d_isPreMetric_358 ∷ T_IsGeneralMetric_332 → T_IsPreMetric_102 Source #

d_isPreorder_360 ∷ T_IsGeneralMetric_332 → T_IsPreorder_70 Source #

d_isProtoMetric_362 ∷ T_IsGeneralMetric_332 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_364 ∷ T_IsGeneralMetric_332 → T_IsQuasiSemiMetric_174 Source #

d_nonNegative_366 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_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_332 → AgdaAny → AgdaAny Source #

du_refl_368 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny Source #

d_reflexive_370 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_sym_372 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_374 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_376 ∷ T_IsGeneralMetric_332 → T_IsEquivalence_26 Source #

d_'8776''8658'0_378 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_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_332 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_380 ∷ T_IsGeneralMetric_332 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_382 ∷ 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_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_382 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_384 ∷ 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_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_384 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_386 ∷ 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_332 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_386 ∷ T_IsGeneralMetric_332 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_388 ∷ 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_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_388 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_390 ∷ 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_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_390 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_394 ∷ 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_332 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_394 ∷ T_IsGeneralMetric_332 → T_IsPartialEquivalence_16 Source #

d_refl_396 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny Source #

d_reflexive_398 ∷ 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_332 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_398 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_400 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_402 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_406 ∷ 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_332 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_406 ∷ T_IsGeneralMetric_332 → T_IsPartialEquivalence_16 Source #

d_refl_408 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny Source #

d_reflexive_410 ∷ 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_332 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_410 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_412 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_414 ∷ T_IsGeneralMetric_332 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #