Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Lattice.Bundles

Documentation

d_Semilattice_10 ∷ p → p → () Source #

data T_Semilattice_10 Source #

Constructors

C_Semilattice'46'constructor_193 (AgdaAny → AgdaAny → AgdaAny) T_IsCommutativeBand_590

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_IsCommutativeBand_590 Source #

d_assoc_34 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_34 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_36 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_38 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny Source #

du_idem_38 ∷ T_Semilattice_10 → AgdaAny → AgdaAny Source #

d_isBand_40 ∷ T_Semilattice_10 → T_IsBand_508 Source #

d_isEquivalence_42 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsEquivalence_26 Source #

du_isEquivalence_42 ∷ T_Semilattice_10 → T_IsEquivalence_26 Source #

d_isMagma_44 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsMagma_176 Source #

du_isMagma_44 ∷ T_Semilattice_10 → T_IsMagma_176 Source #

d_isPartialEquivalence_46 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_46 ∷ T_Semilattice_10 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_48 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsSemigroup_472 Source #

du_isSemigroup_48 ∷ T_Semilattice_10 → T_IsSemigroup_472 Source #

d_refl_50 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny Source #

du_refl_50 ∷ T_Semilattice_10 → AgdaAny → AgdaAny Source #

d_reflexive_52 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Semilattice_10 → T_Setoid_44 Source #

du_setoid_54 ∷ T_Semilattice_10 → T_Setoid_44 Source #

d_sym_56 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_56 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_58 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_58 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_60 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_60 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_62 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_Semilattice_10 → T_Band_596 Source #

du_band_66 ∷ T_Semilattice_10 → T_Band_596 Source #

d__'8777'__70 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → () Source #

d_isBand_72 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsBand_508 Source #

du_isBand_72 ∷ T_Semilattice_10 → T_IsBand_508 Source #

d_isMagma_74 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsMagma_176 Source #

du_isMagma_74 ∷ T_Semilattice_10 → T_IsMagma_176 Source #

d_isSemigroup_76 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsSemigroup_472 Source #

du_isSemigroup_76 ∷ T_Semilattice_10 → T_IsSemigroup_472 Source #

d_magma_78 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_Magma_68 Source #

du_magma_78 ∷ T_Semilattice_10 → T_Magma_68 Source #

d_rawMagma_80 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_RawMagma_36 Source #

du_rawMagma_80 ∷ T_Semilattice_10 → T_RawMagma_36 Source #

d_semigroup_82 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_Semigroup_536 Source #

du_semigroup_82 ∷ T_Semilattice_10 → T_Semigroup_536 Source #

d_MeetSemilattice_88 ∷ p → p → () Source #

data T_MeetSemilattice_88 Source #

Constructors

C_MeetSemilattice'46'constructor_1393 (AgdaAny → AgdaAny → AgdaAny) T_IsCommutativeBand_590

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_IsCommutativeBand_590 Source #

d_assoc_112 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_112 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_114 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_116 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → AgdaAny → AgdaAny Source #

du_idem_116 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny Source #

d_isBand_118 ∷ T_MeetSemilattice_88 → T_IsBand_508 Source #

d_isEquivalence_120 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_IsEquivalence_26 Source #

du_isEquivalence_120 ∷ T_MeetSemilattice_88 → T_IsEquivalence_26 Source #

d_isMagma_122 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_IsMagma_176 Source #

du_isMagma_122 ∷ T_MeetSemilattice_88 → T_IsMagma_176 Source #

d_isPartialEquivalence_124 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_124 ∷ T_MeetSemilattice_88 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_126 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_IsSemigroup_472 Source #

du_isSemigroup_126 ∷ T_MeetSemilattice_88 → T_IsSemigroup_472 Source #

d_refl_128 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → AgdaAny → AgdaAny Source #

du_refl_128 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny Source #

d_reflexive_130 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_MeetSemilattice_88 → T_Setoid_44 Source #

du_setoid_132 ∷ T_MeetSemilattice_88 → T_Setoid_44 Source #

d_sym_134 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_134 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_136 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_136 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_138 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_138 ∷ T_MeetSemilattice_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_140 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_MeetSemilattice_88 → T_Semilattice_10 Source #

du_semilattice_144 ∷ T_MeetSemilattice_88 → T_Semilattice_10 Source #

d_band_148 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_Band_596 Source #

du_band_148 ∷ T_MeetSemilattice_88 → T_Band_596 Source #

d_magma_150 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_Magma_68 Source #

du_magma_150 ∷ T_MeetSemilattice_88 → T_Magma_68 Source #

d_rawMagma_152 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_RawMagma_36 Source #

du_rawMagma_152 ∷ T_MeetSemilattice_88 → T_RawMagma_36 Source #

d_semigroup_154 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_88 → T_Semigroup_536 Source #

du_semigroup_154 ∷ T_MeetSemilattice_88 → T_Semigroup_536 Source #

d_JoinSemilattice_160 ∷ p → p → () Source #

data T_JoinSemilattice_160 Source #

Constructors

C_JoinSemilattice'46'constructor_2531 (AgdaAny → AgdaAny → AgdaAny) T_IsCommutativeBand_590

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_IsCommutativeBand_590 Source #

d_assoc_184 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_184 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_186 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_188 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → AgdaAny → AgdaAny Source #

du_idem_188 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny Source #

d_isBand_190 ∷ T_JoinSemilattice_160 → T_IsBand_508 Source #

d_isEquivalence_192 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_IsEquivalence_26 Source #

du_isEquivalence_192 ∷ T_JoinSemilattice_160 → T_IsEquivalence_26 Source #

d_isMagma_194 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_IsMagma_176 Source #

du_isMagma_194 ∷ T_JoinSemilattice_160 → T_IsMagma_176 Source #

d_isPartialEquivalence_196 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_196 ∷ T_JoinSemilattice_160 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_198 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_IsSemigroup_472 Source #

du_isSemigroup_198 ∷ T_JoinSemilattice_160 → T_IsSemigroup_472 Source #

d_refl_200 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → AgdaAny → AgdaAny Source #

du_refl_200 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny Source #

d_reflexive_202 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_JoinSemilattice_160 → T_Setoid_44 Source #

du_setoid_204 ∷ T_JoinSemilattice_160 → T_Setoid_44 Source #

d_sym_206 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_206 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_208 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_208 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_210 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_210 ∷ T_JoinSemilattice_160 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_212 ∷ T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → 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_18 → T_Level_18 → T_JoinSemilattice_160 → T_Semilattice_10 Source #

du_semilattice_216 ∷ T_JoinSemilattice_160 → T_Semilattice_10 Source #

d_band_220 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_Band_596 Source #

du_band_220 ∷ T_JoinSemilattice_160 → T_Band_596 Source #

d_magma_222 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_Magma_68 Source #

du_magma_222 ∷ T_JoinSemilattice_160 → T_Magma_68 Source #

d_rawMagma_224 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_RawMagma_36 Source #

du_rawMagma_224 ∷ T_JoinSemilattice_160 → T_RawMagma_36 Source #

d_semigroup_226 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_160 → T_Semigroup_536 Source #

du_semigroup_226 ∷ T_JoinSemilattice_160 → T_Semigroup_536 Source #

d_BoundedSemilattice_232 ∷ p → p → () Source #

data T_BoundedSemilattice_232 Source #

Constructors

C_BoundedSemilattice'46'constructor_3703 (AgdaAny → AgdaAny → AgdaAny) AgdaAny T_IsIdempotentCommutativeMonoid_852

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_852 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_18 → T_Level_18 → T_BoundedSemilattice_232 → AgdaAny → AgdaAny Source #

du_identity'691'_268 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny Source #

d_identity'737'_270 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → AgdaAny → AgdaAny Source #

du_identity'737'_270 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny Source #

d_isBand_272 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsBand_508 Source #

du_isBand_272 ∷ T_BoundedSemilattice_232 → T_IsBand_508 Source #

d_isCommutativeMagma_274 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_274 ∷ T_BoundedSemilattice_232 → T_IsCommutativeMagma_212 Source #

d_isCommutativeMonoid_276 ∷ T_BoundedSemilattice_232 → T_IsCommutativeMonoid_736 Source #

d_isCommutativeSemigroup_278 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_278 ∷ T_BoundedSemilattice_232 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_280 ∷ T_BoundedSemilattice_232 → T_IsEquivalence_26 Source #

d_isIdempotentMonoid_282 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsIdempotentMonoid_796 Source #

du_isIdempotentMonoid_282 ∷ T_BoundedSemilattice_232 → T_IsIdempotentMonoid_796 Source #

d_isMagma_284 ∷ T_BoundedSemilattice_232 → T_IsMagma_176 Source #

d_isMonoid_286 ∷ T_BoundedSemilattice_232 → T_IsMonoid_686 Source #

d_isPartialEquivalence_288 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_288 ∷ T_BoundedSemilattice_232 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_290 ∷ T_BoundedSemilattice_232 → T_IsSemigroup_472 Source #

d_isCommutativeBand_292 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_292 ∷ T_BoundedSemilattice_232 → T_IsCommutativeBand_590 Source #

d_isUnitalMagma_294 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_294 ∷ T_BoundedSemilattice_232 → T_IsUnitalMagma_642 Source #

d_refl_296 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny Source #

d_reflexive_298 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_298 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_300 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_Setoid_44 Source #

du_setoid_300 ∷ T_BoundedSemilattice_232 → T_Setoid_44 Source #

d_sym_302 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_304 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_306 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_308 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_308 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_310 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_310 ∷ T_BoundedSemilattice_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semilattice_312 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_Semilattice_10 Source #

du_semilattice_312 ∷ T_BoundedSemilattice_232 → T_Semilattice_10 Source #

d_band_316 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_Band_596 Source #

du_band_316 ∷ T_BoundedSemilattice_232 → T_Band_596 Source #

d_magma_318 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_Magma_68 Source #

du_magma_318 ∷ T_BoundedSemilattice_232 → T_Magma_68 Source #

d_rawMagma_320 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_RawMagma_36 Source #

du_rawMagma_320 ∷ T_BoundedSemilattice_232 → T_RawMagma_36 Source #

d_semigroup_322 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_232 → T_Semigroup_536 Source #

du_semigroup_322 ∷ T_BoundedSemilattice_232 → T_Semigroup_536 Source #

d_BoundedMeetSemilattice_328 ∷ p → p → () Source #

data T_BoundedMeetSemilattice_328 Source #

Constructors

C_BoundedMeetSemilattice'46'constructor_5171 (AgdaAny → AgdaAny → AgdaAny) AgdaAny T_IsIdempotentCommutativeMonoid_852

d_Carrier_344 ∷ T_BoundedMeetSemilattice_328 → () Source #

d__'8776'__346 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → () Source #

d__'8743'__348 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_350 ∷ T_BoundedMeetSemilattice_328 → AgdaAny Source #

d_isBoundedMeetSemilattice_352 ∷ T_BoundedMeetSemilattice_328 → T_IsIdempotentCommutativeMonoid_852 Source #

d_assoc_356 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_356 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_358 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_358 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_360 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

du_idem_360 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

d_identity_362 ∷ T_BoundedMeetSemilattice_328 → T_Σ_14 Source #

d_identity'691'_364 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

du_identity'691'_364 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

d_identity'737'_366 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

du_identity'737'_366 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

d_isBand_368 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_IsBand_508 Source #

du_isBand_368 ∷ T_BoundedMeetSemilattice_328 → T_IsBand_508 Source #

d_isEquivalence_370 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_IsEquivalence_26 Source #

du_isEquivalence_370 ∷ T_BoundedMeetSemilattice_328 → T_IsEquivalence_26 Source #

d_isMagma_372 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_IsMagma_176 Source #

du_isMagma_372 ∷ T_BoundedMeetSemilattice_328 → T_IsMagma_176 Source #

d_isCommutativeBand_374 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_374 ∷ T_BoundedMeetSemilattice_328 → T_IsCommutativeBand_590 Source #

d_isPartialEquivalence_376 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_376 ∷ T_BoundedMeetSemilattice_328 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_378 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_IsSemigroup_472 Source #

du_isSemigroup_378 ∷ T_BoundedMeetSemilattice_328 → T_IsSemigroup_472 Source #

d_refl_380 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

du_refl_380 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny Source #

d_reflexive_382 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_382 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_384 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_Setoid_44 Source #

du_setoid_384 ∷ T_BoundedMeetSemilattice_328 → T_Setoid_44 Source #

d_sym_386 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_386 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_388 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_388 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_390 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_390 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_392 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_392 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_394 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_394 ∷ T_BoundedMeetSemilattice_328 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedSemilattice_396 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_BoundedSemilattice_232 Source #

du_boundedSemilattice_396 ∷ T_BoundedMeetSemilattice_328 → T_BoundedSemilattice_232 Source #

d_band_400 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_Band_596 Source #

du_band_400 ∷ T_BoundedMeetSemilattice_328 → T_Band_596 Source #

d_magma_402 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_Magma_68 Source #

du_magma_402 ∷ T_BoundedMeetSemilattice_328 → T_Magma_68 Source #

d_rawMagma_404 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_RawMagma_36 Source #

du_rawMagma_404 ∷ T_BoundedMeetSemilattice_328 → T_RawMagma_36 Source #

d_semigroup_406 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_Semigroup_536 Source #

du_semigroup_406 ∷ T_BoundedMeetSemilattice_328 → T_Semigroup_536 Source #

d_semilattice_408 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_328 → T_Semilattice_10 Source #

du_semilattice_408 ∷ T_BoundedMeetSemilattice_328 → T_Semilattice_10 Source #

d_BoundedJoinSemilattice_414 ∷ p → p → () Source #

data T_BoundedJoinSemilattice_414 Source #

Constructors

C_BoundedJoinSemilattice'46'constructor_6531 (AgdaAny → AgdaAny → AgdaAny) AgdaAny T_IsIdempotentCommutativeMonoid_852

d_Carrier_430 ∷ T_BoundedJoinSemilattice_414 → () Source #

d__'8776'__432 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → () Source #

d__'8744'__434 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869'_436 ∷ T_BoundedJoinSemilattice_414 → AgdaAny Source #

d_isBoundedJoinSemilattice_438 ∷ T_BoundedJoinSemilattice_414 → T_IsIdempotentCommutativeMonoid_852 Source #

d_assoc_442 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_442 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_444 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_444 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_446 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

du_idem_446 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

d_identity_448 ∷ T_BoundedJoinSemilattice_414 → T_Σ_14 Source #

d_identity'691'_450 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

du_identity'691'_450 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

d_identity'737'_452 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

du_identity'737'_452 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

d_isBand_454 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_IsBand_508 Source #

du_isBand_454 ∷ T_BoundedJoinSemilattice_414 → T_IsBand_508 Source #

d_isEquivalence_456 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_IsEquivalence_26 Source #

du_isEquivalence_456 ∷ T_BoundedJoinSemilattice_414 → T_IsEquivalence_26 Source #

d_isCommutativeBand_458 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_458 ∷ T_BoundedJoinSemilattice_414 → T_IsCommutativeBand_590 Source #

d_isMagma_460 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_IsMagma_176 Source #

du_isMagma_460 ∷ T_BoundedJoinSemilattice_414 → T_IsMagma_176 Source #

d_isPartialEquivalence_462 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_462 ∷ T_BoundedJoinSemilattice_414 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_464 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_IsSemigroup_472 Source #

du_isSemigroup_464 ∷ T_BoundedJoinSemilattice_414 → T_IsSemigroup_472 Source #

d_refl_466 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

du_refl_466 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny Source #

d_reflexive_468 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_468 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_470 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_Setoid_44 Source #

du_setoid_470 ∷ T_BoundedJoinSemilattice_414 → T_Setoid_44 Source #

d_sym_472 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_472 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_474 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_474 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_476 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_476 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_478 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_478 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_480 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_480 ∷ T_BoundedJoinSemilattice_414 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedSemilattice_482 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_BoundedSemilattice_232 Source #

du_boundedSemilattice_482 ∷ T_BoundedJoinSemilattice_414 → T_BoundedSemilattice_232 Source #

d_band_486 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_Band_596 Source #

du_band_486 ∷ T_BoundedJoinSemilattice_414 → T_Band_596 Source #

d_magma_488 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_Magma_68 Source #

du_magma_488 ∷ T_BoundedJoinSemilattice_414 → T_Magma_68 Source #

d_rawMagma_490 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_RawMagma_36 Source #

du_rawMagma_490 ∷ T_BoundedJoinSemilattice_414 → T_RawMagma_36 Source #

d_semigroup_492 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_Semigroup_536 Source #

du_semigroup_492 ∷ T_BoundedJoinSemilattice_414 → T_Semigroup_536 Source #

d_semilattice_494 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_414 → T_Semilattice_10 Source #

du_semilattice_494 ∷ T_BoundedJoinSemilattice_414 → T_Semilattice_10 Source #

d_Lattice_500 ∷ p → p → () Source #

data T_Lattice_500 Source #

Constructors

C_Lattice'46'constructor_7925 (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny) T_IsLattice_2962

d_Carrier_516 ∷ T_Lattice_500 → () Source #

d__'8776'__518 ∷ T_Lattice_500 → AgdaAny → AgdaAny → () Source #

d__'8744'__520 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__522 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_524 ∷ T_Lattice_500 → T_IsLattice_2962 Source #

d_absorptive_528 ∷ T_Lattice_500 → T_Σ_14 Source #

d_isEquivalence_530 ∷ T_Lattice_500 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_532 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_532 ∷ T_Lattice_500 → T_IsPartialEquivalence_16 Source #

d_refl_534 ∷ T_Lattice_500 → AgdaAny → AgdaAny Source #

d_reflexive_536 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_536 ∷ T_Lattice_500 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_538 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_540 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_542 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_542 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_544 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_546 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_548 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_550 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_550 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_552 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_552 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_554 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_554 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_556 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_558 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_560 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_562 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_562 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_564 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_564 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawLattice_566 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_RawLattice_12 Source #

du_rawLattice_566 ∷ T_Lattice_500 → T_RawLattice_12 Source #

d_'8743''45'rawMagma_570 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_RawMagma_36 Source #

du_'8743''45'rawMagma_570 ∷ T_Lattice_500 → T_RawMagma_36 Source #

d_'8744''45'rawMagma_572 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_RawMagma_36 Source #

du_'8744''45'rawMagma_572 ∷ T_Lattice_500 → T_RawMagma_36 Source #

d_setoid_574 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_Setoid_44 Source #

du_setoid_574 ∷ T_Lattice_500 → T_Setoid_44 Source #

d__'8777'__578 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → () Source #

d_DistributiveLattice_584 ∷ p → p → () Source #

data T_DistributiveLattice_584 Source #

Constructors

C_DistributiveLattice'46'constructor_9515 (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny) T_IsDistributiveLattice_3036

d_Carrier_600 ∷ T_DistributiveLattice_584 → () Source #

d__'8776'__602 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → () Source #

d__'8744'__604 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__606 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

d_isDistributiveLattice_608 ∷ T_DistributiveLattice_584 → T_IsDistributiveLattice_3036 Source #

d_absorptive_612 ∷ T_DistributiveLattice_584 → T_Σ_14 Source #

d_isEquivalence_614 ∷ T_DistributiveLattice_584 → T_IsEquivalence_26 Source #

d_isLattice_616 ∷ T_DistributiveLattice_584 → T_IsLattice_2962 Source #

d_isPartialEquivalence_618 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_618 ∷ T_DistributiveLattice_584 → T_IsPartialEquivalence_16 Source #

d_refl_620 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny Source #

d_reflexive_622 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_622 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_624 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_626 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_628 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_628 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_630 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_632 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_634 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_636 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_636 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_638 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_638 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_640 ∷ T_DistributiveLattice_584 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_642 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_642 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_644 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_644 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_646 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_646 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_648 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_650 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_652 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_654 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_654 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_656 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_656 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_658 ∷ T_DistributiveLattice_584 → T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_660 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_660 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_662 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_662 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lattice_664 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Lattice_500 Source #

du_lattice_664 ∷ T_DistributiveLattice_584 → T_Lattice_500 Source #

d__'8777'__668 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny → () Source #

d_rawLattice_670 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_RawLattice_12 Source #

du_rawLattice_670 ∷ T_DistributiveLattice_584 → T_RawLattice_12 Source #

d_setoid_672 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Setoid_44 Source #

du_setoid_672 ∷ T_DistributiveLattice_584 → T_Setoid_44 Source #

d_'8743''45'rawMagma_674 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_RawMagma_36 Source #

du_'8743''45'rawMagma_674 ∷ T_DistributiveLattice_584 → T_RawMagma_36 Source #

d_'8744''45'rawMagma_676 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_RawMagma_36 Source #

du_'8744''45'rawMagma_676 ∷ T_DistributiveLattice_584 → T_RawMagma_36 Source #

d_BooleanAlgebra_682 ∷ p → p → () Source #

data T_BooleanAlgebra_682 Source #

Constructors

C_BooleanAlgebra'46'constructor_11509 (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny) AgdaAny AgdaAny T_IsBooleanAlgebra_3112

d_Carrier_704 ∷ T_BooleanAlgebra_682 → () Source #

d__'8776'__706 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → () Source #

d__'8744'__708 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__710 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172'__712 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8868'_714 ∷ T_BooleanAlgebra_682 → AgdaAny Source #

d_'8869'_716 ∷ T_BooleanAlgebra_682 → AgdaAny Source #

d_isBooleanAlgebra_718 ∷ T_BooleanAlgebra_682 → T_IsBooleanAlgebra_3112 Source #

d_absorptive_722 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_isDistributiveLattice_724 ∷ T_BooleanAlgebra_682 → T_IsDistributiveLattice_3036 Source #

d_isEquivalence_726 ∷ T_BooleanAlgebra_682 → T_IsEquivalence_26 Source #

d_isLattice_728 ∷ T_BooleanAlgebra_682 → T_IsLattice_2962 Source #

d_isPartialEquivalence_730 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_730 ∷ T_BooleanAlgebra_682 → T_IsPartialEquivalence_16 Source #

d_refl_732 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_reflexive_734 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_734 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_736 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_738 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'cong_740 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_742 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_742 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_744 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_746 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'complement_748 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8743''45'complement'691'_750 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'691'_750 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'737'_752 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'737'_752 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'cong_754 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_756 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_756 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_758 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_758 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_760 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_762 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_762 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_764 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_764 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_766 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_766 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_768 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_770 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'complement_772 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8744''45'complement'691'_774 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'691'_774 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'complement'737'_776 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'737'_776 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'cong_778 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_780 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_780 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_782 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_782 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_784 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_786 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_786 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_788 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_788 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distributiveLattice_790 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_DistributiveLattice_584 Source #

du_distributiveLattice_790 ∷ T_BooleanAlgebra_682 → T_DistributiveLattice_584 Source #

d__'8777'__794 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → () Source #

d_lattice_796 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Lattice_500 Source #

du_lattice_796 ∷ T_BooleanAlgebra_682 → T_Lattice_500 Source #

d_rawLattice_798 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_RawLattice_12 Source #

du_rawLattice_798 ∷ T_BooleanAlgebra_682 → T_RawLattice_12 Source #

d_setoid_800 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Setoid_44 Source #

du_setoid_800 ∷ T_BooleanAlgebra_682 → T_Setoid_44 Source #

d_'8743''45'rawMagma_802 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_RawMagma_36 Source #

du_'8743''45'rawMagma_802 ∷ T_BooleanAlgebra_682 → T_RawMagma_36 Source #

d_'8744''45'rawMagma_804 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_RawMagma_36 Source #

du_'8744''45'rawMagma_804 ∷ T_BooleanAlgebra_682 → T_RawMagma_36 Source #