plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Relation.Binary.Lattice.Bundles

Documentation

d_JoinSemilattice_14 :: p -> p -> p -> () #

data T_JoinSemilattice_14 #

Constructors

C_JoinSemilattice'46'constructor_371 (AgdaAny -> AgdaAny -> AgdaAny) T_IsJoinSemilattice_22 

d_Carrier_32 :: T_JoinSemilattice_14 -> () #

d__'8776'__34 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> () #

d__'8804'__36 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> () #

d__'8744'__38 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isJoinSemilattice_40 :: T_JoinSemilattice_14 -> T_IsJoinSemilattice_22 #

d_antisym_44 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_46 :: T_JoinSemilattice_14 -> T_IsEquivalence_26 #

d_isPartialOrder_48 :: T_JoinSemilattice_14 -> T_IsPartialOrder_174 #

d_isPreorder_50 :: T_JoinSemilattice_14 -> T_IsPreorder_70 #

d_refl_52 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny #

du_refl_52 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny #

d_reflexive_54 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_56 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_58 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_60 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_60 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_62 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_62 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_64 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_64 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_66 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_66 :: T_JoinSemilattice_14 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_68 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_68 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_70 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_70 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_72 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_72 :: T_JoinSemilattice_14 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_74 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_74 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_76 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_76 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_80 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_80 :: T_JoinSemilattice_14 -> T_IsPartialEquivalence_16 #

d_refl_82 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny #

d_reflexive_84 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_84 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_86 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_88 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_poset_90 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> T_Poset_314 #

du_poset_90 :: T_JoinSemilattice_14 -> T_Poset_314 #

d_preorder_94 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_JoinSemilattice_14 -> T_Preorder_132 #

du_preorder_94 :: T_JoinSemilattice_14 -> T_Preorder_132 #

d_BoundedJoinSemilattice_102 :: p -> p -> p -> () #

data T_BoundedJoinSemilattice_102 #

Constructors

C_BoundedJoinSemilattice'46'constructor_2401 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsBoundedJoinSemilattice_116 

d_Carrier_122 :: T_BoundedJoinSemilattice_102 -> () #

d__'8776'__124 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> () #

d__'8804'__126 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> () #

d__'8744'__128 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8869'_130 :: T_BoundedJoinSemilattice_102 -> AgdaAny #

d_isBoundedJoinSemilattice_132 :: T_BoundedJoinSemilattice_102 -> T_IsBoundedJoinSemilattice_116 #

d_antisym_136 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_138 :: T_BoundedJoinSemilattice_102 -> T_IsEquivalence_26 #

d_isJoinSemilattice_140 :: T_BoundedJoinSemilattice_102 -> T_IsJoinSemilattice_22 #

d_isPartialOrder_142 :: T_BoundedJoinSemilattice_102 -> T_IsPartialOrder_174 #

d_isPreorder_144 :: T_BoundedJoinSemilattice_102 -> T_IsPreorder_70 #

d_minimum_146 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny #

d_refl_148 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny #

du_refl_148 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny #

d_reflexive_150 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_152 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_154 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_156 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_156 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_158 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_158 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_160 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_160 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_162 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_162 :: T_BoundedJoinSemilattice_102 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_164 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_164 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_166 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_166 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_168 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_168 :: T_BoundedJoinSemilattice_102 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_170 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_170 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_172 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_172 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_176 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_176 :: T_BoundedJoinSemilattice_102 -> T_IsPartialEquivalence_16 #

d_refl_178 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny #

d_reflexive_180 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_180 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_182 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_184 :: T_BoundedJoinSemilattice_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_joinSemilattice_186 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> T_JoinSemilattice_14 #

du_joinSemilattice_186 :: T_BoundedJoinSemilattice_102 -> T_JoinSemilattice_14 #

d_poset_190 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> T_Poset_314 #

du_poset_190 :: T_BoundedJoinSemilattice_102 -> T_Poset_314 #

d_preorder_192 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedJoinSemilattice_102 -> T_Preorder_132 #

du_preorder_192 :: T_BoundedJoinSemilattice_102 -> T_Preorder_132 #

d_MeetSemilattice_200 :: p -> p -> p -> () #

data T_MeetSemilattice_200 #

Constructors

C_MeetSemilattice'46'constructor_4629 (AgdaAny -> AgdaAny -> AgdaAny) T_IsMeetSemilattice_180 

d_Carrier_218 :: T_MeetSemilattice_200 -> () #

d__'8776'__220 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> () #

d__'8804'__222 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> () #

d__'8743'__224 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMeetSemilattice_226 :: T_MeetSemilattice_200 -> T_IsMeetSemilattice_180 #

d_antisym_230 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_232 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_234 :: T_MeetSemilattice_200 -> T_IsEquivalence_26 #

d_isPartialOrder_236 :: T_MeetSemilattice_200 -> T_IsPartialOrder_174 #

d_isPreorder_238 :: T_MeetSemilattice_200 -> T_IsPreorder_70 #

d_refl_240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny #

du_refl_240 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny #

d_reflexive_242 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_244 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_246 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_246 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_248 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_248 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_250 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_250 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_252 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_252 :: T_MeetSemilattice_200 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_254 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_254 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_256 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_256 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_258 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_258 :: T_MeetSemilattice_200 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_260 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_260 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_262 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_262 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_266 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_266 :: T_MeetSemilattice_200 -> T_IsPartialEquivalence_16 #

d_refl_268 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny #

d_reflexive_270 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_270 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_272 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_274 :: T_MeetSemilattice_200 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_poset_276 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> T_Poset_314 #

du_poset_276 :: T_MeetSemilattice_200 -> T_Poset_314 #

d_preorder_280 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_MeetSemilattice_200 -> T_Preorder_132 #

du_preorder_280 :: T_MeetSemilattice_200 -> T_Preorder_132 #

d_BoundedMeetSemilattice_288 :: p -> p -> p -> () #

data T_BoundedMeetSemilattice_288 #

Constructors

C_BoundedMeetSemilattice'46'constructor_6659 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsBoundedMeetSemilattice_274 

d_Carrier_308 :: T_BoundedMeetSemilattice_288 -> () #

d__'8776'__310 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> () #

d__'8804'__312 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> () #

d__'8743'__314 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8868'_316 :: T_BoundedMeetSemilattice_288 -> AgdaAny #

d_isBoundedMeetSemilattice_318 :: T_BoundedMeetSemilattice_288 -> T_IsBoundedMeetSemilattice_274 #

d_antisym_322 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_324 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_326 :: T_BoundedMeetSemilattice_288 -> T_IsEquivalence_26 #

d_isMeetSemilattice_328 :: T_BoundedMeetSemilattice_288 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_330 :: T_BoundedMeetSemilattice_288 -> T_IsPartialOrder_174 #

d_isPreorder_332 :: T_BoundedMeetSemilattice_288 -> T_IsPreorder_70 #

d_maximum_334 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny #

d_refl_336 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny #

du_refl_336 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny #

d_reflexive_338 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_340 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_342 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_342 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_344 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_344 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_346 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_346 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_348 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_348 :: T_BoundedMeetSemilattice_288 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_350 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_350 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_352 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_352 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_354 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_354 :: T_BoundedMeetSemilattice_288 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_356 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_356 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_358 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_358 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_362 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_362 :: T_BoundedMeetSemilattice_288 -> T_IsPartialEquivalence_16 #

d_refl_364 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny #

d_reflexive_366 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_366 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_368 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_370 :: T_BoundedMeetSemilattice_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_meetSemilattice_372 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> T_MeetSemilattice_200 #

du_meetSemilattice_372 :: T_BoundedMeetSemilattice_288 -> T_MeetSemilattice_200 #

d_poset_376 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> T_Poset_314 #

du_poset_376 :: T_BoundedMeetSemilattice_288 -> T_Poset_314 #

d_preorder_378 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedMeetSemilattice_288 -> T_Preorder_132 #

du_preorder_378 :: T_BoundedMeetSemilattice_288 -> T_Preorder_132 #

d_Lattice_386 :: p -> p -> p -> () #

data T_Lattice_386 #

Constructors

C_Lattice'46'constructor_8977 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) T_IsLattice_340 

d_Carrier_406 :: T_Lattice_386 -> () #

d__'8776'__408 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> () #

d__'8804'__410 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> () #

d__'8744'__412 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8743'__414 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isLattice_416 :: T_Lattice_386 -> T_IsLattice_340 #

d_antisym_420 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_422 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_424 :: T_Lattice_386 -> T_IsEquivalence_26 #

d_isJoinSemilattice_426 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_IsJoinSemilattice_22 #

du_isJoinSemilattice_426 :: T_Lattice_386 -> T_IsJoinSemilattice_22 #

d_isMeetSemilattice_428 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_IsMeetSemilattice_180 #

du_isMeetSemilattice_428 :: T_Lattice_386 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_430 :: T_Lattice_386 -> T_IsPartialOrder_174 #

d_isPreorder_432 :: T_Lattice_386 -> T_IsPreorder_70 #

d_refl_434 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny #

du_refl_434 :: T_Lattice_386 -> AgdaAny -> AgdaAny #

d_reflexive_436 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_438 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_440 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_442 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_442 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_444 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_444 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_446 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_446 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_448 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_448 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_450 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_450 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_452 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_452 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_454 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_454 :: T_Lattice_386 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_456 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_456 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_458 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_458 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_460 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_460 :: T_Lattice_386 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_462 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_462 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_464 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_464 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_468 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_468 :: T_Lattice_386 -> T_IsPartialEquivalence_16 #

d_refl_470 :: T_Lattice_386 -> AgdaAny -> AgdaAny #

d_reflexive_472 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_472 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_474 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_476 :: T_Lattice_386 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_setoid_478 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_Setoid_44 #

du_setoid_478 :: T_Lattice_386 -> T_Setoid_44 #

d_joinSemilattice_480 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_JoinSemilattice_14 #

du_joinSemilattice_480 :: T_Lattice_386 -> T_JoinSemilattice_14 #

d_meetSemilattice_482 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_MeetSemilattice_200 #

du_meetSemilattice_482 :: T_Lattice_386 -> T_MeetSemilattice_200 #

d_poset_486 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_Poset_314 #

du_poset_486 :: T_Lattice_386 -> T_Poset_314 #

d_preorder_488 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Lattice_386 -> T_Preorder_132 #

du_preorder_488 :: T_Lattice_386 -> T_Preorder_132 #

d_DistributiveLattice_496 :: p -> p -> p -> () #

data T_DistributiveLattice_496 #

Constructors

C_DistributiveLattice'46'constructor_11867 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) T_IsDistributiveLattice_420 

d_Carrier_516 :: T_DistributiveLattice_496 -> () #

d__'8776'__518 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> () #

d__'8804'__520 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> () #

d__'8744'__522 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8743'__524 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isDistributiveLattice_526 :: T_DistributiveLattice_496 -> T_IsDistributiveLattice_420 #

d_'8743''45'distrib'737''45''8744'_530 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lattice_536 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_Lattice_386 #

du_lattice_536 :: T_DistributiveLattice_496 -> T_Lattice_386 #

d_antisym_540 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_antisym_540 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_542 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_infimum_542 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_544 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsEquivalence_26 #

du_isEquivalence_544 :: T_DistributiveLattice_496 -> T_IsEquivalence_26 #

d_isJoinSemilattice_546 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsJoinSemilattice_22 #

du_isJoinSemilattice_546 :: T_DistributiveLattice_496 -> T_IsJoinSemilattice_22 #

d_isLattice_548 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsLattice_340 #

du_isLattice_548 :: T_DistributiveLattice_496 -> T_IsLattice_340 #

d_isMeetSemilattice_550 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsMeetSemilattice_180 #

du_isMeetSemilattice_550 :: T_DistributiveLattice_496 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_552 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsPartialOrder_174 #

du_isPartialOrder_552 :: T_DistributiveLattice_496 -> T_IsPartialOrder_174 #

d_isPreorder_554 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsPreorder_70 #

du_isPreorder_554 :: T_DistributiveLattice_496 -> T_IsPreorder_70 #

d_joinSemilattice_556 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_JoinSemilattice_14 #

du_joinSemilattice_556 :: T_DistributiveLattice_496 -> T_JoinSemilattice_14 #

d_meetSemilattice_558 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_MeetSemilattice_200 #

du_meetSemilattice_558 :: T_DistributiveLattice_496 -> T_MeetSemilattice_200 #

d_poset_560 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_Poset_314 #

du_poset_560 :: T_DistributiveLattice_496 -> T_Poset_314 #

d_preorder_562 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_Preorder_132 #

du_preorder_562 :: T_DistributiveLattice_496 -> T_Preorder_132 #

d_refl_564 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny #

du_refl_564 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny #

d_reflexive_566 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_reflexive_566 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_setoid_568 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_Setoid_44 #

du_setoid_568 :: T_DistributiveLattice_496 -> T_Setoid_44 #

d_supremum_570 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_supremum_570 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_572 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_572 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_574 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_574 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_576 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_576 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_578 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_578 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_580 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_580 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_582 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_582 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_584 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_584 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_586 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_586 :: T_DistributiveLattice_496 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_588 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_588 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_590 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_590 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_592 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_592 :: T_DistributiveLattice_496 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_594 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_594 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_596 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_596 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_600 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_600 :: T_DistributiveLattice_496 -> T_IsPartialEquivalence_16 #

d_refl_602 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny #

du_refl_602 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny #

d_reflexive_604 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_604 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_606 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_606 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_608 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_608 :: T_DistributiveLattice_496 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_BoundedLattice_616 :: p -> p -> p -> () #

data T_BoundedLattice_616 #

Constructors

C_BoundedLattice'46'constructor_14911 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsBoundedLattice_502 

d_Carrier_640 :: T_BoundedLattice_616 -> () #

d__'8776'__642 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> () #

d__'8804'__644 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> () #

d__'8744'__646 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8743'__648 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8868'_650 :: T_BoundedLattice_616 -> AgdaAny #

d_'8869'_652 :: T_BoundedLattice_616 -> AgdaAny #

d_isBoundedLattice_654 :: T_BoundedLattice_616 -> T_IsBoundedLattice_502 #

d_antisym_658 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_660 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isBoundedJoinSemilattice_662 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_IsBoundedJoinSemilattice_116 #

du_isBoundedJoinSemilattice_662 :: T_BoundedLattice_616 -> T_IsBoundedJoinSemilattice_116 #

d_isBoundedMeetSemilattice_664 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_IsBoundedMeetSemilattice_274 #

du_isBoundedMeetSemilattice_664 :: T_BoundedLattice_616 -> T_IsBoundedMeetSemilattice_274 #

d_isEquivalence_666 :: T_BoundedLattice_616 -> T_IsEquivalence_26 #

d_isJoinSemilattice_668 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_IsJoinSemilattice_22 #

du_isJoinSemilattice_668 :: T_BoundedLattice_616 -> T_IsJoinSemilattice_22 #

d_isLattice_670 :: T_BoundedLattice_616 -> T_IsLattice_340 #

d_isMeetSemilattice_672 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_IsMeetSemilattice_180 #

du_isMeetSemilattice_672 :: T_BoundedLattice_616 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_674 :: T_BoundedLattice_616 -> T_IsPartialOrder_174 #

d_isPreorder_676 :: T_BoundedLattice_616 -> T_IsPreorder_70 #

d_maximum_678 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny #

d_minimum_680 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny #

d_refl_682 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny #

du_refl_682 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny #

d_reflexive_684 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_686 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_688 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_690 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_690 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_692 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_692 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_694 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_694 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_696 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_696 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_698 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_698 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_700 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_700 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_702 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_702 :: T_BoundedLattice_616 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_704 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_704 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_706 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_706 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_708 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_708 :: T_BoundedLattice_616 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_710 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_710 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_712 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_712 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_716 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_716 :: T_BoundedLattice_616 -> T_IsPartialEquivalence_16 #

d_refl_718 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny #

d_reflexive_720 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_720 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_722 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_724 :: T_BoundedLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_boundedJoinSemilattice_726 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_BoundedJoinSemilattice_102 #

du_boundedJoinSemilattice_726 :: T_BoundedLattice_616 -> T_BoundedJoinSemilattice_102 #

d_boundedMeetSemilattice_728 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_BoundedMeetSemilattice_288 #

du_boundedMeetSemilattice_728 :: T_BoundedLattice_616 -> T_BoundedMeetSemilattice_288 #

d_lattice_730 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_Lattice_386 #

du_lattice_730 :: T_BoundedLattice_616 -> T_Lattice_386 #

d_joinSemilattice_734 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_JoinSemilattice_14 #

du_joinSemilattice_734 :: T_BoundedLattice_616 -> T_JoinSemilattice_14 #

d_meetSemilattice_736 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_MeetSemilattice_200 #

du_meetSemilattice_736 :: T_BoundedLattice_616 -> T_MeetSemilattice_200 #

d_poset_738 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_Poset_314 #

du_poset_738 :: T_BoundedLattice_616 -> T_Poset_314 #

d_preorder_740 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_Preorder_132 #

du_preorder_740 :: T_BoundedLattice_616 -> T_Preorder_132 #

d_setoid_742 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BoundedLattice_616 -> T_Setoid_44 #

du_setoid_742 :: T_BoundedLattice_616 -> T_Setoid_44 #

d_HeytingAlgebra_750 :: p -> p -> p -> () #

data T_HeytingAlgebra_750 #

Constructors

C_HeytingAlgebra'46'constructor_18655 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsHeytingAlgebra_598 

d_Carrier_776 :: T_HeytingAlgebra_750 -> () #

d__'8776'__778 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> () #

d__'8804'__780 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> () #

d__'8744'__782 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8743'__784 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8680'__786 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8868'_788 :: T_HeytingAlgebra_750 -> AgdaAny #

d_'8869'_790 :: T_HeytingAlgebra_750 -> AgdaAny #

d_isHeytingAlgebra_792 :: T_HeytingAlgebra_750 -> T_IsHeytingAlgebra_598 #

d_boundedLattice_794 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_BoundedLattice_616 #

du_boundedLattice_794 :: T_HeytingAlgebra_750 -> T_BoundedLattice_616 #

d_exponential_798 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_transpose'45''8680'_800 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_transpose'45''8680'_800 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_transpose'45''8743'_802 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_transpose'45''8743'_802 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_806 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_antisym_806 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_boundedJoinSemilattice_808 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_BoundedJoinSemilattice_102 #

du_boundedJoinSemilattice_808 :: T_HeytingAlgebra_750 -> T_BoundedJoinSemilattice_102 #

d_boundedMeetSemilattice_810 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_BoundedMeetSemilattice_288 #

du_boundedMeetSemilattice_810 :: T_HeytingAlgebra_750 -> T_BoundedMeetSemilattice_288 #

d_infimum_812 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_infimum_812 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isBoundedJoinSemilattice_814 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsBoundedJoinSemilattice_116 #

du_isBoundedJoinSemilattice_814 :: T_HeytingAlgebra_750 -> T_IsBoundedJoinSemilattice_116 #

d_isBoundedLattice_816 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsBoundedLattice_502 #

du_isBoundedLattice_816 :: T_HeytingAlgebra_750 -> T_IsBoundedLattice_502 #

d_isBoundedMeetSemilattice_818 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsBoundedMeetSemilattice_274 #

du_isBoundedMeetSemilattice_818 :: T_HeytingAlgebra_750 -> T_IsBoundedMeetSemilattice_274 #

d_isEquivalence_820 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsEquivalence_26 #

du_isEquivalence_820 :: T_HeytingAlgebra_750 -> T_IsEquivalence_26 #

d_isJoinSemilattice_822 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsJoinSemilattice_22 #

du_isJoinSemilattice_822 :: T_HeytingAlgebra_750 -> T_IsJoinSemilattice_22 #

d_isLattice_824 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsLattice_340 #

du_isLattice_824 :: T_HeytingAlgebra_750 -> T_IsLattice_340 #

d_isMeetSemilattice_826 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsMeetSemilattice_180 #

du_isMeetSemilattice_826 :: T_HeytingAlgebra_750 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_828 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsPartialOrder_174 #

du_isPartialOrder_828 :: T_HeytingAlgebra_750 -> T_IsPartialOrder_174 #

d_isPreorder_830 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsPreorder_70 #

du_isPreorder_830 :: T_HeytingAlgebra_750 -> T_IsPreorder_70 #

d_joinSemilattice_832 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_JoinSemilattice_14 #

du_joinSemilattice_832 :: T_HeytingAlgebra_750 -> T_JoinSemilattice_14 #

d_lattice_834 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_Lattice_386 #

du_lattice_834 :: T_HeytingAlgebra_750 -> T_Lattice_386 #

d_maximum_836 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

du_maximum_836 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

d_meetSemilattice_838 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_MeetSemilattice_200 #

du_meetSemilattice_838 :: T_HeytingAlgebra_750 -> T_MeetSemilattice_200 #

d_minimum_840 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

du_minimum_840 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

d_poset_842 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_Poset_314 #

du_poset_842 :: T_HeytingAlgebra_750 -> T_Poset_314 #

d_preorder_844 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_Preorder_132 #

du_preorder_844 :: T_HeytingAlgebra_750 -> T_Preorder_132 #

d_refl_846 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

du_refl_846 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

d_reflexive_848 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_reflexive_848 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_setoid_850 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_Setoid_44 #

du_setoid_850 :: T_HeytingAlgebra_750 -> T_Setoid_44 #

d_supremum_852 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_supremum_852 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_854 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_854 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_856 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_856 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_858 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_858 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_860 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_860 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_862 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_862 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_864 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_864 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_866 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_866 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_868 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_868 :: T_HeytingAlgebra_750 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_870 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_870 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_872 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_872 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_874 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_874 :: T_HeytingAlgebra_750 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_876 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_876 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_878 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_878 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_882 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_882 :: T_HeytingAlgebra_750 -> T_IsPartialEquivalence_16 #

d_refl_884 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

du_refl_884 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny #

d_reflexive_886 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_886 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_888 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_888 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_890 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_890 :: T_HeytingAlgebra_750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_BooleanAlgebra_898 :: p -> p -> p -> () #

data T_BooleanAlgebra_898 #

Constructors

C_BooleanAlgebra'46'constructor_22683 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsBooleanAlgebra_730 

d_Carrier_924 :: T_BooleanAlgebra_898 -> () #

d__'8776'__926 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> () #

d__'8804'__928 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> () #

d__'8744'__930 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8743'__932 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'172'__934 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

d_'8868'_936 :: T_BooleanAlgebra_898 -> AgdaAny #

d_'8869'_938 :: T_BooleanAlgebra_898 -> AgdaAny #

d_isBooleanAlgebra_940 :: T_BooleanAlgebra_898 -> T_IsBooleanAlgebra_730 #

d_heytingAlgebra_946 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_HeytingAlgebra_750 #

du_heytingAlgebra_946 :: T_BooleanAlgebra_898 -> T_HeytingAlgebra_750 #

d__'8680'__950 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'8680'__950 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_952 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_antisym_952 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_boundedJoinSemilattice_954 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_BoundedJoinSemilattice_102 #

du_boundedJoinSemilattice_954 :: T_BooleanAlgebra_898 -> T_BoundedJoinSemilattice_102 #

d_boundedLattice_956 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_BoundedLattice_616 #

du_boundedLattice_956 :: T_BooleanAlgebra_898 -> T_BoundedLattice_616 #

d_boundedMeetSemilattice_958 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_BoundedMeetSemilattice_288 #

du_boundedMeetSemilattice_958 :: T_BooleanAlgebra_898 -> T_BoundedMeetSemilattice_288 #

d_exponential_960 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_exponential_960 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_infimum_962 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_infimum_962 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isBoundedJoinSemilattice_964 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsBoundedJoinSemilattice_116 #

du_isBoundedJoinSemilattice_964 :: T_BooleanAlgebra_898 -> T_IsBoundedJoinSemilattice_116 #

d_isBoundedLattice_966 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsBoundedLattice_502 #

du_isBoundedLattice_966 :: T_BooleanAlgebra_898 -> T_IsBoundedLattice_502 #

d_isBoundedMeetSemilattice_968 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsBoundedMeetSemilattice_274 #

du_isBoundedMeetSemilattice_968 :: T_BooleanAlgebra_898 -> T_IsBoundedMeetSemilattice_274 #

d_isEquivalence_970 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsEquivalence_26 #

du_isEquivalence_970 :: T_BooleanAlgebra_898 -> T_IsEquivalence_26 #

d_isHeytingAlgebra_972 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsHeytingAlgebra_598 #

du_isHeytingAlgebra_972 :: T_BooleanAlgebra_898 -> T_IsHeytingAlgebra_598 #

d_isJoinSemilattice_974 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsJoinSemilattice_22 #

du_isJoinSemilattice_974 :: T_BooleanAlgebra_898 -> T_IsJoinSemilattice_22 #

d_isLattice_976 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsLattice_340 #

du_isLattice_976 :: T_BooleanAlgebra_898 -> T_IsLattice_340 #

d_isMeetSemilattice_978 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsMeetSemilattice_180 #

du_isMeetSemilattice_978 :: T_BooleanAlgebra_898 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_980 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsPartialOrder_174 #

du_isPartialOrder_980 :: T_BooleanAlgebra_898 -> T_IsPartialOrder_174 #

d_isPreorder_982 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsPreorder_70 #

du_isPreorder_982 :: T_BooleanAlgebra_898 -> T_IsPreorder_70 #

d_joinSemilattice_984 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_JoinSemilattice_14 #

du_joinSemilattice_984 :: T_BooleanAlgebra_898 -> T_JoinSemilattice_14 #

d_lattice_986 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_Lattice_386 #

du_lattice_986 :: T_BooleanAlgebra_898 -> T_Lattice_386 #

d_maximum_988 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

du_maximum_988 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

d_meetSemilattice_990 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_MeetSemilattice_200 #

du_meetSemilattice_990 :: T_BooleanAlgebra_898 -> T_MeetSemilattice_200 #

d_minimum_992 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

du_minimum_992 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

d_poset_994 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_Poset_314 #

du_poset_994 :: T_BooleanAlgebra_898 -> T_Poset_314 #

d_preorder_996 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_Preorder_132 #

du_preorder_996 :: T_BooleanAlgebra_898 -> T_Preorder_132 #

d_refl_998 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

du_refl_998 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

d_reflexive_1000 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_reflexive_1000 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_setoid_1002 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_Setoid_44 #

du_setoid_1002 :: T_BooleanAlgebra_898 -> T_Setoid_44 #

d_supremum_1004 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_supremum_1004 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_1006 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1006 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_transpose'45''8680'_1008 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_transpose'45''8680'_1008 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_transpose'45''8743'_1010 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_transpose'45''8743'_1010 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'x_1012 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'x_1012 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8743'y'8804'y_1014 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8743'y'8804'y_1014 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d_x'8804'x'8744'y_1016 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

du_x'8804'x'8744'y_1016 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d_y'8804'x'8744'y_1018 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

du_y'8804'x'8744'y_1018 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'greatest_1020 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'greatest_1020 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'least_1022 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8744''45'least_1022 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'45''8776'_1024 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_Σ_14 #

du_'8764''45'resp'45''8776'_1024 :: T_BooleanAlgebra_898 -> T_Σ_14 #

d_'8764''45'resp'691''45''8776'_1026 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'691''45''8776'_1026 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8764''45'resp'737''45''8776'_1028 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8764''45'resp'737''45''8776'_1028 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'45''8776'_1030 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_Σ_14 #

du_'8818''45'resp'45''8776'_1030 :: T_BooleanAlgebra_898 -> T_Σ_14 #

d_'8818''45'resp'691''45''8776'_1032 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'691''45''8776'_1032 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8818''45'resp'737''45''8776'_1034 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8818''45'resp'737''45''8776'_1034 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isPartialEquivalence_1038 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1038 :: T_BooleanAlgebra_898 -> T_IsPartialEquivalence_16 #

d_refl_1040 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

du_refl_1040 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny #

d_reflexive_1042 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1042 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_1044 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1044 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1046 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1046 :: T_BooleanAlgebra_898 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #