Documentation

d_poset_14 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Poset_282 Source #

du_poset_14 :: T_Lattice_532 -> T_Poset_282 Source #

d_'8743''45'idem_16 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny Source #

du_'8743''45'idem_16 :: T_Lattice_532 -> AgdaAny -> AgdaAny Source #

d_'8743''45'isBand_18 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsBand_242 Source #

du_'8743''45'isBand_18 :: T_Lattice_532 -> T_IsBand_242 Source #

d_'8743''45'isMagma_20 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsMagma_98 Source #

du_'8743''45'isMagma_20 :: T_Lattice_532 -> T_IsMagma_98 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_22 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_22 :: T_Lattice_532 -> T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_24 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsMeetSemilattice_168 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_24 :: T_Lattice_532 -> T_IsMeetSemilattice_168 Source #

d_'8743''45'isSemigroup_26 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsSemigroup_206 Source #

du_'8743''45'isSemigroup_26 :: T_Lattice_532 -> T_IsSemigroup_206 Source #

d_'8743''45'isSemilattice_28 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsSemilattice_1576 Source #

du_'8743''45'isSemilattice_28 :: T_Lattice_532 -> T_IsSemilattice_1576 Source #

d_'8743''45'orderTheoreticJoinSemilattice_30 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_30 :: T_Lattice_532 -> T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_32 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_MeetSemilattice_188 Source #

du_'8743''45'orderTheoreticMeetSemilattice_32 :: T_Lattice_532 -> T_MeetSemilattice_188 Source #

d_'8743''45'semilattice_34 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Semilattice_10 Source #

du_'8743''45'semilattice_34 :: T_Lattice_532 -> T_Semilattice_10 Source #

d_'8743''45''8744''45'isLattice_36 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsLattice_1876 Source #

du_'8743''45''8744''45'isLattice_36 :: T_Lattice_532 -> T_IsLattice_1876 Source #

d_'8743''45''8744''45'lattice_38 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Lattice_532 Source #

du_'8743''45''8744''45'lattice_38 :: T_Lattice_532 -> T_Lattice_532 Source #

d_'8744''45'idem_40 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny Source #

du_'8744''45'idem_40 :: T_Lattice_532 -> AgdaAny -> AgdaAny Source #

d_'8744''45'isBand_42 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsBand_242 Source #

du_'8744''45'isBand_42 :: T_Lattice_532 -> T_IsBand_242 Source #

d_'8744''45'isMagma_44 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsMagma_98 Source #

du_'8744''45'isMagma_44 :: T_Lattice_532 -> T_IsMagma_98 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_46 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_46 :: T_Lattice_532 -> T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_48 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsMeetSemilattice_168 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_48 :: T_Lattice_532 -> T_IsMeetSemilattice_168 Source #

d_'8744''45'isSemigroup_50 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsSemigroup_206 Source #

du_'8744''45'isSemigroup_50 :: T_Lattice_532 -> T_IsSemigroup_206 Source #

d_'8744''45'isSemilattice_52 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsSemilattice_1576 Source #

du_'8744''45'isSemilattice_52 :: T_Lattice_532 -> T_IsSemilattice_1576 Source #

d_'8743''45'orderTheoreticJoinSemilattice_54 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_54 :: T_Lattice_532 -> T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_56 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_MeetSemilattice_188 Source #

du_'8743''45'orderTheoreticMeetSemilattice_56 :: T_Lattice_532 -> T_MeetSemilattice_188 Source #

d_'8744''45'semilattice_58 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Semilattice_10 Source #

du_'8744''45'semilattice_58 :: T_Lattice_532 -> T_Semilattice_10 Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_60 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsLattice_316 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_60 :: T_Lattice_532 -> T_IsLattice_316 Source #

d_'8744''45''8743''45'orderTheoreticLattice_62 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Lattice_362 Source #

du_'8744''45''8743''45'orderTheoreticLattice_62 :: T_Lattice_532 -> T_Lattice_362 Source #

d_'8743''45'idempotent_124 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny Source #

du_'8743''45'idempotent_124 :: T_Lattice_532 -> AgdaAny -> AgdaAny Source #

d_'8744''45'idempotent_126 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny Source #

du_'8744''45'idempotent_126 :: T_Lattice_532 -> AgdaAny -> AgdaAny Source #

d_isOrderTheoreticLattice_128 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsLattice_316 Source #

du_isOrderTheoreticLattice_128 :: T_Lattice_532 -> T_IsLattice_316 Source #

d_orderTheoreticLattice_130 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Lattice_362 Source #

du_orderTheoreticLattice_130 :: T_Lattice_532 -> T_Lattice_362 Source #

d_replace'45'equality_138 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Equivalence_16) -> T_Lattice_532 Source #

du_replace'45'equality_138 :: T_Lattice_532 -> (AgdaAny -> AgdaAny -> T_Equivalence_16) -> T_Lattice_532 Source #