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_745 (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_3083 T_IsEquivalence_26 (AgdaAny → AgdaAny → T_Dec_20)

d_isEquivalence_50 ∷ T_IsDecEquivalence_44 → T_IsEquivalence_26 Source #

d__'8799'__52 ∷ T_IsDecEquivalence_44 → AgdaAny → AgdaAny → T_Dec_20 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_4003 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_'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 Source #

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

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

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

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

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

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

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

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

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

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

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

d_IsTotalPreorder_124 ∷ p → p → p → p → p → p → () Source #

data T_IsTotalPreorder_124 Source #

Constructors

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

d_isPreorder_132 ∷ T_IsTotalPreorder_124 → T_IsPreorder_70 Source #

d_total_134 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_isEquivalence_138 ∷ T_IsTotalPreorder_124 → T_IsEquivalence_26 Source #

d_refl_140 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_124 → AgdaAny → AgdaAny Source #

du_refl_140 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny Source #

d_reflexive_142 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_144 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_146 ∷ T_IsTotalPreorder_124 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_148 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_150 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_152 ∷ T_IsTotalPreorder_124 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_154 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_156 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_160 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_124 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_160 ∷ T_IsTotalPreorder_124 → T_IsPartialEquivalence_16 Source #

d_refl_162 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny Source #

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

du_reflexive_164 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_166 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_168 ∷ T_IsTotalPreorder_124 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsPartialOrder_174 ∷ p → p → p → p → p → p → () Source #

data T_IsPartialOrder_174 Source #

Constructors

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

d_isPreorder_182 ∷ T_IsPartialOrder_174 → T_IsPreorder_70 Source #

d_antisym_184 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_188 ∷ T_IsPartialOrder_174 → T_IsEquivalence_26 Source #

d_refl_190 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_174 → AgdaAny → AgdaAny Source #

du_refl_190 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny Source #

d_reflexive_192 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_194 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_196 ∷ T_IsPartialOrder_174 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_198 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_200 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_202 ∷ T_IsPartialOrder_174 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_204 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_206 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_210 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_210 ∷ T_IsPartialOrder_174 → T_IsPartialEquivalence_16 Source #

d_refl_212 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny Source #

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

du_reflexive_214 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_216 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_218 ∷ T_IsPartialOrder_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDecPartialOrder_224 ∷ p → p → p → p → p → p → () Source #

data T_IsDecPartialOrder_224 Source #

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

d__'8799'__236 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__238 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_antisym_242 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_244 ∷ T_IsDecPartialOrder_224 → T_IsEquivalence_26 Source #

d_isPreorder_246 ∷ T_IsDecPartialOrder_224 → T_IsPreorder_70 Source #

d_refl_248 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → AgdaAny → AgdaAny Source #

du_refl_248 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny Source #

d_reflexive_250 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_252 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_254 ∷ T_IsDecPartialOrder_224 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_256 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_258 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_260 ∷ T_IsDecPartialOrder_224 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_262 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_264 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_268 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_268 ∷ T_IsDecPartialOrder_224 → T_IsDecEquivalence_44 Source #

d__'8799'__272 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__272 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_274 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → T_IsEquivalence_26 Source #

du_isEquivalence_274 ∷ T_IsDecPartialOrder_224 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_276 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_276 ∷ T_IsDecPartialOrder_224 → T_IsPartialEquivalence_16 Source #

d_refl_278 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → AgdaAny → AgdaAny Source #

du_refl_278 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny Source #

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

du_reflexive_280 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_282 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_282 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_284 ∷ T_IsDecPartialOrder_224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsStrictPartialOrder_290 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictPartialOrder_290 Source #

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

d_irrefl_304 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_trans_306 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'45''8776'_308 ∷ T_IsStrictPartialOrder_290 → T_Σ_14 Source #

d_isPartialEquivalence_312 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_290 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_312 ∷ T_IsStrictPartialOrder_290 → T_IsPartialEquivalence_16 Source #

d_refl_314 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny Source #

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

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

d_sym_318 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_320 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

du_'60''45'resp'691''45''8776'_328 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'60''45'resp'737''45''8776'_330 ∷ T_IsStrictPartialOrder_290 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDecStrictPartialOrder_336 ∷ p → p → p → p → p → p → () Source #

data T_IsDecStrictPartialOrder_336 Source #

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

d__'8799'__348 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'60''63'__350 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_'60''45'resp'45''8776'_354 ∷ T_IsDecStrictPartialOrder_336 → T_Σ_14 Source #

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

du_'60''45'resp'691''45''8776'_356 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'60''45'resp'737''45''8776'_358 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_irrefl_362 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_364 ∷ T_IsDecStrictPartialOrder_336 → T_IsEquivalence_26 Source #

d_trans_366 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_isPartialEquivalence_370 ∷ T_IsDecStrictPartialOrder_336 → T_IsPartialEquivalence_16 Source #

d_refl_372 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny Source #

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

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

d_sym_376 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_378 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_382 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_382 ∷ T_IsDecStrictPartialOrder_336 → T_IsDecEquivalence_44 Source #

d__'8799'__386 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__386 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_388 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → T_IsEquivalence_26 Source #

du_isEquivalence_388 ∷ T_IsDecStrictPartialOrder_336 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_390 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_390 ∷ T_IsDecStrictPartialOrder_336 → T_IsPartialEquivalence_16 Source #

d_refl_392 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny Source #

du_refl_392 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny Source #

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

du_reflexive_394 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_396 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_398 ∷ T_IsDecStrictPartialOrder_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsTotalOrder_404 ∷ p → p → p → p → p → p → () Source #

data T_IsTotalOrder_404 Source #

Constructors

C_IsTotalOrder'46'constructor_20555 T_IsPartialOrder_174 (AgdaAny → AgdaAny → T__'8846'__30)

d_isPartialOrder_412 ∷ T_IsTotalOrder_404 → T_IsPartialOrder_174 Source #

d_total_414 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_antisym_418 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_420 ∷ T_IsTotalOrder_404 → T_IsEquivalence_26 Source #

d_isPreorder_422 ∷ T_IsTotalOrder_404 → T_IsPreorder_70 Source #

d_refl_424 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_404 → AgdaAny → AgdaAny Source #

du_refl_424 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny Source #

d_reflexive_426 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_428 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_430 ∷ T_IsTotalOrder_404 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_432 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_434 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_436 ∷ T_IsTotalOrder_404 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_438 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_440 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_444 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_404 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_444 ∷ T_IsTotalOrder_404 → T_IsPartialEquivalence_16 Source #

d_refl_446 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny Source #

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

du_reflexive_448 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_450 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_452 ∷ T_IsTotalOrder_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isTotalPreorder_454 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_404 → T_IsTotalPreorder_124 Source #

du_isTotalPreorder_454 ∷ T_IsTotalOrder_404 → T_IsTotalPreorder_124 Source #

d_IsDecTotalOrder_460 ∷ p → p → p → p → p → p → () Source #

data T_IsDecTotalOrder_460 Source #

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

d__'8799'__472 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__474 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_antisym_478 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_480 ∷ T_IsDecTotalOrder_460 → T_IsEquivalence_26 Source #

d_isPartialOrder_482 ∷ T_IsDecTotalOrder_460 → T_IsPartialOrder_174 Source #

d_isPreorder_484 ∷ T_IsDecTotalOrder_460 → T_IsPreorder_70 Source #

d_isTotalPreorder_486 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → T_IsTotalPreorder_124 Source #

du_isTotalPreorder_486 ∷ T_IsDecTotalOrder_460 → T_IsTotalPreorder_124 Source #

d_refl_488 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → AgdaAny → AgdaAny Source #

du_refl_488 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny Source #

d_reflexive_490 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_492 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_494 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_496 ∷ T_IsDecTotalOrder_460 → T_Σ_14 Source #

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

du_'8764''45'resp'691''45''8776'_498 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'737''45''8776'_500 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_502 ∷ T_IsDecTotalOrder_460 → T_Σ_14 Source #

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

du_'8818''45'resp'691''45''8776'_504 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'737''45''8776'_506 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecPartialOrder_508 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → T_IsDecPartialOrder_224 Source #

du_isDecPartialOrder_508 ∷ T_IsDecTotalOrder_460 → T_IsDecPartialOrder_224 Source #

d_isDecEquivalence_512 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_512 ∷ T_IsDecTotalOrder_460 → T_IsDecEquivalence_44 Source #

d__'8799'__516 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__516 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → T_IsEquivalence_26 Source #

du_isEquivalence_518 ∷ T_IsDecTotalOrder_460 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_520 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_520 ∷ T_IsDecTotalOrder_460 → T_IsPartialEquivalence_16 Source #

d_refl_522 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → AgdaAny → AgdaAny Source #

du_refl_522 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny Source #

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

du_reflexive_524 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_526 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_526 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_528 ∷ T_IsDecTotalOrder_460 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsStrictTotalOrder_534 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictTotalOrder_534 Source #

Constructors

C_IsStrictTotalOrder'46'constructor_24953 T_IsStrictPartialOrder_290 (AgdaAny → AgdaAny → T_Tri_158)

d_isStrictPartialOrder_542 ∷ T_IsStrictTotalOrder_534 → T_IsStrictPartialOrder_290 Source #

d_compare_544 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_'60''45'resp'45''8776'_548 ∷ T_IsStrictTotalOrder_534 → T_Σ_14 Source #

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

du_'60''45'resp'691''45''8776'_550 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'60''45'resp'737''45''8776'_552 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_irrefl_556 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_558 ∷ T_IsStrictTotalOrder_534 → T_IsEquivalence_26 Source #

d_trans_560 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8799'__562 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__562 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Dec_20 Source #

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

du__'60''63'__564 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecStrictPartialOrder_566 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsDecStrictPartialOrder_336 Source #

du_isDecStrictPartialOrder_566 ∷ T_IsStrictTotalOrder_534 → T_IsDecStrictPartialOrder_336 Source #

d_isDecEquivalence_570 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_570 ∷ T_IsStrictTotalOrder_534 → T_IsDecEquivalence_44 Source #

d__'8799'__574 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__574 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_576 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsEquivalence_26 Source #

du_isEquivalence_576 ∷ T_IsStrictTotalOrder_534 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_578 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_578 ∷ T_IsStrictTotalOrder_534 → T_IsPartialEquivalence_16 Source #

d_refl_580 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny Source #

du_refl_580 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny Source #

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

du_reflexive_582 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_584 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_584 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_586 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecEquivalence_588 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_588 ∷ T_IsStrictTotalOrder_534 → T_IsDecEquivalence_44 Source #

d_IsDenseLinearOrder_594 ∷ p → p → p → p → p → p → () Source #

data T_IsDenseLinearOrder_594 Source #

Constructors

C_IsDenseLinearOrder'46'constructor_28131 T_IsStrictTotalOrder_534 (AgdaAny → AgdaAny → AgdaAny → T_Σ_14)

d_isStrictTotalOrder_602 ∷ T_IsDenseLinearOrder_594 → T_IsStrictTotalOrder_534 Source #

d_dense_604 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

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

du__'60''63'__608 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8799'__610 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__610 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_'60''45'resp'45''8776'_612 ∷ T_IsDenseLinearOrder_594 → T_Σ_14 Source #

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

du_'60''45'resp'691''45''8776'_614 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'60''45'resp'737''45''8776'_616 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_compare_620 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_irrefl_622 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isDecEquivalence_624 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_624 ∷ T_IsDenseLinearOrder_594 → T_IsDecEquivalence_44 Source #

d_isDecStrictPartialOrder_626 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → T_IsDecStrictPartialOrder_336 Source #

du_isDecStrictPartialOrder_626 ∷ T_IsDenseLinearOrder_594 → T_IsDecStrictPartialOrder_336 Source #

d_isEquivalence_628 ∷ T_IsDenseLinearOrder_594 → T_IsEquivalence_26 Source #

d_isStrictPartialOrder_630 ∷ T_IsDenseLinearOrder_594 → T_IsStrictPartialOrder_290 Source #

d_trans_632 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8799'__636 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__636 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecEquivalence_638 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_638 ∷ T_IsDenseLinearOrder_594 → T_IsDecEquivalence_44 Source #

d_isEquivalence_640 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → T_IsEquivalence_26 Source #

du_isEquivalence_640 ∷ T_IsDenseLinearOrder_594 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_642 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_642 ∷ T_IsDenseLinearOrder_594 → T_IsPartialEquivalence_16 Source #

d_refl_644 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny Source #

du_refl_644 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny Source #

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

du_reflexive_646 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_648 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_648 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_650 ∷ T_IsDenseLinearOrder_594 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsApartnessRelation_656 ∷ p → p → p → p → p → p → () Source #

data T_IsApartnessRelation_656 Source #

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

d_sym_668 ∷ T_IsApartnessRelation_656 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cotrans_670 ∷ T_IsApartnessRelation_656 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8846'__30 Source #

d__'172''35'__672 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsApartnessRelation_656 → AgdaAny → AgdaAny → () Source #