Safe HaskellNone

MAlonzo.Code.Relation.Binary.Structures

Documentation

d_IsPartialEquivalence_16 :: p1 -> p2 -> p3 -> p4 -> () Source #

data T_IsPartialEquivalence_16 Source #

Constructors

C_IsPartialEquivalence'46'constructor_169 (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 :: p1 -> p2 -> p3 -> p4 -> () Source #

data T_IsEquivalence_26 Source #

Constructors

C_IsEquivalence'46'constructor_519 (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_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_42 :: T_IsEquivalence_26 -> T_IsPartialEquivalence_16 Source #

d_IsDecEquivalence_44 :: p1 -> p2 -> p3 -> p4 -> () Source #

data T_IsDecEquivalence_44 Source #

Constructors

C_IsDecEquivalence'46'constructor_1689 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> T_Dec_32) 

d_isEquivalence_50 :: T_IsDecEquivalence_44 -> T_IsEquivalence_26 Source #

d__'8799'__52 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_isPartialEquivalence_56 :: T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsPreorder_70 Source #

Constructors

C_IsPreorder'46'constructor_2409 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_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (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_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (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_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny Source #

du_refl_98 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_100 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

d_'8764''45'resp'691''45''8776'_106 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

d_'8764''45'resp'45''8776'_112 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_Σ_14 Source #

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

d_IsTotalPreorder_118 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsTotalPreorder_118 Source #

Constructors

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

d_isPreorder_126 :: T_IsTotalPreorder_118 -> T_IsPreorder_70 Source #

d_total_128 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #

d_isEquivalence_132 :: T_IsTotalPreorder_118 -> T_IsEquivalence_26 Source #

d_refl_134 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny Source #

du_refl_134 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny Source #

d_reflexive_136 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_138 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_140 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_118 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_140 :: T_IsTotalPreorder_118 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_142 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_142 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_144 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_144 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_148 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_118 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_148 :: T_IsTotalPreorder_118 -> T_IsPartialEquivalence_16 Source #

d_refl_150 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny Source #

d_reflexive_152 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_152 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_154 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_156 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsPartialOrder_162 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsPartialOrder_162 Source #

Constructors

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

d_isPreorder_170 :: T_IsPartialOrder_162 -> T_IsPreorder_70 Source #

d_antisym_172 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_176 :: T_IsPartialOrder_162 -> T_IsEquivalence_26 Source #

d_refl_178 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> AgdaAny -> AgdaAny Source #

du_refl_178 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny Source #

d_reflexive_180 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_182 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_184 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_184 :: T_IsPartialOrder_162 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_186 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_186 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_188 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_188 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_192 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_192 :: T_IsPartialOrder_162 -> T_IsPartialEquivalence_16 Source #

d_refl_194 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny Source #

d_reflexive_196 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_196 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_198 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_200 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsDecPartialOrder_206 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsDecPartialOrder_206 Source #

Constructors

C_IsDecPartialOrder'46'constructor_8061 T_IsPartialOrder_162 (AgdaAny -> AgdaAny -> T_Dec_32) (AgdaAny -> AgdaAny -> T_Dec_32) 

d_isPartialOrder_216 :: T_IsDecPartialOrder_206 -> T_IsPartialOrder_162 Source #

d__'8799'__218 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d__'8804''63'__220 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_antisym_224 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_226 :: T_IsDecPartialOrder_206 -> T_IsEquivalence_26 Source #

d_isPreorder_228 :: T_IsDecPartialOrder_206 -> T_IsPreorder_70 Source #

d_refl_230 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny Source #

du_refl_230 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny Source #

d_reflexive_232 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_234 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_236 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_236 :: T_IsDecPartialOrder_206 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_238 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_238 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_240 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_240 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isDecEquivalence_244 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44 Source #

du_isDecEquivalence_244 :: T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44 Source #

d__'8799'__248 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du__'8799'__248 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_isEquivalence_250 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> T_IsEquivalence_26 Source #

du_isEquivalence_250 :: T_IsDecPartialOrder_206 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_252 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_252 :: T_IsDecPartialOrder_206 -> T_IsPartialEquivalence_16 Source #

d_refl_254 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny Source #

du_refl_254 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny Source #

d_reflexive_256 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_256 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_258 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_258 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_260 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_260 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsStrictPartialOrder_266 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsStrictPartialOrder_266 Source #

Constructors

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

d_isEquivalence_278 :: T_IsStrictPartialOrder_266 -> T_IsEquivalence_26 Source #

d_irrefl_280 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #

d_trans_282 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'60''45'resp'45''8776'_284 :: T_IsStrictPartialOrder_266 -> T_Σ_14 Source #

d_isPartialEquivalence_288 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_288 :: T_IsStrictPartialOrder_266 -> T_IsPartialEquivalence_16 Source #

d_refl_290 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny Source #

d_reflexive_292 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_292 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_294 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_296 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_asym_298 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #

d_'60''45'resp'691''45''8776'_304 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'60''45'resp'691''45''8776'_304 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'60''45'resp'737''45''8776'_306 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'60''45'resp'737''45''8776'_306 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsDecStrictPartialOrder_312 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsDecStrictPartialOrder_312 Source #

Constructors

C_IsDecStrictPartialOrder'46'constructor_13497 T_IsStrictPartialOrder_266 (AgdaAny -> AgdaAny -> T_Dec_32) (AgdaAny -> AgdaAny -> T_Dec_32) 

d_isStrictPartialOrder_322 :: T_IsDecStrictPartialOrder_312 -> T_IsStrictPartialOrder_266 Source #

d__'8799'__324 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d__'60''63'__326 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_'60''45'resp'45''8776'_330 :: T_IsDecStrictPartialOrder_312 -> T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_332 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'60''45'resp'691''45''8776'_332 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'60''45'resp'737''45''8776'_334 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'60''45'resp'737''45''8776'_334 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_asym_336 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #

d_irrefl_338 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #

d_isEquivalence_340 :: T_IsDecStrictPartialOrder_312 -> T_IsEquivalence_26 Source #

d_trans_342 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_346 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_346 :: T_IsDecStrictPartialOrder_312 -> T_IsPartialEquivalence_16 Source #

d_refl_348 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny Source #

d_reflexive_350 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_350 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_352 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_354 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isDecEquivalence_358 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> T_IsDecEquivalence_44 Source #

du_isDecEquivalence_358 :: T_IsDecStrictPartialOrder_312 -> T_IsDecEquivalence_44 Source #

d__'8799'__362 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du__'8799'__362 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_isEquivalence_364 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> T_IsEquivalence_26 Source #

du_isEquivalence_364 :: T_IsDecStrictPartialOrder_312 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_366 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_366 :: T_IsDecStrictPartialOrder_312 -> T_IsPartialEquivalence_16 Source #

d_refl_368 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny Source #

du_refl_368 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny Source #

d_reflexive_370 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_370 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_372 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_372 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_374 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_374 :: T_IsDecStrictPartialOrder_312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsTotalOrder_380 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsTotalOrder_380 Source #

Constructors

C_IsTotalOrder'46'constructor_15233 T_IsPartialOrder_162 (AgdaAny -> AgdaAny -> T__'8846'__30) 

d_isPartialOrder_388 :: T_IsTotalOrder_380 -> T_IsPartialOrder_162 Source #

d_total_390 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #

d_antisym_394 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_396 :: T_IsTotalOrder_380 -> T_IsEquivalence_26 Source #

d_isPreorder_398 :: T_IsTotalOrder_380 -> T_IsPreorder_70 Source #

d_refl_400 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> AgdaAny -> AgdaAny Source #

du_refl_400 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny Source #

d_reflexive_402 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_404 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_406 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_406 :: T_IsTotalOrder_380 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_408 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_408 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_410 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_410 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_414 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_414 :: T_IsTotalOrder_380 -> T_IsPartialEquivalence_16 Source #

d_refl_416 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny Source #

d_reflexive_418 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_418 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_420 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_422 :: T_IsTotalOrder_380 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isTotalPreorder_424 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> T_IsTotalPreorder_118 Source #

du_isTotalPreorder_424 :: T_IsTotalOrder_380 -> T_IsTotalPreorder_118 Source #

d_IsDecTotalOrder_430 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsDecTotalOrder_430 Source #

Constructors

C_IsDecTotalOrder'46'constructor_16917 T_IsTotalOrder_380 (AgdaAny -> AgdaAny -> T_Dec_32) (AgdaAny -> AgdaAny -> T_Dec_32) 

d_isTotalOrder_440 :: T_IsDecTotalOrder_430 -> T_IsTotalOrder_380 Source #

d__'8799'__442 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d__'8804''63'__444 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_antisym_448 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_450 :: T_IsDecTotalOrder_430 -> T_IsEquivalence_26 Source #

d_isPartialOrder_452 :: T_IsDecTotalOrder_430 -> T_IsPartialOrder_162 Source #

d_isPreorder_454 :: T_IsDecTotalOrder_430 -> T_IsPreorder_70 Source #

d_isTotalPreorder_456 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_IsTotalPreorder_118 Source #

du_isTotalPreorder_456 :: T_IsDecTotalOrder_430 -> T_IsTotalPreorder_118 Source #

d_refl_458 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny Source #

du_refl_458 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny Source #

d_reflexive_460 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_total_462 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #

d_trans_464 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_466 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_466 :: T_IsDecTotalOrder_430 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_468 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_468 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_470 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_470 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isDecPartialOrder_472 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_IsDecPartialOrder_206 Source #

du_isDecPartialOrder_472 :: T_IsDecTotalOrder_430 -> T_IsDecPartialOrder_206 Source #

d_isDecEquivalence_476 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_IsDecEquivalence_44 Source #

du_isDecEquivalence_476 :: T_IsDecTotalOrder_430 -> T_IsDecEquivalence_44 Source #

d__'8799'__480 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du__'8799'__480 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_isEquivalence_482 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_IsEquivalence_26 Source #

du_isEquivalence_482 :: T_IsDecTotalOrder_430 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_484 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_484 :: T_IsDecTotalOrder_430 -> T_IsPartialEquivalence_16 Source #

d_refl_486 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny Source #

du_refl_486 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny Source #

d_reflexive_488 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_488 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_490 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_490 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_492 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_492 :: T_IsDecTotalOrder_430 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsStrictTotalOrder_498 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsStrictTotalOrder_498 Source #

Constructors

C_IsStrictTotalOrder'46'constructor_18889 T_IsEquivalence_26 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> T_Tri_136) 

d_isEquivalence_508 :: T_IsStrictTotalOrder_498 -> T_IsEquivalence_26 Source #

d_trans_510 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_compare_512 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Tri_136 Source #

d__'8799'__514 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du__'8799'__514 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d__'60''63'__516 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du__'60''63'__516 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_isDecEquivalence_518 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsDecEquivalence_44 Source #

du_isDecEquivalence_518 :: T_IsStrictTotalOrder_498 -> T_IsDecEquivalence_44 Source #

d__'8799'__522 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du__'8799'__522 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_isEquivalence_524 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsEquivalence_26 Source #

du_isEquivalence_524 :: T_IsStrictTotalOrder_498 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_526 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_526 :: T_IsStrictTotalOrder_498 -> T_IsPartialEquivalence_16 Source #

d_refl_528 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny Source #

du_refl_528 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny Source #

d_reflexive_530 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_530 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_532 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_532 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_534 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_534 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isStrictPartialOrder_536 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsStrictPartialOrder_266 Source #

du_isStrictPartialOrder_536 :: T_IsStrictTotalOrder_498 -> T_IsStrictPartialOrder_266 Source #

d_isDecStrictPartialOrder_538 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsDecStrictPartialOrder_312 Source #

du_isDecStrictPartialOrder_538 :: T_IsStrictTotalOrder_498 -> T_IsDecStrictPartialOrder_312 Source #

d_'60''45'resp'45''8776'_542 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_Σ_14 Source #

du_'60''45'resp'45''8776'_542 :: T_IsStrictTotalOrder_498 -> T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_544 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'60''45'resp'691''45''8776'_544 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'60''45'resp'737''45''8776'_546 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'60''45'resp'737''45''8776'_546 :: T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_asym_548 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #

d_irrefl_550 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #