| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Composition
Documentation
d__'894'__32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d_reflexive_58 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
d_respects_68 ∷ 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 → AgdaAny → T_Σ_14 → AgdaAny → AgdaAny Source #
du_respects_68 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → AgdaAny Source #
d_respects'737'_102 ∷ 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 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_respects'737'_102 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_respects'691'_136 ∷ 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 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_respects'691'_136 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_respects'8322'_168 ∷ T_Level_18 → () → 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 Source #
du_respects'8322'_168 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_implies'737'_194 ∷ T_Level_18 → () → 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 → T_Σ_14 Source #
du_implies'737'_194 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #
d_implies'691'_226 ∷ T_Level_18 → () → 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 → T_Σ_14 Source #
du_implies'691'_226 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #
d_transitive_254 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_transitive_254 ∷ (AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_isPreorder_286 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #
du_isPreorder_286 ∷ (AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14) → T_IsPreorder_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #