plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Algebra.Lattice.Structures

Documentation

d__Absorbs__16 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d__DistributesOver__18 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d__DistributesOver'691'__20 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d__DistributesOver'737'__22 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Absorptive_28 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Associative_38 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Commutative_42 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Congruent'8321'_44 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () #

d_Congruent'8322'_46 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Inverse_62 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftCongruent_74 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftInverse_86 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightCongruent_104 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightInverse_116 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsCommutativeBand_154 :: p -> p -> p -> p -> p -> () #

d_IsIdempotentCommutativeMonoid_172 :: p -> p -> p -> p -> p -> p -> () #

d_isPartialEquivalence_338 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_508 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_338 :: T_IsBand_508 -> T_IsPartialEquivalence_16 #

d_reflexive_344 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_508 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_344 :: T_IsBand_508 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_346 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_508 -> T_Setoid_44 #

du_setoid_346 :: T_IsBand_508 -> T_Setoid_44 #

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 #

du_'8729''45'cong'691'_354 :: T_IsBand_508 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_356 :: T_IsBand_508 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_comm_464 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isBand_468 :: T_IsCommutativeBand_590 -> T_IsBand_508 #

d_idem_976 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_identity'691'_980 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'691'_980 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_identity'737'_982 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'737'_982 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_isBand_984 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

du_isBand_984 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

d_isCommutativeBand_986 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

du_isCommutativeBand_986 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

d_isCommutativeMagma_988 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMagma_212 #

du_isCommutativeMagma_988 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMagma_212 #

d_isCommutativeMonoid_990 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMonoid_736 #

d_isCommutativeSemigroup_992 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeSemigroup_548 #

du_isCommutativeSemigroup_992 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeSemigroup_548 #

d_isIdempotentMonoid_996 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsIdempotentMonoid_796 #

du_isIdempotentMonoid_996 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsIdempotentMonoid_796 #

d_isPartialEquivalence_1002 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1002 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

d_isUnitalMagma_1006 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsUnitalMagma_642 #

du_isUnitalMagma_1006 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsUnitalMagma_642 #

d_reflexive_1010 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1010 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1012 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

du_setoid_1012 :: T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

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 #

du_'8729''45'cong'691'_1020 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_1022 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsSemilattice_2658 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_comm_2668 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isBand_2670 :: T_IsCommutativeBand_590 -> T_IsBand_508 #

d_assoc_2674 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_assoc_2674 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_idem_2676 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

du_idem_2676 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

d_isEquivalence_2678 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsEquivalence_26 #

du_isEquivalence_2678 :: T_IsCommutativeBand_590 -> T_IsEquivalence_26 #

d_isMagma_2680 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsMagma_176 #

du_isMagma_2680 :: T_IsCommutativeBand_590 -> T_IsMagma_176 #

d_isPartialEquivalence_2682 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2682 :: T_IsCommutativeBand_590 -> T_IsPartialEquivalence_16 #

d_isSemigroup_2684 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsSemigroup_472 #

du_isSemigroup_2684 :: T_IsCommutativeBand_590 -> T_IsSemigroup_472 #

d_refl_2686 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

du_refl_2686 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

d_reflexive_2688 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2688 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2690 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_Setoid_44 #

du_setoid_2690 :: T_IsCommutativeBand_590 -> T_Setoid_44 #

d_sym_2692 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2692 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2694 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2694 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong_2696 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'691'_2698 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_2700 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMeetSemilattice_2702 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_assoc_2712 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_assoc_2712 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_comm_2714 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny #

d_idem_2716 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

du_idem_2716 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

d_isBand_2718 :: T_IsCommutativeBand_590 -> T_IsBand_508 #

d_isEquivalence_2720 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsEquivalence_26 #

du_isEquivalence_2720 :: T_IsCommutativeBand_590 -> T_IsEquivalence_26 #

d_isMagma_2722 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsMagma_176 #

du_isMagma_2722 :: T_IsCommutativeBand_590 -> T_IsMagma_176 #

d_isPartialEquivalence_2724 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2724 :: T_IsCommutativeBand_590 -> T_IsPartialEquivalence_16 #

d_isSemigroup_2726 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsSemigroup_472 #

du_isSemigroup_2726 :: T_IsCommutativeBand_590 -> T_IsSemigroup_472 #

d_refl_2728 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

du_refl_2728 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

d_reflexive_2730 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2730 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2732 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_Setoid_44 #

du_setoid_2732 :: T_IsCommutativeBand_590 -> T_Setoid_44 #

d_sym_2734 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2734 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2736 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2736 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong_2738 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'691'_2740 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_2742 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsJoinSemilattice_2744 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_assoc_2754 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_assoc_2754 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_comm_2756 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny #

d_idem_2758 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

du_idem_2758 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

d_isBand_2760 :: T_IsCommutativeBand_590 -> T_IsBand_508 #

d_isEquivalence_2762 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsEquivalence_26 #

du_isEquivalence_2762 :: T_IsCommutativeBand_590 -> T_IsEquivalence_26 #

d_isMagma_2764 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsMagma_176 #

du_isMagma_2764 :: T_IsCommutativeBand_590 -> T_IsMagma_176 #

d_isPartialEquivalence_2766 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2766 :: T_IsCommutativeBand_590 -> T_IsPartialEquivalence_16 #

d_isSemigroup_2768 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_IsSemigroup_472 #

du_isSemigroup_2768 :: T_IsCommutativeBand_590 -> T_IsSemigroup_472 #

d_refl_2770 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

du_refl_2770 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny #

d_reflexive_2772 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2772 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2774 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> T_Setoid_44 #

du_setoid_2774 :: T_IsCommutativeBand_590 -> T_Setoid_44 #

d_sym_2776 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2776 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2778 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2778 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong_2780 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'691'_2782 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_2784 :: T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBoundedSemilattice_2786 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> () #

d_assoc_2798 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_comm_2800 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny #

d_idem_2802 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_identity_2804 :: T_IsIdempotentCommutativeMonoid_852 -> T_Σ_14 #

d_identity'691'_2806 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'691'_2806 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_identity'737'_2808 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'737'_2808 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_isBand_2810 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

du_isBand_2810 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

d_isCommutativeMagma_2812 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMagma_212 #

du_isCommutativeMagma_2812 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMagma_212 #

d_isCommutativeMonoid_2814 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMonoid_736 #

d_isCommutativeSemigroup_2816 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeSemigroup_548 #

du_isCommutativeSemigroup_2816 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeSemigroup_548 #

d_isEquivalence_2818 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsEquivalence_26 #

d_isIdempotentMonoid_2820 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsIdempotentMonoid_796 #

du_isIdempotentMonoid_2820 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsIdempotentMonoid_796 #

d_isMagma_2822 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsMagma_176 #

d_isMonoid_2824 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsMonoid_686 #

d_isPartialEquivalence_2826 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2826 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

d_isSemigroup_2828 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsSemigroup_472 #

d_isCommutativeBand_2830 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

du_isCommutativeBand_2830 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

d_isUnitalMagma_2832 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsUnitalMagma_642 #

du_isUnitalMagma_2832 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsUnitalMagma_642 #

d_refl_2834 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_reflexive_2836 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2836 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2838 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

du_setoid_2838 :: T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

d_sym_2840 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2842 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'cong_2844 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'691'_2846 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_2848 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBoundedMeetSemilattice_2850 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> () #

d_identity_2862 :: T_IsIdempotentCommutativeMonoid_852 -> T_Σ_14 #

d_identity'691'_2864 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'691'_2864 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_identity'737'_2866 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'737'_2866 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_isCommutativeBand_2868 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

du_isCommutativeBand_2868 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

d_assoc_2872 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_assoc_2872 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_comm_2874 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny #

du_comm_2874 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny #

d_idem_2876 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_idem_2876 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_isBand_2878 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

du_isBand_2878 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

d_isEquivalence_2880 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsEquivalence_26 #

du_isEquivalence_2880 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsEquivalence_26 #

d_isMagma_2882 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsMagma_176 #

du_isMagma_2882 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsMagma_176 #

d_isPartialEquivalence_2884 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2884 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

d_isSemigroup_2886 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsSemigroup_472 #

du_isSemigroup_2886 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsSemigroup_472 #

d_refl_2888 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_refl_2888 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_reflexive_2890 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2890 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2892 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

du_setoid_2892 :: T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

d_sym_2894 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2894 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2896 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2896 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong_2898 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'691'_2900 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_2902 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBoundedJoinSemilattice_2904 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> () #

d_identity_2916 :: T_IsIdempotentCommutativeMonoid_852 -> T_Σ_14 #

d_identity'691'_2918 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'691'_2918 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_identity'737'_2920 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_identity'737'_2920 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_isCommutativeBand_2922 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

du_isCommutativeBand_2922 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeBand_590 #

d_assoc_2926 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_assoc_2926 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_comm_2928 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny #

du_comm_2928 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny #

d_idem_2930 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_idem_2930 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_isBand_2932 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

du_isBand_2932 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsBand_508 #

d_isEquivalence_2934 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsEquivalence_26 #

du_isEquivalence_2934 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsEquivalence_26 #

d_isMagma_2936 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsMagma_176 #

du_isMagma_2936 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsMagma_176 #

d_isPartialEquivalence_2938 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2938 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsPartialEquivalence_16 #

d_isSemigroup_2940 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_IsSemigroup_472 #

du_isSemigroup_2940 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsSemigroup_472 #

d_refl_2942 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

du_refl_2942 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny #

d_reflexive_2944 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2944 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2946 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

du_setoid_2946 :: T_IsIdempotentCommutativeMonoid_852 -> T_Setoid_44 #

d_sym_2948 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2948 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2950 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2950 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong_2952 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'691'_2954 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8729''45'cong'737'_2956 :: T_IsIdempotentCommutativeMonoid_852 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsLattice_2962 :: p -> p -> p -> p -> p -> p -> () #

data T_IsLattice_2962 #

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 #

d_'8744''45'comm_2986 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'assoc_2988 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'cong_2990 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'comm_2992 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'assoc_2994 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'cong_2996 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_absorptive_2998 :: T_IsLattice_2962 -> T_Σ_14 #

d_isPartialEquivalence_3002 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_2962 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_3002 :: T_IsLattice_2962 -> T_IsPartialEquivalence_16 #

d_refl_3004 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_3006 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_3008 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_3010 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'absorbs'45''8743'_3012 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'absorbs'45''8744'_3014 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'cong'737'_3016 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'cong'691'_3020 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'cong'737'_3024 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'cong'691'_3028 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsDistributiveLattice_3036 :: p -> p -> p -> p -> p -> p -> () #

data T_IsDistributiveLattice_3036 #

Constructors

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

d_isLattice_3048 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962 #

d_'8744''45'distrib'45''8743'_3050 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_'8743''45'distrib'45''8744'_3052 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_absorptive_3056 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_isEquivalence_3058 :: T_IsDistributiveLattice_3036 -> T_IsEquivalence_26 #

d_isPartialEquivalence_3060 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_3036 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_3060 :: T_IsDistributiveLattice_3036 -> T_IsPartialEquivalence_16 #

d_refl_3062 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_3064 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_3066 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_3068 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'absorbs'45''8744'_3070 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'assoc_3072 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'comm_3074 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'cong_3076 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'cong'691'_3078 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'cong'737'_3080 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'absorbs'45''8743'_3082 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'assoc_3084 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'comm_3086 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'cong_3088 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'cong'691'_3090 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'cong'737'_3092 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'distrib'737''45''8743'_3094 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'distrib'691''45''8743'_3096 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'distrib'737''45''8744'_3098 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'distrib'691''45''8744'_3100 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBooleanAlgebra_3112 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBooleanAlgebra_3112 #

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 #

d_'8744''45'complement_3134 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

d_'8743''45'complement_3136 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

d_'172''45'cong_3138 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_absorptive_3142 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

d_isEquivalence_3144 :: T_IsBooleanAlgebra_3112 -> T_IsEquivalence_26 #

d_isLattice_3146 :: T_IsBooleanAlgebra_3112 -> T_IsLattice_2962 #

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 #

du_isPartialEquivalence_3148 :: T_IsBooleanAlgebra_3112 -> T_IsPartialEquivalence_16 #

d_refl_3150 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_3152 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_3154 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_3156 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'absorbs'45''8744'_3158 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'assoc_3160 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'comm_3162 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'cong_3164 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'cong'691'_3166 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'cong'737'_3168 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'distrib'45''8744'_3170 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

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 #

du_'8743''45'distrib'691''45''8744'_3172 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'distrib'737''45''8744'_3174 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'absorbs'45''8743'_3176 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'assoc_3178 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'comm_3180 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'cong_3182 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'cong'691'_3184 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'cong'737'_3186 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'distrib'45''8743'_3188 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

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 #

du_'8744''45'distrib'691''45''8743'_3190 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'distrib'737''45''8743'_3192 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'complement'737'_3194 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny #

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 #

du_'8744''45'complement'691'_3196 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'complement'737'_3198 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'complement'691'_3200 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny #