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_constructor_100 T_IsPartialOrder_248 T_IsEquivalence_28 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

d_isPartialOrder_42 ∷ T_IsProtoMetric_30 → T_IsPartialOrder_248 Source #

d_'8776''45'isEquivalence_44 ∷ T_IsProtoMetric_30 → T_IsEquivalence_28 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_28 Source #

d_isPreorder_56 ∷ T_IsProtoMetric_30 → T_IsPreorder_76 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_104 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsPreMetric_104 Source #

Constructors

C_constructor_174 T_IsProtoMetric_30 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isProtoMetric_112 ∷ T_IsPreMetric_104 → T_IsProtoMetric_30 Source #

d_'8776''8658'0_114 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_118 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_120 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_122 ∷ T_IsPreMetric_104 → T_IsEquivalence_28 Source #

d_isPartialOrder_124 ∷ T_IsPreMetric_104 → T_IsPartialOrder_248 Source #

d_isPreorder_126 ∷ T_IsPreMetric_104 → T_IsPreorder_76 Source #

d_nonNegative_128 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny Source #

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

du_refl_130 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny Source #

d_reflexive_132 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_134 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_136 ∷ T_IsPreMetric_104 → T_IsEquivalence_28 Source #

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

du_'8764''45'resp'45''8776'_138 ∷ T_IsPreMetric_104 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_140 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''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_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_142 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_144 ∷ T_IsPreMetric_104 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_146 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_148 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_152 ∷ 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_104 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_152 ∷ T_IsPreMetric_104 → T_IsPartialEquivalence_16 Source #

d_refl_154 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny Source #

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

du_reflexive_156 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_158 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_160 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_164 ∷ 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_104 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_164 ∷ T_IsPreMetric_104 → T_IsPartialEquivalence_16 Source #

d_refl_166 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny Source #

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

du_reflexive_168 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_170 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_172 ∷ T_IsPreMetric_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsQuasiSemiMetric_178 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsQuasiSemiMetric_178 Source #

Constructors

C_constructor_252 T_IsPreMetric_104 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isPreMetric_186 ∷ T_IsQuasiSemiMetric_178 → T_IsPreMetric_104 Source #

d_0'8658''8776'_188 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_192 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_194 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_196 ∷ T_IsQuasiSemiMetric_178 → T_IsEquivalence_28 Source #

d_isPartialOrder_198 ∷ T_IsQuasiSemiMetric_178 → T_IsPartialOrder_248 Source #

d_isPreorder_200 ∷ T_IsQuasiSemiMetric_178 → T_IsPreorder_76 Source #

d_isProtoMetric_202 ∷ T_IsQuasiSemiMetric_178 → T_IsProtoMetric_30 Source #

d_nonNegative_204 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_206 ∷ 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_178 → AgdaAny → AgdaAny Source #

du_refl_206 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny Source #

d_reflexive_208 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_210 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_212 ∷ T_IsQuasiSemiMetric_178 → T_IsEquivalence_28 Source #

d_'8776''8658'0_214 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_216 ∷ T_IsQuasiSemiMetric_178 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_218 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''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_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_220 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_222 ∷ T_IsQuasiSemiMetric_178 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_224 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_226 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_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_178 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_230 ∷ T_IsQuasiSemiMetric_178 → T_IsPartialEquivalence_16 Source #

d_refl_232 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny Source #

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

du_reflexive_234 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_236 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_238 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_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_178 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_242 ∷ T_IsQuasiSemiMetric_178 → T_IsPartialEquivalence_16 Source #

d_refl_244 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny Source #

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

du_reflexive_246 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_248 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_250 ∷ T_IsQuasiSemiMetric_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemiMetric_256 ∷ p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsSemiMetric_256 Source #

Constructors

C_constructor_334 T_IsQuasiSemiMetric_178 (AgdaAny → AgdaAny → AgdaAny)

d_isQuasiSemiMetric_264 ∷ T_IsSemiMetric_256 → T_IsQuasiSemiMetric_178 Source #

d_sym_266 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny Source #

d_0'8658''8776'_270 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_272 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_274 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_276 ∷ T_IsSemiMetric_256 → T_IsEquivalence_28 Source #

d_isPartialOrder_278 ∷ T_IsSemiMetric_256 → T_IsPartialOrder_248 Source #

d_isPreMetric_280 ∷ T_IsSemiMetric_256 → T_IsPreMetric_104 Source #

d_isPreorder_282 ∷ T_IsSemiMetric_256 → T_IsPreorder_76 Source #

d_isProtoMetric_284 ∷ T_IsSemiMetric_256 → T_IsProtoMetric_30 Source #

d_nonNegative_286 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_288 ∷ 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_256 → AgdaAny → AgdaAny Source #

du_refl_288 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny Source #

d_reflexive_290 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_292 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_294 ∷ T_IsSemiMetric_256 → T_IsEquivalence_28 Source #

d_'8776''8658'0_296 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''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_256 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_298 ∷ T_IsSemiMetric_256 → T_Σ_14 Source #

d_'8764''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_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_300 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''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_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_302 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_304 ∷ T_IsSemiMetric_256 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_306 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_308 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_312 ∷ 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_256 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_312 ∷ T_IsSemiMetric_256 → T_IsPartialEquivalence_16 Source #

d_refl_314 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny Source #

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

du_reflexive_316 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_318 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_320 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_324 ∷ 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_256 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_324 ∷ T_IsSemiMetric_256 → T_IsPartialEquivalence_16 Source #

d_refl_326 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny Source #

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

du_reflexive_328 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_330 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_332 ∷ T_IsSemiMetric_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGeneralMetric_340 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsGeneralMetric_340 Source #

Constructors

C_constructor_424 T_IsSemiMetric_256 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isSemiMetric_350 ∷ T_IsGeneralMetric_340 → T_IsSemiMetric_256 Source #

d_triangle_352 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_0'8658''8776'_356 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_358 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_360 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_362 ∷ T_IsGeneralMetric_340 → T_IsEquivalence_28 Source #

d_isPartialOrder_364 ∷ T_IsGeneralMetric_340 → T_IsPartialOrder_248 Source #

d_isPreMetric_366 ∷ T_IsGeneralMetric_340 → T_IsPreMetric_104 Source #

d_isPreorder_368 ∷ T_IsGeneralMetric_340 → T_IsPreorder_76 Source #

d_isProtoMetric_370 ∷ T_IsGeneralMetric_340 → T_IsProtoMetric_30 Source #

d_isQuasiSemiMetric_372 ∷ T_IsGeneralMetric_340 → T_IsQuasiSemiMetric_178 Source #

d_nonNegative_374 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny Source #

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

du_refl_376 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny Source #

d_reflexive_378 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_sym_380 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_382 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8776''45'isEquivalence_384 ∷ T_IsGeneralMetric_340 → T_IsEquivalence_28 Source #

d_'8776''8658'0_386 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_388 ∷ T_IsGeneralMetric_340 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_390 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_392 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_394 ∷ T_IsGeneralMetric_340 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_396 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_398 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_402 ∷ 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_340 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_402 ∷ T_IsGeneralMetric_340 → T_IsPartialEquivalence_16 Source #

d_refl_404 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny Source #

d_reflexive_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_340 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_406 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_408 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_410 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_414 ∷ 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_340 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_414 ∷ T_IsGeneralMetric_340 → T_IsPartialEquivalence_16 Source #

d_refl_416 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny Source #

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

du_reflexive_418 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_420 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_422 ∷ T_IsGeneralMetric_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #