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_733 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_partialSetoid_70 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_PartialSetoid_10 Source #

du_partialSetoid_70 ∷ T_Setoid_44 → T_PartialSetoid_10 Source #

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

d_sym_76 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_76 ∷ T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_78 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_78 ∷ T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DecSetoid_84 ∷ p → p → () Source #

newtype T_DecSetoid_84 Source #

Constructors

C_DecSetoid'46'constructor_1389 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_20 Source #

d_isEquivalence_106 ∷ T_DecSetoid_84 → T_IsEquivalence_26 Source #

d_setoid_108 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_Setoid_44 Source #

du_setoid_108 ∷ T_DecSetoid_84 → T_Setoid_44 Source #

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

d_isPartialEquivalence_114 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_114 ∷ T_DecSetoid_84 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_116 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_PartialSetoid_10 Source #

du_partialSetoid_116 ∷ T_DecSetoid_84 → T_PartialSetoid_10 Source #

d_refl_118 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → AgdaAny → AgdaAny Source #

du_refl_118 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny Source #

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

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

d_sym_122 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_122 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_124 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_124 ∷ T_DecSetoid_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

newtype T_Preorder_132 Source #

Constructors

C_Preorder'46'constructor_2267 T_IsPreorder_70

d_Carrier_148 ∷ T_Preorder_132 → () Source #

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

d__'8818'__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_'8818''45'resp'45''8776'_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_172 ∷ T_Preorder_132 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_174 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_176 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Setoid_44 Source #

du_setoid_180 ∷ T_Preorder_132 → T_Setoid_44 Source #

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

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

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

d_isEquivalence_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_IsEquivalence_26 Source #

du_isEquivalence_190 ∷ T_Preorder_132 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_192 ∷ T_Preorder_132 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_PartialSetoid_10 Source #

du_partialSetoid_194 ∷ T_Preorder_132 → T_PartialSetoid_10 Source #

d_refl_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny Source #

du_refl_196 ∷ T_Preorder_132 → AgdaAny → AgdaAny Source #

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

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

d_sym_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_200 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_202 ∷ T_Preorder_132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8934'__204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d__'8819'__210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d__'8935'__212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d__'8764'__214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → AgdaAny → AgdaAny → () Source #

d_TotalPreorder_222 ∷ p → p → p → () Source #

newtype T_TotalPreorder_222 Source #

Constructors

C_TotalPreorder'46'constructor_4573 T_IsTotalPreorder_124

d_Carrier_238 ∷ T_TotalPreorder_222 → () Source #

d__'8776'__240 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d__'8818'__242 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d_isTotalPreorder_244 ∷ T_TotalPreorder_222 → T_IsTotalPreorder_124 Source #

d_isPreorder_248 ∷ T_TotalPreorder_222 → T_IsPreorder_70 Source #

d_total_250 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_preorder_252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_Preorder_132 Source #

du_preorder_252 ∷ T_TotalPreorder_222 → T_Preorder_132 Source #

d__'8764'__256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d__'8819'__258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d__'8934'__260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d__'8935'__262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_IsEquivalence_26 Source #

du_isEquivalence_264 ∷ T_TotalPreorder_222 → T_IsEquivalence_26 Source #

d_refl_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny Source #

du_refl_266 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny Source #

d_reflexive_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_268 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_270 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_272 ∷ T_TotalPreorder_222 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_274 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_276 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_278 ∷ T_TotalPreorder_222 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_280 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_282 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d__'8777'__288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → () Source #

d_Carrier_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → () Source #

d_isEquivalence_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_IsEquivalence_26 Source #

du_isEquivalence_292 ∷ T_TotalPreorder_222 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_294 ∷ T_TotalPreorder_222 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_PartialSetoid_10 Source #

du_partialSetoid_296 ∷ T_TotalPreorder_222 → T_PartialSetoid_10 Source #

d_refl_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny Source #

du_refl_298 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny Source #

d_reflexive_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_300 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_Setoid_44 Source #

du_setoid_302 ∷ T_TotalPreorder_222 → T_Setoid_44 Source #

d_sym_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_304 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_306 ∷ T_TotalPreorder_222 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Poset_314 ∷ p → p → p → () Source #

newtype T_Poset_314 Source #

Constructors

C_Poset'46'constructor_6389 T_IsPartialOrder_174

d_Carrier_330 ∷ T_Poset_314 → () Source #

d__'8776'__332 ∷ T_Poset_314 → AgdaAny → AgdaAny → () Source #

d__'8804'__334 ∷ T_Poset_314 → AgdaAny → AgdaAny → () Source #

d_isPartialOrder_336 ∷ T_Poset_314 → T_IsPartialOrder_174 Source #

d_antisym_340 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPreorder_342 ∷ T_Poset_314 → T_IsPreorder_70 Source #

d_preorder_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_Preorder_132 Source #

du_preorder_344 ∷ T_Poset_314 → T_Preorder_132 Source #

d__'8764'__348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #

d__'8819'__350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #

d__'8934'__352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #

d__'8935'__354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #

d_isEquivalence_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_IsEquivalence_26 Source #

du_isEquivalence_356 ∷ T_Poset_314 → T_IsEquivalence_26 Source #

d_refl_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny Source #

du_refl_358 ∷ T_Poset_314 → AgdaAny → AgdaAny Source #

d_reflexive_360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_360 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_362 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_364 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_364 ∷ T_Poset_314 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_366 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_368 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_370 ∷ T_Poset_314 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_372 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_374 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #

d__'8777'__380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #

d_Carrier_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → () Source #

d_isEquivalence_384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_IsEquivalence_26 Source #

du_isEquivalence_384 ∷ T_Poset_314 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_386 ∷ T_Poset_314 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_388 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_PartialSetoid_10 Source #

du_partialSetoid_388 ∷ T_Poset_314 → T_PartialSetoid_10 Source #

d_refl_390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny Source #

du_refl_390 ∷ T_Poset_314 → AgdaAny → AgdaAny Source #

d_reflexive_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_392 ∷ T_Poset_314 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_Setoid_44 Source #

du_setoid_394 ∷ T_Poset_314 → T_Setoid_44 Source #

d_sym_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_396 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_398 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_398 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DecPoset_406 ∷ p → p → p → () Source #

newtype T_DecPoset_406 Source #

Constructors

C_DecPoset'46'constructor_8213 T_IsDecPartialOrder_224

d_Carrier_422 ∷ T_DecPoset_406 → () Source #

d__'8776'__424 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d__'8804'__426 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d_isDecPartialOrder_428 ∷ T_DecPoset_406 → T_IsDecPartialOrder_224 Source #

d__'8799'__432 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__434 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isPartialOrder_440 ∷ T_DecPoset_406 → T_IsPartialOrder_174 Source #

d_poset_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_Poset_314 Source #

du_poset_480 ∷ T_DecPoset_406 → T_Poset_314 Source #

d__'8764'__484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d__'8819'__486 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d__'8934'__488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d__'8935'__490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d_antisym_492 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_492 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_IsEquivalence_26 Source #

du_isEquivalence_494 ∷ T_DecPoset_406 → T_IsEquivalence_26 Source #

d_isPreorder_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_IsPreorder_70 Source #

du_isPreorder_496 ∷ T_DecPoset_406 → T_IsPreorder_70 Source #

d_preorder_498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_Preorder_132 Source #

du_preorder_498 ∷ T_DecPoset_406 → T_Preorder_132 Source #

d_refl_500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny Source #

du_refl_500 ∷ T_DecPoset_406 → AgdaAny → AgdaAny Source #

d_reflexive_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_502 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_504 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_504 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_506 ∷ T_DecPoset_406 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_508 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_508 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_510 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_512 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_512 ∷ T_DecPoset_406 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_514 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_514 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_516 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_516 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_520 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_DecSetoid_84 Source #

du_decSetoid_520 ∷ T_DecPoset_406 → T_DecSetoid_84 Source #

d__'8776'__524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d__'8777'__526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → () Source #

d__'8799'__528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__528 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → () Source #

d_isDecEquivalence_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_532 ∷ T_DecPoset_406 → T_IsDecEquivalence_44 Source #

d_isEquivalence_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_IsEquivalence_26 Source #

du_isEquivalence_534 ∷ T_DecPoset_406 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_536 ∷ T_DecPoset_406 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_PartialSetoid_10 Source #

du_partialSetoid_538 ∷ T_DecPoset_406 → T_PartialSetoid_10 Source #

d_refl_540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny Source #

du_refl_540 ∷ T_DecPoset_406 → AgdaAny → AgdaAny Source #

d_reflexive_542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_542 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → T_Setoid_44 Source #

du_setoid_544 ∷ T_DecPoset_406 → T_Setoid_44 Source #

d_sym_546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_546 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_548 ∷ T_DecPoset_406 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_StrictPartialOrder_556 ∷ p → p → p → () Source #

newtype T_StrictPartialOrder_556 Source #

Constructors

C_StrictPartialOrder'46'constructor_11097 T_IsStrictPartialOrder_290

d_Carrier_572 ∷ T_StrictPartialOrder_556 → () Source #

d__'8776'__574 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d__'60'__576 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d_isStrictPartialOrder_578 ∷ T_StrictPartialOrder_556 → T_IsStrictPartialOrder_290 Source #

d_'60''45'resp'45''8776'_582 ∷ T_StrictPartialOrder_556 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_584 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_586 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_590 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_592 ∷ T_StrictPartialOrder_556 → T_IsEquivalence_26 Source #

d_trans_594 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → T_Setoid_44 Source #

du_setoid_598 ∷ T_StrictPartialOrder_556 → T_Setoid_44 Source #

d__'8776'__602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d__'8777'__604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d_Carrier_606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → () Source #

d_isEquivalence_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → T_IsEquivalence_26 Source #

du_isEquivalence_608 ∷ T_StrictPartialOrder_556 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_610 ∷ T_StrictPartialOrder_556 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_612 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → T_PartialSetoid_10 Source #

du_partialSetoid_612 ∷ T_StrictPartialOrder_556 → T_PartialSetoid_10 Source #

d_refl_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny Source #

du_refl_614 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny Source #

d_reflexive_616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_616 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_618 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_620 ∷ T_StrictPartialOrder_556 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8814'__622 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d__'62'__628 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d__'8815'__630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → AgdaAny → AgdaAny → () Source #

d_DecStrictPartialOrder_638 ∷ p → p → p → () Source #

newtype T_DecStrictPartialOrder_638 Source #

Constructors

C_DecStrictPartialOrder'46'constructor_13245 T_IsDecStrictPartialOrder_336

d_Carrier_654 ∷ T_DecStrictPartialOrder_638 → () Source #

d__'8776'__656 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d__'60'__658 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d_isDecStrictPartialOrder_660 ∷ T_DecStrictPartialOrder_638 → T_IsDecStrictPartialOrder_336 Source #

d__'60''63'__664 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8799'__666 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isStrictPartialOrder_680 ∷ T_DecStrictPartialOrder_638 → T_IsStrictPartialOrder_290 Source #

d_strictPartialOrder_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_StrictPartialOrder_556 Source #

du_strictPartialOrder_702 ∷ T_DecStrictPartialOrder_638 → T_StrictPartialOrder_556 Source #

d__'62'__706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d__'8814'__708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d__'8815'__710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d_'60''45'resp'45''8776'_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_712 ∷ T_DecStrictPartialOrder_638 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_714 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_716 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_IsEquivalence_26 Source #

du_isEquivalence_722 ∷ T_DecStrictPartialOrder_638 → T_IsEquivalence_26 Source #

d_trans_724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_724 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_DecSetoid_84 Source #

du_decSetoid_728 ∷ T_DecStrictPartialOrder_638 → T_DecSetoid_84 Source #

d__'8776'__732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d__'8777'__734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → () Source #

d__'8799'__736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__736 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → () Source #

d_isDecEquivalence_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_740 ∷ T_DecStrictPartialOrder_638 → T_IsDecEquivalence_44 Source #

d_isEquivalence_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_IsEquivalence_26 Source #

du_isEquivalence_742 ∷ T_DecStrictPartialOrder_638 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_744 ∷ T_DecStrictPartialOrder_638 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_PartialSetoid_10 Source #

du_partialSetoid_746 ∷ T_DecStrictPartialOrder_638 → T_PartialSetoid_10 Source #

d_refl_748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny Source #

du_refl_748 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny Source #

d_reflexive_750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_750 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → T_Setoid_44 Source #

du_setoid_752 ∷ T_DecStrictPartialOrder_638 → T_Setoid_44 Source #

d_sym_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_754 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_756 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_756 ∷ T_DecStrictPartialOrder_638 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_TotalOrder_764 ∷ p → p → p → () Source #

newtype T_TotalOrder_764 Source #

Constructors

C_TotalOrder'46'constructor_15747 T_IsTotalOrder_404

d_Carrier_780 ∷ T_TotalOrder_764 → () Source #

d__'8776'__782 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d__'8804'__784 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d_isTotalOrder_786 ∷ T_TotalOrder_764 → T_IsTotalOrder_404 Source #

d_isPartialOrder_790 ∷ T_TotalOrder_764 → T_IsPartialOrder_174 Source #

d_isTotalPreorder_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_IsTotalPreorder_124 Source #

du_isTotalPreorder_792 ∷ T_TotalOrder_764 → T_IsTotalPreorder_124 Source #

d_total_794 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_poset_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Poset_314 Source #

du_poset_796 ∷ T_TotalOrder_764 → T_Poset_314 Source #

d__'8764'__800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d__'8819'__802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d__'8934'__804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d__'8935'__806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d_antisym_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_808 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_IsEquivalence_26 Source #

du_isEquivalence_810 ∷ T_TotalOrder_764 → T_IsEquivalence_26 Source #

d_isPreorder_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_IsPreorder_70 Source #

du_isPreorder_812 ∷ T_TotalOrder_764 → T_IsPreorder_70 Source #

d_preorder_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Preorder_132 Source #

du_preorder_814 ∷ T_TotalOrder_764 → T_Preorder_132 Source #

d_refl_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny Source #

du_refl_816 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny Source #

d_reflexive_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_818 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_820 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_822 ∷ T_TotalOrder_764 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_824 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_826 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_828 ∷ T_TotalOrder_764 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_830 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_832 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d__'8777'__838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #

d_Carrier_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → () Source #

d_isEquivalence_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_IsEquivalence_26 Source #

du_isEquivalence_842 ∷ T_TotalOrder_764 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_844 ∷ T_TotalOrder_764 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_PartialSetoid_10 Source #

du_partialSetoid_846 ∷ T_TotalOrder_764 → T_PartialSetoid_10 Source #

d_refl_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny Source #

du_refl_848 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny Source #

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

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

d_setoid_852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Setoid_44 Source #

du_setoid_852 ∷ T_TotalOrder_764 → T_Setoid_44 Source #

d_sym_854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_854 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_856 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_totalPreorder_858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_TotalPreorder_222 Source #

du_totalPreorder_858 ∷ T_TotalOrder_764 → T_TotalPreorder_222 Source #

d_DecTotalOrder_866 ∷ p → p → p → () Source #

newtype T_DecTotalOrder_866 Source #

Constructors

C_DecTotalOrder'46'constructor_17849 T_IsDecTotalOrder_460

d_Carrier_882 ∷ T_DecTotalOrder_866 → () Source #

d__'8776'__884 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d__'8804'__886 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d_isDecTotalOrder_888 ∷ T_DecTotalOrder_866 → T_IsDecTotalOrder_460 Source #

d__'8799'__892 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8804''63'__894 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_isDecPartialOrder_898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsDecPartialOrder_224 Source #

du_isDecPartialOrder_898 ∷ T_DecTotalOrder_866 → T_IsDecPartialOrder_224 Source #

d_isTotalOrder_906 ∷ T_DecTotalOrder_866 → T_IsTotalOrder_404 Source #

d_totalOrder_948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_TotalOrder_764 Source #

du_totalOrder_948 ∷ T_DecTotalOrder_866 → T_TotalOrder_764 Source #

d__'8764'__952 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d__'8819'__954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d__'8934'__956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d__'8935'__958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d_antisym_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_960 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsEquivalence_26 Source #

du_isEquivalence_962 ∷ T_DecTotalOrder_866 → T_IsEquivalence_26 Source #

d_isPartialOrder_964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsPartialOrder_174 Source #

du_isPartialOrder_964 ∷ T_DecTotalOrder_866 → T_IsPartialOrder_174 Source #

d_isPreorder_966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsPreorder_70 Source #

du_isPreorder_966 ∷ T_DecTotalOrder_866 → T_IsPreorder_70 Source #

d_isTotalPreorder_968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsTotalPreorder_124 Source #

du_isTotalPreorder_968 ∷ T_DecTotalOrder_866 → T_IsTotalPreorder_124 Source #

d_poset_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_Poset_314 Source #

du_poset_970 ∷ T_DecTotalOrder_866 → T_Poset_314 Source #

d_preorder_972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_Preorder_132 Source #

du_preorder_972 ∷ T_DecTotalOrder_866 → T_Preorder_132 Source #

d_refl_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny Source #

du_refl_974 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny Source #

d_reflexive_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_976 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → T__'8846'__30 Source #

du_total_978 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_totalPreorder_980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_TotalPreorder_222 Source #

du_totalPreorder_980 ∷ T_DecTotalOrder_866 → T_TotalPreorder_222 Source #

d_trans_982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_982 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_984 ∷ T_DecTotalOrder_866 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_986 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_988 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_990 ∷ T_DecTotalOrder_866 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_992 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_994 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decPoset_996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_DecPoset_406 Source #

du_decPoset_996 ∷ T_DecTotalOrder_866 → T_DecPoset_406 Source #

d__'8776'__1002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d__'8777'__1004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → () Source #

d__'8799'__1006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1006 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_1008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → () Source #

d_decSetoid_1010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_DecSetoid_84 Source #

du_decSetoid_1010 ∷ T_DecTotalOrder_866 → T_DecSetoid_84 Source #

d_isDecEquivalence_1012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_1012 ∷ T_DecTotalOrder_866 → T_IsDecEquivalence_44 Source #

d_isEquivalence_1014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsEquivalence_26 Source #

du_isEquivalence_1014 ∷ T_DecTotalOrder_866 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1016 ∷ T_DecTotalOrder_866 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_PartialSetoid_10 Source #

du_partialSetoid_1018 ∷ T_DecTotalOrder_866 → T_PartialSetoid_10 Source #

d_refl_1020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny Source #

du_refl_1020 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny Source #

d_reflexive_1022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1022 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → T_Setoid_44 Source #

du_setoid_1024 ∷ T_DecTotalOrder_866 → T_Setoid_44 Source #

d_sym_1026 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1026 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1028 ∷ T_DecTotalOrder_866 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_StrictTotalOrder_1036 ∷ p → p → p → () Source #

newtype T_StrictTotalOrder_1036 Source #

Constructors

C_StrictTotalOrder'46'constructor_21059 T_IsStrictTotalOrder_534

d_Carrier_1052 ∷ T_StrictTotalOrder_1036 → () Source #

d__'8776'__1054 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d__'60'__1056 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d_isStrictTotalOrder_1058 ∷ T_StrictTotalOrder_1036 → T_IsStrictTotalOrder_534 Source #

d__'60''63'__1062 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'60''63'__1062 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8799'__1064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1064 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_compare_1066 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_isDecEquivalence_1068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_1068 ∷ T_StrictTotalOrder_1036 → T_IsDecEquivalence_44 Source #

d_isDecStrictPartialOrder_1070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_IsDecStrictPartialOrder_336 Source #

du_isDecStrictPartialOrder_1070 ∷ T_StrictTotalOrder_1036 → T_IsDecStrictPartialOrder_336 Source #

d_isStrictPartialOrder_1072 ∷ T_StrictTotalOrder_1036 → T_IsStrictPartialOrder_290 Source #

d_strictPartialOrder_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_StrictPartialOrder_556 Source #

du_strictPartialOrder_1074 ∷ T_StrictTotalOrder_1036 → T_StrictPartialOrder_556 Source #

d__'62'__1078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d__'8814'__1080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d__'8815'__1082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d_'60''45'resp'45''8776'_1084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_1084 ∷ T_StrictTotalOrder_1036 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_1086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_1086 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_1088 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_1088 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_1090 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_irrefl_1092 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isEquivalence_1094 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_IsEquivalence_26 Source #

du_isEquivalence_1094 ∷ T_StrictTotalOrder_1036 → T_IsEquivalence_26 Source #

d_trans_1096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1096 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decStrictPartialOrder_1098 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_DecStrictPartialOrder_638 Source #

du_decStrictPartialOrder_1098 ∷ T_StrictTotalOrder_1036 → T_DecStrictPartialOrder_638 Source #

d__'8776'__1104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d__'8777'__1106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → () Source #

d__'8799'__1108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1108 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_1110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → () Source #

d_decSetoid_1112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_DecSetoid_84 Source #

du_decSetoid_1112 ∷ T_StrictTotalOrder_1036 → T_DecSetoid_84 Source #

d_isDecEquivalence_1114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_1114 ∷ T_StrictTotalOrder_1036 → T_IsDecEquivalence_44 Source #

d_isEquivalence_1116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_IsEquivalence_26 Source #

du_isEquivalence_1116 ∷ T_StrictTotalOrder_1036 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1118 ∷ T_StrictTotalOrder_1036 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_PartialSetoid_10 Source #

du_partialSetoid_1120 ∷ T_StrictTotalOrder_1036 → T_PartialSetoid_10 Source #

d_refl_1122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny Source #

du_refl_1122 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny Source #

d_reflexive_1124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1124 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Setoid_44 Source #

du_setoid_1126 ∷ T_StrictTotalOrder_1036 → T_Setoid_44 Source #

d_sym_1128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1128 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1130 ∷ T_StrictTotalOrder_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_decSetoid_1132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_DecSetoid_84 Source #

du_decSetoid_1132 ∷ T_StrictTotalOrder_1036 → T_DecSetoid_84 Source #

d_DenseLinearOrder_1140 ∷ p → p → p → () Source #

newtype T_DenseLinearOrder_1140 Source #

Constructors

C_DenseLinearOrder'46'constructor_23325 T_IsDenseLinearOrder_594

d_Carrier_1156 ∷ T_DenseLinearOrder_1140 → () Source #

d__'8776'__1158 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d__'60'__1160 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d_isDenseLinearOrder_1162 ∷ T_DenseLinearOrder_1140 → T_IsDenseLinearOrder_594 Source #

d_dense_1166 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isStrictTotalOrder_1168 ∷ T_DenseLinearOrder_1140 → T_IsStrictTotalOrder_534 Source #

d_strictTotalOrder_1170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_StrictTotalOrder_1036 Source #

du_strictTotalOrder_1170 ∷ T_DenseLinearOrder_1140 → T_StrictTotalOrder_1036 Source #

d__'60''63'__1174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'60''63'__1174 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'62'__1176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d__'8799'__1178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1178 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Dec_20 Source #

d__'8814'__1180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d__'8815'__1182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d_'60''45'resp'45''8776'_1184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_Σ_14 Source #

du_'60''45'resp'45''8776'_1184 ∷ T_DenseLinearOrder_1140 → T_Σ_14 Source #

d_'60''45'resp'691''45''8776'_1186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'691''45''8776'_1186 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'60''45'resp'737''45''8776'_1188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'60''45'resp'737''45''8776'_1188 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_asym_1190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_compare_1192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Tri_158 Source #

du_compare_1192 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_decSetoid_1194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_DecSetoid_84 Source #

du_decSetoid_1194 ∷ T_DenseLinearOrder_1140 → T_DecSetoid_84 Source #

d_decStrictPartialOrder_1196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_DecStrictPartialOrder_638 Source #

du_decStrictPartialOrder_1196 ∷ T_DenseLinearOrder_1140 → T_DecStrictPartialOrder_638 Source #

d_irrefl_1198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_isDecEquivalence_1200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_1200 ∷ T_DenseLinearOrder_1140 → T_IsDecEquivalence_44 Source #

d_isDecStrictPartialOrder_1202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsDecStrictPartialOrder_336 Source #

du_isDecStrictPartialOrder_1202 ∷ T_DenseLinearOrder_1140 → T_IsDecStrictPartialOrder_336 Source #

d_isEquivalence_1204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsEquivalence_26 Source #

du_isEquivalence_1204 ∷ T_DenseLinearOrder_1140 → T_IsEquivalence_26 Source #

d_isStrictPartialOrder_1206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsStrictPartialOrder_290 Source #

du_isStrictPartialOrder_1206 ∷ T_DenseLinearOrder_1140 → T_IsStrictPartialOrder_290 Source #

d_strictPartialOrder_1208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_StrictPartialOrder_556 Source #

du_strictPartialOrder_1208 ∷ T_DenseLinearOrder_1140 → T_StrictPartialOrder_556 Source #

d_trans_1210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1210 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d__'8777'__1216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → () Source #

d__'8799'__1218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Dec_20 Source #

du__'8799'__1218 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_Carrier_1220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → () Source #

d_decSetoid_1222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_DecSetoid_84 Source #

du_decSetoid_1222 ∷ T_DenseLinearOrder_1140 → T_DecSetoid_84 Source #

d_isDecEquivalence_1224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsDecEquivalence_44 Source #

du_isDecEquivalence_1224 ∷ T_DenseLinearOrder_1140 → T_IsDecEquivalence_44 Source #

d_isEquivalence_1226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsEquivalence_26 Source #

du_isEquivalence_1226 ∷ T_DenseLinearOrder_1140 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1228 ∷ T_DenseLinearOrder_1140 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_PartialSetoid_10 Source #

du_partialSetoid_1230 ∷ T_DenseLinearOrder_1140 → T_PartialSetoid_10 Source #

d_refl_1232 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny Source #

du_refl_1232 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny Source #

d_reflexive_1234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1234 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → T_Setoid_44 Source #

du_setoid_1236 ∷ T_DenseLinearOrder_1140 → T_Setoid_44 Source #

d_sym_1238 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1238 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1240 ∷ T_DenseLinearOrder_1140 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_ApartnessRelation_1248 ∷ p → p → p → () Source #

newtype T_ApartnessRelation_1248 Source #

Constructors

C_ApartnessRelation'46'constructor_25337 T_IsApartnessRelation_656

d_Carrier_1264 ∷ T_ApartnessRelation_1248 → () Source #

d__'8776'__1266 ∷ T_ApartnessRelation_1248 → AgdaAny → AgdaAny → () Source #

d__'35'__1268 ∷ T_ApartnessRelation_1248 → AgdaAny → AgdaAny → () Source #

d_isApartnessRelation_1270 ∷ T_ApartnessRelation_1248 → T_IsApartnessRelation_656 Source #

d__'172''35'__1274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_ApartnessRelation_1248 → AgdaAny → AgdaAny → () Source #

d_cotrans_1276 ∷ T_ApartnessRelation_1248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_irrefl_1278 ∷ T_ApartnessRelation_1248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_sym_1280 ∷ T_ApartnessRelation_1248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #