Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Relation.Binary.Lattice.Structures

Documentation

d_IsJoinSemilattice_22 ∷ p → p → p → p → p → p → p → () Source #

data T_IsJoinSemilattice_22 Source #

Constructors

C_IsJoinSemilattice'46'constructor_527 T_IsPartialOrder_174 (AgdaAny → AgdaAny → T_Σ_14)

d_isPartialOrder_30 ∷ T_IsJoinSemilattice_22 → T_IsPartialOrder_174 Source #

d_supremum_32 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_x'8804'x'8744'y_38 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_38 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_50 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_64 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_64 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_76 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_78 ∷ T_IsJoinSemilattice_22 → T_IsEquivalence_26 Source #

d_isPreorder_80 ∷ T_IsJoinSemilattice_22 → T_IsPreorder_70 Source #

d_refl_82 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny Source #

du_refl_82 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny Source #

d_reflexive_84 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_86 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_88 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_88 ∷ T_IsJoinSemilattice_22 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_90 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_90 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_92 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_92 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_94 ∷ T_IsJoinSemilattice_22 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_96 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_98 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_98 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_102 ∷ T_IsJoinSemilattice_22 → T_IsPartialEquivalence_16 Source #

d_refl_104 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny Source #

d_reflexive_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_106 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_108 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_110 ∷ T_IsJoinSemilattice_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedJoinSemilattice_116 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedJoinSemilattice_116 Source #

Constructors

C_IsBoundedJoinSemilattice'46'constructor_5215 T_IsJoinSemilattice_22 (AgdaAny → AgdaAny)

d_isJoinSemilattice_126 ∷ T_IsBoundedJoinSemilattice_116 → T_IsJoinSemilattice_22 Source #

d_minimum_128 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny Source #

d_antisym_132 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_134 ∷ T_IsBoundedJoinSemilattice_116 → T_IsEquivalence_26 Source #

d_isPartialOrder_136 ∷ T_IsBoundedJoinSemilattice_116 → T_IsPartialOrder_174 Source #

d_isPreorder_138 ∷ T_IsBoundedJoinSemilattice_116 → T_IsPreorder_70 Source #

d_refl_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny Source #

du_refl_140 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny Source #

d_reflexive_142 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_144 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_146 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_148 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_150 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_152 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_154 ∷ T_IsBoundedJoinSemilattice_116 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_156 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_158 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_160 ∷ T_IsBoundedJoinSemilattice_116 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_162 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_164 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_168 ∷ T_IsBoundedJoinSemilattice_116 → T_IsPartialEquivalence_16 Source #

d_refl_170 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny Source #

d_reflexive_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_172 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_174 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_176 ∷ T_IsBoundedJoinSemilattice_116 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMeetSemilattice_180 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMeetSemilattice_180 Source #

Constructors

C_IsMeetSemilattice'46'constructor_7577 T_IsPartialOrder_174 (AgdaAny → AgdaAny → T_Σ_14)

d_isPartialOrder_188 ∷ T_IsMeetSemilattice_180 → T_IsPartialOrder_174 Source #

d_infimum_190 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_x'8743'y'8804'x_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_196 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_208 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_222 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_234 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_236 ∷ T_IsMeetSemilattice_180 → T_IsEquivalence_26 Source #

d_isPreorder_238 ∷ T_IsMeetSemilattice_180 → T_IsPreorder_70 Source #

d_refl_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny Source #

du_refl_240 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny Source #

d_reflexive_242 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_244 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_246 ∷ T_IsMeetSemilattice_180 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_248 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_250 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_252 ∷ T_IsMeetSemilattice_180 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_254 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_256 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_260 ∷ T_IsMeetSemilattice_180 → T_IsPartialEquivalence_16 Source #

d_refl_262 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny Source #

d_reflexive_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_264 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_266 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_268 ∷ T_IsMeetSemilattice_180 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedMeetSemilattice_274 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedMeetSemilattice_274 Source #

Constructors

C_IsBoundedMeetSemilattice'46'constructor_12265 T_IsMeetSemilattice_180 (AgdaAny → AgdaAny)

d_isMeetSemilattice_284 ∷ T_IsBoundedMeetSemilattice_274 → T_IsMeetSemilattice_180 Source #

d_maximum_286 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny Source #

d_antisym_290 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_292 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_294 ∷ T_IsBoundedMeetSemilattice_274 → T_IsEquivalence_26 Source #

d_isPartialOrder_296 ∷ T_IsBoundedMeetSemilattice_274 → T_IsPartialOrder_174 Source #

d_isPreorder_298 ∷ T_IsBoundedMeetSemilattice_274 → T_IsPreorder_70 Source #

d_refl_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny Source #

du_refl_300 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny Source #

d_reflexive_302 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_304 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_306 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_308 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_310 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_310 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_312 ∷ T_IsBoundedMeetSemilattice_274 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_314 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_316 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_318 ∷ T_IsBoundedMeetSemilattice_274 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_320 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_322 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_326 ∷ T_IsBoundedMeetSemilattice_274 → T_IsPartialEquivalence_16 Source #

d_refl_328 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny Source #

d_reflexive_330 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_330 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_332 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_334 ∷ T_IsBoundedMeetSemilattice_274 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsLattice_340 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsLattice_340 Source #

Constructors

C_IsLattice'46'constructor_14941 T_IsPartialOrder_174 (AgdaAny → AgdaAny → T_Σ_14) (AgdaAny → AgdaAny → T_Σ_14)

d_isPartialOrder_352 ∷ T_IsLattice_340 → T_IsPartialOrder_174 Source #

d_supremum_354 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_356 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isJoinSemilattice_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_358 ∷ T_IsLattice_340 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_360 ∷ T_IsLattice_340 → T_IsMeetSemilattice_180 Source #

d_x'8804'x'8744'y_364 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_364 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_366 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_368 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_372 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_374 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_376 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_380 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_382 ∷ T_IsLattice_340 → T_IsEquivalence_26 Source #

d_isPreorder_384 ∷ T_IsLattice_340 → T_IsPreorder_70 Source #

d_refl_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny Source #

du_refl_386 ∷ T_IsLattice_340 → AgdaAny → AgdaAny Source #

d_reflexive_388 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_390 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_392 ∷ T_IsLattice_340 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_394 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_396 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_398 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_398 ∷ T_IsLattice_340 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_400 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_402 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_406 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_406 ∷ T_IsLattice_340 → T_IsPartialEquivalence_16 Source #

d_refl_408 ∷ T_IsLattice_340 → AgdaAny → AgdaAny Source #

d_reflexive_410 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_340 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_410 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_412 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_414 ∷ T_IsLattice_340 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_420 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsDistributiveLattice_420 Source #

Constructors

C_IsDistributiveLattice'46'constructor_18193 T_IsLattice_340 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isLattice_430 ∷ T_IsDistributiveLattice_420 → T_IsLattice_340 Source #

d_'8743''45'distrib'737''45''8744'_432 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_436 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_438 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_440 ∷ T_IsDistributiveLattice_420 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_442 ∷ T_IsDistributiveLattice_420 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_444 ∷ T_IsDistributiveLattice_420 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_446 ∷ T_IsDistributiveLattice_420 → T_IsPartialOrder_174 Source #

d_isPreorder_448 ∷ T_IsDistributiveLattice_420 → T_IsPreorder_70 Source #

d_refl_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny Source #

du_refl_450 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny Source #

d_reflexive_452 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_454 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_456 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_458 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_460 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_462 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_464 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_466 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_468 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_470 ∷ T_IsDistributiveLattice_420 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_472 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_474 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_476 ∷ T_IsDistributiveLattice_420 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_478 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_480 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_484 ∷ T_IsDistributiveLattice_420 → T_IsPartialEquivalence_16 Source #

d_refl_486 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny Source #

d_reflexive_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_488 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_490 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_492 ∷ T_IsDistributiveLattice_420 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedLattice_502 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedLattice_502 Source #

Constructors

C_IsBoundedLattice'46'constructor_21319 T_IsLattice_340 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

d_isLattice_518 ∷ T_IsBoundedLattice_502 → T_IsLattice_340 Source #

d_maximum_520 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny Source #

d_minimum_522 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny Source #

d_antisym_526 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_528 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_530 ∷ T_IsBoundedLattice_502 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_532 ∷ T_IsBoundedLattice_502 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_534 ∷ T_IsBoundedLattice_502 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_536 ∷ T_IsBoundedLattice_502 → T_IsPartialOrder_174 Source #

d_isPreorder_538 ∷ T_IsBoundedLattice_502 → T_IsPreorder_70 Source #

d_refl_540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny Source #

du_refl_540 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny Source #

d_reflexive_542 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_544 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_546 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_548 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_550 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_552 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_554 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_556 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_558 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_560 ∷ T_IsBoundedLattice_502 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_562 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_564 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_566 ∷ T_IsBoundedLattice_502 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_568 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_570 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_574 ∷ T_IsBoundedLattice_502 → T_IsPartialEquivalence_16 Source #

d_refl_576 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny Source #

d_reflexive_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_578 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_580 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_582 ∷ T_IsBoundedLattice_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isBoundedJoinSemilattice_584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_IsBoundedJoinSemilattice_116 Source #

du_isBoundedJoinSemilattice_584 ∷ T_IsBoundedLattice_502 → T_IsBoundedJoinSemilattice_116 Source #

d_isBoundedMeetSemilattice_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_502 → T_IsBoundedMeetSemilattice_274 Source #

du_isBoundedMeetSemilattice_586 ∷ T_IsBoundedLattice_502 → T_IsBoundedMeetSemilattice_274 Source #

d_IsHeytingAlgebra_598 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsHeytingAlgebra_598 Source #

Constructors

C_IsHeytingAlgebra'46'constructor_25303 T_IsBoundedLattice_502 (AgdaAny → AgdaAny → AgdaAny → T_Σ_14)

d_isBoundedLattice_614 ∷ T_IsHeytingAlgebra_598 → T_IsBoundedLattice_502 Source #

d_exponential_616 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_transpose'45''8680'_624 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_624 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_640 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_652 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_654 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_656 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_IsBoundedJoinSemilattice_116 Source #

du_isBoundedJoinSemilattice_656 ∷ T_IsHeytingAlgebra_598 → T_IsBoundedJoinSemilattice_116 Source #

d_isBoundedMeetSemilattice_658 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_IsBoundedMeetSemilattice_274 Source #

du_isBoundedMeetSemilattice_658 ∷ T_IsHeytingAlgebra_598 → T_IsBoundedMeetSemilattice_274 Source #

d_isEquivalence_660 ∷ T_IsHeytingAlgebra_598 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_662 ∷ T_IsHeytingAlgebra_598 → T_IsJoinSemilattice_22 Source #

d_isLattice_664 ∷ T_IsHeytingAlgebra_598 → T_IsLattice_340 Source #

d_isMeetSemilattice_666 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_666 ∷ T_IsHeytingAlgebra_598 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_668 ∷ T_IsHeytingAlgebra_598 → T_IsPartialOrder_174 Source #

d_isPreorder_670 ∷ T_IsHeytingAlgebra_598 → T_IsPreorder_70 Source #

d_maximum_672 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny Source #

d_minimum_674 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny Source #

d_refl_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny Source #

du_refl_676 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny Source #

d_reflexive_678 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_680 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_682 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_684 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_686 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_688 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_690 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_692 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_694 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_696 ∷ T_IsHeytingAlgebra_598 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_698 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_700 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_702 ∷ T_IsHeytingAlgebra_598 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_704 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_706 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_710 ∷ T_IsHeytingAlgebra_598 → T_IsPartialEquivalence_16 Source #

d_refl_712 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny Source #

d_reflexive_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_714 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_716 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_718 ∷ T_IsHeytingAlgebra_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBooleanAlgebra_730 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

newtype T_IsBooleanAlgebra_730 Source #

Constructors

C_IsBooleanAlgebra'46'constructor_31651 T_IsHeytingAlgebra_598

d__'8680'__750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8680'__750 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_isHeytingAlgebra_756 ∷ T_IsBooleanAlgebra_730 → T_IsHeytingAlgebra_598 Source #

d_antisym_760 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_exponential_762 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_764 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_IsBoundedJoinSemilattice_116 Source #

du_isBoundedJoinSemilattice_766 ∷ T_IsBooleanAlgebra_730 → T_IsBoundedJoinSemilattice_116 Source #

d_isBoundedLattice_768 ∷ T_IsBooleanAlgebra_730 → T_IsBoundedLattice_502 Source #

d_isBoundedMeetSemilattice_770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_IsBoundedMeetSemilattice_274 Source #

du_isBoundedMeetSemilattice_770 ∷ T_IsBooleanAlgebra_730 → T_IsBoundedMeetSemilattice_274 Source #

d_isEquivalence_772 ∷ T_IsBooleanAlgebra_730 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_774 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_774 ∷ T_IsBooleanAlgebra_730 → T_IsJoinSemilattice_22 Source #

d_isLattice_776 ∷ T_IsBooleanAlgebra_730 → T_IsLattice_340 Source #

d_isMeetSemilattice_778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_778 ∷ T_IsBooleanAlgebra_730 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_780 ∷ T_IsBooleanAlgebra_730 → T_IsPartialOrder_174 Source #

d_isPreorder_782 ∷ T_IsBooleanAlgebra_730 → T_IsPreorder_70 Source #

d_maximum_784 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny Source #

d_minimum_786 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny Source #

d_refl_788 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny Source #

du_refl_788 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny Source #

d_reflexive_790 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_792 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_794 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8680'_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_796 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_798 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_800 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_802 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_804 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_806 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_808 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_810 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_812 ∷ T_IsBooleanAlgebra_730 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_814 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_816 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_818 ∷ T_IsBooleanAlgebra_730 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_820 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_822 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_826 ∷ T_IsBooleanAlgebra_730 → T_IsPartialEquivalence_16 Source #

d_refl_828 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny Source #

d_reflexive_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_830 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_832 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_834 ∷ T_IsBooleanAlgebra_730 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #