Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Lattice.Structures

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_154 ∷ p → p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_172 ∷ p → p → p → p → p → p → () Source #

d_isPartialEquivalence_338 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_338 ∷ T_IsBand_508 → T_IsPartialEquivalence_16 Source #

d_reflexive_344 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_344 ∷ T_IsBand_508 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_346 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_Setoid_44 Source #

du_setoid_346 ∷ T_IsBand_508 → T_Setoid_44 Source #

d_'8729''45'cong'691'_354 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_354 ∷ T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_356 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_356 ∷ T_IsBand_508 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_464 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_468 ∷ T_IsCommutativeBand_590 → T_IsBand_508 Source #

d_idem_976 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_identity'691'_980 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'691'_980 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_identity'737'_982 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'737'_982 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_isBand_984 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

du_isBand_984 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

d_isCommutativeBand_986 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_986 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

d_isCommutativeMagma_988 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_988 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMagma_212 Source #

d_isCommutativeMonoid_990 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMonoid_736 Source #

d_isCommutativeSemigroup_992 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_992 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeSemigroup_548 Source #

d_isIdempotentMonoid_996 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsIdempotentMonoid_796 Source #

du_isIdempotentMonoid_996 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsIdempotentMonoid_796 Source #

d_isPartialEquivalence_1002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1002 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_1006 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsUnitalMagma_642 Source #

d_reflexive_1010 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1010 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1012 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

du_setoid_1012 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

d_'8729''45'cong'691'_1020 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1020 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1022 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1022 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_comm_2668 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #

d_isBand_2670 ∷ T_IsCommutativeBand_590 → T_IsBand_508 Source #

d_assoc_2674 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2674 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2676 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

du_idem_2676 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_isEquivalence_2678 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

du_isEquivalence_2678 ∷ T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

d_isMagma_2680 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsMagma_176 Source #

du_isMagma_2680 ∷ T_IsCommutativeBand_590 → T_IsMagma_176 Source #

d_isPartialEquivalence_2682 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2682 ∷ T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2684 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

du_isSemigroup_2684 ∷ T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

d_refl_2686 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

du_refl_2686 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_reflexive_2688 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2688 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2690 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_Setoid_44 Source #

du_setoid_2690 ∷ T_IsCommutativeBand_590 → T_Setoid_44 Source #

d_sym_2692 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2692 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2694 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2694 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2696 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2696 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2698 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2698 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2700 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2700 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_2712 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2712 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2714 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2716 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

du_idem_2716 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_isBand_2718 ∷ T_IsCommutativeBand_590 → T_IsBand_508 Source #

d_isEquivalence_2720 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

du_isEquivalence_2720 ∷ T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

d_isMagma_2722 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsMagma_176 Source #

du_isMagma_2722 ∷ T_IsCommutativeBand_590 → T_IsMagma_176 Source #

d_isPartialEquivalence_2724 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2724 ∷ T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2726 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

du_isSemigroup_2726 ∷ T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

d_refl_2728 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

du_refl_2728 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_reflexive_2730 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2730 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2732 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_Setoid_44 Source #

du_setoid_2732 ∷ T_IsCommutativeBand_590 → T_Setoid_44 Source #

d_sym_2734 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2734 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2736 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2736 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2738 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2738 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2740 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2740 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2742 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_2754 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2754 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2756 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2758 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

du_idem_2758 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_isBand_2760 ∷ T_IsCommutativeBand_590 → T_IsBand_508 Source #

d_isEquivalence_2762 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

du_isEquivalence_2762 ∷ T_IsCommutativeBand_590 → T_IsEquivalence_26 Source #

d_isMagma_2764 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsMagma_176 Source #

du_isMagma_2764 ∷ T_IsCommutativeBand_590 → T_IsMagma_176 Source #

d_isPartialEquivalence_2766 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2766 ∷ T_IsCommutativeBand_590 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2768 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

du_isSemigroup_2768 ∷ T_IsCommutativeBand_590 → T_IsSemigroup_472 Source #

d_refl_2770 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

du_refl_2770 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny Source #

d_reflexive_2772 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2772 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2774 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_Setoid_44 Source #

du_setoid_2774 ∷ T_IsCommutativeBand_590 → T_Setoid_44 Source #

d_sym_2776 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2776 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2778 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2778 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2780 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2780 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2782 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2782 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2784 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2784 ∷ T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_assoc_2798 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2800 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2802 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_identity_2804 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Σ_14 Source #

d_identity'691'_2806 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'691'_2806 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_identity'737'_2808 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'737'_2808 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_isBand_2810 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

du_isBand_2810 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

d_isCommutativeMagma_2812 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMagma_212 Source #

du_isCommutativeMagma_2812 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMagma_212 Source #

d_isCommutativeMonoid_2814 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMonoid_736 Source #

d_isCommutativeSemigroup_2816 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeSemigroup_548 Source #

du_isCommutativeSemigroup_2816 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeSemigroup_548 Source #

d_isEquivalence_2818 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsEquivalence_26 Source #

d_isIdempotentMonoid_2820 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsIdempotentMonoid_796 Source #

du_isIdempotentMonoid_2820 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsIdempotentMonoid_796 Source #

d_isMagma_2822 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsMagma_176 Source #

d_isMonoid_2824 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsMonoid_686 Source #

d_isPartialEquivalence_2826 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2826 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2828 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsSemigroup_472 Source #

d_isCommutativeBand_2830 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_2830 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

d_isUnitalMagma_2832 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsUnitalMagma_642 Source #

du_isUnitalMagma_2832 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsUnitalMagma_642 Source #

d_refl_2834 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_reflexive_2836 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2836 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2838 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

du_setoid_2838 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

d_sym_2840 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2842 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2844 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2846 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2846 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2848 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2848 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_identity_2862 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Σ_14 Source #

d_identity'691'_2864 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'691'_2864 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_identity'737'_2866 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'737'_2866 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_isCommutativeBand_2868 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_2868 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

d_assoc_2872 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2872 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2874 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_2874 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2876 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_idem_2876 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_isBand_2878 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

du_isBand_2878 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

d_isEquivalence_2880 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsEquivalence_26 Source #

du_isEquivalence_2880 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsEquivalence_26 Source #

d_isMagma_2882 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsMagma_176 Source #

du_isMagma_2882 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsMagma_176 Source #

d_isPartialEquivalence_2884 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2884 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2886 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsSemigroup_472 Source #

du_isSemigroup_2886 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsSemigroup_472 Source #

d_refl_2888 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_refl_2888 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_reflexive_2890 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2890 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2892 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

du_setoid_2892 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

d_sym_2894 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2894 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2896 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2896 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2898 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2898 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2900 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2900 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2902 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_2902 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_identity_2916 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Σ_14 Source #

d_identity'691'_2918 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'691'_2918 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_identity'737'_2920 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_identity'737'_2920 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_isCommutativeBand_2922 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

du_isCommutativeBand_2922 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeBand_590 Source #

d_assoc_2926 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_2926 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2928 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_2928 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_2930 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_idem_2930 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

d_isBand_2932 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

du_isBand_2932 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsBand_508 Source #

d_isEquivalence_2934 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsEquivalence_26 Source #

du_isEquivalence_2934 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsEquivalence_26 Source #

d_isMagma_2936 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsMagma_176 Source #

du_isMagma_2936 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsMagma_176 Source #

d_isPartialEquivalence_2938 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2938 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_2940 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_IsSemigroup_472 Source #

du_isSemigroup_2940 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsSemigroup_472 Source #

d_refl_2942 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

du_refl_2942 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny Source #

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

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

d_setoid_2946 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

du_setoid_2946 ∷ T_IsIdempotentCommutativeMonoid_852 → T_Setoid_44 Source #

d_sym_2948 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2948 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2950 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2950 ∷ T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2952 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsIdempotentCommutativeMonoid_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_2952 ∷ T_IsIdempotentCommutativeMonoid_852 → 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_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_2954 ∷ T_IsIdempotentCommutativeMonoid_852 → 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_852 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

d_IsLattice_2962 ∷ p → p → p → p → p → p → () Source #

data T_IsLattice_2962 Source #

Constructors

C_IsLattice'46'constructor_36793 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) T_Σ_14

d_isEquivalence_2984 ∷ T_IsLattice_2962 → T_IsEquivalence_26 Source #

d_'8744''45'comm_2986 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_2988 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_2990 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_2992 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_2994 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_2996 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_2998 ∷ T_IsLattice_2962 → T_Σ_14 Source #

d_isPartialEquivalence_3002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3002 ∷ T_IsLattice_2962 → T_IsPartialEquivalence_16 Source #

d_refl_3004 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny Source #

d_reflexive_3006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3006 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_3008 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3010 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_3012 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_3012 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_3014 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_3014 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_3016 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_3016 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_3020 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_3020 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_3024 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_3024 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_3028 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_3028 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_3036 ∷ p → p → p → p → p → p → () Source #

data T_IsDistributiveLattice_3036 Source #

Constructors

C_IsDistributiveLattice'46'constructor_40943 T_IsLattice_2962 T_Σ_14 T_Σ_14

d_isLattice_3048 ∷ T_IsDistributiveLattice_3036 → T_IsLattice_2962 Source #

d_'8744''45'distrib'45''8743'_3050 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_'8743''45'distrib'45''8744'_3052 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_absorptive_3056 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_isEquivalence_3058 ∷ T_IsDistributiveLattice_3036 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_3060 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3060 ∷ T_IsDistributiveLattice_3036 → T_IsPartialEquivalence_16 Source #

d_refl_3062 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny Source #

d_reflexive_3064 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3064 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_3066 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3068 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_3070 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_3070 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_3072 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_3074 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_3076 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_3078 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_3078 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_3080 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_3080 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_3082 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_3082 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_3084 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_3086 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_3088 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_3090 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_3090 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_3092 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_3092 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_3094 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_3094 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'691''45''8743'_3096 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_3096 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_3098 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_3098 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'691''45''8744'_3100 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_3100 ∷ T_IsDistributiveLattice_3036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBooleanAlgebra_3112 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsBooleanAlgebra_3112 Source #

Constructors

C_IsBooleanAlgebra'46'constructor_44015 T_IsDistributiveLattice_3036 T_Σ_14 T_Σ_14 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isDistributiveLattice_3132 ∷ T_IsBooleanAlgebra_3112 → T_IsDistributiveLattice_3036 Source #

d_'8744''45'complement_3134 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_'8743''45'complement_3136 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_'172''45'cong_3138 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_absorptive_3142 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_isEquivalence_3144 ∷ T_IsBooleanAlgebra_3112 → T_IsEquivalence_26 Source #

d_isLattice_3146 ∷ T_IsBooleanAlgebra_3112 → T_IsLattice_2962 Source #

d_isPartialEquivalence_3148 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3148 ∷ T_IsBooleanAlgebra_3112 → T_IsPartialEquivalence_16 Source #

d_refl_3150 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

d_reflexive_3152 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3152 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_3154 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3156 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_3158 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_3158 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_3160 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_3162 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_3164 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_3166 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_3166 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_3168 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_3168 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_3170 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_3172 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_3172 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_3174 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_3174 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_3176 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_3176 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_3178 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_3180 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_3182 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_3184 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_3184 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_3186 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_3186 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_3188 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_3190 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_3190 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_3192 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_3192 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'complement'737'_3194 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'737'_3194 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

d_'8744''45'complement'691'_3196 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'691'_3196 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'737'_3198 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'737'_3198 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'691'_3200 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'691'_3200 ∷ T_IsBooleanAlgebra_3112 → AgdaAny → AgdaAny Source #