Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Relation.Binary.Structures

Documentation

d_IsPartialEquivalence_16 :: p -> p -> p -> p -> () #

data T_IsPartialEquivalence_16 #

Constructors

C_IsPartialEquivalence'46'constructor_273 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_sym_22 :: T_IsPartialEquivalence_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_24 :: T_IsPartialEquivalence_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsEquivalence_26 :: p -> p -> p -> p -> () #

data T_IsEquivalence_26 #

Constructors

C_IsEquivalence'46'constructor_745 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_refl_34 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny #

d_sym_36 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_38 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_reflexive_40 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_40 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_42 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_42 :: T_IsEquivalence_26 -> T_IsPartialEquivalence_16 #

d_IsDecEquivalence_44 :: p -> p -> p -> p -> () #

data T_IsDecEquivalence_44 #

Constructors

C_IsDecEquivalence'46'constructor_3083 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> T_Dec_20)

d_isEquivalence_50 :: T_IsDecEquivalence_44 -> T_IsEquivalence_26 #

d__'8799'__52 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isPartialEquivalence_56 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_56 :: T_IsDecEquivalence_44 -> T_IsPartialEquivalence_16 #

d_refl_58 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny #

d_reflexive_60 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_60 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_62 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_64 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsPreorder_70 :: p -> p -> p -> p -> p -> p -> () #

data T_IsPreorder_70 #

Constructors

C_IsPreorder'46'constructor_4003 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isEquivalence_80 :: T_IsPreorder_70 -> T_IsEquivalence_26 #

d_reflexive_82 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_84 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_88 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_88 :: T_IsPreorder_70 -> T_IsPartialEquivalence_16 #

d_refl_90 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny #

d_reflexive_92 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_92 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_94 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_96 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_refl_98 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny #

du_refl_98 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_100 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_100 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'691''45''8776'_106 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_106 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_112 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_112 :: T_IsPreorder_70 -> T_Σ_14 #

d_'8764''45'resp'737''45''8776'_114 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_114 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'691''45''8776'_116 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_116 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_118 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_118 :: T_IsPreorder_70 -> T_Σ_14 #

d_IsTotalPreorder_124 :: p -> p -> p -> p -> p -> p -> () #

data T_IsTotalPreorder_124 #

Constructors

C_IsTotalPreorder'46'constructor_8325 T_IsPreorder_70 (AgdaAny -> AgdaAny -> T__'8846'__30)

d_isPreorder_132 :: T_IsTotalPreorder_124 -> T_IsPreorder_70 #

d_total_134 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> T__'8846'__30 #

d_isEquivalence_138 :: T_IsTotalPreorder_124 -> T_IsEquivalence_26 #

d_refl_140 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny #

du_refl_140 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny #

d_reflexive_142 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_144 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_146 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_146 :: T_IsTotalPreorder_124 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_148 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_148 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_150 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_150 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_152 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_152 :: T_IsTotalPreorder_124 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_154 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_154 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_156 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_156 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_160 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_160 :: T_IsTotalPreorder_124 -> T_IsPartialEquivalence_16 #

d_refl_162 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny #

d_reflexive_164 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_164 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_166 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_168 :: T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsPartialOrder_174 :: p -> p -> p -> p -> p -> p -> () #

data T_IsPartialOrder_174 #

Constructors

C_IsPartialOrder'46'constructor_9853 T_IsPreorder_70 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isPreorder_182 :: T_IsPartialOrder_174 -> T_IsPreorder_70 #

d_antisym_184 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_188 :: T_IsPartialOrder_174 -> T_IsEquivalence_26 #

d_refl_190 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> AgdaAny -> AgdaAny #

du_refl_190 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny #

d_reflexive_192 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_194 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_196 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_196 :: T_IsPartialOrder_174 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_198 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_198 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_200 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_200 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_202 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_202 :: T_IsPartialOrder_174 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_204 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_204 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_206 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_206 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_210 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_210 :: T_IsPartialOrder_174 -> T_IsPartialEquivalence_16 #

d_refl_212 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny #

d_reflexive_214 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_214 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_216 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_218 :: T_IsPartialOrder_174 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsDecPartialOrder_224 :: p -> p -> p -> p -> p -> p -> () #

data T_IsDecPartialOrder_224 #

Constructors

C_IsDecPartialOrder'46'constructor_11683 T_IsPartialOrder_174 (AgdaAny -> AgdaAny -> T_Dec_20) (AgdaAny -> AgdaAny -> T_Dec_20)

d_isPartialOrder_234 :: T_IsDecPartialOrder_224 -> T_IsPartialOrder_174 #

d__'8799'__236 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d__'8804''63'__238 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_antisym_242 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_244 :: T_IsDecPartialOrder_224 -> T_IsEquivalence_26 #

d_isPreorder_246 :: T_IsDecPartialOrder_224 -> T_IsPreorder_70 #

d_refl_248 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny #

du_refl_248 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny #

d_reflexive_250 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_252 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_254 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_254 :: T_IsDecPartialOrder_224 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_256 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_256 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_258 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_258 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_260 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_260 :: T_IsDecPartialOrder_224 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_262 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_262 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_264 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_264 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isDecEquivalence_268 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_268 :: T_IsDecPartialOrder_224 -> T_IsDecEquivalence_44 #

d__'8799'__272 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__272 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isEquivalence_274 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_IsEquivalence_26 #

du_isEquivalence_274 :: T_IsDecPartialOrder_224 -> T_IsEquivalence_26 #

d_isPartialEquivalence_276 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_276 :: T_IsDecPartialOrder_224 -> T_IsPartialEquivalence_16 #

d_refl_278 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny #

du_refl_278 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny #

d_reflexive_280 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_280 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_282 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_282 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_284 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_284 :: T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsStrictPartialOrder_290 :: p -> p -> p -> p -> p -> p -> () #

data T_IsStrictPartialOrder_290 #

Constructors

C_IsStrictPartialOrder'46'constructor_14045 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14

d_isEquivalence_302 :: T_IsStrictPartialOrder_290 -> T_IsEquivalence_26 #

d_irrefl_304 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_trans_306 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'60''45'resp'45''8776'_308 :: T_IsStrictPartialOrder_290 -> T_Σ_14 #

d_isPartialEquivalence_312 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_312 :: T_IsStrictPartialOrder_290 -> T_IsPartialEquivalence_16 #

d_refl_314 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny #

d_reflexive_316 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_316 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_318 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_320 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_asym_322 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_'60''45'resp'691''45''8776'_328 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'691''45''8776'_328 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'60''45'resp'737''45''8776'_330 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'737''45''8776'_330 :: T_IsStrictPartialOrder_290 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsDecStrictPartialOrder_336 :: p -> p -> p -> p -> p -> p -> () #

data T_IsDecStrictPartialOrder_336 #

Constructors

C_IsDecStrictPartialOrder'46'constructor_18663 T_IsStrictPartialOrder_290 (AgdaAny -> AgdaAny -> T_Dec_20) (AgdaAny -> AgdaAny -> T_Dec_20)

d_isStrictPartialOrder_346 :: T_IsDecStrictPartialOrder_336 -> T_IsStrictPartialOrder_290 #

d__'8799'__348 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d__'60''63'__350 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_'60''45'resp'45''8776'_354 :: T_IsDecStrictPartialOrder_336 -> T_Σ_14 #

d_'60''45'resp'691''45''8776'_356 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'691''45''8776'_356 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'60''45'resp'737''45''8776'_358 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'737''45''8776'_358 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_asym_360 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_irrefl_362 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_isEquivalence_364 :: T_IsDecStrictPartialOrder_336 -> T_IsEquivalence_26 #

d_trans_366 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_370 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_370 :: T_IsDecStrictPartialOrder_336 -> T_IsPartialEquivalence_16 #

d_refl_372 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny #

d_reflexive_374 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_374 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_376 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_378 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isDecEquivalence_382 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_382 :: T_IsDecStrictPartialOrder_336 -> T_IsDecEquivalence_44 #

d__'8799'__386 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__386 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isEquivalence_388 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> T_IsEquivalence_26 #

du_isEquivalence_388 :: T_IsDecStrictPartialOrder_336 -> T_IsEquivalence_26 #

d_isPartialEquivalence_390 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_390 :: T_IsDecStrictPartialOrder_336 -> T_IsPartialEquivalence_16 #

