Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Relation.Binary.Bundles

Documentation

d_PartialSetoid_10 ∷ p → p → () Source #

newtype T_PartialSetoid_10 Source #

Constructors

C_PartialSetoid'46'constructor_133 T_IsPartialEquivalence_16

d_Carrier_22 ∷ T_PartialSetoid_10 → () Source #

d__'8776'__24 ∷ T_PartialSetoid_10 → AgdaAny → AgdaAny → () Source #

d_isPartialEquivalence_26 ∷ T_PartialSetoid_10 → T_IsPartialEquivalence_16 Source #

d_sym_30 ∷ T_PartialSetoid_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_32 ∷ T_PartialSetoid_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8777'__34 ∷ T_Level_18 → T_Level_18 → T_PartialSetoid_10 → AgdaAny → AgdaAny → () Source #

d_Setoid_44 ∷ p → p → () Source #

newtype T_Setoid_44 Source #

Constructors

C_Setoid'46'constructor_727 T_IsEquivalence_26

d_Carrier_56 ∷ T_Setoid_44 → () Source #

d__'8776'__58 ∷ T_Setoid_44 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_60 ∷ T_Setoid_44 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_64 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_64 ∷ T_Setoid_44 → T_IsPartialEquivalence_16 Source #

d_refl_66 ∷ T_Setoid_44 → AgdaAny → AgdaAny Source #

d_reflexive_68 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_68 ∷ T_Setoid_44 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_70 ∷ T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_72 ∷ T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_partialSetoid_74 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_PartialSetoid_10 Source #

du_partialSetoid_74 ∷ T_Setoid_44 → T_PartialSetoid_10 Source #

d__'8777'__78 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → () Source #

d_DecSetoid_84 ∷ p → p → () Source #

newtype T_DecSetoid_84 Source #

Constructors

C_DecSetoid'46'constructor_1385 T_IsDecEquivalence_44

d_Carrier_96 ∷ T_DecSetoid_84 → () Source #

d__'8776'__98 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → () Source #

d_isDecEquivalence_100 ∷ T_DecSetoid_84 → T_IsDecEquivalence_44 Source #

d__'8799'__104 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_isEquivalence_106 ∷ T_DecSetoid_84 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_108 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_108 ∷ T_DecSetoid_84 → T_IsPartialEquivalence_16 Source #

d_refl_110 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny Source #

d_reflexive_112 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_112 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_114 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_116 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_118 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_Setoid_44 Source #

du_setoid_118 ∷ T_DecSetoid_84 → T_Setoid_44 Source #

d__'8777'__122 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → AgdaAny → AgdaAny → () Source #

d_partialSetoid_124 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_PartialSetoid_10 Source #

du_partialSetoid_124 ∷ T_DecSetoid_84 → T_PartialSetoid_10 Source #

d_Preorder_132 ∷ p → p → p → () Source #

newtype T_Preorder_132 Source #

Constructors

C_Preorder'46'constructor_2269 T_IsPreorder_70

d_Carrier_148 ∷ T_Preorder_132 → () Source #

d__'8776'__150 ∷ T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d__'8764'__152 ∷ T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d_isPreorder_154 ∷ T_Preorder_132 → T_IsPreorder_70 Source #

d_isEquivalence_158 ∷ T_Preorder_132 → T_IsEquivalence_26 Source #

d_refl_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny Source #

du_refl_160 ∷ T_Preorder_132 → AgdaAny → AgdaAny Source #

d_reflexive_162 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_164 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_166 ∷ T_Preorder_132 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_168 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_170 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Setoid_44 Source #

du_setoid_174 ∷ T_Preorder_132 → T_Setoid_44 Source #

d__'8776'__178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d__'8777'__180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d_Carrier_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → () Source #

d_isEquivalence_184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_IsEquivalence_26 Source #

du_isEquivalence_184 ∷ T_Preorder_132 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_186 ∷ T_Preorder_132 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_PartialSetoid_10 Source #

du_partialSetoid_188 ∷ T_Preorder_132 → T_PartialSetoid_10 Source #

d_refl_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny Source #

du_refl_190 ∷ T_Preorder_132 → AgdaAny → AgdaAny Source #

d_reflexive_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_192 ∷ T_Preorder_132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_194 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_196 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_TotalPreorder_204 ∷ p → p → p → () Source #

newtype T_TotalPreorder_204 Source #

Constructors

C_TotalPreorder'46'constructor_3669 T_IsTotalPreorder_118

d_Carrier_220 ∷ T_TotalPreorder_204 → () Source #

d__'8776'__222 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → () Source #

d__'8818'__224 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → () Source #

d_isTotalPreorder_226 ∷ T_TotalPreorder_204 → T_IsTotalPreorder_118 Source #

d_isEquivalence_230 ∷ T_TotalPreorder_204 → T_IsEquivalence_26 Source #

d_isPreorder_232 ∷ T_TotalPreorder_204 → T_IsPreorder_70 Source #

d_refl_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny Source #

du_refl_234 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny Source #

d_reflexive_236 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_238 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_240 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_242 ∷ T_TotalPreorder_204 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_244 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_246 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_preorder_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_Preorder_132 Source #

du_preorder_248 ∷ T_TotalPreorder_204 → T_Preorder_132 Source #

d__'8776'__254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → () Source #

d__'8777'__256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → () Source #

d_Carrier_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → () Source #

d_isEquivalence_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_IsEquivalence_26 Source #

du_isEquivalence_260 ∷ T_TotalPreorder_204 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_262 ∷ T_TotalPreorder_204 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_PartialSetoid_10 Source #

du_partialSetoid_264 ∷ T_TotalPreorder_204 → T_PartialSetoid_10 Source #

d_refl_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny Source #

du_refl_266 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny Source #

d_reflexive_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_268 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_Setoid_44 Source #

du_setoid_270 ∷ T_TotalPreorder_204 → T_Setoid_44 Source #

d_sym_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_272 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_274 ∷ T_TotalPreorder_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Poset_282 ∷ p → p → p → () Source #

newtype T_Poset_282 Source #

Constructors

C_Poset'46'constructor_5219 T_IsPartialOrder_162

d_Carrier_298 ∷ T_Poset_282 → () Source #

d__'8776'__300 ∷ T_Poset_282 → AgdaAny → AgdaAny → () Source #

d__'8804'__302 ∷ T_Poset_282 → AgdaAny → AgdaAny → () Source #

d_isPartialOrder_304 ∷ T_Poset_282 → T_IsPartialOrder_162 Source #

d_antisym_308 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_310 ∷ T_Poset_282 → T_IsEquivalence_26 Source #

d_isPreorder_312 ∷ T_Poset_282 → T_IsPreorder_70 Source #

d_refl_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny Source #

du_refl_314 ∷ T_Poset_282 → AgdaAny → AgdaAny Source #

d_reflexive_316 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_318 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_320 ∷ T_Poset_282 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_322 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_324 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_preorder_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_Preorder_132 Source #

du_preorder_326 ∷ T_Poset_282 → T_Preorder_132 Source #

d__'8776'__332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → () Source #

d__'8777'__334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → () Source #

d_Carrier_336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → () Source #

d_isEquivalence_338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_IsEquivalence_26 Source #

du_isEquivalence_338 ∷ T_Poset_282 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_340 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_340 ∷ T_Poset_282 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_PartialSetoid_10 Source #

du_partialSetoid_342 ∷ T_Poset_282 → T_PartialSetoid_10 Source #

d_refl_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny Source #

du_refl_344 ∷ T_Poset_282 → AgdaAny → AgdaAny Source #

d_reflexive_346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_346 ∷ T_Poset_282 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_Setoid_44 Source #

du_setoid_348 ∷ T_Poset_282 → T_Setoid_44 Source #

d_sym_350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_350 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_352 ∷ T_Poset_282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DecPoset_360 ∷ p → p → p → () Source #

newtype T_DecPoset_360 Source #

Constructors

C_DecPoset'46'constructor_6777 T_IsDecPartialOrder_206

d_Carrier_376 ∷ T_DecPoset_360 → () Source #

d__'8776'__378 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → () Source #

d__'8804'__380 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → () Source #

d_isDecPartialOrder_382 ∷ T_DecPoset_360 → T_IsDecPartialOrder_206 Source #

d__'8799'__386 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'8804''63'__388 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_antisym_390 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_392 ∷ T_DecPoset_360 → T_IsEquivalence_26 Source #

d_isPartialOrder_394 ∷ T_DecPoset_360 → T_IsPartialOrder_162 Source #

d_isPreorder_396 ∷ T_DecPoset_360 → T_IsPreorder_70 Source #

d_refl_398 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny Source #

du_refl_398 ∷ T_DecPoset_360 → AgdaAny → AgdaAny Source #

d_reflexive_400 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_402 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_404 ∷ T_DecPoset_360 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_406 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_406 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_408 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_Poset_282 Source #

du_poset_428 ∷ T_DecPoset_360 → T_Poset_282 Source #

