Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Relation.Binary.Lattice.Structures

Documentation

d_IsJoinSemilattice_22 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsJoinSemilattice_22 #

Constructors

C_IsJoinSemilattice'46'constructor_527 T_IsPartialOrder_174 (AgdaAny -> AgdaAny -> T_Σ_14)

d_isPartialOrder_30 :: T_IsJoinSemilattice_22 -> T_IsPartialOrder_174 #

d_supremum_32 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> T_Σ_14 #

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 #

du_x'8804'x'8744'y_38 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_50 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

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

d_antisym_76 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_78 :: T_IsJoinSemilattice_22 -> T_IsEquivalence_26 #

d_isPreorder_80 :: T_IsJoinSemilattice_22 -> T_IsPreorder_70 #

d_refl_82 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny #

du_refl_82 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny #

d_reflexive_84 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_86 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_88 :: T_IsJoinSemilattice_22 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_90 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_92 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_94 :: T_IsJoinSemilattice_22 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_96 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_98 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_102 :: T_IsJoinSemilattice_22 -> T_IsPartialEquivalence_16 #

d_refl_104 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_106 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_108 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_110 :: T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBoundedJoinSemilattice_116 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBoundedJoinSemilattice_116 #

Constructors

C_IsBoundedJoinSemilattice'46'constructor_5215 T_IsJoinSemilattice_22 (AgdaAny -> AgdaAny)

d_isJoinSemilattice_126 :: T_IsBoundedJoinSemilattice_116 -> T_IsJoinSemilattice_22 #

d_minimum_128 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny #

d_antisym_132 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_134 :: T_IsBoundedJoinSemilattice_116 -> T_IsEquivalence_26 #

d_isPartialOrder_136 :: T_IsBoundedJoinSemilattice_116 -> T_IsPartialOrder_174 #

d_isPreorder_138 :: T_IsBoundedJoinSemilattice_116 -> T_IsPreorder_70 #

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 #

du_refl_140 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny #

d_reflexive_142 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_144 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_146 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8804'x'8744'y_148 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_150 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'least_152 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_154 :: T_IsBoundedJoinSemilattice_116 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_156 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_158 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_160 :: T_IsBoundedJoinSemilattice_116 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_162 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_164 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_168 :: T_IsBoundedJoinSemilattice_116 -> T_IsPartialEquivalence_16 #

d_refl_170 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_172 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_174 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_176 :: T_IsBoundedJoinSemilattice_116 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMeetSemilattice_180 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMeetSemilattice_180 #

Constructors

C_IsMeetSemilattice'46'constructor_7577 T_IsPartialOrder_174 (AgdaAny -> AgdaAny -> T_Σ_14)

d_isPartialOrder_188 :: T_IsMeetSemilattice_180 -> T_IsPartialOrder_174 #

d_infimum_190 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> T_Σ_14 #

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 #

du_x'8743'y'8804'x_196 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_208 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_222 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_234 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_236 :: T_IsMeetSemilattice_180 -> T_IsEquivalence_26 #

d_isPreorder_238 :: T_IsMeetSemilattice_180 -> T_IsPreorder_70 #

d_refl_240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny #

du_refl_240 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny #

d_reflexive_242 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_244 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_246 :: T_IsMeetSemilattice_180 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_248 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_250 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_252 :: T_IsMeetSemilattice_180 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_254 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_256 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_260 :: T_IsMeetSemilattice_180 -> T_IsPartialEquivalence_16 #

d_refl_262 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_264 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_266 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_268 :: T_IsMeetSemilattice_180 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBoundedMeetSemilattice_274 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBoundedMeetSemilattice_274 #

Constructors

C_IsBoundedMeetSemilattice'46'constructor_12265 T_IsMeetSemilattice_180 (AgdaAny -> AgdaAny)

d_isMeetSemilattice_284 :: T_IsBoundedMeetSemilattice_274 -> T_IsMeetSemilattice_180 #

d_maximum_286 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny #

d_antisym_290 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_292 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_294 :: T_IsBoundedMeetSemilattice_274 -> T_IsEquivalence_26 #

d_isPartialOrder_296 :: T_IsBoundedMeetSemilattice_274 -> T_IsPartialOrder_174 #

d_isPreorder_298 :: T_IsBoundedMeetSemilattice_274 -> T_IsPreorder_70 #

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 #

du_refl_300 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny #

d_reflexive_302 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_304 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'x_306 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_308 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_310 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_312 :: T_IsBoundedMeetSemilattice_274 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_314 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_316 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_318 :: T_IsBoundedMeetSemilattice_274 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_320 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_322 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_326 :: T_IsBoundedMeetSemilattice_274 -> T_IsPartialEquivalence_16 #

d_refl_328 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_330 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_332 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_334 :: T_IsBoundedMeetSemilattice_274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsLattice_340 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsLattice_340 #

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 #

d_supremum_354 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_infimum_356 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> T_Σ_14 #

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 #

du_isJoinSemilattice_358 :: T_IsLattice_340 -> T_IsJoinSemilattice_22 #

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 #

du_isMeetSemilattice_360 :: T_IsLattice_340 -> T_IsMeetSemilattice_180 #

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 #

du_x'8804'x'8744'y_364 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_366 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'least_368 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'x_372 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_374 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_376 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_380 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_382 :: T_IsLattice_340 -> T_IsEquivalence_26 #

d_isPreorder_384 :: T_IsLattice_340 -> T_IsPreorder_70 #

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 #

du_refl_386 :: T_IsLattice_340 -> AgdaAny -> AgdaAny #

d_reflexive_388 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_390 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_392 :: T_IsLattice_340 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_394 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_396 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_398 :: T_IsLattice_340 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_400 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_402 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_406 :: T_IsLattice_340 -> T_IsPartialEquivalence_16 #

d_refl_408 :: T_IsLattice_340 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_410 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_412 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_414 :: T_IsLattice_340 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsDistributiveLattice_420 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsDistributiveLattice_420 #

Constructors

C_IsDistributiveLattice'46'constructor_18193 T_IsLattice_340 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isLattice_430 :: T_IsDistributiveLattice_420 -> T_IsLattice_340 #

d_'8743''45'distrib'737''45''8744'_432 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_436 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_438 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_440 :: T_IsDistributiveLattice_420 -> T_IsEquivalence_26 #

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 #

du_isJoinSemilattice_442 :: T_IsDistributiveLattice_420 -> T_IsJoinSemilattice_22 #

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 #

du_isMeetSemilattice_444 :: T_IsDistributiveLattice_420 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_446 :: T_IsDistributiveLattice_420 -> T_IsPartialOrder_174 #

d_isPreorder_448 :: T_IsDistributiveLattice_420 -> T_IsPreorder_70 #

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 #

du_refl_450 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny #

d_reflexive_452 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_454 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_456 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'x_458 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_460 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8804'x'8744'y_462 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_464 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_466 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'least_468 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_470 :: T_IsDistributiveLattice_420 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_472 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_474 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_476 :: T_IsDistributiveLattice_420 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_478 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_480 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_484 :: T_IsDistributiveLattice_420 -> T_IsPartialEquivalence_16 #

d_refl_486 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_488 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_490 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_492 :: T_IsDistributiveLattice_420 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBoundedLattice_502 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBoundedLattice_502 #

Constructors

C_IsBoundedLattice'46'constructor_21319 T_IsLattice_340 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_isLattice_518 :: T_IsBoundedLattice_502 -> T_IsLattice_340 #

d_maximum_520 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny #

d_minimum_522 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny #

d_antisym_526 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_528 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_isEquivalence_530 :: T_IsBoundedLattice_502 -> T_IsEquivalence_26 #

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 #

du_isJoinSemilattice_532 :: T_IsBoundedLattice_502 -> T_IsJoinSemilattice_22 #

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 #

du_isMeetSemilattice_534 :: T_IsBoundedLattice_502 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_536 :: T_IsBoundedLattice_502 -> T_IsPartialOrder_174 #

d_isPreorder_538 :: T_IsBoundedLattice_502 -> T_IsPreorder_70 #

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 #

du_refl_540 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny #

d_reflexive_542 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_544 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_546 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'x_548 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_550 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8804'x'8744'y_552 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_554 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_556 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'least_558 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_560 :: T_IsBoundedLattice_502 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_562 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_564 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_566 :: T_IsBoundedLattice_502 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_568 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_570 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_574 :: T_IsBoundedLattice_502 -> T_IsPartialEquivalence_16 #

d_refl_576 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_578 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_580 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_582 :: T_IsBoundedLattice_502 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isBoundedJoinSemilattice_584 :: T_IsBoundedLattice_502 -> T_IsBoundedJoinSemilattice_116 #

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 #

du_isBoundedMeetSemilattice_586 :: T_IsBoundedLattice_502 -> T_IsBoundedMeetSemilattice_274 #

d_IsHeytingAlgebra_598 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsHeytingAlgebra_598 #

Constructors

C_IsHeytingAlgebra'46'constructor_25303 T_IsBoundedLattice_502 (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)

d_isBoundedLattice_614 :: T_IsHeytingAlgebra_598 -> T_IsBoundedLattice_502 #

d_exponential_616 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 #

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 #

du_transpose'45''8680'_624 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_transpose'45''8743'_640 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_antisym_652 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_infimum_654 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> T_Σ_14 #

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 #

du_isBoundedJoinSemilattice_656 :: T_IsHeytingAlgebra_598 -> T_IsBoundedJoinSemilattice_116 #

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 #

du_isBoundedMeetSemilattice_658 :: T_IsHeytingAlgebra_598 -> T_IsBoundedMeetSemilattice_274 #

d_isEquivalence_660 :: T_IsHeytingAlgebra_598 -> T_IsEquivalence_26 #

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 #

du_isJoinSemilattice_662 :: T_IsHeytingAlgebra_598 -> T_IsJoinSemilattice_22 #

d_isLattice_664 :: T_IsHeytingAlgebra_598 -> T_IsLattice_340 #

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 #

du_isMeetSemilattice_666 :: T_IsHeytingAlgebra_598 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_668 :: T_IsHeytingAlgebra_598 -> T_IsPartialOrder_174 #

d_isPreorder_670 :: T_IsHeytingAlgebra_598 -> T_IsPreorder_70 #

d_maximum_672 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny #

d_minimum_674 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny #

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 #

du_refl_676 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny #

d_reflexive_678 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_680 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_682 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'x_684 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_686 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8804'x'8744'y_688 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_690 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_692 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'least_694 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_696 :: T_IsHeytingAlgebra_598 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_698 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_700 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_702 :: T_IsHeytingAlgebra_598 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_704 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_706 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_710 :: T_IsHeytingAlgebra_598 -> T_IsPartialEquivalence_16 #

d_refl_712 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_714 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_716 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_718 :: T_IsHeytingAlgebra_598 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBooleanAlgebra_730 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

newtype T_IsBooleanAlgebra_730 #

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 #

du__'8680'__750 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

d_isHeytingAlgebra_756 :: T_IsBooleanAlgebra_730 -> T_IsHeytingAlgebra_598 #

d_antisym_760 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_exponential_762 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_infimum_764 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> T_Σ_14 #

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 #

du_isBoundedJoinSemilattice_766 :: T_IsBooleanAlgebra_730 -> T_IsBoundedJoinSemilattice_116 #

d_isBoundedLattice_768 :: T_IsBooleanAlgebra_730 -> T_IsBoundedLattice_502 #

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 #

du_isBoundedMeetSemilattice_770 :: T_IsBooleanAlgebra_730 -> T_IsBoundedMeetSemilattice_274 #

d_isEquivalence_772 :: T_IsBooleanAlgebra_730 -> T_IsEquivalence_26 #

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 #

du_isJoinSemilattice_774 :: T_IsBooleanAlgebra_730 -> T_IsJoinSemilattice_22 #

d_isLattice_776 :: T_IsBooleanAlgebra_730 -> T_IsLattice_340 #

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 #

du_isMeetSemilattice_778 :: T_IsBooleanAlgebra_730 -> T_IsMeetSemilattice_180 #

d_isPartialOrder_780 :: T_IsBooleanAlgebra_730 -> T_IsPartialOrder_174 #

d_isPreorder_782 :: T_IsBooleanAlgebra_730 -> T_IsPreorder_70 #

d_maximum_784 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny #

d_minimum_786 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny #

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 #

du_refl_788 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny #

d_reflexive_790 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_792 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_trans_794 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_transpose'45''8680'_796 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_transpose'45''8743'_798 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'x_800 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8743'y'8804'y_802 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_x'8804'x'8744'y_804 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_y'8804'x'8744'y_806 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'greatest_808 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'least_810 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'45''8776'_812 :: T_IsBooleanAlgebra_730 -> T_Σ_14 #

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 #

du_'8764''45'resp'691''45''8776'_814 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8764''45'resp'737''45''8776'_816 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'45''8776'_818 :: T_IsBooleanAlgebra_730 -> T_Σ_14 #

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 #

du_'8818''45'resp'691''45''8776'_820 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8818''45'resp'737''45''8776'_822 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_isPartialEquivalence_826 :: T_IsBooleanAlgebra_730 -> T_IsPartialEquivalence_16 #

d_refl_828 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_830 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_832 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_834 :: T_IsBooleanAlgebra_730 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #