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 -> () #

data T_IsProtoMetric_30 #

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 #

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

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

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

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

d_isEquivalence_54 :: T_IsProtoMetric_30 -> T_IsEquivalence_26 #

d_isPreorder_56 :: T_IsProtoMetric_30 -> T_IsPreorder_70 #

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 #

du_refl_58 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny #

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

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

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 #

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

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 #

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

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 #

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

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 #

du_'8818''45'resp'45''8776'_70 :: T_IsProtoMetric_30 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_72 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_74 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_78 :: T_IsProtoMetric_30 -> T_IsPartialEquivalence_16 #

d_refl_80 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_82 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_84 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_86 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_90 :: T_IsProtoMetric_30 -> T_IsPartialEquivalence_16 #

d_refl_92 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_94 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_96 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_98 :: T_IsProtoMetric_30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsPreMetric_102 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsPreMetric_102 #

Constructors

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

d_isProtoMetric_110 :: T_IsPreMetric_102 -> T_IsProtoMetric_30 #

d_'8776''8658'0_112 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_116 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_118 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_120 :: T_IsPreMetric_102 -> T_IsEquivalence_26 #

d_isPartialOrder_122 :: T_IsPreMetric_102 -> T_IsPartialOrder_174 #

d_isPreorder_124 :: T_IsPreMetric_102 -> T_IsPreorder_70 #

d_nonNegative_126 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_refl_128 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny #

d_reflexive_130 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_132 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8776''45'isEquivalence_134 :: T_IsPreMetric_102 -> T_IsEquivalence_26 #

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 #

du_'8764''45'resp'45''8776'_136 :: T_IsPreMetric_102 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_138 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_140 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_142 :: T_IsPreMetric_102 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_144 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_146 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_150 :: T_IsPreMetric_102 -> T_IsPartialEquivalence_16 #

d_refl_152 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_154 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_156 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_158 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_162 :: T_IsPreMetric_102 -> T_IsPartialEquivalence_16 #

d_refl_164 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_166 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_168 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_170 :: T_IsPreMetric_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsQuasiSemiMetric_174 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsQuasiSemiMetric_174 #

Constructors

C_IsQuasiSemiMetric'46'constructor_10111 T_IsPreMetric_102 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isPreMetric_182 :: T_IsQuasiSemiMetric_174 -> T_IsPreMetric_102 #

d_0'8658''8776'_184 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_188 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_190 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_192 :: T_IsQuasiSemiMetric_174 -> T_IsEquivalence_26 #

d_isPartialOrder_194 :: T_IsQuasiSemiMetric_174 -> T_IsPartialOrder_174 #

d_isPreorder_196 :: T_IsQuasiSemiMetric_174 -> T_IsPreorder_70 #

d_isProtoMetric_198 :: T_IsQuasiSemiMetric_174 -> T_IsProtoMetric_30 #

d_nonNegative_200 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_refl_202 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny #

d_reflexive_204 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_206 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8776''45'isEquivalence_208 :: T_IsQuasiSemiMetric_174 -> T_IsEquivalence_26 #

d_'8776''8658'0_210 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_212 :: T_IsQuasiSemiMetric_174 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_214 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_216 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_218 :: T_IsQuasiSemiMetric_174 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_220 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_222 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_226 :: T_IsQuasiSemiMetric_174 -> T_IsPartialEquivalence_16 #

d_refl_228 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_230 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_232 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_234 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_238 :: T_IsQuasiSemiMetric_174 -> T_IsPartialEquivalence_16 #

d_refl_240 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_242 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_244 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_246 :: T_IsQuasiSemiMetric_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsSemiMetric_250 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSemiMetric_250 #

Constructors

C_IsSemiMetric'46'constructor_14005 T_IsQuasiSemiMetric_174 (AgdaAny -> AgdaAny -> AgdaAny)

d_isQuasiSemiMetric_258 :: T_IsSemiMetric_250 -> T_IsQuasiSemiMetric_174 #

d_sym_260 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny #

d_0'8658''8776'_264 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_266 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_268 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_270 :: T_IsSemiMetric_250 -> T_IsEquivalence_26 #

d_isPartialOrder_272 :: T_IsSemiMetric_250 -> T_IsPartialOrder_174 #

d_isPreMetric_274 :: T_IsSemiMetric_250 -> T_IsPreMetric_102 #

d_isPreorder_276 :: T_IsSemiMetric_250 -> T_IsPreorder_70 #

d_isProtoMetric_278 :: T_IsSemiMetric_250 -> T_IsProtoMetric_30 #

d_nonNegative_280 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_refl_282 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny #

d_reflexive_284 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_286 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8776''45'isEquivalence_288 :: T_IsSemiMetric_250 -> T_IsEquivalence_26 #

d_'8776''8658'0_290 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_292 :: T_IsSemiMetric_250 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_294 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_296 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_298 :: T_IsSemiMetric_250 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_300 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_302 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_306 :: T_IsSemiMetric_250 -> T_IsPartialEquivalence_16 #

d_refl_308 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_310 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_312 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_314 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_318 :: T_IsSemiMetric_250 -> T_IsPartialEquivalence_16 #

d_refl_320 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_322 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_324 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_326 :: T_IsSemiMetric_250 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsGeneralMetric_332 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsGeneralMetric_332 #

Constructors

C_IsGeneralMetric'46'constructor_18255 T_IsSemiMetric_250 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isSemiMetric_342 :: T_IsGeneralMetric_332 -> T_IsSemiMetric_250 #

d_triangle_344 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_0'8658''8776'_348 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_350 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_352 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_354 :: T_IsGeneralMetric_332 -> T_IsEquivalence_26 #

d_isPartialOrder_356 :: T_IsGeneralMetric_332 -> T_IsPartialOrder_174 #

d_isPreMetric_358 :: T_IsGeneralMetric_332 -> T_IsPreMetric_102 #

d_isPreorder_360 :: T_IsGeneralMetric_332 -> T_IsPreorder_70 #

d_isProtoMetric_362 :: T_IsGeneralMetric_332 -> T_IsProtoMetric_30 #

d_isQuasiSemiMetric_364 :: T_IsGeneralMetric_332 -> T_IsQuasiSemiMetric_174 #

d_nonNegative_366 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_refl_368 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny #

d_reflexive_370 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_sym_372 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_374 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8776''45'isEquivalence_376 :: T_IsGeneralMetric_332 -> T_IsEquivalence_26 #

d_'8776''8658'0_378 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_380 :: T_IsGeneralMetric_332 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_382 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_384 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_386 :: T_IsGeneralMetric_332 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_388 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_390 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_394 :: T_IsGeneralMetric_332 -> T_IsPartialEquivalence_16 #

d_refl_396 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_398 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_400 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_402 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_406 :: T_IsGeneralMetric_332 -> T_IsPartialEquivalence_16 #

d_refl_408 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_410 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_412 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_414 :: T_IsGeneralMetric_332 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #