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_constructor_26 (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_28 ∷ p → p → p → p → () Source #

data T_IsEquivalence_28 Source #

Constructors

C_constructor_46 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_refl_36 ∷ T_IsEquivalence_28 → AgdaAny → AgdaAny Source #

d_sym_38 ∷ T_IsEquivalence_28 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_40 ∷ T_IsEquivalence_28 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_reflexive_42 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_42 ∷ T_IsEquivalence_28 → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_44 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_44 ∷ T_IsEquivalence_28 → T_IsPartialEquivalence_16 Source #

d_IsDecEquivalence_48 ∷ p → p → p → p → () Source #

data T_IsDecEquivalence_48 Source #

Constructors

C_constructor_70 T_IsEquivalence_28 (AgdaAny → AgdaAny → T_Dec_20)

d_isEquivalence_54 ∷ T_IsDecEquivalence_48 → T_IsEquivalence_28 Source #

d__'8799'__56 ∷ T_IsDecEquivalence_48 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isPartialEquivalence_60 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_48 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_60 ∷ T_IsDecEquivalence_48 → T_IsPartialEquivalence_16 Source #

d_refl_62 ∷ T_IsDecEquivalence_48 → AgdaAny → AgdaAny Source #

d_reflexive_64 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_48 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_64 ∷ T_IsDecEquivalence_48 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_66 ∷ T_IsDecEquivalence_48 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_68 ∷ T_IsDecEquivalence_48 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsPreorder_76 ∷ p → p → p → p → p → p → () Source #

data T_IsPreorder_76 Source #

Constructors

C_constructor_126 T_IsEquivalence_28 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isEquivalence_86 ∷ T_IsPreorder_76 → T_IsEquivalence_28 Source #

d_reflexive_88 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_90 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_94 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_94 ∷ T_IsPreorder_76 → T_IsPartialEquivalence_16 Source #

d_refl_96 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny Source #

d_reflexive_98 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_98 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_100 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_102 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny Source #

du_refl_104 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_106 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'691''45''8776'_112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_112 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_118 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_118 ∷ T_IsPreorder_76 → T_Σ_14 Source #

d_'8764''45'resp'737''45''8776'_120 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_120 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'691''45''8776'_122 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_122 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_124 ∷ T_IsPreorder_76 → T_Σ_14 Source #

d_IsTotalPreorder_132 ∷ p → p → p → p → p → p → () Source #

data T_IsTotalPreorder_132 Source #

Constructors

C_constructor_178 T_IsPreorder_76 (AgdaAny → AgdaAny → T__'8846'__30)

d_isPreorder_140 ∷ T_IsTotalPreorder_132 → T_IsPreorder_76 Source #

d_total_142 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_isEquivalence_146 ∷ T_IsTotalPreorder_132 → T_IsEquivalence_28 Source #

d_refl_148 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → AgdaAny → AgdaAny Source #

du_refl_148 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny Source #

d_reflexive_150 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_152 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_154 ∷ T_IsTotalPreorder_132 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_156 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_156 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_158 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_158 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_160 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_160 ∷ T_IsTotalPreorder_132 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_162 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_162 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_164 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_164 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_168 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_168 ∷ T_IsTotalPreorder_132 → T_IsPartialEquivalence_16 Source #

d_refl_170 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny Source #

d_reflexive_172 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_172 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_174 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_176 ∷ T_IsTotalPreorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDecPreorder_184 ∷ p → p → p → p → p → p → () Source #

data T_IsDecPreorder_184 Source #

Constructors

C_constructor_242 T_IsPreorder_76 (AgdaAny → AgdaAny → T_Dec_20) (AgdaAny → AgdaAny → T_Dec_20)

d_isPreorder_194 ∷ T_IsDecPreorder_184 → T_IsPreorder_76 Source #

d__'8799'__196 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8818''63'__198 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_202 ∷ T_IsDecPreorder_184 → T_IsEquivalence_28 Source #

d_refl_204 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny Source #

du_refl_204 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny Source #

d_reflexive_206 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_208 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_210 ∷ T_IsDecPreorder_184 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_212 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_212 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_214 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_214 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_216 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_216 ∷ T_IsDecPreorder_184 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_218 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_218 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_220 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_220 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_224 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_224 ∷ T_IsDecPreorder_184 → T_IsDecEquivalence_48 Source #

d__'8799'__228 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__228 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_230 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → T_IsEquivalence_28 Source #

du_isEquivalence_230 ∷ T_IsDecPreorder_184 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_232 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_232 ∷ T_IsDecPreorder_184 → T_IsPartialEquivalence_16 Source #

d_refl_234 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny Source #

du_refl_234 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny Source #

d_reflexive_236 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_236 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_238 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_238 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_240 ∷ T_IsDecPreorder_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsPartialOrder_248 ∷ p → p → p → p → p → p → () Source #

data T_IsPartialOrder_248 Source #

Constructors

C_constructor_294 T_IsPreorder_76 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isPreorder_256 ∷ T_IsPartialOrder_248 → T_IsPreorder_76 Source #

d_antisym_258 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_262 ∷ T_IsPartialOrder_248 → T_IsEquivalence_28 Source #

d_refl_264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny Source #

du_refl_264 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny Source #

d_reflexive_266 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_268 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_270 ∷ T_IsPartialOrder_248 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_272 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_272 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_274 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_274 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_276 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_276 ∷ T_IsPartialOrder_248 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_278 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_278 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_280 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_284 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_284 ∷ T_IsPartialOrder_248 → T_IsPartialEquivalence_16 Source #

d_refl_286 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny Source #

d_reflexive_288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_288 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_290 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_292 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDecPartialOrder_300 ∷ p → p → p → p → p → p → () Source #

data T_IsDecPartialOrder_300 Source #

Constructors

C_constructor_364 T_IsPartialOrder_248 (AgdaAny → AgdaAny → T_Dec_20) (AgdaAny → AgdaAny → T_Dec_20)

d_isPartialOrder_310 ∷ T_IsDecPartialOrder_300 → T_IsPartialOrder_248 Source #

d__'8799'__312 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__314 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_antisym_318 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_320 ∷ T_IsDecPartialOrder_300 → T_IsEquivalence_28 Source #

d_isPreorder_322 ∷ T_IsDecPartialOrder_300 → T_IsPreorder_76 Source #

d_refl_324 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny Source #

du_refl_324 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny Source #

d_reflexive_326 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_328 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_330 ∷ T_IsDecPartialOrder_300 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_332 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_332 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_334 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_336 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_336 ∷ T_IsDecPartialOrder_300 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_338 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_338 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_340 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecPreorder_342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_IsDecPreorder_184 Source #

du_isDecPreorder_342 ∷ T_IsDecPartialOrder_300 → T_IsDecPreorder_184 Source #

d__'8799'__348 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__348 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecEquivalence_350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_350 ∷ T_IsDecPartialOrder_300 → T_IsDecEquivalence_48 Source #

d_isEquivalence_352 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_IsEquivalence_28 Source #

du_isEquivalence_352 ∷ T_IsDecPartialOrder_300 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_354 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_354 ∷ T_IsDecPartialOrder_300 → T_IsPartialEquivalence_16 Source #

d_refl_356 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny Source #

du_refl_356 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny Source #

d_reflexive_358 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_358 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_360 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_360 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_362 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_362 ∷ T_IsDecPartialOrder_300 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsStrictPartialOrder_370 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictPartialOrder_370 Source #

Constructors

C_constructor_412 T_IsEquivalence_28 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) T_Σ_14

