Documentation

d_PartialSetoid_10 ∷ p → p → () Source #

newtype T_PartialSetoid_10 Source #

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_rawSetoid_34 ∷ T_Level_18 → T_Level_18 → T_PartialSetoid_10 → T_RawSetoid_12 Source #

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

d_Setoid_46 ∷ p → p → () Source #

newtype T_Setoid_46 Source #

d_Carrier_58 ∷ T_Setoid_46 → () Source #

d__'8776'__60 ∷ T_Setoid_46 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_62 ∷ T_Setoid_46 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_66 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_66 ∷ T_Setoid_46 → T_IsPartialEquivalence_16 Source #

d_refl_68 ∷ T_Setoid_46 → AgdaAny → AgdaAny Source #

d_reflexive_70 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_70 ∷ T_Setoid_46 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_partialSetoid_72 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_PartialSetoid_10 Source #

du_partialSetoid_72 ∷ T_Setoid_46 → T_PartialSetoid_10 Source #

d__'8777'__76 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #

d_rawSetoid_78 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_RawSetoid_12 Source #

d_sym_80 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_80 ∷ T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_82 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_82 ∷ T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DecSetoid_90 ∷ p → p → () Source #

newtype T_DecSetoid_90 Source #

d_Carrier_102 ∷ T_DecSetoid_90 → () Source #

d__'8776'__104 ∷ T_DecSetoid_90 → AgdaAny → AgdaAny → () Source #

d_isDecEquivalence_106 ∷ T_DecSetoid_90 → T_IsDecEquivalence_48 Source #

d__'8799'__110 ∷ T_DecSetoid_90 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isEquivalence_112 ∷ T_DecSetoid_90 → T_IsEquivalence_28 Source #

d_setoid_114 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_Setoid_46 Source #

du_setoid_114 ∷ T_DecSetoid_90 → T_Setoid_46 Source #

d__'8777'__118 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → AgdaAny → AgdaAny → () Source #

d_isPartialEquivalence_120 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_120 ∷ T_DecSetoid_90 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_122 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_PartialSetoid_10 Source #

du_partialSetoid_122 ∷ T_DecSetoid_90 → T_PartialSetoid_10 Source #

d_rawSetoid_124 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_RawSetoid_12 Source #

d_refl_126 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → AgdaAny → AgdaAny Source #

du_refl_126 ∷ T_DecSetoid_90 → AgdaAny → AgdaAny Source #

d_reflexive_128 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_128 ∷ T_DecSetoid_90 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_130 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_130 ∷ T_DecSetoid_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_132 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_132 ∷ T_DecSetoid_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Preorder_142 ∷ p → p → p → () Source #

newtype T_Preorder_142 Source #

d_Carrier_158 ∷ T_Preorder_142 → () Source #

d__'8776'__160 ∷ T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d__'8818'__162 ∷ T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d_isPreorder_164 ∷ T_Preorder_142 → T_IsPreorder_76 Source #

d_isEquivalence_168 ∷ T_Preorder_142 → T_IsEquivalence_28 Source #

d_refl_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny Source #

du_refl_170 ∷ T_Preorder_142 → AgdaAny → AgdaAny Source #

d_reflexive_172 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_174 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_176 ∷ T_Preorder_142 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_178 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_180 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_182 ∷ T_Preorder_142 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_184 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_186 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_Setoid_46 Source #

du_setoid_190 ∷ T_Preorder_142 → T_Setoid_46 Source #

d__'8776'__194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d__'8777'__196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d_Carrier_198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → () Source #

d_isEquivalence_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_IsEquivalence_28 Source #

du_isEquivalence_200 ∷ T_Preorder_142 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_202 ∷ T_Preorder_142 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_PartialSetoid_10 Source #

du_partialSetoid_204 ∷ T_Preorder_142 → T_PartialSetoid_10 Source #

d_rawSetoid_206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_RawSetoid_12 Source #

d_refl_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny Source #

du_refl_208 ∷ T_Preorder_142 → AgdaAny → AgdaAny Source #

d_reflexive_210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_210 ∷ T_Preorder_142 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_212 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_214 ∷ T_Preorder_142 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawRelation_216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_RawRelation_40 Source #

d__'8764'__220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d__'8777'__222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d__'8764''7506'__224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d__'8769'__226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → AgdaAny → AgdaAny → () Source #

d_rawSetoid_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_RawSetoid_12 Source #

d_TotalPreorder_240 ∷ p → p → p → () Source #

newtype T_TotalPreorder_240 Source #

d_Carrier_256 ∷ T_TotalPreorder_240 → () Source #

d__'8776'__258 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d__'8818'__260 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d_isTotalPreorder_262 ∷ T_TotalPreorder_240 → T_IsTotalPreorder_132 Source #

d_isPreorder_266 ∷ T_TotalPreorder_240 → T_IsPreorder_76 Source #

d_total_268 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_preorder_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_Preorder_142 Source #

du_preorder_270 ∷ T_TotalPreorder_240 → T_Preorder_142 Source #

d__'8764'__274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d__'8777'__276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d__'8764''7506'__278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d__'8769'__280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_IsEquivalence_28 Source #

du_isEquivalence_284 ∷ T_TotalPreorder_240 → T_IsEquivalence_28 Source #

d_rawRelation_286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_RawRelation_40 Source #

d_rawSetoid_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_RawSetoid_12 Source #

d_refl_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny Source #

du_refl_290 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny Source #

d_reflexive_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_292 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_294 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_296 ∷ T_TotalPreorder_240 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_298 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_300 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_302 ∷ T_TotalPreorder_240 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_304 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_306 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__310 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d__'8777'__312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → () Source #

d_Carrier_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → () Source #

d_isEquivalence_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_IsEquivalence_28 Source #

du_isEquivalence_316 ∷ T_TotalPreorder_240 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_318 ∷ T_TotalPreorder_240 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_PartialSetoid_10 Source #

du_partialSetoid_320 ∷ T_TotalPreorder_240 → T_PartialSetoid_10 Source #

d_rawSetoid_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_RawSetoid_12 Source #

d_refl_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny Source #

du_refl_324 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny Source #

d_reflexive_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_326 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_Setoid_46 Source #

du_setoid_328 ∷ T_TotalPreorder_240 → T_Setoid_46 Source #

d_sym_330 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_330 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_332 ∷ T_TotalPreorder_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DecPreorder_342 ∷ p → p → p → () Source #

newtype T_DecPreorder_342 Source #

d_Carrier_358 ∷ T_DecPreorder_342 → () Source #

d__'8776'__360 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8818'__362 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d_isDecPreorder_364 ∷ T_DecPreorder_342 → T_IsDecPreorder_184 Source #

d__'8799'__368 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8818''63'__370 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isPreorder_374 ∷ T_DecPreorder_342 → T_IsPreorder_76 Source #

d_preorder_412 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_Preorder_142 Source #

du_preorder_412 ∷ T_DecPreorder_342 → T_Preorder_142 Source #

d__'8764'__416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8777'__418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8764''7506'__420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8769'__422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__424 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_426 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_IsEquivalence_28 Source #

du_isEquivalence_426 ∷ T_DecPreorder_342 → T_IsEquivalence_28 Source #

d_rawRelation_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_RawRelation_40 Source #

d_rawSetoid_430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_RawSetoid_12 Source #

d_refl_432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny Source #

du_refl_432 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny Source #

d_reflexive_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_434 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_436 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_438 ∷ T_DecPreorder_342 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_440 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_442 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_444 ∷ T_DecPreorder_342 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_446 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_448 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_DecSetoid_90 Source #

du_decSetoid_452 ∷ T_DecPreorder_342 → T_DecSetoid_90 Source #

d__'8776'__456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8777'__458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → () Source #

d__'8799'__460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__460 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → () Source #

d_isDecEquivalence_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_464 ∷ T_DecPreorder_342 → T_IsDecEquivalence_48 Source #

d_isEquivalence_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_IsEquivalence_28 Source #

du_isEquivalence_466 ∷ T_DecPreorder_342 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_468 ∷ T_DecPreorder_342 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_PartialSetoid_10 Source #

du_partialSetoid_470 ∷ T_DecPreorder_342 → T_PartialSetoid_10 Source #

d_rawSetoid_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_RawSetoid_12 Source #

d_refl_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny Source #

du_refl_474 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny Source #

d_reflexive_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → T_Setoid_46 Source #

du_setoid_478 ∷ T_DecPreorder_342 → T_Setoid_46 Source #

d_sym_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_480 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_482 ∷ T_DecPreorder_342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Poset_492 ∷ p → p → p → () Source #

newtype T_Poset_492 Source #

d_Carrier_508 ∷ T_Poset_492 → () Source #

d__'8776'__510 ∷ T_Poset_492 → AgdaAny → AgdaAny → () Source #

d__'8804'__512 ∷ T_Poset_492 → AgdaAny → AgdaAny → () Source #

d_isPartialOrder_514 ∷ T_Poset_492 → T_IsPartialOrder_248 Source #

d_antisym_518 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPreorder_520 ∷ T_Poset_492 → T_IsPreorder_76 Source #

d_preorder_522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Preorder_142 Source #

du_preorder_522 ∷ T_Poset_492 → T_Preorder_142 Source #

d__'8764'__526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d__'8777'__528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_IsEquivalence_28 Source #

du_isEquivalence_530 ∷ T_Poset_492 → T_IsEquivalence_28 Source #

d_rawRelation_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_RawRelation_40 Source #

d_rawSetoid_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_RawSetoid_12 Source #

d_refl_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny Source #

du_refl_536 ∷ T_Poset_492 → AgdaAny → AgdaAny Source #

d_reflexive_538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_538 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_540 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_542 ∷ T_Poset_492 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_544 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_546 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_548 ∷ T_Poset_492 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_550 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_552 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d__'8777'__558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d_Carrier_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → () Source #

d_isEquivalence_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_IsEquivalence_28 Source #

du_isEquivalence_562 ∷ T_Poset_492 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_564 ∷ T_Poset_492 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_PartialSetoid_10 Source #

du_partialSetoid_566 ∷ T_Poset_492 → T_PartialSetoid_10 Source #

d_rawSetoid_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_RawSetoid_12 Source #

d_refl_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny Source #

du_refl_570 ∷ T_Poset_492 → AgdaAny → AgdaAny Source #

d_reflexive_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_572 ∷ T_Poset_492 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Setoid_46 Source #

du_setoid_574 ∷ T_Poset_492 → T_Setoid_46 Source #

d_sym_576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_576 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_578 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8764''7506'__582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d__'8769'__584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #

d_DecPoset_596 ∷ p → p → p → () Source #

newtype T_DecPoset_596 Source #

d_Carrier_612 ∷ T_DecPoset_596 → () Source #

d__'8776'__614 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8804'__616 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d_isDecPartialOrder_618 ∷ T_DecPoset_596 → T_IsDecPartialOrder_300 Source #

d__'8799'__622 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__624 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecPreorder_628 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_IsDecPreorder_184 Source #

du_isDecPreorder_628 ∷ T_DecPoset_596 → T_IsDecPreorder_184 Source #

d_isPartialOrder_632 ∷ T_DecPoset_596 → T_IsPartialOrder_248 Source #

d_poset_672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_Poset_492 Source #

du_poset_672 ∷ T_DecPoset_596 → T_Poset_492 Source #

d__'8764'__676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8777'__678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8764''7506'__680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8769'__682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d_antisym_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_686 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_IsEquivalence_28 Source #

du_isEquivalence_688 ∷ T_DecPoset_596 → T_IsEquivalence_28 Source #

d_isPreorder_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_IsPreorder_76 Source #

du_isPreorder_690 ∷ T_DecPoset_596 → T_IsPreorder_76 Source #

d_preorder_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_Preorder_142 Source #

du_preorder_692 ∷ T_DecPoset_596 → T_Preorder_142 Source #

d_rawRelation_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_RawRelation_40 Source #

d_rawSetoid_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_RawSetoid_12 Source #

d_refl_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny Source #

du_refl_698 ∷ T_DecPoset_596 → AgdaAny → AgdaAny Source #

d_reflexive_700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_700 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_702 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_704 ∷ T_DecPoset_596 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_706 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_708 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_710 ∷ T_DecPoset_596 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_712 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_714 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decPreorder_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_DecPreorder_342 Source #

du_decPreorder_716 ∷ T_DecPoset_596 → T_DecPreorder_342 Source #

d__'8776'__722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8777'__724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → () Source #

d__'8799'__726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__726 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → () Source #

d_decSetoid_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_DecSetoid_90 Source #

du_decSetoid_730 ∷ T_DecPoset_596 → T_DecSetoid_90 Source #

d_isDecEquivalence_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_732 ∷ T_DecPoset_596 → T_IsDecEquivalence_48 Source #

d_isEquivalence_734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_IsEquivalence_28 Source #

du_isEquivalence_734 ∷ T_DecPoset_596 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_736 ∷ T_DecPoset_596 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_PartialSetoid_10 Source #

du_partialSetoid_738 ∷ T_DecPoset_596 → T_PartialSetoid_10 Source #

d_rawSetoid_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_RawSetoid_12 Source #

d_refl_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny Source #

du_refl_742 ∷ T_DecPoset_596 → AgdaAny → AgdaAny Source #

d_reflexive_744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_744 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → T_Setoid_46 Source #

du_setoid_746 ∷ T_DecPoset_596 → T_Setoid_46 Source #

d_sym_748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_748 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_750 ∷ T_DecPoset_596 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_StrictPartialOrder_760 ∷ p → p → p → () Source #

newtype T_StrictPartialOrder_760 Source #

d_Carrier_776 ∷ T_StrictPartialOrder_760 → () Source #

d__'8776'__778 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d__'60'__780 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d_isStrictPartialOrder_782 ∷ T_StrictPartialOrder_760 → T_IsStrictPartialOrder_370 Source #

d_'60''45'resp'45''8776'_786 ∷ T_StrictPartialOrder_760 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_788 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_788 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_790 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_794 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_796 ∷ T_StrictPartialOrder_760 → T_IsEquivalence_28 Source #

d_trans_798 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_Setoid_46 Source #

du_setoid_802 ∷ T_StrictPartialOrder_760 → T_Setoid_46 Source #

d__'8776'__806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d__'8777'__808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d_Carrier_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → () Source #

d_isEquivalence_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_IsEquivalence_28 Source #

du_isEquivalence_812 ∷ T_StrictPartialOrder_760 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_814 ∷ T_StrictPartialOrder_760 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_PartialSetoid_10 Source #

du_partialSetoid_816 ∷ T_StrictPartialOrder_760 → T_PartialSetoid_10 Source #

d_rawSetoid_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_RawSetoid_12 Source #

d_refl_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny Source #

du_refl_820 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny Source #

d_reflexive_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_822 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_824 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_826 ∷ T_StrictPartialOrder_760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawRelation_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_RawRelation_40 Source #

d__'8764''7506'__832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d__'8777'__834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d__'8769'__836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → AgdaAny → AgdaAny → () Source #

d_rawSetoid_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_RawSetoid_12 Source #

d_DecStrictPartialOrder_850 ∷ p → p → p → () Source #

newtype T_DecStrictPartialOrder_850 Source #

d_Carrier_866 ∷ T_DecStrictPartialOrder_850 → () Source #

d__'8776'__868 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d__'60'__870 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d_isDecStrictPartialOrder_872 ∷ T_DecStrictPartialOrder_850 → T_IsDecStrictPartialOrder_418 Source #

d__'60''63'__876 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8799'__878 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isStrictPartialOrder_892 ∷ T_DecStrictPartialOrder_850 → T_IsStrictPartialOrder_370 Source #

d_strictPartialOrder_914 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_StrictPartialOrder_760 Source #

du_strictPartialOrder_914 ∷ T_DecStrictPartialOrder_850 → T_StrictPartialOrder_760 Source #

d__'8764''7506'__918 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d__'8777'__920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d__'8769'__922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__924 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d_'60''45'resp'45''8776'_926 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_926 ∷ T_DecStrictPartialOrder_850 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_928 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_928 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_930 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_934 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_936 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_IsEquivalence_28 Source #

du_isEquivalence_936 ∷ T_DecStrictPartialOrder_850 → T_IsEquivalence_28 Source #

d_rawRelation_938 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_RawRelation_40 Source #

