Safe HaskellNone

MAlonzo.Code.Algebra.Lattice.Structures

Documentation

d__Absorbs__16 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver__18 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver'691'__20 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver'737'__22 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Absorptive_26 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Associative_34 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Commutative_38 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Congruent'8321'_40 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Congruent'8322'_42 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Inverse_54 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftCongruent_60 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftInverse_72 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightCongruent_78 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightInverse_90 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_IsBand_102 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

d_IsIdempotentCommutativeMonoid_120 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_isPartialEquivalence_228 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_228 :: T_IsBand_242 -> T_IsPartialEquivalence_16 Source #

d_reflexive_234 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_234 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_236 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_Setoid_44 Source #

du_setoid_236 :: T_IsBand_242 -> T_Setoid_44 Source #

d_'8729''45'cong'691'_244 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_244 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_246 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_246 :: T_IsBand_242 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'691'_778 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'691'_778 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_identity'737'_780 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'737'_780 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isBand_782 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

du_isBand_782 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

d_isCommutativeMagma_784 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_784 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeSemigroup_788 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_788 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeSemigroup_282 Source #

d_isPartialEquivalence_796 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_796 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_800 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_800 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsUnitalMagma_326 Source #

d_reflexive_804 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_804 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_806 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

du_setoid_806 :: T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

d_'8729''45'cong'691'_814 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_814 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_816 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_816 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsSemilattice_1576 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_IsSemilattice_1576 Source #

Constructors

C_IsSemilattice'46'constructor_19667 T_IsBand_242 (AgdaAny -> AgdaAny -> AgdaAny) 

d_isBand_1584 :: T_IsSemilattice_1576 -> T_IsBand_242 Source #

d_comm_1586 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_1590 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_1592 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_1594 :: T_IsSemilattice_1576 -> T_IsEquivalence_26 Source #

d_isMagma_1596 :: T_IsSemilattice_1576 -> T_IsMagma_98 Source #

d_isPartialEquivalence_1598 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1598 :: T_IsSemilattice_1576 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1600 :: T_IsSemilattice_1576 -> T_IsSemigroup_206 Source #

d_refl_1602 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny Source #

d_reflexive_1604 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1604 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1606 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_Setoid_44 Source #

du_setoid_1606 :: T_IsSemilattice_1576 -> T_Setoid_44 Source #

d_sym_1608 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1610 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1612 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1614 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1614 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1616 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1616 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMeetSemilattice_1618 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_assoc_1628 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1630 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_1632 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny Source #

d_isBand_1634 :: T_IsSemilattice_1576 -> T_IsBand_242 Source #

d_isEquivalence_1636 :: T_IsSemilattice_1576 -> T_IsEquivalence_26 Source #

d_isMagma_1638 :: T_IsSemilattice_1576 -> T_IsMagma_98 Source #

d_isPartialEquivalence_1640 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1640 :: T_IsSemilattice_1576 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1642 :: T_IsSemilattice_1576 -> T_IsSemigroup_206 Source #

d_refl_1644 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny Source #

d_reflexive_1646 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1646 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1648 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_Setoid_44 Source #

du_setoid_1648 :: T_IsSemilattice_1576 -> T_Setoid_44 Source #

d_sym_1650 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1652 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1654 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1656 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1656 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1658 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1658 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsJoinSemilattice_1660 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_assoc_1670 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1672 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_1674 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny Source #

d_isBand_1676 :: T_IsSemilattice_1576 -> T_IsBand_242 Source #

d_isEquivalence_1678 :: T_IsSemilattice_1576 -> T_IsEquivalence_26 Source #

d_isMagma_1680 :: T_IsSemilattice_1576 -> T_IsMagma_98 Source #

d_isPartialEquivalence_1682 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1682 :: T_IsSemilattice_1576 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1684 :: T_IsSemilattice_1576 -> T_IsSemigroup_206 Source #

d_refl_1686 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny Source #

d_reflexive_1688 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1688 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1690 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> T_Setoid_44 Source #

du_setoid_1690 :: T_IsSemilattice_1576 -> T_Setoid_44 Source #

d_sym_1692 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1694 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1696 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1698 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1698 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1700 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1700 :: T_IsSemilattice_1576 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBoundedSemilattice_1702 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> () Source #

d_assoc_1714 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1716 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_1718 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_identity_1720 :: T_IsIdempotentCommutativeMonoid_480 -> T_Σ_14 Source #

d_identity'691'_1722 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1722 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1724 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1724 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isBand_1726 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

du_isBand_1726 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

d_isCommutativeMagma_1728 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_1728 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_1730 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_1732 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_1732 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_1734 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsEquivalence_26 Source #

d_isMagma_1736 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsMagma_98 Source #

d_isMonoid_1738 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_1740 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1740 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1742 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_1744 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1744 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsUnitalMagma_326 Source #

d_refl_1746 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_1748 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1748 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1750 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

du_setoid_1750 :: T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

d_sym_1752 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1754 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1756 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1758 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1758 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1760 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1760 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemilattice_1762 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsSemilattice_1576 Source #

du_isSemilattice_1762 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemilattice_1576 Source #

d_IsBoundedMeetSemilattice_1764 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> () Source #

d_identity_1776 :: T_IsIdempotentCommutativeMonoid_480 -> T_Σ_14 Source #

d_identity'691'_1778 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1778 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1780 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1780 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isSemilattice_1782 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsSemilattice_1576 Source #

du_isSemilattice_1782 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemilattice_1576 Source #

d_assoc_1786 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_assoc_1786 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1788 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_comm_1788 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_1790 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_idem_1790 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isBand_1792 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

du_isBand_1792 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

d_isEquivalence_1794 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsEquivalence_26 Source #

du_isEquivalence_1794 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsEquivalence_26 Source #

d_isMagma_1796 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsMagma_98 Source #

du_isMagma_1796 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsMagma_98 Source #

d_isPartialEquivalence_1798 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1798 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1800 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsSemigroup_206 Source #

du_isSemigroup_1800 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemigroup_206 Source #

d_refl_1802 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_refl_1802 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_1804 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1804 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1806 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

du_setoid_1806 :: T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

d_sym_1808 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_1808 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1810 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_1810 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1812 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong_1812 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1814 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1814 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1816 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1816 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBoundedJoinSemilattice_1818 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> () Source #

d_identity_1830 :: T_IsIdempotentCommutativeMonoid_480 -> T_Σ_14 Source #

d_identity'691'_1832 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1832 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1834 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1834 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isSemilattice_1836 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsSemilattice_1576 Source #

du_isSemilattice_1836 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemilattice_1576 Source #

d_assoc_1840 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_assoc_1840 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_1842 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_comm_1842 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_idem_1844 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_idem_1844 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_isBand_1846 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

du_isBand_1846 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsBand_242 Source #

d_isEquivalence_1848 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsEquivalence_26 Source #

du_isEquivalence_1848 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsEquivalence_26 Source #

d_isMagma_1850 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsMagma_98 Source #

du_isMagma_1850 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsMagma_98 Source #

d_isPartialEquivalence_1852 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1852 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_1854 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsSemigroup_206 Source #

du_isSemigroup_1854 :: T_IsIdempotentCommutativeMonoid_480 -> T_IsSemigroup_206 Source #

d_refl_1856 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

du_refl_1856 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny Source #

d_reflexive_1858 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1858 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1860 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

du_setoid_1860 :: T_IsIdempotentCommutativeMonoid_480 -> T_Setoid_44 Source #

d_sym_1862 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_1862 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1864 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_1864 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_1866 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong_1866 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_1868 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1868 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1870 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1870 :: T_IsIdempotentCommutativeMonoid_480 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsLattice_1876 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsLattice_1876 Source #

Constructors

C_IsLattice'46'constructor_22031 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_1898 :: T_IsLattice_1876 -> T_IsEquivalence_26 Source #

d_'8744''45'comm_1900 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'assoc_1902 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong_1904 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'comm_1906 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'assoc_1908 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong_1910 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_absorptive_1912 :: T_IsLattice_1876 -> T_Σ_14 Source #

d_isPartialEquivalence_1916 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1916 :: T_IsLattice_1876 -> T_IsPartialEquivalence_16 Source #

d_refl_1918 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny Source #

