Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Relation.Binary.Structures

Documentation

d_IsPartialEquivalence_16 ∷ p → p → p → p → () Source #

data T_IsPartialEquivalence_16 Source #

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 Source #

d_trans_24 ∷ T_IsPartialEquivalence_16 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsEquivalence_26 ∷ p → p → p → p → () Source #

data T_IsEquivalence_26 Source #

Constructors

C_IsEquivalence'46'constructor_743 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_refl_34 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny Source #

d_sym_36 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_38 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_reflexive_40 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_40 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_42 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_42 ∷ T_IsEquivalence_26 → T_IsPartialEquivalence_16 Source #

d_IsDecEquivalence_44 ∷ p → p → p → p → () Source #

data T_IsDecEquivalence_44 Source #

Constructors

C_IsDecEquivalence'46'constructor_3075 T_IsEquivalence_26 (AgdaAny → AgdaAny → T_Dec_32)

d_isEquivalence_50 ∷ T_IsDecEquivalence_44 → T_IsEquivalence_26 Source #

d__'8799'__52 ∷ T_IsDecEquivalence_44 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isPartialEquivalence_56 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_56 ∷ T_IsDecEquivalence_44 → T_IsPartialEquivalence_16 Source #

d_refl_58 ∷ T_IsDecEquivalence_44 → AgdaAny → AgdaAny Source #

d_reflexive_60 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_60 ∷ T_IsDecEquivalence_44 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_62 ∷ T_IsDecEquivalence_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_64 ∷ T_IsDecEquivalence_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsPreorder_70 ∷ p → p → p → p → p → p → () Source #

data T_IsPreorder_70 Source #

Constructors

C_IsPreorder'46'constructor_3993 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isEquivalence_80 ∷ T_IsPreorder_70 → T_IsEquivalence_26 Source #

d_reflexive_82 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_84 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_88 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_88 ∷ T_IsPreorder_70 → T_IsPartialEquivalence_16 Source #

d_refl_90 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny Source #

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 Source #

du_reflexive_92 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_94 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_96 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_98 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → AgdaAny → AgdaAny Source #

du_refl_98 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_100 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'691''45''8776'_106 ∷ T_IsPreorder_70 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_112 ∷ T_IsPreorder_70 → T_Σ_14 Source #

d_IsTotalPreorder_118 ∷ p → p → p → p → p → p → () Source #

data T_IsTotalPreorder_118 Source #

Constructors

C_IsTotalPreorder'46'constructor_7939 T_IsPreorder_70 (AgdaAny → AgdaAny → T__'8846'__30)

d_isPreorder_126 ∷ T_IsTotalPreorder_118 → T_IsPreorder_70 Source #

d_total_128 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_isEquivalence_132 ∷ T_IsTotalPreorder_118 → T_IsEquivalence_26 Source #

d_refl_134 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → AgdaAny → AgdaAny Source #

du_refl_134 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny Source #

d_reflexive_136 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_138 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_140 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_140 ∷ T_IsTotalPreorder_118 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_142 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_142 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_144 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_144 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_148 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_148 ∷ T_IsTotalPreorder_118 → T_IsPartialEquivalence_16 Source #

d_refl_150 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny Source #

d_reflexive_152 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_152 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_154 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_156 ∷ T_IsTotalPreorder_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsPartialOrder_162 ∷ p → p → p → p → p → p → () Source #

data T_IsPartialOrder_162 Source #

Constructors

C_IsPartialOrder'46'constructor_9297 T_IsPreorder_70 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isPreorder_170 ∷ T_IsPartialOrder_162 → T_IsPreorder_70 Source #

d_antisym_172 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_176 ∷ T_IsPartialOrder_162 → T_IsEquivalence_26 Source #

d_refl_178 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → AgdaAny → AgdaAny Source #

du_refl_178 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny Source #

d_reflexive_180 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_182 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_184 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_184 ∷ T_IsPartialOrder_162 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_186 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_186 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_188 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_188 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_192 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_192 ∷ T_IsPartialOrder_162 → T_IsPartialEquivalence_16 Source #

d_refl_194 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny Source #

d_reflexive_196 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_196 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_198 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_200 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDecPartialOrder_206 ∷ p → p → p → p → p → p → () Source #

data T_IsDecPartialOrder_206 Source #

Constructors

C_IsDecPartialOrder'46'constructor_10957 T_IsPartialOrder_162 (AgdaAny → AgdaAny → T_Dec_32) (AgdaAny → AgdaAny → T_Dec_32)

d_isPartialOrder_216 ∷ T_IsDecPartialOrder_206 → T_IsPartialOrder_162 Source #

d__'8799'__218 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'8804''63'__220 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_antisym_224 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_226 ∷ T_IsDecPartialOrder_206 → T_IsEquivalence_26 Source #

d_isPreorder_228 ∷ T_IsDecPartialOrder_206 → T_IsPreorder_70 Source #

d_refl_230 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny Source #

du_refl_230 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny Source #

d_reflexive_232 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_234 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_236 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_236 ∷ T_IsDecPartialOrder_206 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_238 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_238 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_240 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_244 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_244 ∷ T_IsDecPartialOrder_206 → T_IsDecEquivalence_44 Source #

d__'8799'__248 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__248 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isEquivalence_250 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsEquivalence_26 Source #

du_isEquivalence_250 ∷ T_IsDecPartialOrder_206 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_252 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_252 ∷ T_IsDecPartialOrder_206 → T_IsPartialEquivalence_16 Source #

d_refl_254 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny Source #

du_refl_254 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny Source #

d_reflexive_256 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_256 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_258 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_258 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_260 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_260 ∷ T_IsDecPartialOrder_206 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsStrictPartialOrder_266 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictPartialOrder_266 Source #

Constructors

C_IsStrictPartialOrder'46'constructor_13145 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) T_Σ_14

d_isEquivalence_278 ∷ T_IsStrictPartialOrder_266 → T_IsEquivalence_26 Source #

d_irrefl_280 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_trans_282 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'45''8776'_284 ∷ T_IsStrictPartialOrder_266 → T_Σ_14 Source #

d_isPartialEquivalence_288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_288 ∷ T_IsStrictPartialOrder_266 → T_IsPartialEquivalence_16 Source #

d_refl_290 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny Source #

d_reflexive_292 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_292 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_294 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_296 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_298 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_'60''45'resp'691''45''8776'_304 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_304 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_306 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_306 ∷ T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asymmetric_308 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_IsDecStrictPartialOrder_314 ∷ p → p → p → p → p → p → () Source #

data T_IsDecStrictPartialOrder_314 Source #

Constructors

C_IsDecStrictPartialOrder'46'constructor_17873 T_IsStrictPartialOrder_266 (AgdaAny → AgdaAny → T_Dec_32) (AgdaAny → AgdaAny → T_Dec_32)

d_isStrictPartialOrder_324 ∷ T_IsDecStrictPartialOrder_314 → T_IsStrictPartialOrder_266 Source #

d__'8799'__326 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'60''63'__328 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_'60''45'resp'45''8776'_332 ∷ T_IsDecStrictPartialOrder_314 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_334 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_336 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_336 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_338 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_asymmetric_340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_irrefl_342 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_isEquivalence_344 ∷ T_IsDecStrictPartialOrder_314 → T_IsEquivalence_26 Source #

d_trans_346 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_350 ∷ T_IsDecStrictPartialOrder_314 → T_IsPartialEquivalence_16 Source #

d_refl_352 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny Source #

d_reflexive_354 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_354 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_356 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_358 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_362 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_362 ∷ T_IsDecStrictPartialOrder_314 → T_IsDecEquivalence_44 Source #

d__'8799'__366 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__366 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isEquivalence_368 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsEquivalence_26 Source #

du_isEquivalence_368 ∷ T_IsDecStrictPartialOrder_314 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_370 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_370 ∷ T_IsDecStrictPartialOrder_314 → T_IsPartialEquivalence_16 Source #

d_refl_372 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny Source #

du_refl_372 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny Source #

d_reflexive_374 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_374 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_376 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_376 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_378 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_378 ∷ T_IsDecStrictPartialOrder_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsTotalOrder_384 ∷ p → p → p → p → p → p → () Source #

data T_IsTotalOrder_384 Source #

Constructors

C_IsTotalOrder'46'constructor_19815 T_IsPartialOrder_162 (AgdaAny → AgdaAny → T__'8846'__30)

d_isPartialOrder_392 ∷ T_IsTotalOrder_384 → T_IsPartialOrder_162 Source #

d_total_394 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_antisym_398 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_400 ∷ T_IsTotalOrder_384 → T_IsEquivalence_26 Source #

d_isPreorder_402 ∷ T_IsTotalOrder_384 → T_IsPreorder_70 Source #

d_refl_404 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → AgdaAny → AgdaAny Source #

du_refl_404 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny Source #

d_reflexive_406 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_408 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_410 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_410 ∷ T_IsTotalOrder_384 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_412 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_412 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_414 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_414 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_418 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_418 ∷ T_IsTotalOrder_384 → T_IsPartialEquivalence_16 Source #

d_refl_420 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny Source #

d_reflexive_422 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_422 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_424 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_426 ∷ T_IsTotalOrder_384 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isTotalPreorder_428 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_IsTotalPreorder_118 Source #

du_isTotalPreorder_428 ∷ T_IsTotalOrder_384 → T_IsTotalPreorder_118 Source #

d_IsDecTotalOrder_434 ∷ p → p → p → p → p → p → () Source #

data T_IsDecTotalOrder_434 Source #

Constructors

C_IsDecTotalOrder'46'constructor_21785 T_IsTotalOrder_384 (AgdaAny → AgdaAny → T_Dec_32) (AgdaAny → AgdaAny → T_Dec_32)

d_isTotalOrder_444 ∷ T_IsDecTotalOrder_434 → T_IsTotalOrder_384 Source #

d__'8799'__446 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'8804''63'__448 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_antisym_452 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_454 ∷ T_IsDecTotalOrder_434 → T_IsEquivalence_26 Source #

d_isPartialOrder_456 ∷ T_IsDecTotalOrder_434 → T_IsPartialOrder_162 Source #

d_isPreorder_458 ∷ T_IsDecTotalOrder_434 → T_IsPreorder_70 Source #

d_isTotalPreorder_460 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsTotalPreorder_118 Source #

du_isTotalPreorder_460 ∷ T_IsDecTotalOrder_434 → T_IsTotalPreorder_118 Source #

d_refl_462 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny Source #

du_refl_462 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny Source #

d_reflexive_464 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_466 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_468 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_470 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_470 ∷ T_IsDecTotalOrder_434 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_472 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_472 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_474 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_474 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecPartialOrder_476 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsDecPartialOrder_206 Source #

du_isDecPartialOrder_476 ∷ T_IsDecTotalOrder_434 → T_IsDecPartialOrder_206 Source #

d_isDecEquivalence_480 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_480 ∷ T_IsDecTotalOrder_434 → T_IsDecEquivalence_44 Source #

d__'8799'__484 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__484 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isEquivalence_486 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsEquivalence_26 Source #

du_isEquivalence_486 ∷ T_IsDecTotalOrder_434 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_488 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_488 ∷ T_IsDecTotalOrder_434 → T_IsPartialEquivalence_16 Source #

d_refl_490 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny Source #

du_refl_490 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny Source #

d_reflexive_492 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_492 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_494 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_494 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_496 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_496 ∷ T_IsDecTotalOrder_434 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsStrictTotalOrder_502 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictTotalOrder_502 Source #

Constructors

C_IsStrictTotalOrder'46'constructor_23999 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → T_Tri_136)

d_isEquivalence_512 ∷ T_IsStrictTotalOrder_502 → T_IsEquivalence_26 Source #

d_trans_514 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_compare_516 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Tri_136 Source #

d__'8799'__518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__518 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'60''63'__520 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'60''63'__520 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isDecEquivalence_522 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_522 ∷ T_IsStrictTotalOrder_502 → T_IsDecEquivalence_44 Source #

d__'8799'__526 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__526 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isEquivalence_528 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsEquivalence_26 Source #

du_isEquivalence_528 ∷ T_IsStrictTotalOrder_502 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_530 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_530 ∷ T_IsStrictTotalOrder_502 → T_IsPartialEquivalence_16 Source #

d_refl_532 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny Source #

du_refl_532 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny Source #

d_reflexive_534 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_534 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_536 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_536 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_538 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_538 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isStrictPartialOrder_540 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictPartialOrder_266 Source #

du_isStrictPartialOrder_540 ∷ T_IsStrictTotalOrder_502 → T_IsStrictPartialOrder_266 Source #

d_isDecStrictPartialOrder_542 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsDecStrictPartialOrder_314 Source #

du_isDecStrictPartialOrder_542 ∷ T_IsStrictTotalOrder_502 → T_IsDecStrictPartialOrder_314 Source #

d_'60''45'resp'45''8776'_546 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_546 ∷ T_IsStrictTotalOrder_502 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_548 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_548 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_550 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_550 ∷ T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_552 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_irrefl_554 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #