Documentation

d_Commutative_44 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Idempotent_52 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Selective_88 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsBand_96 ∷ p → p → p → p → p → p → () Source #

d_IsMagma_124 ∷ p → p → p → p → p → p → () Source #

d_IsSemigroup_134 ∷ p → p → p → p → p → p → () Source #

d_IsSemilattice_136 ∷ p → p → p → p → p → p → () Source #

d__'8804'__1516 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_reflexive_1522 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_1522 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_1584 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_refl_1584 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_antisym_1592 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_1592 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_total_1646 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #

du_total_1646 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #

d_trans_1692 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1692 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_resp'691'_1760 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_resp'691'_1760 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_resp'737'_1824 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_resp'737'_1824 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_resp'8322'_1888 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → T_Σ_14 Source #

du_resp'8322'_1888 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 → T_Σ_14 Source #

d_dec_1892 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #

du_dec_1892 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #

d_x'8729'y'8804'x_1968 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8729'y'8804'x_1968 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8729'y'8804'y_1978 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8729'y'8804'y_1978 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'pres'691''45''8804'_1990 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'pres'691''45''8804'_1990 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_2002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_2002 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isPreorder_2008 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_IsPreorder_70 Source #

du_isPreorder_2008 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_IsPreorder_70 Source #

d_isPartialOrder_2042 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_IsPartialOrder_162 Source #

du_isPartialOrder_2042 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_IsPartialOrder_162 Source #

d_isDecPartialOrder_2084 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T_Dec_32) → T_IsDecPartialOrder_206 Source #

du_isDecPartialOrder_2084 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T_Dec_32) → T_IsDecPartialOrder_206 Source #

d_isTotalOrder_2090 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → T_IsTotalOrder_384 Source #

du_isTotalOrder_2090 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → T_IsTotalOrder_384 Source #

d_isDecTotalOrder_2134 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_32) → T_IsDecTotalOrder_434 Source #

du_isDecTotalOrder_2134 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_32) → T_IsDecTotalOrder_434 Source #

d_preorder_2142 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_Preorder_132 Source #

du_preorder_2142 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 → T_Preorder_132 Source #

d_poset_2146 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_Poset_282 Source #

du_poset_2146 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → T_Poset_282 Source #

d_decPoset_2150 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T_Dec_32) → T_DecPoset_360 Source #

du_decPoset_2150 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T_Dec_32) → T_DecPoset_360 Source #

d_totalOrder_2156 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → T_TotalOrder_652 Source #

du_totalOrder_2156 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → T_TotalOrder_652 Source #

d_decTotalOrder_2162 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_32) → T_DecTotalOrder_740 Source #

du_decTotalOrder_2162 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_32) → T_DecTotalOrder_740 Source #