Documentation

d__Absorbs__16 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver__18 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__20 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__22 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Absorptive_28 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_38 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_42 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8321'_44 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_46 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_62 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftCongruent_74 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_86 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightCongruent_104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_116 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsCommutativeBand_162 ∷ p → p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_198 ∷ p → p → p → p → p → p → () Source #

d_isPartialEquivalence_424 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_424 ∷ T_IsBand_526 → T_IsPartialEquivalence_16 Source #

d_reflexive_430 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_430 ∷ T_IsBand_526 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_432 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_Setoid_46 Source #

du_setoid_432 ∷ T_IsBand_526 → T_Setoid_46 Source #

d_'8729''45'cong'691'_440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_440 ∷ T_IsBand_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_442 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_442 ∷ T_IsBand_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_550 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_554 ∷ T_IsCommutativeBand_612 → T_IsBand_526 Source #

d_idem_1072 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_identity'691'_1076 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'691'_1076 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_identity'737'_1078 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'737'_1078 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_isBand_1080 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

du_isBand_1080 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

d_isCommutativeBand_1082 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_1082 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

d_isCommutativeMagma_1084 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_1084 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_1086 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_1088 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_1088 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

d_isIdempotentMonoid_1092 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsIdempotentMonoid_826 Source #

du_isIdempotentMonoid_1092 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsIdempotentMonoid_826 Source #

d_isPartialEquivalence_1098 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1098 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1102 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1102 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

d_reflexive_1106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1106 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1108 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

du_setoid_1108 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

d_'8729''45'cong'691'_1116 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1116 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1118 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1118 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemilattice_2766 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_comm_2776 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_2778 ∷ T_IsCommutativeBand_612 → T_IsBand_526 Source #

d_assoc_2782 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2782 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2784 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

du_idem_2784 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

d_isEquivalence_2786 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

du_isEquivalence_2786 ∷ T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

d_isMagma_2788 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsMagma_178 Source #

du_isMagma_2788 ∷ T_IsCommutativeBand_612 → T_IsMagma_178 Source #

d_isPartialEquivalence_2790 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2790 ∷ T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2792 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

du_isSemigroup_2792 ∷ T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

d_refl_2794 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

du_refl_2794 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

d_reflexive_2796 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2796 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2798 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_Setoid_46 Source #

du_setoid_2798 ∷ T_IsCommutativeBand_612 → T_Setoid_46 Source #

d_sym_2800 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2800 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2802 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2802 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2804 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2804 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2806 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2806 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2808 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2808 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMeetSemilattice_2810 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_assoc_2820 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2820 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2822 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2824 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

du_idem_2824 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

d_isBand_2826 ∷ T_IsCommutativeBand_612 → T_IsBand_526 Source #

d_isEquivalence_2828 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

du_isEquivalence_2828 ∷ T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

d_isMagma_2830 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsMagma_178 Source #

du_isMagma_2830 ∷ T_IsCommutativeBand_612 → T_IsMagma_178 Source #

d_isPartialEquivalence_2832 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2832 ∷ T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2834 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

du_isSemigroup_2834 ∷ T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

d_refl_2836 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

du_refl_2836 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

d_reflexive_2838 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2838 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2840 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_Setoid_46 Source #

du_setoid_2840 ∷ T_IsCommutativeBand_612 → T_Setoid_46 Source #

d_sym_2842 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2842 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2844 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2844 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2846 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2846 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2848 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2848 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2850 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2850 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsJoinSemilattice_2852 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_assoc_2862 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2862 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2864 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2866 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

du_idem_2866 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

d_isBand_2868 ∷ T_IsCommutativeBand_612 → T_IsBand_526 Source #

d_isEquivalence_2870 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

du_isEquivalence_2870 ∷ T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

d_isMagma_2872 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsMagma_178 Source #

du_isMagma_2872 ∷ T_IsCommutativeBand_612 → T_IsMagma_178 Source #

d_isPartialEquivalence_2874 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2874 ∷ T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2876 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

du_isSemigroup_2876 ∷ T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

d_refl_2878 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

du_refl_2878 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny Source #

d_reflexive_2880 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2880 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2882 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_Setoid_46 Source #

du_setoid_2882 ∷ T_IsCommutativeBand_612 → T_Setoid_46 Source #

d_sym_2884 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2884 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2886 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2886 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2888 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2888 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2890 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2890 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2892 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2892 ∷ T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedSemilattice_2894 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → () Source #

d_assoc_2906 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2908 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2910 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_identity_2912 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Σ_14 Source #

d_identity'691'_2914 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'691'_2914 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_identity'737'_2916 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'737'_2916 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_isBand_2918 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

du_isBand_2918 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

d_isCommutativeMagma_2920 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_2920 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_2922 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_2924 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_2924 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_2926 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

d_isIdempotentMonoid_2928 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsIdempotentMonoid_826 Source #

du_isIdempotentMonoid_2928 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsIdempotentMonoid_826 Source #

d_isMagma_2930 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

d_isMonoid_2932 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMonoid_712 Source #

d_isPartialEquivalence_2934 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2934 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2936 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

d_isCommutativeBand_2938 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_2938 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

d_isUnitalMagma_2940 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_2940 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

d_refl_2942 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_reflexive_2944 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2944 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2946 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

du_setoid_2946 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

d_sym_2948 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2950 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2952 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2954 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2954 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2956 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2956 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedMeetSemilattice_2958 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → () Source #

d_identity_2970 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Σ_14 Source #

d_identity'691'_2972 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'691'_2972 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_identity'737'_2974 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'737'_2974 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_isCommutativeBand_2976 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_2976 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

d_assoc_2980 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2980 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2982 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_2982 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2984 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_idem_2984 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_isBand_2986 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

du_isBand_2986 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

d_isEquivalence_2988 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

du_isEquivalence_2988 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

d_isMagma_2990 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

du_isMagma_2990 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

d_isPartialEquivalence_2992 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2992 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2994 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

du_isSemigroup_2994 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

d_refl_2996 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_refl_2996 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_reflexive_2998 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2998 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_3000 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

du_setoid_3000 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

d_sym_3002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_3002 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3004 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_3004 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_3006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_3006 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_3008 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_3008 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3010 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_3010 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedJoinSemilattice_3012 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → () Source #

d_identity_3024 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Σ_14 Source #

d_identity'691'_3026 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'691'_3026 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_identity'737'_3028 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_identity'737'_3028 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_isCommutativeBand_3030 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_3030 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

d_assoc_3034 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_3034 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_3036 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_3036 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_3038 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_idem_3038 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_isBand_3040 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

du_isBand_3040 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

d_isEquivalence_3042 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

du_isEquivalence_3042 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

d_isMagma_3044 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

du_isMagma_3044 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

d_isPartialEquivalence_3046 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3046 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_3048 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

du_isSemigroup_3048 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

d_refl_3050 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

du_refl_3050 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny Source #

d_reflexive_3052 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3052 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_3054 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

du_setoid_3054 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

d_sym_3056 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_3056 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3058 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_3058 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_3060 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_3060 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_3062 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_3062 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3064 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_3064 ∷ T_IsIdempotentCommutativeMonoid_884 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsLattice_3070 ∷ p → p → p → p → p → p → () Source #

data T_IsLattice_3070 Source #

d_isEquivalence_3092 ∷ T_IsLattice_3070 → T_IsEquivalence_28 Source #

d_'8744''45'comm_3094 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_3096 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_3098 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_3100 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_3102 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_3104 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_3106 ∷ T_IsLattice_3070 → T_Σ_14 Source #

d_isPartialEquivalence_3110 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3110 ∷ T_IsLattice_3070 → T_IsPartialEquivalence_16 Source #

d_refl_3112 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny Source #

d_reflexive_3114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3114 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_3116 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3118 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_3120 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_3120 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_3122 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_3122 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_3124 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_3124 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_3128 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_3128 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_3132 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_3132 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_3136 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_3136 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_3146 ∷ p → p → p → p → p → p → () Source #

data T_IsDistributiveLattice_3146 Source #

d_isLattice_3158 ∷ T_IsDistributiveLattice_3146 → T_IsLattice_3070 Source #

d_'8744''45'distrib'45''8743'_3160 ∷ T_IsDistributiveLattice_3146 → T_Σ_14 Source #

d_'8743''45'distrib'45''8744'_3162 ∷ T_IsDistributiveLattice_3146 → T_Σ_14 Source #

d_absorptive_3166 ∷ T_IsDistributiveLattice_3146 → T_Σ_14 Source #

d_isEquivalence_3168 ∷ T_IsDistributiveLattice_3146 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_3170 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3170 ∷ T_IsDistributiveLattice_3146 → T_IsPartialEquivalence_16 Source #

d_refl_3172 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny Source #

d_reflexive_3174 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3174 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_3176 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3178 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_3180 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_3180 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_3182 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_3184 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_3186 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_3188 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_3188 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_3190 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_3190 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_3192 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_3192 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_3194 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_3196 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_3198 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_3200 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_3200 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_3202 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_3202 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_3204 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_3204 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'691''45''8743'_3206 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_3206 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_3208 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_3208 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'691''45''8744'_3210 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_3210 ∷ T_IsDistributiveLattice_3146 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBooleanAlgebra_3224 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsBooleanAlgebra_3224 Source #

d_isDistributiveLattice_3244 ∷ T_IsBooleanAlgebra_3224 → T_IsDistributiveLattice_3146 Source #

d_'8744''45'complement_3246 ∷ T_IsBooleanAlgebra_3224 → T_Σ_14 Source #

d_'8743''45'complement_3248 ∷ T_IsBooleanAlgebra_3224 → T_Σ_14 Source #

d_'172''45'cong_3250 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_3254 ∷ T_IsBooleanAlgebra_3224 → T_Σ_14 Source #

d_isEquivalence_3256 ∷ T_IsBooleanAlgebra_3224 → T_IsEquivalence_28 Source #

d_isLattice_3258 ∷ T_IsBooleanAlgebra_3224 → T_IsLattice_3070 Source #

d_isPartialEquivalence_3260 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3260 ∷ T_IsBooleanAlgebra_3224 → T_IsPartialEquivalence_16 Source #

d_refl_3262 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

d_reflexive_3264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3264 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_3266 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3268 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_3270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_3270 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_3272 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_3274 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_3276 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_3278 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_3278 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_3280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_3280 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_3282 ∷ T_IsBooleanAlgebra_3224 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_3284 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_3284 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_3286 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_3286 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_3288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_3288 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_3290 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_3292 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_3294 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_3296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_3296 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_3298 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_3298 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_3300 ∷ T_IsBooleanAlgebra_3224 → T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_3302 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_3302 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_3304 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_3304 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'complement'737'_3306 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'737'_3306 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

d_'8744''45'complement'691'_3308 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'691'_3308 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'737'_3310 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'737'_3310 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'691'_3312 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'691'_3312 ∷ T_IsBooleanAlgebra_3224 → AgdaAny → AgdaAny Source #