d_preorder_432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_Preorder_132 Source #

du_preorder_432 ∷ T_DecPoset_360 → T_Preorder_132 Source #

d_decSetoid_436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_DecSetoid_84 Source #

du_decSetoid_436 ∷ T_DecPoset_360 → T_DecSetoid_84 Source #

d__'8776'__440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → () Source #

d__'8777'__442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → () Source #

d__'8799'__444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__444 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_Carrier_446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → () Source #

d_isDecEquivalence_448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_448 ∷ T_DecPoset_360 → T_IsDecEquivalence_44 Source #

d_isEquivalence_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_IsEquivalence_26 Source #

du_isEquivalence_450 ∷ T_DecPoset_360 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_452 ∷ T_DecPoset_360 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_PartialSetoid_10 Source #

du_partialSetoid_454 ∷ T_DecPoset_360 → T_PartialSetoid_10 Source #

d_refl_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny Source #

du_refl_456 ∷ T_DecPoset_360 → AgdaAny → AgdaAny Source #

d_reflexive_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_458 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → T_Setoid_44 Source #

du_setoid_460 ∷ T_DecPoset_360 → T_Setoid_44 Source #

d_sym_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_462 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_464 ∷ T_DecPoset_360 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_StrictPartialOrder_472 ∷ p → p → p → () Source #

newtype T_StrictPartialOrder_472 Source #

Constructors

C_StrictPartialOrder'46'constructor_8957 T_IsStrictPartialOrder_266

d_Carrier_488 ∷ T_StrictPartialOrder_472 → () Source #

d__'8776'__490 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → () Source #

d__'60'__492 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → () Source #

d_isStrictPartialOrder_494 ∷ T_StrictPartialOrder_472 → T_IsStrictPartialOrder_266 Source #

d_'60''45'resp'45''8776'_498 ∷ T_StrictPartialOrder_472 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_500 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_502 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_504 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_asymmetric_506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_irrefl_508 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_isEquivalence_510 ∷ T_StrictPartialOrder_472 → T_IsEquivalence_26 Source #

d_trans_512 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_516 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_Setoid_44 Source #

du_setoid_516 ∷ T_StrictPartialOrder_472 → T_Setoid_44 Source #

d__'8776'__520 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → () Source #

d__'8777'__522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → () Source #

d_Carrier_524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → () Source #

d_isEquivalence_526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_IsEquivalence_26 Source #

du_isEquivalence_526 ∷ T_StrictPartialOrder_472 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_528 ∷ T_StrictPartialOrder_472 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_PartialSetoid_10 Source #

du_partialSetoid_530 ∷ T_StrictPartialOrder_472 → T_PartialSetoid_10 Source #

d_refl_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny Source #

du_refl_532 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny Source #

d_reflexive_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_sym_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_536 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_538 ∷ T_StrictPartialOrder_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DecStrictPartialOrder_546 ∷ p → p → p → () Source #

newtype T_DecStrictPartialOrder_546 Source #

Constructors

C_DecStrictPartialOrder'46'constructor_10419 T_IsDecStrictPartialOrder_314

d_Carrier_562 ∷ T_DecStrictPartialOrder_546 → () Source #

d__'8776'__564 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → () Source #

d__'60'__566 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → () Source #

d_isDecStrictPartialOrder_568 ∷ T_DecStrictPartialOrder_546 → T_IsDecStrictPartialOrder_314 Source #

d__'60''63'__572 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'8799'__574 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_'60''45'resp'45''8776'_576 ∷ T_DecStrictPartialOrder_546 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_578 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_580 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_asymmetric_584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_irrefl_586 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_isEquivalence_588 ∷ T_DecStrictPartialOrder_546 → T_IsEquivalence_26 Source #

d_isStrictPartialOrder_590 ∷ T_DecStrictPartialOrder_546 → T_IsStrictPartialOrder_266 Source #

d_trans_592 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_strictPartialOrder_612 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_StrictPartialOrder_472 Source #

du_strictPartialOrder_612 ∷ T_DecStrictPartialOrder_546 → T_StrictPartialOrder_472 Source #

d_decSetoid_616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_DecSetoid_84 Source #

du_decSetoid_616 ∷ T_DecStrictPartialOrder_546 → T_DecSetoid_84 Source #

d__'8776'__620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → () Source #

d__'8777'__622 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → () Source #

d__'8799'__624 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__624 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_Carrier_626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → () Source #

d_isDecEquivalence_628 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_628 ∷ T_DecStrictPartialOrder_546 → T_IsDecEquivalence_44 Source #

d_isEquivalence_630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_IsEquivalence_26 Source #

du_isEquivalence_630 ∷ T_DecStrictPartialOrder_546 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_632 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_632 ∷ T_DecStrictPartialOrder_546 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_634 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_PartialSetoid_10 Source #

du_partialSetoid_634 ∷ T_DecStrictPartialOrder_546 → T_PartialSetoid_10 Source #

d_refl_636 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny Source #

du_refl_636 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny Source #

d_reflexive_638 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_638 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → T_Setoid_44 Source #

du_setoid_640 ∷ T_DecStrictPartialOrder_546 → T_Setoid_44 Source #

d_sym_642 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_642 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_644 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_644 ∷ T_DecStrictPartialOrder_546 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_TotalOrder_652 ∷ p → p → p → () Source #

newtype T_TotalOrder_652 Source #

Constructors

C_TotalOrder'46'constructor_12489 T_IsTotalOrder_384

d_Carrier_668 ∷ T_TotalOrder_652 → () Source #

d__'8776'__670 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → () Source #

d__'8804'__672 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → () Source #

d_isTotalOrder_674 ∷ T_TotalOrder_652 → T_IsTotalOrder_384 Source #

d_antisym_678 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_680 ∷ T_TotalOrder_652 → T_IsEquivalence_26 Source #

d_isPartialOrder_682 ∷ T_TotalOrder_652 → T_IsPartialOrder_162 Source #

d_isPreorder_684 ∷ T_TotalOrder_652 → T_IsPreorder_70 Source #

d_isTotalPreorder_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_IsTotalPreorder_118 Source #

du_isTotalPreorder_686 ∷ T_TotalOrder_652 → T_IsTotalPreorder_118 Source #

d_refl_688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny Source #

du_refl_688 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny Source #

d_reflexive_690 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_692 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_694 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_696 ∷ T_TotalOrder_652 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_698 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_700 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Poset_282 Source #

du_poset_702 ∷ T_TotalOrder_652 → T_Poset_282 Source #

d_preorder_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Preorder_132 Source #

du_preorder_706 ∷ T_TotalOrder_652 → T_Preorder_132 Source #

d__'8776'__710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → () Source #

d__'8777'__712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → () Source #

d_Carrier_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → () Source #

d_isEquivalence_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_IsEquivalence_26 Source #

du_isEquivalence_716 ∷ T_TotalOrder_652 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_718 ∷ T_TotalOrder_652 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_PartialSetoid_10 Source #

du_partialSetoid_720 ∷ T_TotalOrder_652 → T_PartialSetoid_10 Source #

d_refl_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny Source #

du_refl_722 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny Source #

d_reflexive_724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_724 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Setoid_44 Source #

du_setoid_726 ∷ T_TotalOrder_652 → T_Setoid_44 Source #

d_sym_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_728 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_730 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_totalPreorder_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_TotalPreorder_204 Source #

du_totalPreorder_732 ∷ T_TotalOrder_652 → T_TotalPreorder_204 Source #

d_DecTotalOrder_740 ∷ p → p → p → () Source #

newtype T_DecTotalOrder_740 Source #

Constructors

C_DecTotalOrder'46'constructor_14337 T_IsDecTotalOrder_434

d_Carrier_756 ∷ T_DecTotalOrder_740 → () Source #

d__'8776'__758 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → () Source #

d__'8804'__760 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → () Source #

d_isDecTotalOrder_762 ∷ T_DecTotalOrder_740 → T_IsDecTotalOrder_434 Source #

d__'8799'__766 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'8804''63'__768 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_antisym_770 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isDecPartialOrder_772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_IsDecPartialOrder_206 Source #

du_isDecPartialOrder_772 ∷ T_DecTotalOrder_740 → T_IsDecPartialOrder_206 Source #

d_isEquivalence_774 ∷ T_DecTotalOrder_740 → T_IsEquivalence_26 Source #

d_isPartialOrder_776 ∷ T_DecTotalOrder_740 → T_IsPartialOrder_162 Source #

d_isPreorder_778 ∷ T_DecTotalOrder_740 → T_IsPreorder_70 Source #

d_isTotalOrder_780 ∷ T_DecTotalOrder_740 → T_IsTotalOrder_384 Source #

d_isTotalPreorder_782 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_IsTotalPreorder_118 Source #

du_isTotalPreorder_782 ∷ T_DecTotalOrder_740 → T_IsTotalPreorder_118 Source #

d_refl_784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny Source #

du_refl_784 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny Source #

d_reflexive_786 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_788 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_790 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_792 ∷ T_DecTotalOrder_740 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_794 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_796 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_totalOrder_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_TotalOrder_652 Source #

du_totalOrder_816 ∷ T_DecTotalOrder_740 → T_TotalOrder_652 Source #

d_poset_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_Poset_282 Source #

du_poset_820 ∷ T_DecTotalOrder_740 → T_Poset_282 Source #

d_preorder_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_Preorder_132 Source #

du_preorder_822 ∷ T_DecTotalOrder_740 → T_Preorder_132 Source #

d_decPoset_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_DecPoset_360 Source #

du_decPoset_824 ∷ T_DecTotalOrder_740 → T_DecPoset_360 Source #

d__'8776'__830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → () Source #

d__'8777'__832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → () Source #

d__'8799'__834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__834 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_Carrier_836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → () Source #

d_decSetoid_838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_DecSetoid_84 Source #

du_decSetoid_838 ∷ T_DecTotalOrder_740 → T_DecSetoid_84 Source #

d_isDecEquivalence_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_840 ∷ T_DecTotalOrder_740 → T_IsDecEquivalence_44 Source #

d_isEquivalence_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_IsEquivalence_26 Source #

du_isEquivalence_842 ∷ T_DecTotalOrder_740 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_844 ∷ T_DecTotalOrder_740 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_PartialSetoid_10 Source #

du_partialSetoid_846 ∷ T_DecTotalOrder_740 → T_PartialSetoid_10 Source #

d_refl_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny Source #

du_refl_848 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny Source #

d_reflexive_850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_850 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_Setoid_44 Source #

du_setoid_852 ∷ T_DecTotalOrder_740 → T_Setoid_44 Source #

d_sym_854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_854 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_856 ∷ T_DecTotalOrder_740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_StrictTotalOrder_864 ∷ p → p → p → () Source #

newtype T_StrictTotalOrder_864 Source #

Constructors

C_StrictTotalOrder'46'constructor_16739 T_IsStrictTotalOrder_502

d_Carrier_880 ∷ T_StrictTotalOrder_864 → () Source #

d__'8776'__882 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → () Source #

d__'60'__884 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → () Source #

d_isStrictTotalOrder_886 ∷ T_StrictTotalOrder_864 → T_IsStrictTotalOrder_502 Source #

d__'60''63'__890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'60''63'__890 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'8799'__892 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T_Dec_32 Source #

du__'8799'__892 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T_Dec_32 Source #

d_'60''45'resp'45''8776'_894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_894 ∷ T_StrictTotalOrder_864 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_896 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_898 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_900 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_compare_902 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T_Tri_136 Source #

d_irrefl_904 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #

d_isDecEquivalence_906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_906 ∷ T_StrictTotalOrder_864 → T_IsDecEquivalence_44 Source #

d_isDecStrictPartialOrder_908 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_IsDecStrictPartialOrder_314 Source #

du_isDecStrictPartialOrder_908 ∷ T_StrictTotalOrder_864 → T_IsDecStrictPartialOrder_314 Source #

d_isEquivalence_910 ∷ T_StrictTotalOrder_864 → T_IsEquivalence_26 Source #

d_isStrictPartialOrder_912 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_IsStrictPartialOrder_266 Source #

du_isStrictPartialOrder_912 ∷ T_StrictTotalOrder_864 → T_IsStrictPartialOrder_266 Source #

d_trans_914 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_strictPartialOrder_916 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_StrictPartialOrder_472 Source #

du_strictPartialOrder_916 ∷ T_StrictTotalOrder_864 → T_StrictPartialOrder_472 Source #

d__'8776'__922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → () Source #

d__'8777'__924 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → () Source #

d_Carrier_926 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → () Source #

d_isEquivalence_928 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_IsEquivalence_26 Source #

du_isEquivalence_928 ∷ T_StrictTotalOrder_864 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_930 ∷ T_StrictTotalOrder_864 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_PartialSetoid_10 Source #

du_partialSetoid_932 ∷ T_StrictTotalOrder_864 → T_PartialSetoid_10 Source #

d_refl_934 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny Source #

du_refl_934 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny Source #

d_reflexive_936 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_936 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_938 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Setoid_44 Source #

du_setoid_938 ∷ T_StrictTotalOrder_864 → T_Setoid_44 Source #

d_sym_940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_940 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_942 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_942 ∷ T_StrictTotalOrder_864 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_944 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_DecSetoid_84 Source #

du_decSetoid_944 ∷ T_StrictTotalOrder_864 → T_DecSetoid_84 Source #