d_reflexive_1920 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1920 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_1922 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1924 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'absorbs'45''8743'_1926 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'absorbs'45''8743'_1926 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'absorbs'45''8744'_1928 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'absorbs'45''8744'_1928 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'737'_1930 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'737'_1930 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'691'_1934 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'691'_1934 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'737'_1938 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'737'_1938 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'691'_1942 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'691'_1942 :: T_IsLattice_1876 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsDistributiveLattice_1950 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsDistributiveLattice_1950 Source #

Constructors

C_IsDistributiveLattice'46'constructor_25337 T_IsLattice_1876 T_Σ_14 T_Σ_14 

d_isLattice_1962 :: T_IsDistributiveLattice_1950 -> T_IsLattice_1876 Source #

d_'8744''45'distrib'45''8743'_1964 :: T_IsDistributiveLattice_1950 -> T_Σ_14 Source #

d_'8743''45'distrib'45''8744'_1966 :: T_IsDistributiveLattice_1950 -> T_Σ_14 Source #

d_absorptive_1970 :: T_IsDistributiveLattice_1950 -> T_Σ_14 Source #

d_isEquivalence_1972 :: T_IsDistributiveLattice_1950 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1974 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1974 :: T_IsDistributiveLattice_1950 -> T_IsPartialEquivalence_16 Source #

d_refl_1976 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny Source #

d_reflexive_1978 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1978 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_1980 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1982 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'absorbs'45''8744'_1984 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'absorbs'45''8744'_1984 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'assoc_1986 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'comm_1988 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong_1990 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'691'_1992 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'691'_1992 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'737'_1994 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'737'_1994 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'absorbs'45''8743'_1996 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'absorbs'45''8743'_1996 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'assoc_1998 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'comm_2000 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong_2002 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'691'_2004 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'691'_2004 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'737'_2006 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'737'_2006 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_2008 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_2008 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'691''45''8743'_2010 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_2010 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_2012 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_2012 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'691''45''8744'_2014 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_2014 :: T_IsDistributiveLattice_1950 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsBooleanAlgebra_2026 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsBooleanAlgebra_2026 Source #

Constructors

C_IsBooleanAlgebra'46'constructor_27979 T_IsDistributiveLattice_1950 T_Σ_14 T_Σ_14 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_isDistributiveLattice_2046 :: T_IsBooleanAlgebra_2026 -> T_IsDistributiveLattice_1950 Source #

d_'8744''45'complement_2048 :: T_IsBooleanAlgebra_2026 -> T_Σ_14 Source #

d_'8743''45'complement_2050 :: T_IsBooleanAlgebra_2026 -> T_Σ_14 Source #

d_'172''45'cong_2052 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_absorptive_2056 :: T_IsBooleanAlgebra_2026 -> T_Σ_14 Source #

d_isEquivalence_2058 :: T_IsBooleanAlgebra_2026 -> T_IsEquivalence_26 Source #

d_isLattice_2060 :: T_IsBooleanAlgebra_2026 -> T_IsLattice_1876 Source #

d_isPartialEquivalence_2062 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2062 :: T_IsBooleanAlgebra_2026 -> T_IsPartialEquivalence_16 Source #

d_refl_2064 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

d_reflexive_2066 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_2066 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_2068 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_2070 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'absorbs'45''8744'_2072 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'absorbs'45''8744'_2072 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'assoc_2074 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'comm_2076 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong_2078 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'691'_2080 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'691'_2080 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'cong'737'_2082 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'cong'737'_2082 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'45''8744'_2084 :: T_IsBooleanAlgebra_2026 -> T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_2086 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_2086 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_2088 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_2088 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'absorbs'45''8743'_2090 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'absorbs'45''8743'_2090 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'assoc_2092 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'comm_2094 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong_2096 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'691'_2098 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'691'_2098 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'cong'737'_2100 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'cong'737'_2100 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'45''8743'_2102 :: T_IsBooleanAlgebra_2026 -> T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_2104 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_2104 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_2106 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_2106 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'complement'737'_2108 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

du_'8744''45'complement'737'_2108 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

d_'8744''45'complement'691'_2110 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

du_'8744''45'complement'691'_2110 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

d_'8743''45'complement'737'_2112 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

du_'8743''45'complement'737'_2112 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

d_'8743''45'complement'691'_2114 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #

du_'8743''45'complement'691'_2114 :: T_IsBooleanAlgebra_2026 -> AgdaAny -> AgdaAny Source #