d_rawSetoid_940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_RawSetoid_12 Source #

d_trans_942 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_942 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_DecSetoid_90 Source #

du_decSetoid_946 ∷ T_DecStrictPartialOrder_850 → T_DecSetoid_90 Source #

d__'8776'__950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d__'8777'__952 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → () Source #

d__'8799'__954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__954 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → () Source #

d_isDecEquivalence_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_958 ∷ T_DecStrictPartialOrder_850 → T_IsDecEquivalence_48 Source #

d_isEquivalence_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_IsEquivalence_28 Source #

du_isEquivalence_960 ∷ T_DecStrictPartialOrder_850 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_962 ∷ T_DecStrictPartialOrder_850 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_PartialSetoid_10 Source #

du_partialSetoid_964 ∷ T_DecStrictPartialOrder_850 → T_PartialSetoid_10 Source #

d_rawSetoid_966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_RawSetoid_12 Source #

d_refl_968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny Source #

du_refl_968 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny Source #

d_reflexive_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_970 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → T_Setoid_46 Source #

du_setoid_972 ∷ T_DecStrictPartialOrder_850 → T_Setoid_46 Source #

d_sym_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_974 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_976 ∷ T_DecStrictPartialOrder_850 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_TotalOrder_986 ∷ p → p → p → () Source #

newtype T_TotalOrder_986 Source #

d_Carrier_1002 ∷ T_TotalOrder_986 → () Source #

d__'8776'__1004 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d__'8804'__1006 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d_isTotalOrder_1008 ∷ T_TotalOrder_986 → T_IsTotalOrder_488 Source #

d_isPartialOrder_1012 ∷ T_TotalOrder_986 → T_IsPartialOrder_248 Source #

d_isTotalPreorder_1014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_IsTotalPreorder_132 Source #

du_isTotalPreorder_1014 ∷ T_TotalOrder_986 → T_IsTotalPreorder_132 Source #

d_total_1016 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_poset_1018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Poset_492 Source #

du_poset_1018 ∷ T_TotalOrder_986 → T_Poset_492 Source #

d__'8764'__1022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d__'8777'__1024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d__'8764''7506'__1026 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d__'8769'__1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__1030 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d_antisym_1032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_1032 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_IsEquivalence_28 Source #

du_isEquivalence_1034 ∷ T_TotalOrder_986 → T_IsEquivalence_28 Source #

d_isPreorder_1036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_IsPreorder_76 Source #

du_isPreorder_1036 ∷ T_TotalOrder_986 → T_IsPreorder_76 Source #

d_preorder_1038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Preorder_142 Source #

du_preorder_1038 ∷ T_TotalOrder_986 → T_Preorder_142 Source #

d_rawRelation_1040 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_RawRelation_40 Source #

d_rawSetoid_1042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_RawSetoid_12 Source #

d_refl_1044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny Source #

du_refl_1044 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny Source #

d_reflexive_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_1046 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1048 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1050 ∷ T_TotalOrder_986 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1052 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1052 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1054 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_1056 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_1056 ∷ T_TotalOrder_986 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_1058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_1058 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_1060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_1060 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d__'8777'__1066 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #

d_Carrier_1068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → () Source #

d_isEquivalence_1070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_IsEquivalence_28 Source #

du_isEquivalence_1070 ∷ T_TotalOrder_986 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1072 ∷ T_TotalOrder_986 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_PartialSetoid_10 Source #

du_partialSetoid_1074 ∷ T_TotalOrder_986 → T_PartialSetoid_10 Source #

d_rawSetoid_1076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_RawSetoid_12 Source #

d_refl_1078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny Source #

du_refl_1078 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny Source #

d_reflexive_1080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1080 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Setoid_46 Source #

du_setoid_1082 ∷ T_TotalOrder_986 → T_Setoid_46 Source #

d_sym_1084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1084 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1086 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_totalPreorder_1088 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_TotalPreorder_240 Source #

du_totalPreorder_1088 ∷ T_TotalOrder_986 → T_TotalPreorder_240 Source #

d_DecTotalOrder_1098 ∷ p → p → p → () Source #

newtype T_DecTotalOrder_1098 Source #

d_Carrier_1114 ∷ T_DecTotalOrder_1098 → () Source #

d__'8776'__1116 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8804'__1118 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d_isDecTotalOrder_1120 ∷ T_DecTotalOrder_1098 → T_IsDecTotalOrder_546 Source #

d__'8799'__1124 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__1126 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecPartialOrder_1130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsDecPartialOrder_300 Source #

du_isDecPartialOrder_1130 ∷ T_DecTotalOrder_1098 → T_IsDecPartialOrder_300 Source #

d_isTotalOrder_1140 ∷ T_DecTotalOrder_1098 → T_IsTotalOrder_488 Source #

d_totalOrder_1182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_TotalOrder_986 Source #

du_totalOrder_1182 ∷ T_DecTotalOrder_1098 → T_TotalOrder_986 Source #

d__'8764'__1186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8777'__1188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8764''7506'__1190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8769'__1192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__1194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d_antisym_1196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_1196 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsEquivalence_28 Source #

du_isEquivalence_1198 ∷ T_DecTotalOrder_1098 → T_IsEquivalence_28 Source #

d_isPartialOrder_1200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsPartialOrder_248 Source #

du_isPartialOrder_1200 ∷ T_DecTotalOrder_1098 → T_IsPartialOrder_248 Source #

d_isPreorder_1202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsPreorder_76 Source #

du_isPreorder_1202 ∷ T_DecTotalOrder_1098 → T_IsPreorder_76 Source #

d_isTotalPreorder_1204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsTotalPreorder_132 Source #

du_isTotalPreorder_1204 ∷ T_DecTotalOrder_1098 → T_IsTotalPreorder_132 Source #

d_poset_1206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_Poset_492 Source #

du_poset_1206 ∷ T_DecTotalOrder_1098 → T_Poset_492 Source #

d_preorder_1208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_Preorder_142 Source #

du_preorder_1208 ∷ T_DecTotalOrder_1098 → T_Preorder_142 Source #

d_rawRelation_1210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_RawRelation_40 Source #

d_rawSetoid_1212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_RawSetoid_12 Source #

d_refl_1214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny Source #

du_refl_1214 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny Source #

d_reflexive_1216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_1216 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_1218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T__'8846'__30 Source #

du_total_1218 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_totalPreorder_1220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_TotalPreorder_240 Source #

du_totalPreorder_1220 ∷ T_DecTotalOrder_1098 → T_TotalPreorder_240 Source #

d_trans_1222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1222 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1224 ∷ T_DecTotalOrder_1098 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1226 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1228 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_1230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_1230 ∷ T_DecTotalOrder_1098 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_1232 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_1232 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_1234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_1234 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decPoset_1236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_DecPoset_596 Source #

du_decPoset_1236 ∷ T_DecTotalOrder_1098 → T_DecPoset_596 Source #

d__'8776'__1242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8777'__1244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → () Source #

d__'8799'__1246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1246 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_1248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → () Source #

d_decSetoid_1250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_DecSetoid_90 Source #

du_decSetoid_1250 ∷ T_DecTotalOrder_1098 → T_DecSetoid_90 Source #

d_isDecEquivalence_1252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_1252 ∷ T_DecTotalOrder_1098 → T_IsDecEquivalence_48 Source #

d_isEquivalence_1254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsEquivalence_28 Source #

du_isEquivalence_1254 ∷ T_DecTotalOrder_1098 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1256 ∷ T_DecTotalOrder_1098 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_PartialSetoid_10 Source #

du_partialSetoid_1258 ∷ T_DecTotalOrder_1098 → T_PartialSetoid_10 Source #

d_rawSetoid_1260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_RawSetoid_12 Source #

d_refl_1262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny Source #

du_refl_1262 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny Source #

d_reflexive_1264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1264 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_Setoid_46 Source #

du_setoid_1266 ∷ T_DecTotalOrder_1098 → T_Setoid_46 Source #

d_sym_1268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1268 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1270 ∷ T_DecTotalOrder_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_StrictTotalOrder_1280 ∷ p → p → p → () Source #

newtype T_StrictTotalOrder_1280 Source #

d_Carrier_1296 ∷ T_StrictTotalOrder_1280 → () Source #

d__'8776'__1298 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d__'60'__1300 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d_isStrictTotalOrder_1302 ∷ T_StrictTotalOrder_1280 → T_IsStrictTotalOrder_624 Source #

d__'60''63'__1306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'60''63'__1306 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8799'__1308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1308 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_compare_1310 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_isDecEquivalence_1312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_1312 ∷ T_StrictTotalOrder_1280 → T_IsDecEquivalence_48 Source #

d_isDecStrictPartialOrder_1314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_IsDecStrictPartialOrder_418 Source #

du_isDecStrictPartialOrder_1314 ∷ T_StrictTotalOrder_1280 → T_IsDecStrictPartialOrder_418 Source #

d_isStrictPartialOrder_1316 ∷ T_StrictTotalOrder_1280 → T_IsStrictPartialOrder_370 Source #

d_strictPartialOrder_1318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_StrictPartialOrder_760 Source #

du_strictPartialOrder_1318 ∷ T_StrictTotalOrder_1280 → T_StrictPartialOrder_760 Source #

d__'8764''7506'__1322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d__'8777'__1324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d__'8769'__1326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__1328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d_'60''45'resp'45''8776'_1330 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_1330 ∷ T_StrictTotalOrder_1280 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_1332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_1332 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_1334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_1334 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_1336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_1338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_1340 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_IsEquivalence_28 Source #

du_isEquivalence_1340 ∷ T_StrictTotalOrder_1280 → T_IsEquivalence_28 Source #

d_rawRelation_1342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_RawRelation_40 Source #

d_rawSetoid_1344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_RawSetoid_12 Source #

d_trans_1346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1346 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decStrictPartialOrder_1348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_DecStrictPartialOrder_850 Source #

du_decStrictPartialOrder_1348 ∷ T_StrictTotalOrder_1280 → T_DecStrictPartialOrder_850 Source #

d__'8776'__1354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d__'8777'__1356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → () Source #

d__'8799'__1358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1358 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_1360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → () Source #

d_decSetoid_1362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_DecSetoid_90 Source #

du_decSetoid_1362 ∷ T_StrictTotalOrder_1280 → T_DecSetoid_90 Source #

d_isDecEquivalence_1364 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_1364 ∷ T_StrictTotalOrder_1280 → T_IsDecEquivalence_48 Source #

d_isEquivalence_1366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_IsEquivalence_28 Source #

du_isEquivalence_1366 ∷ T_StrictTotalOrder_1280 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1368 ∷ T_StrictTotalOrder_1280 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_PartialSetoid_10 Source #

du_partialSetoid_1370 ∷ T_StrictTotalOrder_1280 → T_PartialSetoid_10 Source #

d_rawSetoid_1372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_RawSetoid_12 Source #

d_refl_1374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny Source #

du_refl_1374 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny Source #

d_reflexive_1376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1376 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Setoid_46 Source #

du_setoid_1378 ∷ T_StrictTotalOrder_1280 → T_Setoid_46 Source #

d_sym_1380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1380 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1382 ∷ T_StrictTotalOrder_1280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_1384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_DecSetoid_90 Source #

du_decSetoid_1384 ∷ T_StrictTotalOrder_1280 → T_DecSetoid_90 Source #

d_DenseLinearOrder_1394 ∷ p → p → p → () Source #

newtype T_DenseLinearOrder_1394 Source #

d_Carrier_1410 ∷ T_DenseLinearOrder_1394 → () Source #

d__'8776'__1412 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d__'60'__1414 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d_isDenseLinearOrder_1416 ∷ T_DenseLinearOrder_1394 → T_IsDenseLinearOrder_686 Source #

d_dense_1420 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isStrictTotalOrder_1422 ∷ T_DenseLinearOrder_1394 → T_IsStrictTotalOrder_624 Source #

d_strictTotalOrder_1424 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_StrictTotalOrder_1280 Source #

du_strictTotalOrder_1424 ∷ T_DenseLinearOrder_1394 → T_StrictTotalOrder_1280 Source #

d__'60''63'__1428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'60''63'__1428 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8764''7506'__1430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d__'8777'__1432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d__'8799'__1434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1434 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8769'__1436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__1438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d_'60''45'resp'45''8776'_1440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_1440 ∷ T_DenseLinearOrder_1394 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_1442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_1442 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_1444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_1444 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_1446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_compare_1448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Tri_158 Source #

du_compare_1448 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_decSetoid_1450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_DecSetoid_90 Source #

du_decSetoid_1450 ∷ T_DenseLinearOrder_1394 → T_DecSetoid_90 Source #

d_decStrictPartialOrder_1452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_DecStrictPartialOrder_850 Source #

du_decStrictPartialOrder_1452 ∷ T_DenseLinearOrder_1394 → T_DecStrictPartialOrder_850 Source #

d_irrefl_1454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isDecEquivalence_1456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_1456 ∷ T_DenseLinearOrder_1394 → T_IsDecEquivalence_48 Source #

d_isDecStrictPartialOrder_1458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsDecStrictPartialOrder_418 Source #

du_isDecStrictPartialOrder_1458 ∷ T_DenseLinearOrder_1394 → T_IsDecStrictPartialOrder_418 Source #

d_isEquivalence_1460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsEquivalence_28 Source #

du_isEquivalence_1460 ∷ T_DenseLinearOrder_1394 → T_IsEquivalence_28 Source #

d_isStrictPartialOrder_1462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsStrictPartialOrder_370 Source #

du_isStrictPartialOrder_1462 ∷ T_DenseLinearOrder_1394 → T_IsStrictPartialOrder_370 Source #

d_rawRelation_1464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_RawRelation_40 Source #

d_rawSetoid_1466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_RawSetoid_12 Source #

d_strictPartialOrder_1468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_StrictPartialOrder_760 Source #

du_strictPartialOrder_1468 ∷ T_DenseLinearOrder_1394 → T_StrictPartialOrder_760 Source #

d_trans_1470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1470 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d__'8777'__1476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → () Source #

d__'8799'__1478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1478 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_1480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → () Source #

d_decSetoid_1482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_DecSetoid_90 Source #

du_decSetoid_1482 ∷ T_DenseLinearOrder_1394 → T_DecSetoid_90 Source #

d_isDecEquivalence_1484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_1484 ∷ T_DenseLinearOrder_1394 → T_IsDecEquivalence_48 Source #

d_isEquivalence_1486 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsEquivalence_28 Source #

du_isEquivalence_1486 ∷ T_DenseLinearOrder_1394 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1488 ∷ T_DenseLinearOrder_1394 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_PartialSetoid_10 Source #

du_partialSetoid_1490 ∷ T_DenseLinearOrder_1394 → T_PartialSetoid_10 Source #

d_rawSetoid_1492 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_RawSetoid_12 Source #

d_refl_1494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny Source #

du_refl_1494 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny Source #

d_reflexive_1496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1496 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → T_Setoid_46 Source #

du_setoid_1498 ∷ T_DenseLinearOrder_1394 → T_Setoid_46 Source #

d_sym_1500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1500 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1502 ∷ T_DenseLinearOrder_1394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_ApartnessRelation_1512 ∷ p → p → p → () Source #

newtype T_ApartnessRelation_1512 Source #

d_Carrier_1528 ∷ T_ApartnessRelation_1512 → () Source #

d__'8776'__1530 ∷ T_ApartnessRelation_1512 → AgdaAny → AgdaAny → () Source #

d__'35'__1532 ∷ T_ApartnessRelation_1512 → AgdaAny → AgdaAny → () Source #

d_isApartnessRelation_1534 ∷ T_ApartnessRelation_1512 → T_IsApartnessRelation_750 Source #

d_cotrans_1538 ∷ T_ApartnessRelation_1512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_irrefl_1540 ∷ T_ApartnessRelation_1512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_sym_1542 ∷ T_ApartnessRelation_1512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawRelation_1544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1512 → T_RawRelation_40 Source #

d__'8764''7506'__1548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1512 → AgdaAny → AgdaAny → () Source #

d__'8769'__1550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1512 → AgdaAny → AgdaAny → () Source #

d__'8769''7506'__1552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1512 → AgdaAny → AgdaAny → () Source #

d__'8777'__1554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1512 → AgdaAny → AgdaAny → () Source #

d_rawSetoid_1556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1512 → T_RawSetoid_12 Source #