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_constructor_112 T_IsPartialOrder_248 (AgdaAny → AgdaAny → T_Σ_14)

d_isPartialOrder_30 ∷ T_IsJoinSemilattice_22 → T_IsPartialOrder_248 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_28 Source #

d_isPreorder_80 ∷ T_IsJoinSemilattice_22 → T_IsPreorder_76 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_118 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedJoinSemilattice_118 Source #

Constructors

C_constructor_180 T_IsJoinSemilattice_22 (AgdaAny → AgdaAny)

d_isJoinSemilattice_128 ∷ T_IsBoundedJoinSemilattice_118 → T_IsJoinSemilattice_22 Source #

d_minimum_130 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny Source #

d_antisym_134 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_136 ∷ T_IsBoundedJoinSemilattice_118 → T_IsEquivalence_28 Source #

d_isPartialOrder_138 ∷ T_IsBoundedJoinSemilattice_118 → T_IsPartialOrder_248 Source #

d_isPreorder_140 ∷ T_IsBoundedJoinSemilattice_118 → T_IsPreorder_76 Source #

d_refl_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny Source #

du_refl_142 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny Source #

d_reflexive_144 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_146 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_148 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_150 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_152 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_154 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_156 ∷ T_IsBoundedJoinSemilattice_118 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_158 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_160 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_162 ∷ T_IsBoundedJoinSemilattice_118 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_164 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_166 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_170 ∷ T_IsBoundedJoinSemilattice_118 → T_IsPartialEquivalence_16 Source #

d_refl_172 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny Source #

d_reflexive_174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_174 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_176 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_178 ∷ T_IsBoundedJoinSemilattice_118 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMeetSemilattice_184 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMeetSemilattice_184 Source #

Constructors

C_constructor_274 T_IsPartialOrder_248 (AgdaAny → AgdaAny → T_Σ_14)

d_isPartialOrder_192 ∷ T_IsMeetSemilattice_184 → T_IsPartialOrder_248 Source #

d_infimum_194 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_x'8743'y'8804'x_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_200 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_212 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_226 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_238 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_240 ∷ T_IsMeetSemilattice_184 → T_IsEquivalence_28 Source #

d_isPreorder_242 ∷ T_IsMeetSemilattice_184 → T_IsPreorder_76 Source #

d_refl_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny Source #

du_refl_244 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny Source #

d_reflexive_246 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_248 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_250 ∷ T_IsMeetSemilattice_184 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_252 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_254 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_256 ∷ T_IsMeetSemilattice_184 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_258 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_260 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_264 ∷ T_IsMeetSemilattice_184 → T_IsPartialEquivalence_16 Source #

d_refl_266 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny Source #

d_reflexive_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_268 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_270 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_272 ∷ T_IsMeetSemilattice_184 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedMeetSemilattice_280 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedMeetSemilattice_280 Source #

Constructors

C_constructor_342 T_IsMeetSemilattice_184 (AgdaAny → AgdaAny)

d_isMeetSemilattice_290 ∷ T_IsBoundedMeetSemilattice_280 → T_IsMeetSemilattice_184 Source #

d_maximum_292 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny Source #

d_antisym_296 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_298 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_300 ∷ T_IsBoundedMeetSemilattice_280 → T_IsEquivalence_28 Source #

d_isPartialOrder_302 ∷ T_IsBoundedMeetSemilattice_280 → T_IsPartialOrder_248 Source #

d_isPreorder_304 ∷ T_IsBoundedMeetSemilattice_280 → T_IsPreorder_76 Source #

d_refl_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny Source #

du_refl_306 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny Source #

d_reflexive_308 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_310 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_312 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_314 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_316 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_318 ∷ T_IsBoundedMeetSemilattice_280 → T_Σ_14 Source #

d_'8764''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_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_320 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''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_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_322 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_324 ∷ T_IsBoundedMeetSemilattice_280 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_326 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_328 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_332 ∷ T_IsBoundedMeetSemilattice_280 → T_IsPartialEquivalence_16 Source #

d_refl_334 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny Source #

d_reflexive_336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_336 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_338 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_340 ∷ T_IsBoundedMeetSemilattice_280 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsLattice_348 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsLattice_348 Source #

Constructors

C_constructor_424 T_IsPartialOrder_248 (AgdaAny → AgdaAny → T_Σ_14) (AgdaAny → AgdaAny → T_Σ_14)

d_isPartialOrder_360 ∷ T_IsLattice_348 → T_IsPartialOrder_248 Source #

d_supremum_362 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_364 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isJoinSemilattice_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_366 ∷ T_IsLattice_348 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_368 ∷ T_IsLattice_348 → T_IsMeetSemilattice_184 Source #

d_x'8804'x'8744'y_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_372 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_374 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_376 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_380 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_382 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_384 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_388 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_390 ∷ T_IsLattice_348 → T_IsEquivalence_28 Source #

d_isPreorder_392 ∷ T_IsLattice_348 → T_IsPreorder_76 Source #

d_refl_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny Source #

du_refl_394 ∷ T_IsLattice_348 → AgdaAny → AgdaAny Source #

d_reflexive_396 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_398 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_400 ∷ T_IsLattice_348 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_402 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_404 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_406 ∷ T_IsLattice_348 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_408 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_410 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_410 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_414 ∷ T_IsLattice_348 → T_IsPartialEquivalence_16 Source #

d_refl_416 ∷ T_IsLattice_348 → AgdaAny → AgdaAny Source #

d_reflexive_418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_348 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_418 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_420 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_422 ∷ T_IsLattice_348 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_430 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsDistributiveLattice_430 Source #

Constructors

C_constructor_504 T_IsLattice_348 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isLattice_440 ∷ T_IsDistributiveLattice_430 → T_IsLattice_348 Source #

d_'8743''45'distrib'737''45''8744'_442 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_446 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_448 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_450 ∷ T_IsDistributiveLattice_430 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_452 ∷ T_IsDistributiveLattice_430 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_454 ∷ T_IsDistributiveLattice_430 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_456 ∷ T_IsDistributiveLattice_430 → T_IsPartialOrder_248 Source #

d_isPreorder_458 ∷ T_IsDistributiveLattice_430 → T_IsPreorder_76 Source #

d_refl_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny Source #

du_refl_460 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny Source #

d_reflexive_462 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_464 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_466 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_468 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_470 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_472 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_474 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_476 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_478 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_480 ∷ T_IsDistributiveLattice_430 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_482 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_484 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_486 ∷ T_IsDistributiveLattice_430 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_488 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_490 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_494 ∷ T_IsDistributiveLattice_430 → T_IsPartialEquivalence_16 Source #

d_refl_496 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny Source #

d_reflexive_498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_498 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_500 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_502 ∷ T_IsDistributiveLattice_430 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedLattice_514 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedLattice_514 Source #

Constructors

C_constructor_600 T_IsLattice_348 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

d_isLattice_530 ∷ T_IsBoundedLattice_514 → T_IsLattice_348 Source #

d_maximum_532 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny Source #

d_minimum_534 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny Source #

d_antisym_538 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_540 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_542 ∷ T_IsBoundedLattice_514 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_544 ∷ T_IsBoundedLattice_514 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_546 ∷ T_IsBoundedLattice_514 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_548 ∷ T_IsBoundedLattice_514 → T_IsPartialOrder_248 Source #

d_isPreorder_550 ∷ T_IsBoundedLattice_514 → T_IsPreorder_76 Source #

d_refl_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny Source #

du_refl_552 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny Source #

d_reflexive_554 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_556 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_558 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_560 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_562 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_564 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_566 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_568 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_570 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8764''45'resp'45''8776'_572 ∷ T_IsBoundedLattice_514 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_574 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_576 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_'8818''45'resp'45''8776'_578 ∷ T_IsBoundedLattice_514 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_580 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_582 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_586 ∷ T_IsBoundedLattice_514 → T_IsPartialEquivalence_16 Source #

d_refl_588 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny Source #

d_reflexive_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_590 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_592 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_594 ∷ T_IsBoundedLattice_514 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isBoundedJoinSemilattice_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → T_IsBoundedJoinSemilattice_118 Source #

du_isBoundedJoinSemilattice_596 ∷ T_IsBoundedLattice_514 → T_IsBoundedJoinSemilattice_118 Source #

d_isBoundedMeetSemilattice_598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_514 → T_IsBoundedMeetSemilattice_280 Source #

du_isBoundedMeetSemilattice_598 ∷ T_IsBoundedLattice_514 → T_IsBoundedMeetSemilattice_280 Source #

d_IsHeytingAlgebra_612 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsHeytingAlgebra_612 Source #

Constructors

C_constructor_734 T_IsBoundedLattice_514 (AgdaAny → AgdaAny → AgdaAny → T_Σ_14)

d_isBoundedLattice_628 ∷ T_IsHeytingAlgebra_612 → T_IsBoundedLattice_514 Source #

d_exponential_630 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_transpose'45''8680'_638 ∷ 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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_638 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_654 ∷ 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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_654 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_666 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_668 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_670 ∷ 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_612 → T_IsBoundedJoinSemilattice_118 Source #

du_isBoundedJoinSemilattice_670 ∷ T_IsHeytingAlgebra_612 → T_IsBoundedJoinSemilattice_118 Source #

d_isBoundedMeetSemilattice_672 ∷ 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_612 → T_IsBoundedMeetSemilattice_280 Source #

du_isBoundedMeetSemilattice_672 ∷ T_IsHeytingAlgebra_612 → T_IsBoundedMeetSemilattice_280 Source #

d_isEquivalence_674 ∷ T_IsHeytingAlgebra_612 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_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_612 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_676 ∷ T_IsHeytingAlgebra_612 → T_IsJoinSemilattice_22 Source #

d_isLattice_678 ∷ T_IsHeytingAlgebra_612 → T_IsLattice_348 Source #

d_isMeetSemilattice_680 ∷ 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_612 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_680 ∷ T_IsHeytingAlgebra_612 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_682 ∷ T_IsHeytingAlgebra_612 → T_IsPartialOrder_248 Source #

d_isPreorder_684 ∷ T_IsHeytingAlgebra_612 → T_IsPreorder_76 Source #

d_maximum_686 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny Source #

d_minimum_688 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny Source #

d_refl_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_612 → AgdaAny → AgdaAny Source #

du_refl_690 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny Source #

d_reflexive_692 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_694 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_696 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_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_612 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_698 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_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_612 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_700 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_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_612 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_702 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_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_612 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_704 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_706 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_708 ∷ 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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_708 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_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_612 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_710 ∷ T_IsHeytingAlgebra_612 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_712 ∷ 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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_712 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_714 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_716 ∷ 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_612 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_716 ∷ T_IsHeytingAlgebra_612 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_718 ∷ 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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_718 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_720 ∷ 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_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_720 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_724 ∷ 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_612 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_724 ∷ T_IsHeytingAlgebra_612 → T_IsPartialEquivalence_16 Source #

d_refl_726 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny Source #

d_reflexive_728 ∷ 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_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_728 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_730 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_732 ∷ T_IsHeytingAlgebra_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBooleanAlgebra_746 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

newtype T_IsBooleanAlgebra_746 Source #

Constructors

C_constructor_852 T_IsHeytingAlgebra_612

d__'8680'__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_746 → AgdaAny → AgdaAny → AgdaAny Source #

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

d_isHeytingAlgebra_772 ∷ T_IsBooleanAlgebra_746 → T_IsHeytingAlgebra_612 Source #

d_antisym_776 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_exponential_778 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_780 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_782 ∷ 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_746 → T_IsBoundedJoinSemilattice_118 Source #

du_isBoundedJoinSemilattice_782 ∷ T_IsBooleanAlgebra_746 → T_IsBoundedJoinSemilattice_118 Source #

d_isBoundedLattice_784 ∷ T_IsBooleanAlgebra_746 → T_IsBoundedLattice_514 Source #

d_isBoundedMeetSemilattice_786 ∷ 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_746 → T_IsBoundedMeetSemilattice_280 Source #

du_isBoundedMeetSemilattice_786 ∷ T_IsBooleanAlgebra_746 → T_IsBoundedMeetSemilattice_280 Source #

d_isEquivalence_788 ∷ T_IsBooleanAlgebra_746 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_790 ∷ 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_746 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_790 ∷ T_IsBooleanAlgebra_746 → T_IsJoinSemilattice_22 Source #

d_isLattice_792 ∷ T_IsBooleanAlgebra_746 → T_IsLattice_348 Source #

d_isMeetSemilattice_794 ∷ 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_746 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_794 ∷ T_IsBooleanAlgebra_746 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_796 ∷ T_IsBooleanAlgebra_746 → T_IsPartialOrder_248 Source #

d_isPreorder_798 ∷ T_IsBooleanAlgebra_746 → T_IsPreorder_76 Source #

d_maximum_800 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny Source #

d_minimum_802 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny Source #

d_refl_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_746 → AgdaAny → AgdaAny Source #

du_refl_804 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny Source #

d_reflexive_806 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_808 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_810 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8680'_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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_812 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_814 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_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_746 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_816 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_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_746 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_818 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_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_746 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_820 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_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_746 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_822 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_824 ∷ 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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_824 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_826 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_828 ∷ 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_746 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_828 ∷ T_IsBooleanAlgebra_746 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_830 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_832 ∷ 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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_832 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_834 ∷ 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_746 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_834 ∷ T_IsBooleanAlgebra_746 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_836 ∷ 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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_836 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_838 ∷ 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_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_838 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_842 ∷ 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_746 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_842 ∷ T_IsBooleanAlgebra_746 → T_IsPartialEquivalence_16 Source #

d_refl_844 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny Source #

d_reflexive_846 ∷ 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_746 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_846 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_848 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_850 ∷ T_IsBooleanAlgebra_746 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #