Safe Haskell	None

MAlonzo.Code.Algebra.Lattice.Bundles

Documentation

d_Semilattice_10 :: p1 -> p2 -> () Source #

data T_Semilattice_10 Source #

Constructors

C_Semilattice'46'constructor_119 (AgdaAny -> AgdaAny -> AgdaAny) T_IsSemilattice_1576

d_Carrier_24 :: T_Semilattice_10 -> () Source #

d__'8776'__26 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__28 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemilattice_30 :: T_Semilattice_10 -> T_IsSemilattice_1576 Source #

d_assoc_34 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_36 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_38 :: T_Semilattice_10 -> AgdaAny -> AgdaAny Source #

d_isBand_40 :: T_Semilattice_10 -> T_IsBand_242 Source #

d_isEquivalence_42 :: T_Semilattice_10 -> T_IsEquivalence_26 Source #

d_isMagma_44 :: T_Semilattice_10 -> T_IsMagma_98 Source #

d_isPartialEquivalence_46 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_46 :: T_Semilattice_10 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_48 :: T_Semilattice_10 -> T_IsSemigroup_206 Source #

d_refl_50 :: T_Semilattice_10 -> AgdaAny -> AgdaAny Source #

d_reflexive_52 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_52 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_54 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_Setoid_44 Source #

du_setoid_54 :: T_Semilattice_10 -> T_Setoid_44 Source #

d_sym_56 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_58 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_60 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_62 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_62 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_64 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_64 :: T_Semilattice_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_band_66 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_Band_266 Source #

du_band_66 :: T_Semilattice_10 -> T_Band_266 Source #

d__'8777'__70 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> AgdaAny -> AgdaAny -> () Source #

d_isBand_72 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_IsBand_242 Source #

du_isBand_72 :: T_Semilattice_10 -> T_IsBand_242 Source #

d_isMagma_74 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_IsMagma_98 Source #

du_isMagma_74 :: T_Semilattice_10 -> T_IsMagma_98 Source #

d_isSemigroup_76 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_IsSemigroup_206 Source #

du_isSemigroup_76 :: T_Semilattice_10 -> T_IsSemigroup_206 Source #

d_magma_78 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_Magma_36 Source #

du_magma_78 :: T_Semilattice_10 -> T_Magma_36 Source #

d_rawMagma_80 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_RawMagma_8 Source #

du_rawMagma_80 :: T_Semilattice_10 -> T_RawMagma_8 Source #

d_semigroup_82 :: T_Level_14 -> T_Level_14 -> T_Semilattice_10 -> T_Semigroup_206 Source #

du_semigroup_82 :: T_Semilattice_10 -> T_Semigroup_206 Source #

d_MeetSemilattice_88 :: p1 -> p2 -> () Source #

data T_MeetSemilattice_88 Source #

Constructors

C_MeetSemilattice'46'constructor_1247 (AgdaAny -> AgdaAny -> AgdaAny) T_IsSemilattice_1576

d_Carrier_102 :: T_MeetSemilattice_88 -> () Source #

d__'8776'__104 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> () Source #

d__'8743'__106 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMeetSemilattice_108 :: T_MeetSemilattice_88 -> T_IsSemilattice_1576 Source #

d_assoc_112 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_114 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_116 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny Source #

d_isBand_118 :: T_MeetSemilattice_88 -> T_IsBand_242 Source #

d_isEquivalence_120 :: T_MeetSemilattice_88 -> T_IsEquivalence_26 Source #

d_isMagma_122 :: T_MeetSemilattice_88 -> T_IsMagma_98 Source #

d_isPartialEquivalence_124 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_124 :: T_MeetSemilattice_88 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_126 :: T_MeetSemilattice_88 -> T_IsSemigroup_206 Source #

d_refl_128 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny Source #

d_reflexive_130 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_130 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_132 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_Setoid_44 Source #

du_setoid_132 :: T_MeetSemilattice_88 -> T_Setoid_44 Source #

d_sym_134 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_136 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_138 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_140 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_140 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_142 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_142 :: T_MeetSemilattice_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semilattice_144 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_Semilattice_10 Source #

du_semilattice_144 :: T_MeetSemilattice_88 -> T_Semilattice_10 Source #

d_band_148 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_Band_266 Source #

du_band_148 :: T_MeetSemilattice_88 -> T_Band_266 Source #

d_magma_150 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_Magma_36 Source #

du_magma_150 :: T_MeetSemilattice_88 -> T_Magma_36 Source #

d_rawMagma_152 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_RawMagma_8 Source #

du_rawMagma_152 :: T_MeetSemilattice_88 -> T_RawMagma_8 Source #

d_semigroup_154 :: T_Level_14 -> T_Level_14 -> T_MeetSemilattice_88 -> T_Semigroup_206 Source #

du_semigroup_154 :: T_MeetSemilattice_88 -> T_Semigroup_206 Source #

d_JoinSemilattice_160 :: p1 -> p2 -> () Source #

data T_JoinSemilattice_160 Source #

Constructors

C_JoinSemilattice'46'constructor_2277 (AgdaAny -> AgdaAny -> AgdaAny) T_IsSemilattice_1576

d_Carrier_174 :: T_JoinSemilattice_160 -> () Source #

d__'8776'__176 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__178 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isJoinSemilattice_180 :: T_JoinSemilattice_160 -> T_IsSemilattice_1576 Source #

d_assoc_184 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_186 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_188 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny Source #

d_isBand_190 :: T_JoinSemilattice_160 -> T_IsBand_242 Source #

d_isEquivalence_192 :: T_JoinSemilattice_160 -> T_IsEquivalence_26 Source #

d_isMagma_194 :: T_JoinSemilattice_160 -> T_IsMagma_98 Source #

d_isPartialEquivalence_196 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_196 :: T_JoinSemilattice_160 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_198 :: T_JoinSemilattice_160 -> T_IsSemigroup_206 Source #

d_refl_200 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny Source #

d_reflexive_202 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_202 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_204 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_Setoid_44 Source #

du_setoid_204 :: T_JoinSemilattice_160 -> T_Setoid_44 Source #

d_sym_206 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_208 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_210 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_212 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_212 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_214 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_214 :: T_JoinSemilattice_160 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semilattice_216 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_Semilattice_10 Source #

du_semilattice_216 :: T_JoinSemilattice_160 -> T_Semilattice_10 Source #

d_band_220 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_Band_266 Source #

du_band_220 :: T_JoinSemilattice_160 -> T_Band_266 Source #

d_magma_222 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_Magma_36 Source #

du_magma_222 :: T_JoinSemilattice_160 -> T_Magma_36 Source #

d_rawMagma_224 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_RawMagma_8 Source #

du_rawMagma_224 :: T_JoinSemilattice_160 -> T_RawMagma_8 Source #

d_semigroup_226 :: T_Level_14 -> T_Level_14 -> T_JoinSemilattice_160 -> T_Semigroup_206 Source #

du_semigroup_226 :: T_JoinSemilattice_160 -> T_Semigroup_206 Source #

d_BoundedSemilattice_232 :: p1 -> p2 -> () Source #

data T_BoundedSemilattice_232 Source #

Constructors

C_BoundedSemilattice'46'constructor_3325 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsIdempotentCommutativeMonoid_480

d_Carrier_248 :: T_BoundedSemilattice_232 -> () Source #

d__'8776'__250 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> () Source #

d__'8729'__252 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_ε_254 :: T_BoundedSemilattice_232 -> AgdaAny Source #

d_isBoundedSemilattice_256 :: T_BoundedSemilattice_232 -> T_IsIdempotentCommutativeMonoid_480 Source #

d_assoc_260 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_262 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_264 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny Source #

d_identity_266 :: T_BoundedSemilattice_232 -> T_Σ_14 Source #

d_identity'691'_268 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny Source #

du_identity'691'_268 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny Source #

d_identity'737'_270 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny Source #

du_identity'737'_270 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny Source #

d_isBand_272 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_IsBand_242 Source #

du_isBand_272 :: T_BoundedSemilattice_232 -> T_IsBand_242 Source #

d_isCommutativeMagma_274 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_274 :: T_BoundedSemilattice_232 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_276 :: T_BoundedSemilattice_232 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_278 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_278 :: T_BoundedSemilattice_232 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_280 :: T_BoundedSemilattice_232 -> T_IsEquivalence_26 Source #

d_isMagma_282 :: T_BoundedSemilattice_232 -> T_IsMagma_98 Source #

d_isMonoid_284 :: T_BoundedSemilattice_232 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_286 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_286 :: T_BoundedSemilattice_232 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_288 :: T_BoundedSemilattice_232 -> T_IsSemigroup_206 Source #

d_isSemilattice_290 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_IsSemilattice_1576 Source #

du_isSemilattice_290 :: T_BoundedSemilattice_232 -> T_IsSemilattice_1576 Source #

d_isUnitalMagma_292 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_292 :: T_BoundedSemilattice_232 -> T_IsUnitalMagma_326 Source #

d_refl_294 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny Source #

d_reflexive_296 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_296 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_298 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_Setoid_44 Source #

du_setoid_298 :: T_BoundedSemilattice_232 -> T_Setoid_44 Source #

d_sym_300 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_302 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_304 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_306 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_306 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_308 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_308 :: T_BoundedSemilattice_232 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_semilattice_310 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_Semilattice_10 Source #

du_semilattice_310 :: T_BoundedSemilattice_232 -> T_Semilattice_10 Source #

d_band_314 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_Band_266 Source #

du_band_314 :: T_BoundedSemilattice_232 -> T_Band_266 Source #

d_magma_316 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_Magma_36 Source #

du_magma_316 :: T_BoundedSemilattice_232 -> T_Magma_36 Source #

d_rawMagma_318 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_RawMagma_8 Source #

du_rawMagma_318 :: T_BoundedSemilattice_232 -> T_RawMagma_8 Source #

d_semigroup_320 :: T_Level_14 -> T_Level_14 -> T_BoundedSemilattice_232 -> T_Semigroup_206 Source #

du_semigroup_320 :: T_BoundedSemilattice_232 -> T_Semigroup_206 Source #

d_BoundedMeetSemilattice_326 :: p1 -> p2 -> () Source #

data T_BoundedMeetSemilattice_326 Source #

Constructors

C_BoundedMeetSemilattice'46'constructor_4601 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsIdempotentCommutativeMonoid_480

d_Carrier_342 :: T_BoundedMeetSemilattice_326 -> () Source #

d__'8776'__344 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> () Source #

d__'8743'__346 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8868'_348 :: T_BoundedMeetSemilattice_326 -> AgdaAny Source #

d_isBoundedMeetSemilattice_350 :: T_BoundedMeetSemilattice_326 -> T_IsIdempotentCommutativeMonoid_480 Source #

d_assoc_354 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_assoc_354 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_356 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_comm_356 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_358 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

du_idem_358 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

d_identity_360 :: T_BoundedMeetSemilattice_326 -> T_Σ_14 Source #

d_identity'691'_362 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

du_identity'691'_362 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

d_identity'737'_364 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

du_identity'737'_364 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

d_isBand_366 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_IsBand_242 Source #

du_isBand_366 :: T_BoundedMeetSemilattice_326 -> T_IsBand_242 Source #

d_isEquivalence_368 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_IsEquivalence_26 Source #

du_isEquivalence_368 :: T_BoundedMeetSemilattice_326 -> T_IsEquivalence_26 Source #

d_isMagma_370 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_IsMagma_98 Source #

du_isMagma_370 :: T_BoundedMeetSemilattice_326 -> T_IsMagma_98 Source #

d_isSemilattice_372 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_IsSemilattice_1576 Source #

du_isSemilattice_372 :: T_BoundedMeetSemilattice_326 -> T_IsSemilattice_1576 Source #

d_isPartialEquivalence_374 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_374 :: T_BoundedMeetSemilattice_326 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_376 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_IsSemigroup_206 Source #

du_isSemigroup_376 :: T_BoundedMeetSemilattice_326 -> T_IsSemigroup_206 Source #

d_refl_378 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

du_refl_378 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny Source #

d_reflexive_380 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

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

d_setoid_382 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_Setoid_44 Source #

du_setoid_382 :: T_BoundedMeetSemilattice_326 -> T_Setoid_44 Source #

d_sym_384 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_384 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_386 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_386 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_388 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong_388 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_390 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_390 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_392 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_392 :: T_BoundedMeetSemilattice_326 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_boundedSemilattice_394 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_BoundedSemilattice_232 Source #

du_boundedSemilattice_394 :: T_BoundedMeetSemilattice_326 -> T_BoundedSemilattice_232 Source #

d_band_398 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_Band_266 Source #

du_band_398 :: T_BoundedMeetSemilattice_326 -> T_Band_266 Source #

d_magma_400 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_Magma_36 Source #

du_magma_400 :: T_BoundedMeetSemilattice_326 -> T_Magma_36 Source #

d_rawMagma_402 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_RawMagma_8 Source #

du_rawMagma_402 :: T_BoundedMeetSemilattice_326 -> T_RawMagma_8 Source #

d_semigroup_404 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_Semigroup_206 Source #

du_semigroup_404 :: T_BoundedMeetSemilattice_326 -> T_Semigroup_206 Source #

d_semilattice_406 :: T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_326 -> T_Semilattice_10 Source #

du_semilattice_406 :: T_BoundedMeetSemilattice_326 -> T_Semilattice_10 Source #

d_BoundedJoinSemilattice_412 :: p1 -> p2 -> () Source #

data T_BoundedJoinSemilattice_412 Source #

Constructors

C_BoundedJoinSemilattice'46'constructor_5781 (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny T_IsIdempotentCommutativeMonoid_480

d_Carrier_428 :: T_BoundedJoinSemilattice_412 -> () Source #

d__'8776'__430 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__432 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8869'_434 :: T_BoundedJoinSemilattice_412 -> AgdaAny Source #

d_isBoundedJoinSemilattice_436 :: T_BoundedJoinSemilattice_412 -> T_IsIdempotentCommutativeMonoid_480 Source #

d_assoc_440 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_assoc_440 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_442 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_comm_442 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_444 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

du_idem_444 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

d_identity_446 :: T_BoundedJoinSemilattice_412 -> T_Σ_14 Source #

d_identity'691'_448 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

du_identity'691'_448 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

d_identity'737'_450 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

du_identity'737'_450 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

d_isBand_452 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_IsBand_242 Source #

du_isBand_452 :: T_BoundedJoinSemilattice_412 -> T_IsBand_242 Source #

d_isEquivalence_454 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_IsEquivalence_26 Source #

du_isEquivalence_454 :: T_BoundedJoinSemilattice_412 -> T_IsEquivalence_26 Source #

d_isSemilattice_456 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_IsSemilattice_1576 Source #

du_isSemilattice_456 :: T_BoundedJoinSemilattice_412 -> T_IsSemilattice_1576 Source #

d_isMagma_458 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_IsMagma_98 Source #

du_isMagma_458 :: T_BoundedJoinSemilattice_412 -> T_IsMagma_98 Source #

d_isPartialEquivalence_460 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_460 :: T_BoundedJoinSemilattice_412 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_462 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_IsSemigroup_206 Source #

du_isSemigroup_462 :: T_BoundedJoinSemilattice_412 -> T_IsSemigroup_206 Source #

d_refl_464 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

du_refl_464 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny Source #

d_reflexive_466 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_466 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_468 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_Setoid_44 Source #

du_setoid_468 :: T_BoundedJoinSemilattice_412 -> T_Setoid_44 Source #

d_sym_470 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_470 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_472 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_472 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_474 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong_474 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_476 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_476 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_478 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_478 :: T_BoundedJoinSemilattice_412 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_boundedSemilattice_480 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_BoundedSemilattice_232 Source #

du_boundedSemilattice_480 :: T_BoundedJoinSemilattice_412 -> T_BoundedSemilattice_232 Source #

d_band_484 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_Band_266 Source #

du_band_484 :: T_BoundedJoinSemilattice_412 -> T_Band_266 Source #

d_magma_486 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_Magma_36 Source #

du_magma_486 :: T_BoundedJoinSemilattice_412 -> T_Magma_36 Source #

d_rawMagma_488 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_RawMagma_8 Source #

du_rawMagma_488 :: T_BoundedJoinSemilattice_412 -> T_RawMagma_8 Source #

d_semigroup_490 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_Semigroup_206 Source #

du_semigroup_490 :: T_BoundedJoinSemilattice_412 -> T_Semigroup_206 Source #

d_semilattice_492 :: T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_412 -> T_Semilattice_10 Source #

du_semilattice_492 :: T_BoundedJoinSemilattice_412 -> T_Semilattice_10 Source #

d_RawLattice_498 :: p1 -> p2 -> () Source #

data T_RawLattice_498 Source #

Constructors

C_RawLattice'46'constructor_6893 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)

d_Carrier_512 :: T_RawLattice_498 -> () Source #

d__'8776'__514 :: T_RawLattice_498 -> AgdaAny -> AgdaAny -> () Source #

d__'8743'__516 :: T_RawLattice_498 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8744'__518 :: T_RawLattice_498 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'rawMagma_520 :: T_Level_14 -> T_Level_14 -> T_RawLattice_498 -> T_RawMagma_8 Source #

du_'8744''45'rawMagma_520 :: T_RawLattice_498 -> T_RawMagma_8 Source #

d_'8743''45'rawMagma_522 :: T_Level_14 -> T_Level_14 -> T_RawLattice_498 -> T_RawMagma_8 Source #

du_'8743''45'rawMagma_522 :: T_RawLattice_498 -> T_RawMagma_8 Source #

d__'8777'__526 :: T_Level_14 -> T_Level_14 -> T_RawLattice_498 -> AgdaAny -> AgdaAny -> () Source #

d_Lattice_532 :: p1 -> p2 -> () Source #

data T_Lattice_532 Source #

Constructors

C_Lattice'46'constructor_7423 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) T_IsLattice_1876

d_Carrier_548 :: T_Lattice_532 -> () Source #

d__'8776'__550 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__552 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__554 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isLattice_556 :: T_Lattice_532 -> T_IsLattice_1876 Source #

d_absorptive_560 :: T_Lattice_532 -> T_Σ_14 Source #

d_isEquivalence_562 :: T_Lattice_532 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_564 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_564 :: T_Lattice_532 -> T_IsPartialEquivalence_16 Source #

d_refl_566 :: T_Lattice_532 -> AgdaAny -> AgdaAny Source #

d_reflexive_568 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_568 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_570 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_572 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'absorbs'45''8744'_574 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'absorbs'45''8744'_574 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'assoc_576 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'comm_578 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong_580 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'691'_582 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'691'_582 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'737'_584 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'737'_584 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'absorbs'45''8743'_586 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'absorbs'45''8743'_586 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'assoc_588 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'comm_590 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong_592 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'691'_594 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'691'_594 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'737'_596 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'737'_596 :: T_Lattice_532 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_rawLattice_598 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_RawLattice_498 Source #

du_rawLattice_598 :: T_Lattice_532 -> T_RawLattice_498 Source #

d_'8743''45'rawMagma_602 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_RawMagma_8 Source #

du_'8743''45'rawMagma_602 :: T_Lattice_532 -> T_RawMagma_8 Source #

d_'8744''45'rawMagma_604 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_RawMagma_8 Source #

du_'8744''45'rawMagma_604 :: T_Lattice_532 -> T_RawMagma_8 Source #

d_setoid_606 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> T_Setoid_44 Source #

du_setoid_606 :: T_Lattice_532 -> T_Setoid_44 Source #

d__'8777'__610 :: T_Level_14 -> T_Level_14 -> T_Lattice_532 -> AgdaAny -> AgdaAny -> () Source #

d_DistributiveLattice_616 :: p1 -> p2 -> () Source #

data T_DistributiveLattice_616 Source #

Constructors

C_DistributiveLattice'46'constructor_8807 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) T_IsDistributiveLattice_1950

d_Carrier_632 :: T_DistributiveLattice_616 -> () Source #

d__'8776'__634 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__636 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__638 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isDistributiveLattice_640 :: T_DistributiveLattice_616 -> T_IsDistributiveLattice_1950 Source #

d_absorptive_644 :: T_DistributiveLattice_616 -> T_Σ_14 Source #

d_isEquivalence_646 :: T_DistributiveLattice_616 -> T_IsEquivalence_26 Source #

d_isLattice_648 :: T_DistributiveLattice_616 -> T_IsLattice_1876 Source #

d_isPartialEquivalence_650 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_650 :: T_DistributiveLattice_616 -> T_IsPartialEquivalence_16 Source #

d_refl_652 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny Source #

d_reflexive_654 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_654 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_656 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_658 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'absorbs'45''8744'_660 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'absorbs'45''8744'_660 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'assoc_662 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'comm_664 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong_666 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'691'_668 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'691'_668 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'737'_670 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'737'_670 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'45''8744'_672 :: T_DistributiveLattice_616 -> T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_674 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_674 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_676 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_676 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'absorbs'45''8743'_678 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'absorbs'45''8743'_678 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'assoc_680 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'comm_682 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong_684 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'691'_686 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'691'_686 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'737'_688 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'737'_688 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'45''8743'_690 :: T_DistributiveLattice_616 -> T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_692 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_692 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_694 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_694 :: T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_lattice_696 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> T_Lattice_532 Source #

du_lattice_696 :: T_DistributiveLattice_616 -> T_Lattice_532 Source #

d__'8777'__700 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> AgdaAny -> AgdaAny -> () Source #

d_rawLattice_702 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> T_RawLattice_498 Source #

du_rawLattice_702 :: T_DistributiveLattice_616 -> T_RawLattice_498 Source #

d_setoid_704 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> T_Setoid_44 Source #

du_setoid_704 :: T_DistributiveLattice_616 -> T_Setoid_44 Source #

d_'8743''45'rawMagma_706 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> T_RawMagma_8 Source #

du_'8743''45'rawMagma_706 :: T_DistributiveLattice_616 -> T_RawMagma_8 Source #

d_'8744''45'rawMagma_708 :: T_Level_14 -> T_Level_14 -> T_DistributiveLattice_616 -> T_RawMagma_8 Source #

du_'8744''45'rawMagma_708 :: T_DistributiveLattice_616 -> T_RawMagma_8 Source #

d_BooleanAlgebra_714 :: p1 -> p2 -> () Source #

data T_BooleanAlgebra_714 Source #

Constructors

C_BooleanAlgebra'46'constructor_10533 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) AgdaAny AgdaAny T_IsBooleanAlgebra_2026

d_Carrier_736 :: T_BooleanAlgebra_714 -> () Source #

d__'8776'__738 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__740 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__742 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'172'__744 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

d_'8868'_746 :: T_BooleanAlgebra_714 -> AgdaAny Source #

d_'8869'_748 :: T_BooleanAlgebra_714 -> AgdaAny Source #

d_isBooleanAlgebra_750 :: T_BooleanAlgebra_714 -> T_IsBooleanAlgebra_2026 Source #

d_absorptive_754 :: T_BooleanAlgebra_714 -> T_Σ_14 Source #

d_isDistributiveLattice_756 :: T_BooleanAlgebra_714 -> T_IsDistributiveLattice_1950 Source #

d_isEquivalence_758 :: T_BooleanAlgebra_714 -> T_IsEquivalence_26 Source #

d_isLattice_760 :: T_BooleanAlgebra_714 -> T_IsLattice_1876 Source #

d_isPartialEquivalence_762 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_762 :: T_BooleanAlgebra_714 -> T_IsPartialEquivalence_16 Source #

d_refl_764 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

d_reflexive_766 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_766 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_768 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_770 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'172''45'cong_772 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'absorbs'45''8744'_774 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'absorbs'45''8744'_774 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'assoc_776 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'comm_778 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'complement_780 :: T_BooleanAlgebra_714 -> T_Σ_14 Source #

d_'8743''45'complement'691'_782 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

du_'8743''45'complement'691'_782 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

d_'8743''45'complement'737'_784 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

du_'8743''45'complement'737'_784 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong_786 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'691'_788 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'691'_788 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'737'_790 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'737'_790 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'45''8744'_792 :: T_BooleanAlgebra_714 -> T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_794 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_794 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_796 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_796 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'absorbs'45''8743'_798 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'absorbs'45''8743'_798 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'assoc_800 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'comm_802 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'complement_804 :: T_BooleanAlgebra_714 -> T_Σ_14 Source #

d_'8744''45'complement'691'_806 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

du_'8744''45'complement'691'_806 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

d_'8744''45'complement'737'_808 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

du_'8744''45'complement'737'_808 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong_810 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'691'_812 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'691'_812 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'737'_814 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'737'_814 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'45''8743'_816 :: T_BooleanAlgebra_714 -> T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_818 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_818 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_820 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_820 :: T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_distributiveLattice_822 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_DistributiveLattice_616 Source #

du_distributiveLattice_822 :: T_BooleanAlgebra_714 -> T_DistributiveLattice_616 Source #

d__'8777'__826 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> AgdaAny -> AgdaAny -> () Source #

d_lattice_828 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_Lattice_532 Source #

du_lattice_828 :: T_BooleanAlgebra_714 -> T_Lattice_532 Source #

d_rawLattice_830 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_RawLattice_498 Source #

du_rawLattice_830 :: T_BooleanAlgebra_714 -> T_RawLattice_498 Source #

d_setoid_832 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_Setoid_44 Source #

du_setoid_832 :: T_BooleanAlgebra_714 -> T_Setoid_44 Source #

d_'8743''45'rawMagma_834 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_RawMagma_8 Source #

du_'8743''45'rawMagma_834 :: T_BooleanAlgebra_714 -> T_RawMagma_8 Source #

d_'8744''45'rawMagma_836 :: T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_714 -> T_RawMagma_8 Source #

du_'8744''45'rawMagma_836 :: T_BooleanAlgebra_714 -> T_RawMagma_8 Source #