Documentation

d_Commutative_44 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Idempotent_52 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Selective_100 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_IsBand_108 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsMagma_134 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsSemigroup_148 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsSemilattice_1598 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d__'8804'__2002 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_reflexive_2008 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_reflexive_2008 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_2070 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

du_refl_2070 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_antisym_2078 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_antisym_2078 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_total_2132 :: T_Level_14 -> T_Level_14 -> () -> (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_2132 :: (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_2178 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_2178 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_resp'691'_2246 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_resp'691'_2246 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_resp'737'_2310 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_resp'737'_2310 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_resp'8322'_2374 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> T_Σ_14 Source #

du_resp'8322'_2374 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> T_Σ_14 Source #

d_dec_2378 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du_dec_2378 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_x'8729'y'8804'x_2454 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8729'y'8804'x_2454 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8729'y'8804'y_2464 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8729'y'8804'y_2464 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'pres'691''45''8804'_2476 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'pres'691''45''8804'_2476 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_2488 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_infimum_2488 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isPreorder_2494 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_IsPreorder_70 Source #

du_isPreorder_2494 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_IsPreorder_70 Source #

d_isPartialOrder_2528 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_IsPartialOrder_162 Source #

du_isPartialOrder_2528 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_IsPartialOrder_162 Source #

d_isDecPartialOrder_2570 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecPartialOrder_206 Source #

du_isDecPartialOrder_2570 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecPartialOrder_206 Source #

d_isTotalOrder_2576 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_380 Source #

du_isTotalOrder_2576 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_380 Source #

d_isDecTotalOrder_2620 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecTotalOrder_430 Source #

du_isDecTotalOrder_2620 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecTotalOrder_430 Source #

d_preorder_2628 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_Preorder_132 Source #

du_preorder_2628 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_Preorder_132 Source #

d_poset_2632 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_Poset_282 Source #

du_poset_2632 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_Poset_282 Source #

d_decPoset_2636 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecPoset_360 Source #

du_decPoset_2636 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecPoset_360 Source #

d_totalOrder_2642 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_TotalOrder_648 Source #

du_totalOrder_2642 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_TotalOrder_648 Source #

d_decTotalOrder_2648 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecTotalOrder_736 Source #

du_decTotalOrder_2648 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecTotalOrder_736 Source #