Safe Haskell	None

MAlonzo.Code.Relation.Binary.Lattice.Structures

Documentation

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

data T_IsJoinSemilattice_22 Source #

Constructors

C_IsJoinSemilattice'46'constructor_329 T_IsPartialOrder_162 (AgdaAny -> AgdaAny -> T_Σ_14)

d_isPartialOrder_30 :: T_IsJoinSemilattice_22 -> T_IsPartialOrder_162 Source #

d_supremum_32 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_x'8804'x'8744'y_38 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_38 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_50 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_50 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_64 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_64 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_76 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_78 :: T_IsJoinSemilattice_22 -> T_IsEquivalence_26 Source #

d_isPreorder_80 :: T_IsJoinSemilattice_22 -> T_IsPreorder_70 Source #

d_refl_82 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny Source #

du_refl_82 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny Source #

d_reflexive_84 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_86 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_88 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_88 :: T_IsJoinSemilattice_22 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_90 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_90 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_92 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_92 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_96 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_96 :: T_IsJoinSemilattice_22 -> T_IsPartialEquivalence_16 Source #

d_refl_98 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny Source #

d_reflexive_100 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_100 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_102 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_104 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBoundedJoinSemilattice_110 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsBoundedJoinSemilattice_110 Source #

Constructors

C_IsBoundedJoinSemilattice'46'constructor_4051 T_IsJoinSemilattice_22 (AgdaAny -> AgdaAny)

d_isJoinSemilattice_120 :: T_IsBoundedJoinSemilattice_110 -> T_IsJoinSemilattice_22 Source #

d_minimum_122 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny Source #

d_antisym_126 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_128 :: T_IsBoundedJoinSemilattice_110 -> T_IsEquivalence_26 Source #

d_isPartialOrder_130 :: T_IsBoundedJoinSemilattice_110 -> T_IsPartialOrder_162 Source #

d_isPreorder_132 :: T_IsBoundedJoinSemilattice_110 -> T_IsPreorder_70 Source #

d_refl_134 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny Source #

du_refl_134 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny Source #

d_reflexive_136 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_138 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_140 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_142 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_144 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_144 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_146 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_146 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_148 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_148 :: T_IsBoundedJoinSemilattice_110 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_150 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_150 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_152 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_152 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_156 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_156 :: T_IsBoundedJoinSemilattice_110 -> T_IsPartialEquivalence_16 Source #

d_refl_158 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny Source #

d_reflexive_160 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_160 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_162 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_164 :: T_IsBoundedJoinSemilattice_110 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

data T_IsMeetSemilattice_168 Source #

Constructors

C_IsMeetSemilattice'46'constructor_6037 T_IsPartialOrder_162 (AgdaAny -> AgdaAny -> T_Σ_14)

d_isPartialOrder_176 :: T_IsMeetSemilattice_168 -> T_IsPartialOrder_162 Source #

d_infimum_178 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_x'8743'y'8804'x_184 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_184 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_196 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_196 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_210 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_210 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_222 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_224 :: T_IsMeetSemilattice_168 -> T_IsEquivalence_26 Source #

d_isPreorder_226 :: T_IsMeetSemilattice_168 -> T_IsPreorder_70 Source #

d_refl_228 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny Source #

du_refl_228 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny Source #

d_reflexive_230 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_232 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_234 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_234 :: T_IsMeetSemilattice_168 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_236 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_236 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_238 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_238 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_242 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_242 :: T_IsMeetSemilattice_168 -> T_IsPartialEquivalence_16 Source #

d_refl_244 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny Source #

d_reflexive_246 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_246 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_248 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_250 :: T_IsMeetSemilattice_168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBoundedMeetSemilattice_256 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsBoundedMeetSemilattice_256 Source #

Constructors

C_IsBoundedMeetSemilattice'46'constructor_9759 T_IsMeetSemilattice_168 (AgdaAny -> AgdaAny)

d_isMeetSemilattice_266 :: T_IsBoundedMeetSemilattice_256 -> T_IsMeetSemilattice_168 Source #

d_maximum_268 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny Source #

d_antisym_272 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_274 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_276 :: T_IsBoundedMeetSemilattice_256 -> T_IsEquivalence_26 Source #

d_isPartialOrder_278 :: T_IsBoundedMeetSemilattice_256 -> T_IsPartialOrder_162 Source #

d_isPreorder_280 :: T_IsBoundedMeetSemilattice_256 -> T_IsPreorder_70 Source #

d_refl_282 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny Source #

du_refl_282 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny Source #

d_reflexive_284 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_286 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_288 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_288 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_290 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_290 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_292 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_292 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_294 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_294 :: T_IsBoundedMeetSemilattice_256 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_296 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_296 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_298 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_302 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_302 :: T_IsBoundedMeetSemilattice_256 -> T_IsPartialEquivalence_16 Source #

d_refl_304 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny Source #

d_reflexive_306 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_306 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_308 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_310 :: T_IsBoundedMeetSemilattice_256 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsLattice_316 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsLattice_316 Source #

Constructors

C_IsLattice'46'constructor_11935 T_IsPartialOrder_162 (AgdaAny -> AgdaAny -> T_Σ_14) (AgdaAny -> AgdaAny -> T_Σ_14)

d_isPartialOrder_328 :: T_IsLattice_316 -> T_IsPartialOrder_162 Source #

d_supremum_330 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_infimum_332 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isJoinSemilattice_334 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_334 :: T_IsLattice_316 -> T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_336 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_336 :: T_IsLattice_316 -> T_IsMeetSemilattice_168 Source #

d_x'8804'x'8744'y_340 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_340 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_342 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_342 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_344 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_344 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_348 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_348 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_350 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_350 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_352 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_352 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_356 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_358 :: T_IsLattice_316 -> T_IsEquivalence_26 Source #

d_isPreorder_360 :: T_IsLattice_316 -> T_IsPreorder_70 Source #

d_refl_362 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny Source #

du_refl_362 :: T_IsLattice_316 -> AgdaAny -> AgdaAny Source #

d_reflexive_364 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_366 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_368 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_368 :: T_IsLattice_316 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_370 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_370 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_372 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_372 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_376 :: T_IsLattice_316 -> T_IsPartialEquivalence_16 Source #

d_refl_378 :: T_IsLattice_316 -> AgdaAny -> AgdaAny Source #

d_reflexive_380 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_316 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_380 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_382 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_384 :: T_IsLattice_316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsDistributiveLattice_390 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsDistributiveLattice_390 Source #

Constructors

C_IsDistributiveLattice'46'constructor_14667 T_IsLattice_316 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isLattice_400 :: T_IsDistributiveLattice_390 -> T_IsLattice_316 Source #

d_'8743''45'distrib'737''45''8744'_402 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_406 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_408 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_410 :: T_IsDistributiveLattice_390 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_412 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_412 :: T_IsDistributiveLattice_390 -> T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_414 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_414 :: T_IsDistributiveLattice_390 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_416 :: T_IsDistributiveLattice_390 -> T_IsPartialOrder_162 Source #

d_isPreorder_418 :: T_IsDistributiveLattice_390 -> T_IsPreorder_70 Source #

d_refl_420 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny Source #

du_refl_420 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny Source #

d_reflexive_422 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_424 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_426 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_428 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_428 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_430 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_430 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_432 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_434 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_434 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_436 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_436 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_438 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_438 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_440 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_440 :: T_IsDistributiveLattice_390 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_442 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_442 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_444 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_444 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_448 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_448 :: T_IsDistributiveLattice_390 -> T_IsPartialEquivalence_16 Source #

d_refl_450 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny Source #

d_reflexive_452 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_452 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_454 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_456 :: T_IsDistributiveLattice_390 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBoundedLattice_466 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> () Source #

data T_IsBoundedLattice_466 Source #

Constructors

C_IsBoundedLattice'46'constructor_17269 T_IsLattice_316 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_isLattice_482 :: T_IsBoundedLattice_466 -> T_IsLattice_316 Source #

d_maximum_484 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny Source #

d_minimum_486 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny Source #

d_antisym_490 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_492 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_494 :: T_IsBoundedLattice_466 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_496 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_496 :: T_IsBoundedLattice_466 -> T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_498 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_498 :: T_IsBoundedLattice_466 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_500 :: T_IsBoundedLattice_466 -> T_IsPartialOrder_162 Source #

d_isPreorder_502 :: T_IsBoundedLattice_466 -> T_IsPreorder_70 Source #

d_refl_504 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny Source #

du_refl_504 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny Source #

d_reflexive_506 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_508 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_510 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_512 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_512 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_514 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_514 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_516 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_516 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_518 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_518 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_520 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_520 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_522 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_522 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_524 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_524 :: T_IsBoundedLattice_466 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_526 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_526 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_528 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_528 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_532 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_532 :: T_IsBoundedLattice_466 -> T_IsPartialEquivalence_16 Source #

d_refl_534 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny Source #

d_reflexive_536 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_536 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_538 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_540 :: T_IsBoundedLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isBoundedJoinSemilattice_542 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> T_IsBoundedJoinSemilattice_110 Source #

du_isBoundedJoinSemilattice_542 :: T_IsBoundedLattice_466 -> T_IsBoundedJoinSemilattice_110 Source #

d_isBoundedMeetSemilattice_544 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBoundedLattice_466 -> T_IsBoundedMeetSemilattice_256 Source #

du_isBoundedMeetSemilattice_544 :: T_IsBoundedLattice_466 -> T_IsBoundedMeetSemilattice_256 Source #

d_IsHeytingAlgebra_556 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> () Source #

data T_IsHeytingAlgebra_556 Source #

Constructors

C_IsHeytingAlgebra'46'constructor_20703 T_IsBoundedLattice_466 (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)

d_isBoundedLattice_572 :: T_IsHeytingAlgebra_556 -> T_IsBoundedLattice_466 Source #

d_exponential_574 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_transpose'45''8680'_582 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8680'_582 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_transpose'45''8743'_598 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8743'_598 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_610 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_612 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isBoundedJoinSemilattice_614 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> T_IsBoundedJoinSemilattice_110 Source #

du_isBoundedJoinSemilattice_614 :: T_IsHeytingAlgebra_556 -> T_IsBoundedJoinSemilattice_110 Source #

d_isBoundedMeetSemilattice_616 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> T_IsBoundedMeetSemilattice_256 Source #

du_isBoundedMeetSemilattice_616 :: T_IsHeytingAlgebra_556 -> T_IsBoundedMeetSemilattice_256 Source #

d_isEquivalence_618 :: T_IsHeytingAlgebra_556 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_620 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_620 :: T_IsHeytingAlgebra_556 -> T_IsJoinSemilattice_22 Source #

d_isLattice_622 :: T_IsHeytingAlgebra_556 -> T_IsLattice_316 Source #

d_isMeetSemilattice_624 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_624 :: T_IsHeytingAlgebra_556 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_626 :: T_IsHeytingAlgebra_556 -> T_IsPartialOrder_162 Source #

d_isPreorder_628 :: T_IsHeytingAlgebra_556 -> T_IsPreorder_70 Source #

d_maximum_630 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny Source #

d_minimum_632 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny Source #

d_refl_634 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny Source #

du_refl_634 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny Source #

d_reflexive_636 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_638 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_640 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_642 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_642 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_644 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_644 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_646 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_646 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_648 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_648 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_650 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_650 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_652 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_652 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_654 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_654 :: T_IsHeytingAlgebra_556 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_656 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_656 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_658 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_658 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_662 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_662 :: T_IsHeytingAlgebra_556 -> T_IsPartialEquivalence_16 Source #

d_refl_664 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny Source #

d_reflexive_666 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_666 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_668 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_670 :: T_IsHeytingAlgebra_556 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBooleanAlgebra_682 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> () Source #

newtype T_IsBooleanAlgebra_682 Source #

Constructors

C_IsBooleanAlgebra'46'constructor_25999 T_IsHeytingAlgebra_556

d__'8680'__702 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'8680'__702 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isHeytingAlgebra_708 :: T_IsBooleanAlgebra_682 -> T_IsHeytingAlgebra_556 Source #

d_antisym_712 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_exponential_714 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_infimum_716 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isBoundedJoinSemilattice_718 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> T_IsBoundedJoinSemilattice_110 Source #

du_isBoundedJoinSemilattice_718 :: T_IsBooleanAlgebra_682 -> T_IsBoundedJoinSemilattice_110 Source #

d_isBoundedLattice_720 :: T_IsBooleanAlgebra_682 -> T_IsBoundedLattice_466 Source #

d_isBoundedMeetSemilattice_722 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> T_IsBoundedMeetSemilattice_256 Source #

du_isBoundedMeetSemilattice_722 :: T_IsBooleanAlgebra_682 -> T_IsBoundedMeetSemilattice_256 Source #

d_isEquivalence_724 :: T_IsBooleanAlgebra_682 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_726 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_726 :: T_IsBooleanAlgebra_682 -> T_IsJoinSemilattice_22 Source #

d_isLattice_728 :: T_IsBooleanAlgebra_682 -> T_IsLattice_316 Source #

d_isMeetSemilattice_730 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_730 :: T_IsBooleanAlgebra_682 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_732 :: T_IsBooleanAlgebra_682 -> T_IsPartialOrder_162 Source #

d_isPreorder_734 :: T_IsBooleanAlgebra_682 -> T_IsPreorder_70 Source #

d_maximum_736 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny Source #

d_minimum_738 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny Source #

d_refl_740 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny Source #

du_refl_740 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny Source #

d_reflexive_742 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_744 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_746 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_transpose'45''8680'_748 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8680'_748 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_transpose'45''8743'_750 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8743'_750 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_752 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_752 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_754 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_754 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_756 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_756 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_758 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_758 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_760 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_760 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_762 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_762 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_764 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_764 :: T_IsBooleanAlgebra_682 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_766 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_766 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_768 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_768 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_772 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_772 :: T_IsBooleanAlgebra_682 -> T_IsPartialEquivalence_16 Source #

d_refl_774 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny Source #

d_reflexive_776 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_776 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_778 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_780 :: T_IsBooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #