Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise

Documentation

d_Pointwise_34 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_Pointwise_34 Source #

Constructors

C_inj'8321'_64 AgdaAny
C_inj'8322'_70 AgdaAny

d_drop'45'inj'8321'_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Pointwise_34 → AgdaAny Source #

du_drop'45'inj'8321'_96 ∷ T_Pointwise_34 → AgdaAny Source #

d_drop'45'inj'8322'_104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Pointwise_34 → AgdaAny Source #

du_drop'45'inj'8322'_104 ∷ T_Pointwise_34 → AgdaAny Source #

d_'8846''45'refl_108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_34 Source #

du_'8846''45'refl_108 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_34 Source #

d_'8846''45'symmetric_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 Source #

du_'8846''45'symmetric_122 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 Source #

d_'8846''45'transitive_136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_Pointwise_34 Source #

du_'8846''45'transitive_136 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_Pointwise_34 Source #

d_'8846''45'asymmetric_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_'8869'_4 Source #

d_'46'extendedlambda0_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_34 → T_'8869'_4 Source #

d_'46'extendedlambda1_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_34 → T_'8869'_4 Source #

d_'8846''45'substitutive_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (T__'8846'__30 → ()) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → AgdaAny → AgdaAny Source #

du_'8846''45'substitutive_178 ∷ ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (T__'8846'__30 → ()) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → AgdaAny → AgdaAny Source #

d_'8846''45'decidable_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → T__'8846'__30 → T__'8846'__30 → T_Dec_32 Source #

du_'8846''45'decidable_196 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → T__'8846'__30 → T__'8846'__30 → T_Dec_32 Source #

d_'8846''45'reflexive_258 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 Source #

du_'8846''45'reflexive_258 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 Source #

d_'8846''45'irreflexive_272 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_'8869'_4 Source #

d_'8846''45'antisymmetric_290 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_Pointwise_34 Source #

du_'8846''45'antisymmetric_290 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_Pointwise_34 Source #

du_'8846''45'respects'737'_308 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_Pointwise_34 Source #

du_'8846''45'respects'691'_326 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T_Pointwise_34 → T_Pointwise_34 Source #

d_'8846''45'respects'8322'_344 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #

du_'8846''45'respects'8322'_344 ∷ T_Σ_14 → T_Σ_14 → T_Σ_14 Source #

d_'8846''45'isEquivalence_374 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 → T_IsEquivalence_26 Source #

du_'8846''45'isEquivalence_374 ∷ T_IsEquivalence_26 → T_IsEquivalence_26 → T_IsEquivalence_26 Source #

d_'8846''45'isDecEquivalence_384 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #

du_'8846''45'isDecEquivalence_384 ∷ T_IsDecEquivalence_44 → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #

d_'8846''45'isPreorder_422 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #

du_'8846''45'isPreorder_422 ∷ T_IsPreorder_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #

d_'8846''45'isPartialOrder_432 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #

du_'8846''45'isPartialOrder_432 ∷ T_IsPartialOrder_162 → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #

d_'8846''45'isStrictPartialOrder_442 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #

du_'8846''45'isStrictPartialOrder_442 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #

d_'8846''45'setoid_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #

du_'8846''45'setoid_464 ∷ T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #

d_'8846''45'decSetoid_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_DecSetoid_84 → T_DecSetoid_84 Source #

du_'8846''45'decSetoid_474 ∷ T_DecSetoid_84 → T_DecSetoid_84 → T_DecSetoid_84 Source #

d__'8846''8347'__484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #

du__'8846''8347'__484 ∷ T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #

d_'8846''45'preorder_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Preorder_132 → T_Preorder_132 Source #

du_'8846''45'preorder_502 ∷ T_Preorder_132 → T_Preorder_132 → T_Preorder_132 Source #

d_'8846''45'poset_512 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_Poset_282 → T_Poset_282 Source #

du_'8846''45'poset_512 ∷ T_Poset_282 → T_Poset_282 → T_Poset_282 Source #

d_Pointwise'45''8801''8658''8801'_534 ∷ T_Level_18 → T_Level_18 → () → () → T__'8846'__30 → T__'8846'__30 → T_Pointwise_34 → T__'8801'__12 Source #

d_'8801''8658'Pointwise'45''8801'_540 ∷ T_Level_18 → T_Level_18 → () → () → T__'8846'__30 → T__'8846'__30 → T__'8801'__12 → T_Pointwise_34 Source #

du_'8801''8658'Pointwise'45''8801'_540 ∷ T__'8846'__30 → T_Pointwise_34 Source #

d_Pointwise'45''8801''8596''8801'_550 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 Source #

du_Pointwise'45''8801''8596''8801'_550 ∷ T_Inverse_58 Source #

d_'8321''8764''8321'_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_34 Source #

du_'8321''8764''8321'_588 ∷ AgdaAny → T_Pointwise_34 Source #

d_'8322''8764''8322'_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_34 Source #

du_'8322''8764''8322'_594 ∷ AgdaAny → T_Pointwise_34 Source #

d__'8846''45''8799'__604 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → T__'8846'__30 → T__'8846'__30 → T_Dec_32 Source #

du__'8846''45''8799'__604 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → T__'8846'__30 → T__'8846'__30 → T_Dec_32 Source #