Documentation

d_Idempotent_106 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_IsBand_162 :: p1 -> p2 -> p3 -> p4 -> () Source #

d_IsMagma_188 :: p1 -> p2 -> p3 -> p4 -> () Source #

d_IsSemigroup_202 :: p1 -> p2 -> p3 -> p4 -> () Source #

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

d_IsSemilattice_1652 :: p1 -> p2 -> p3 -> p4 -> () Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

du_poset_2134 :: T_Lattice_532 -> T_Poset_282 Source #

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

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

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

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

d_sound_2166 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sound_2166 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_complete_2178 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_complete_2178 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_2186 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_supremum_2186 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

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

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