d_refl_392 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny #

du_refl_392 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny #

d_reflexive_394 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_394 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_396 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_396 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_398 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_398 :: T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsTotalOrder_404 :: p -> p -> p -> p -> p -> p -> () #

data T_IsTotalOrder_404 #

Constructors

C_IsTotalOrder'46'constructor_20555 T_IsPartialOrder_174 (AgdaAny -> AgdaAny -> T__'8846'__30)

d_isPartialOrder_412 :: T_IsTotalOrder_404 -> T_IsPartialOrder_174 #

d_total_414 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> T__'8846'__30 #

d_antisym_418 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_420 :: T_IsTotalOrder_404 -> T_IsEquivalence_26 #

d_isPreorder_422 :: T_IsTotalOrder_404 -> T_IsPreorder_70 #

d_refl_424 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> AgdaAny -> AgdaAny #

du_refl_424 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny #

d_reflexive_426 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_428 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_430 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_430 :: T_IsTotalOrder_404 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_432 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_432 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_434 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_434 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_436 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_436 :: T_IsTotalOrder_404 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_438 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_438 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_440 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_440 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_444 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_444 :: T_IsTotalOrder_404 -> T_IsPartialEquivalence_16 #

d_refl_446 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny #

d_reflexive_448 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_448 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_450 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_452 :: T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isTotalPreorder_454 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_IsTotalPreorder_124 #

du_isTotalPreorder_454 :: T_IsTotalOrder_404 -> T_IsTotalPreorder_124 #

d_IsDecTotalOrder_460 :: p -> p -> p -> p -> p -> p -> () #

data T_IsDecTotalOrder_460 #

Constructors

C_IsDecTotalOrder'46'constructor_22695 T_IsTotalOrder_404 (AgdaAny -> AgdaAny -> T_Dec_20) (AgdaAny -> AgdaAny -> T_Dec_20)

d_isTotalOrder_470 :: T_IsDecTotalOrder_460 -> T_IsTotalOrder_404 #

d__'8799'__472 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d__'8804''63'__474 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_antisym_478 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_480 :: T_IsDecTotalOrder_460 -> T_IsEquivalence_26 #

d_isPartialOrder_482 :: T_IsDecTotalOrder_460 -> T_IsPartialOrder_174 #

d_isPreorder_484 :: T_IsDecTotalOrder_460 -> T_IsPreorder_70 #

d_isTotalPreorder_486 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsTotalPreorder_124 #

du_isTotalPreorder_486 :: T_IsDecTotalOrder_460 -> T_IsTotalPreorder_124 #

d_refl_488 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny #

du_refl_488 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny #

d_reflexive_490 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_total_492 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T__'8846'__30 #

d_trans_494 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_496 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_496 :: T_IsDecTotalOrder_460 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_498 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_498 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_500 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_500 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_502 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_502 :: T_IsDecTotalOrder_460 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_504 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_504 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_506 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_506 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isDecPartialOrder_508 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsDecPartialOrder_224 #

du_isDecPartialOrder_508 :: T_IsDecTotalOrder_460 -> T_IsDecPartialOrder_224 #

d_isDecEquivalence_512 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_512 :: T_IsDecTotalOrder_460 -> T_IsDecEquivalence_44 #

d__'8799'__516 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__516 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isEquivalence_518 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsEquivalence_26 #

du_isEquivalence_518 :: T_IsDecTotalOrder_460 -> T_IsEquivalence_26 #

d_isPartialEquivalence_520 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_520 :: T_IsDecTotalOrder_460 -> T_IsPartialEquivalence_16 #

d_refl_522 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny #

du_refl_522 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny #

d_reflexive_524 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_524 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_526 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_526 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_528 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_528 :: T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsStrictTotalOrder_534 :: p -> p -> p -> p -> p -> p -> () #

data T_IsStrictTotalOrder_534 #

Constructors

C_IsStrictTotalOrder'46'constructor_24953 T_IsStrictPartialOrder_290 (AgdaAny -> AgdaAny -> T_Tri_158)

d_isStrictPartialOrder_542 :: T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290 #

d_compare_544 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158 #

d_'60''45'resp'45''8776'_548 :: T_IsStrictTotalOrder_534 -> T_Σ_14 #

d_'60''45'resp'691''45''8776'_550 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'691''45''8776'_550 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'60''45'resp'737''45''8776'_552 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'737''45''8776'_552 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_asym_554 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_irrefl_556 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_isEquivalence_558 :: T_IsStrictTotalOrder_534 -> T_IsEquivalence_26 #

d_trans_560 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8799'__562 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__562 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d__'60''63'__564 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'60''63'__564 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isDecStrictPartialOrder_566 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsDecStrictPartialOrder_336 #

du_isDecStrictPartialOrder_566 :: T_IsStrictTotalOrder_534 -> T_IsDecStrictPartialOrder_336 #

d_isDecEquivalence_570 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_570 :: T_IsStrictTotalOrder_534 -> T_IsDecEquivalence_44 #

d__'8799'__574 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__574 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isEquivalence_576 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsEquivalence_26 #

du_isEquivalence_576 :: T_IsStrictTotalOrder_534 -> T_IsEquivalence_26 #

d_isPartialEquivalence_578 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_578 :: T_IsStrictTotalOrder_534 -> T_IsPartialEquivalence_16 #

d_refl_580 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny #

du_refl_580 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny #

d_reflexive_582 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_582 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_584 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_584 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_586 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_586 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isDecEquivalence_588 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_588 :: T_IsStrictTotalOrder_534 -> T_IsDecEquivalence_44 #

d_IsDenseLinearOrder_594 :: p -> p -> p -> p -> p -> p -> () #

data T_IsDenseLinearOrder_594 #

Constructors

C_IsDenseLinearOrder'46'constructor_28131 T_IsStrictTotalOrder_534 (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)

d_isStrictTotalOrder_602 :: T_IsDenseLinearOrder_594 -> T_IsStrictTotalOrder_534 #

d_dense_604 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 #

d__'60''63'__608 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'60''63'__608 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d__'8799'__610 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__610 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_'60''45'resp'45''8776'_612 :: T_IsDenseLinearOrder_594 -> T_Σ_14 #

d_'60''45'resp'691''45''8776'_614 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'691''45''8776'_614 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'60''45'resp'737''45''8776'_616 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'60''45'resp'737''45''8776'_616 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_asym_618 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_compare_620 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Tri_158 #

d_irrefl_622 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_isDecEquivalence_624 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_624 :: T_IsDenseLinearOrder_594 -> T_IsDecEquivalence_44 #

d_isDecStrictPartialOrder_626 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> T_IsDecStrictPartialOrder_336 #

du_isDecStrictPartialOrder_626 :: T_IsDenseLinearOrder_594 -> T_IsDecStrictPartialOrder_336 #

d_isEquivalence_628 :: T_IsDenseLinearOrder_594 -> T_IsEquivalence_26 #

d_isStrictPartialOrder_630 :: T_IsDenseLinearOrder_594 -> T_IsStrictPartialOrder_290 #

d_trans_632 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8799'__636 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du__'8799'__636 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_isDecEquivalence_638 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> T_IsDecEquivalence_44 #

du_isDecEquivalence_638 :: T_IsDenseLinearOrder_594 -> T_IsDecEquivalence_44 #

d_isEquivalence_640 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> T_IsEquivalence_26 #

du_isEquivalence_640 :: T_IsDenseLinearOrder_594 -> T_IsEquivalence_26 #

d_isPartialEquivalence_642 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_642 :: T_IsDenseLinearOrder_594 -> T_IsPartialEquivalence_16 #

d_refl_644 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny #

du_refl_644 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny #

d_reflexive_646 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_646 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_648 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_648 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_650 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_650 :: T_IsDenseLinearOrder_594 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsApartnessRelation_656 :: p -> p -> p -> p -> p -> p -> () #

data T_IsApartnessRelation_656 #

Constructors

C_IsApartnessRelation'46'constructor_30225 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30)

d_irrefl_666 :: T_IsApartnessRelation_656 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #

d_sym_668 :: T_IsApartnessRelation_656 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cotrans_670 :: T_IsApartnessRelation_656 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30 #

d__'172''35'__672 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsApartnessRelation_656 -> AgdaAny -> AgdaAny -> () #