d_isEquivalence_382 ∷ T_IsStrictPartialOrder_370 → T_IsEquivalence_28 Source #

d_irrefl_384 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_trans_386 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'45''8776'_388 ∷ T_IsStrictPartialOrder_370 → T_Σ_14 Source #

d_isPartialEquivalence_392 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_392 ∷ T_IsStrictPartialOrder_370 → T_IsPartialEquivalence_16 Source #

d_refl_394 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny Source #

d_reflexive_396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_396 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_398 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_400 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_402 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_'60''45'resp'691''45''8776'_408 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_408 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_410 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_410 ∷ T_IsStrictPartialOrder_370 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDecStrictPartialOrder_418 ∷ p → p → p → p → p → p → () Source #

data T_IsDecStrictPartialOrder_418 Source #

Constructors

C_constructor_482 T_IsStrictPartialOrder_370 (AgdaAny → AgdaAny → T_Dec_20) (AgdaAny → AgdaAny → T_Dec_20)

d_isStrictPartialOrder_428 ∷ T_IsDecStrictPartialOrder_418 → T_IsStrictPartialOrder_370 Source #

d__'8799'__430 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'60''63'__432 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_'60''45'resp'45''8776'_436 ∷ T_IsDecStrictPartialOrder_418 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_438 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_438 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_440 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_442 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_444 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_446 ∷ T_IsDecStrictPartialOrder_418 → T_IsEquivalence_28 Source #

d_trans_448 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_452 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_452 ∷ T_IsDecStrictPartialOrder_418 → T_IsPartialEquivalence_16 Source #

d_refl_454 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny Source #

d_reflexive_456 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_456 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_458 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_460 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_464 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_464 ∷ T_IsDecStrictPartialOrder_418 → T_IsDecEquivalence_48 Source #

d__'8799'__468 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__468 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_470 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsEquivalence_28 Source #

du_isEquivalence_470 ∷ T_IsDecStrictPartialOrder_418 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_472 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_472 ∷ T_IsDecStrictPartialOrder_418 → T_IsPartialEquivalence_16 Source #

d_refl_474 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny Source #

du_refl_474 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny Source #

d_reflexive_476 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_476 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_478 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_478 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_480 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_480 ∷ T_IsDecStrictPartialOrder_418 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsTotalOrder_488 ∷ p → p → p → p → p → p → () Source #

data T_IsTotalOrder_488 Source #

Constructors

C_constructor_540 T_IsPartialOrder_248 (AgdaAny → AgdaAny → T__'8846'__30)

d_isPartialOrder_496 ∷ T_IsTotalOrder_488 → T_IsPartialOrder_248 Source #

d_total_498 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_antisym_502 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_504 ∷ T_IsTotalOrder_488 → T_IsEquivalence_28 Source #

d_isPreorder_506 ∷ T_IsTotalOrder_488 → T_IsPreorder_76 Source #

d_refl_508 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → AgdaAny → AgdaAny Source #

du_refl_508 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny Source #

d_reflexive_510 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_512 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_514 ∷ T_IsTotalOrder_488 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_516 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_516 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_518 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_520 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_520 ∷ T_IsTotalOrder_488 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_522 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_522 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_524 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_524 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_528 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_528 ∷ T_IsTotalOrder_488 → T_IsPartialEquivalence_16 Source #

d_refl_530 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny Source #

d_reflexive_532 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_532 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_534 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_536 ∷ T_IsTotalOrder_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isTotalPreorder_538 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → T_IsTotalPreorder_132 Source #

du_isTotalPreorder_538 ∷ T_IsTotalOrder_488 → T_IsTotalPreorder_132 Source #

d_IsDecTotalOrder_546 ∷ p → p → p → p → p → p → () Source #

data T_IsDecTotalOrder_546 Source #

Constructors

C_constructor_618 T_IsTotalOrder_488 (AgdaAny → AgdaAny → T_Dec_20) (AgdaAny → AgdaAny → T_Dec_20)

d_isTotalOrder_556 ∷ T_IsDecTotalOrder_546 → T_IsTotalOrder_488 Source #

d__'8799'__558 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__560 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_antisym_564 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_566 ∷ T_IsDecTotalOrder_546 → T_IsEquivalence_28 Source #

d_isPartialOrder_568 ∷ T_IsDecTotalOrder_546 → T_IsPartialOrder_248 Source #

d_isPreorder_570 ∷ T_IsDecTotalOrder_546 → T_IsPreorder_76 Source #

d_isTotalPreorder_572 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsTotalPreorder_132 Source #

du_isTotalPreorder_572 ∷ T_IsDecTotalOrder_546 → T_IsTotalPreorder_132 Source #

d_refl_574 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny Source #

du_refl_574 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny Source #

d_reflexive_576 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_578 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_580 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_582 ∷ T_IsDecTotalOrder_546 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_584 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_584 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_586 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_586 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_588 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_588 ∷ T_IsDecTotalOrder_546 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_590 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_590 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_592 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_592 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecPartialOrder_594 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsDecPartialOrder_300 Source #

du_isDecPartialOrder_594 ∷ T_IsDecTotalOrder_546 → T_IsDecPartialOrder_300 Source #

d_isDecPreorder_598 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsDecPreorder_184 Source #

du_isDecPreorder_598 ∷ T_IsDecTotalOrder_546 → T_IsDecPreorder_184 Source #

d__'8799'__602 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__602 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecEquivalence_604 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_604 ∷ T_IsDecTotalOrder_546 → T_IsDecEquivalence_48 Source #

d_isEquivalence_606 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsEquivalence_28 Source #

du_isEquivalence_606 ∷ T_IsDecTotalOrder_546 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_608 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_608 ∷ T_IsDecTotalOrder_546 → T_IsPartialEquivalence_16 Source #

d_refl_610 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny Source #

du_refl_610 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny Source #

d_reflexive_612 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_612 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_614 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_614 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_616 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_616 ∷ T_IsDecTotalOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsStrictTotalOrder_624 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictTotalOrder_624 Source #

Constructors

C_constructor_680 T_IsStrictPartialOrder_370 (AgdaAny → AgdaAny → T_Tri_158)

d_isStrictPartialOrder_632 ∷ T_IsStrictTotalOrder_624 → T_IsStrictPartialOrder_370 Source #

d_compare_634 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_'60''45'resp'45''8776'_638 ∷ T_IsStrictTotalOrder_624 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_640 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_640 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_642 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_642 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_644 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_646 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_648 ∷ T_IsStrictTotalOrder_624 → T_IsEquivalence_28 Source #

d_trans_650 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8799'__652 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__652 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'60''63'__654 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'60''63'__654 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecStrictPartialOrder_656 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsDecStrictPartialOrder_418 Source #

du_isDecStrictPartialOrder_656 ∷ T_IsStrictTotalOrder_624 → T_IsDecStrictPartialOrder_418 Source #

d_isDecEquivalence_660 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_660 ∷ T_IsStrictTotalOrder_624 → T_IsDecEquivalence_48 Source #

d__'8799'__664 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__664 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_666 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsEquivalence_28 Source #

du_isEquivalence_666 ∷ T_IsStrictTotalOrder_624 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_668 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_668 ∷ T_IsStrictTotalOrder_624 → T_IsPartialEquivalence_16 Source #

d_refl_670 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny Source #

du_refl_670 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny Source #

d_reflexive_672 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_672 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_674 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_674 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_676 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_676 ∷ T_IsStrictTotalOrder_624 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_678 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_678 ∷ T_IsStrictTotalOrder_624 → T_IsDecEquivalence_48 Source #

d_IsDenseLinearOrder_686 ∷ p → p → p → p → p → p → () Source #

data T_IsDenseLinearOrder_686 Source #

Constructors

C_constructor_744 T_IsStrictTotalOrder_624 (AgdaAny → AgdaAny → AgdaAny → T_Σ_14)

d_isStrictTotalOrder_694 ∷ T_IsDenseLinearOrder_686 → T_IsStrictTotalOrder_624 Source #

d_dense_696 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d__'60''63'__700 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'60''63'__700 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8799'__702 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__702 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_'60''45'resp'45''8776'_704 ∷ T_IsDenseLinearOrder_686 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_706 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_706 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_708 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_708 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_710 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_compare_712 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_irrefl_714 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isDecEquivalence_716 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_716 ∷ T_IsDenseLinearOrder_686 → T_IsDecEquivalence_48 Source #

d_isDecStrictPartialOrder_718 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → T_IsDecStrictPartialOrder_418 Source #

du_isDecStrictPartialOrder_718 ∷ T_IsDenseLinearOrder_686 → T_IsDecStrictPartialOrder_418 Source #

d_isEquivalence_720 ∷ T_IsDenseLinearOrder_686 → T_IsEquivalence_28 Source #

d_isStrictPartialOrder_722 ∷ T_IsDenseLinearOrder_686 → T_IsStrictPartialOrder_370 Source #

d_trans_724 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8799'__728 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__728 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecEquivalence_730 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_730 ∷ T_IsDenseLinearOrder_686 → T_IsDecEquivalence_48 Source #

d_isEquivalence_732 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → T_IsEquivalence_28 Source #

du_isEquivalence_732 ∷ T_IsDenseLinearOrder_686 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_734 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_734 ∷ T_IsDenseLinearOrder_686 → T_IsPartialEquivalence_16 Source #

d_refl_736 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny Source #

du_refl_736 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny Source #

d_reflexive_738 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_738 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_740 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_740 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_742 ∷ T_IsDenseLinearOrder_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsApartnessRelation_750 ∷ p → p → p → p → p → p → () Source #

data T_IsApartnessRelation_750 Source #

Constructors

C_constructor_772 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8846'__30)

d_irrefl_760 ∷ T_IsApartnessRelation_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_sym_762 ∷ T_IsApartnessRelation_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cotrans_764 ∷ T_IsApartnessRelation_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8846'__30 Source #

d__'172''35'__766 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsApartnessRelation_750 → AgdaAny → AgdaAny → () Source #