Documentation

d__'8776'__22 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> () #

d__'8818'__24 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> () #

d_x'8804'y'8658'x'8851'z'8804'y_98 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'y'8658'x'8851'z'8804'y_98 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'y'8658'z'8851'x'8804'y_100 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'y'8658'z'8851'x'8804'y_100 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'y'8851'z'8658'x'8804'y_102 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'y'8851'z'8658'x'8804'y_102 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'y'8851'z'8658'x'8804'z_104 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'y'8851'z'8658'x'8804'z_104 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8851'y'8776'x'8658'x'8804'y_106 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8851'y'8776'x'8658'x'8804'y_106 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8851'y'8776'y'8658'y'8804'x_108 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8851'y'8776'y'8658'y'8804'x_108 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8851'y'8804'x_110 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8851'y'8804'x_110 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8851'y'8804'y_112 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8851'y'8804'y_112 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'assoc_114 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'assoc_114 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'band_116 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Band_596 #

du_'8851''45'band_116 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Band_596 #

d_'8851''45'comm_118 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'comm_118 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'commutativeSemigroup_120 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_CommutativeSemigroup_662 #

du_'8851''45'commutativeSemigroup_120 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_CommutativeSemigroup_662 #

d_'8851''45'cong_122 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'cong_122 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'cong'691'_124 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'cong'691'_124 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'cong'737'_126 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'cong'737'_126 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'glb_128 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'glb_128 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'idem_130 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny #

du_'8851''45'idem_130 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny #

d_'8851''45'identity_132 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14 #

du_'8851''45'identity_132 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14 #

d_'8851''45'identity'691'_134 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8851''45'identity'691'_134 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8851''45'identity'737'_136 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8851''45'identity'737'_136 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8851''45'isBand_138 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsBand_508 #

du_'8851''45'isBand_138 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsBand_508 #

d_'8851''45'isCommutativeSemigroup_140 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsCommutativeSemigroup_548 #

du_'8851''45'isCommutativeSemigroup_140 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsCommutativeSemigroup_548 #

d_'8851''45'isMagma_142 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsMagma_176 #

du_'8851''45'isMagma_142 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsMagma_176 #

d_'8851''45'isMonoid_144 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsMonoid_686 #

du_'8851''45'isMonoid_144 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsMonoid_686 #

d_'8851''45'isSelectiveMagma_146 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSelectiveMagma_436 #

du_'8851''45'isSelectiveMagma_146 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSelectiveMagma_436 #

d_'8851''45'isSemigroup_148 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSemigroup_472 #

du_'8851''45'isSemigroup_148 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSemigroup_472 #

d_'8851''45'magma_150 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Magma_68 #

du_'8851''45'magma_150 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Magma_68 #

d_'8851''45'mono'45''8804'_152 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'mono'45''8804'_152 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'monoid_154 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Monoid_882 #

du_'8851''45'monoid_154 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Monoid_882 #

d_'8851''45'mono'691''45''8804'_156 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'mono'691''45''8804'_156 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'mono'737''45''8804'_158 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'mono'737''45''8804'_158 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'sel_162 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> T__'8846'__30 #

du_'8851''45'sel_162 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> T__'8846'__30 #

d_'8851''45'selectiveMagma_164 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_SelectiveMagma_122 #

du_'8851''45'selectiveMagma_164 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_SelectiveMagma_122 #

d_'8851''45'semigroup_166 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semigroup_536 #

du_'8851''45'semigroup_166 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semigroup_536 #

d_'8851''45'triangulate_168 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8851''45'triangulate_168 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'zero_170 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14 #

du_'8851''45'zero_170 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14 #

d_'8851''45'zero'691'_172 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8851''45'zero'691'_172 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8851''45'zero'737'_174 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8851''45'zero'737'_174 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_mono'45''8804''45'distrib'45''8852'_182 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MaxOperator_128 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

du_mono'45''8804''45'distrib'45''8852'_182 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #