| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent
Documentation
d_Pointwise_28 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → () Source #
d_'215''45'reflexive_42 ∷ 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_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'reflexive_42 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'refl_56 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_'215''45'irreflexive'8321'_70 ∷ 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_'8869'_4) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_'8869'_4 Source #
d_'215''45'irreflexive'8322'_86 ∷ 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_'8869'_4) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_'8869'_4 Source #
d_'215''45'symmetric_98 ∷ 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_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'symmetric_98 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'transitive_112 ∷ 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_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'transitive_112 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'antisymmetric_130 ∷ 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 → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'antisymmetric_130 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'asymmetric'8321'_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_'8869'_4 Source #
d_'215''45'asymmetric'8322'_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_'8869'_4 Source #
d_'215''45'respects'8322'_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d__'8764'__194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → () Source #
d__'8776'__196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → () Source #
d_resp'185'_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_resp'178'_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'total_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T__'8846'__30) → T_Σ_14 → T_Σ_14 → T__'8846'__30 Source #
du_'215''45'total_222 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T__'8846'__30) → T_Σ_14 → T_Σ_14 → T__'8846'__30 Source #
d_'215''45'decidable_318 ∷ 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_Σ_14 → T_Σ_14 → T_Dec_32 Source #
du_'215''45'decidable_318 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → T_Σ_14 → T_Σ_14 → T_Dec_32 Source #
d_'215''45'isEquivalence_336 ∷ 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_'215''45'isEquivalence_336 ∷ T_IsEquivalence_26 → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_'215''45'isDecEquivalence_354 ∷ 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_'215''45'isDecEquivalence_354 ∷ T_IsDecEquivalence_44 → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
d_'215''45'isPreorder_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_'215''45'isPartialOrder_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
du_'215''45'isPartialOrder_394 ∷ T_IsPartialOrder_162 → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d_'215''45'isStrictPartialOrder_416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_'215''45'isStrictPartialOrder_416 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_'215''45'preorder_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Preorder_132 → T_Preorder_132 Source #
d_'215''45'setoid_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #
d_'215''45'decSetoid_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_DecSetoid_84 → T_DecSetoid_84 Source #
d_'215''45'poset_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_Poset_282 → T_Poset_282 Source #
d_'215''45'strictPartialOrder_484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 Source #
du_'215''45'strictPartialOrder_484 ∷ T_StrictPartialOrder_472 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 Source #
d__'215''8347'__494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #
d_'8801''215''8801''8658''8801'_508 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #
d_'8801''8658''8801''215''8801'_510 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #
d_Pointwise'45''8801''8596''8801'_512 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 Source #
d__'215''45'Rel__518 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → () Source #
d_Rel'8596''8801'_520 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 Source #
d__'215''45'reflexive__522 ∷ 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_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d__'215''45'refl__524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d__'215''45'symmetric__526 ∷ 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_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d__'215''45'transitive__528 ∷ 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_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d__'215''45'antisymmetric__530 ∷ 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 → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d__'215''45''8776''45'respects'8322'__532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d__'215''45'decidable__534 ∷ 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_Σ_14 → T_Σ_14 → T_Dec_32 Source #
d__'215''45'isEquivalence__536 ∷ 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 #
d__'215''45'isDecEquivalence__538 ∷ 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 #
d__'215''45'isPreorder__540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #
d__'215''45'isPartialOrder__542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d__'215''45'isStrictPartialOrder__544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d__'215''45'preorder__546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Preorder_132 → T_Preorder_132 Source #
d__'215''45'setoid__548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #
d__'215''45'decSetoid__550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_DecSetoid_84 → T_DecSetoid_84 Source #
d__'215''45'poset__552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_282 → T_Poset_282 → T_Poset_282 Source #
d__'215''45'strictPartialOrder__554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 Source #