Documentation

d_IsAbelianGroup_116 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_140 ∷ p → p → p → p → p → () Source #

d_IsCommutativeRing_144 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring_152 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroup_164 ∷ p → p → p → p → p → p → () Source #

d_IsMagma_204 ∷ p → p → p → p → () Source #

d_IsMonoid_216 ∷ p → p → p → p → p → () Source #

d_IsRing_248 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemigroup_260 ∷ p → p → p → p → () Source #

d_IsSemiring_268 ∷ p → p → p → p → p → p → p → () Source #

d_comm_294 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroup_316 ∷ T_IsAbelianGroup_1172 → T_IsGroup_1074 Source #

d_comm_584 ∷ T_IsCommutativeMonoid_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoid_600 ∷ T_IsCommutativeMonoid_764 → T_IsMonoid_712 Source #

d_'42''45'comm_630 ∷ T_IsCommutativeRing_2888 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRing_718 ∷ T_IsCommutativeRing_2888 → T_IsRing_2740 Source #

d_'42''45'comm_784 ∷ T_IsCommutativeSemiring_1750 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemiring_854 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiring_1640 Source #

d_inverse_992 ∷ T_IsGroup_1074 → T_Σ_14 Source #

d_isMonoid_1006 ∷ T_IsGroup_1074 → T_IsMonoid_712 Source #

d_'8315''185''45'cong_1028 ∷ T_IsGroup_1074 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1556 ∷ T_IsMagma_178 → T_IsEquivalence_28 Source #

d_'8729''45'cong_1570 ∷ T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1666 ∷ T_IsMonoid_712 → T_Σ_14 Source #

d_isSemigroup_1678 ∷ T_IsMonoid_712 → T_IsSemigroup_488 Source #

d_'42''45'assoc_2184 ∷ T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_2186 ∷ T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'identity_2192 ∷ T_IsRing_2740 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_2220 ∷ T_IsRing_2740 → T_IsAbelianGroup_1172 Source #

d_distrib_2250 ∷ T_IsRing_2740 → T_Σ_14 Source #

d_assoc_2412 ∷ T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_2416 ∷ T_IsSemigroup_488 → T_IsMagma_178 Source #

d_isSemiringWithoutAnnihilatingZero_2530 ∷ T_IsSemiring_1640 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

d_zero_2544 ∷ T_IsSemiring_1640 → T_Σ_14 Source #

d__DistributesOver__2740 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__2742 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__2744 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_2760 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_2764 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_2768 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_2780 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_2784 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Involutive_2788 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_2806 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_2808 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_2814 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_2836 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_2838 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_2844 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Zero_2864 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsBooleanAlgebra_3006 ∷ p → p → p → p → p → p → p → p → () Source #

d_isDistributiveLattice_3034 ∷ T_IsBooleanAlgebra_3224 → T_IsDistributiveLattice_3146 Source #

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

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

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

d_poset_3476 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Poset_492 Source #

du_poset_3476 ∷ T_BooleanAlgebra_698 → T_Poset_492 Source #

d_'8743''45'idem_3478 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_3478 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'isBand_3480 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsBand_526 Source #

du_'8743''45'isBand_3480 ∷ T_BooleanAlgebra_698 → T_IsBand_526 Source #

d_'8743''45'isMagma_3482 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMagma_178 Source #

du_'8743''45'isMagma_3482 ∷ T_BooleanAlgebra_698 → T_IsMagma_178 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_3484 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_3484 ∷ T_BooleanAlgebra_698 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_3486 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMeetSemilattice_184 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_3486 ∷ T_BooleanAlgebra_698 → T_IsMeetSemilattice_184 Source #

d_'8743''45'isSemigroup_3488 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsSemigroup_488 Source #

du_'8743''45'isSemigroup_3488 ∷ T_BooleanAlgebra_698 → T_IsSemigroup_488 Source #

d_'8743''45'isSemilattice_3490 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeBand_612 Source #

du_'8743''45'isSemilattice_3490 ∷ T_BooleanAlgebra_698 → T_IsCommutativeBand_612 Source #

d_'8743''45'orderTheoreticJoinSemilattice_3492 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_3492 ∷ T_BooleanAlgebra_698 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_3494 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_MeetSemilattice_204 Source #

du_'8743''45'orderTheoreticMeetSemilattice_3494 ∷ T_BooleanAlgebra_698 → T_MeetSemilattice_204 Source #

d_'8743''45'semilattice_3496 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Semilattice_10 Source #

du_'8743''45'semilattice_3496 ∷ T_BooleanAlgebra_698 → T_Semilattice_10 Source #

d_'8743''45''8744''45'distributiveLattice_3498 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_DistributiveLattice_598 Source #

du_'8743''45''8744''45'distributiveLattice_3498 ∷ T_BooleanAlgebra_698 → T_DistributiveLattice_598 Source #

d_'8743''45''8744''45'isDistributiveLattice_3500 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsDistributiveLattice_3146 Source #

du_'8743''45''8744''45'isDistributiveLattice_3500 ∷ T_BooleanAlgebra_698 → T_IsDistributiveLattice_3146 Source #

d_'8743''45''8744''45'isLattice_3502 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsLattice_3070 Source #

du_'8743''45''8744''45'isLattice_3502 ∷ T_BooleanAlgebra_698 → T_IsLattice_3070 Source #

d_'8743''45''8744''45'lattice_3504 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Lattice_512 Source #

du_'8743''45''8744''45'lattice_3504 ∷ T_BooleanAlgebra_698 → T_Lattice_512 Source #

d_'8744''45'idem_3506 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_3506 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'isBand_3508 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsBand_526 Source #

du_'8744''45'isBand_3508 ∷ T_BooleanAlgebra_698 → T_IsBand_526 Source #

d_'8744''45'isMagma_3510 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMagma_178 Source #

du_'8744''45'isMagma_3510 ∷ T_BooleanAlgebra_698 → T_IsMagma_178 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_3512 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_3512 ∷ T_BooleanAlgebra_698 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_3514 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMeetSemilattice_184 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_3514 ∷ T_BooleanAlgebra_698 → T_IsMeetSemilattice_184 Source #

d_'8744''45'isSemigroup_3516 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsSemigroup_488 Source #

du_'8744''45'isSemigroup_3516 ∷ T_BooleanAlgebra_698 → T_IsSemigroup_488 Source #

d_'8744''45'isSemilattice_3518 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeBand_612 Source #

du_'8744''45'isSemilattice_3518 ∷ T_BooleanAlgebra_698 → T_IsCommutativeBand_612 Source #

d_'8743''45'orderTheoreticJoinSemilattice_3520 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_3520 ∷ T_BooleanAlgebra_698 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_3522 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_MeetSemilattice_204 Source #

du_'8743''45'orderTheoreticMeetSemilattice_3522 ∷ T_BooleanAlgebra_698 → T_MeetSemilattice_204 Source #

d_'8744''45'semilattice_3524 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Semilattice_10 Source #

du_'8744''45'semilattice_3524 ∷ T_BooleanAlgebra_698 → T_Semilattice_10 Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_3526 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsLattice_348 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_3526 ∷ T_BooleanAlgebra_698 → T_IsLattice_348 Source #

d_'8744''45''8743''45'orderTheoreticLattice_3528 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Lattice_394 Source #

du_'8744''45''8743''45'orderTheoreticLattice_3528 ∷ T_BooleanAlgebra_698 → T_Lattice_394 Source #

d_'8743''45''8744''45'isBooleanAlgebra_3530 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsBooleanAlgebra_3224 Source #

du_'8743''45''8744''45'isBooleanAlgebra_3530 ∷ T_BooleanAlgebra_698 → T_IsBooleanAlgebra_3224 Source #

d_'8743''45''8744''45'booleanAlgebra_3532 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_BooleanAlgebra_698 Source #

du_'8743''45''8744''45'booleanAlgebra_3532 ∷ T_BooleanAlgebra_698 → T_BooleanAlgebra_698 Source #

d_'8743''45'identity'691'_3534 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'identity'691'_3534 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'identity'737'_3538 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'identity'737'_3538 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'identity_3540 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8743''45'identity_3540 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8744''45'identity'691'_3542 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'identity'691'_3542 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'identity'737'_3546 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'identity'737'_3546 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'identity_3548 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8744''45'identity_3548 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8743''45'zero'691'_3550 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'zero'691'_3550 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'zero'737'_3554 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'zero'737'_3554 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'zero_3556 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8743''45'zero_3556 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8744''45'zero'691'_3560 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'zero'691'_3560 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'zero'737'_3564 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'zero'737'_3564 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'zero_3566 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8744''45'zero_3566 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8744''45''8869''45'isMonoid_3568 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMonoid_712 Source #

du_'8744''45''8869''45'isMonoid_3568 ∷ T_BooleanAlgebra_698 → T_IsMonoid_712 Source #

d_'8743''45''8868''45'isMonoid_3570 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMonoid_712 Source #

du_'8743''45''8868''45'isMonoid_3570 ∷ T_BooleanAlgebra_698 → T_IsMonoid_712 Source #

d_'8744''45''8869''45'isCommutativeMonoid_3572 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeMonoid_764 Source #

du_'8744''45''8869''45'isCommutativeMonoid_3572 ∷ T_BooleanAlgebra_698 → T_IsCommutativeMonoid_764 Source #

d_'8743''45''8868''45'isCommutativeMonoid_3574 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeMonoid_764 Source #

du_'8743''45''8868''45'isCommutativeMonoid_3574 ∷ T_BooleanAlgebra_698 → T_IsCommutativeMonoid_764 Source #

d_'8744''45''8743''45'isSemiring_3576 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsSemiring_1640 Source #

du_'8744''45''8743''45'isSemiring_3576 ∷ T_BooleanAlgebra_698 → T_IsSemiring_1640 Source #

d_'8743''45''8744''45'isSemiring_3578 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsSemiring_1640 Source #

du_'8743''45''8744''45'isSemiring_3578 ∷ T_BooleanAlgebra_698 → T_IsSemiring_1640 Source #

d_'8744''45''8743''45'isCommutativeSemiring_3580 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeSemiring_1750 Source #

du_'8744''45''8743''45'isCommutativeSemiring_3580 ∷ T_BooleanAlgebra_698 → T_IsCommutativeSemiring_1750 Source #

d_'8743''45''8744''45'isCommutativeSemiring_3582 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeSemiring_1750 Source #

du_'8743''45''8744''45'isCommutativeSemiring_3582 ∷ T_BooleanAlgebra_698 → T_IsCommutativeSemiring_1750 Source #

d_'8744''45''8743''45'commutativeSemiring_3584 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_CommutativeSemiring_2524 Source #

du_'8744''45''8743''45'commutativeSemiring_3584 ∷ T_BooleanAlgebra_698 → T_CommutativeSemiring_2524 Source #

d_'8743''45''8744''45'commutativeSemiring_3586 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_CommutativeSemiring_2524 Source #

du_'8743''45''8744''45'commutativeSemiring_3586 ∷ T_BooleanAlgebra_698 → T_CommutativeSemiring_2524 Source #

d_lemma_3592 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lemma_3592 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''8869''8776''8868'_3602 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny Source #

du_'172''8869''8776''8868'_3602 ∷ T_BooleanAlgebra_698 → AgdaAny Source #

d_'172''8868''8776''8869'_3604 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny Source #

du_'172''8868''8776''8869'_3604 ∷ T_BooleanAlgebra_698 → AgdaAny Source #

d_'172''45'involutive_3606 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'172''45'involutive_3606 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_deMorgan'8321'_3614 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_deMorgan'8321'_3614 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_3624 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_3624 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_3626 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_3626 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_3628 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_3628 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_deMorgan'8322'_3634 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_deMorgan'8322'_3634 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8853'__3650 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du__'8853'__3650 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_helper_3660 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_helper_3660 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'cong_3666 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'cong_3666 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'comm_3680 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'comm_3680 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'737''45''8853'_3690 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'737''45''8853'_3690 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_lem_3704 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem_3704 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'691''45''8853'_3714 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'691''45''8853'_3714 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'annihilates'45''172'_3724 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'annihilates'45''172'_3724 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'identity'737'_3730 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'identity'737'_3730 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'identity'691'_3734 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'identity'691'_3734 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'identity_3736 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8853''45'identity_3736 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8853''45'inverse'737'_3738 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'737'_3738 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'inverse'691'_3742 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'691'_3742 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'inverse_3744 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8853''45'inverse_3744 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8743''45'distrib'737''45''8853'_3746 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8853'_3746 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_3758 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_3758 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_3760 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_3760 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_3762 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_3762 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'691''45''8853'_3764 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8853'_3764 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8853'_3766 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8743''45'distrib'45''8853'_3766 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_lemma'8322'_3776 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lemma'8322'_3776 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'assoc_3786 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'assoc_3786 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_3798 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_3798 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322''8242'_3800 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322''8242'_3800 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_3802 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_3802 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_3804 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_3804 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8324''8242'_3806 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8324''8242'_3806 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8324'_3808 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8324'_3808 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8325'_3810 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8325'_3810 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'isMagma_3812 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 Source #

du_'8853''45'isMagma_3812 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 Source #

d_'8853''45'isSemigroup_3814 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_488 Source #

du_'8853''45'isSemigroup_3814 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_488 Source #

d_'8853''45''8869''45'isMonoid_3816 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMonoid_712 Source #

du_'8853''45''8869''45'isMonoid_3816 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMonoid_712 Source #

d_'8853''45''8869''45'isGroup_3818 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsGroup_1074 Source #

du_'8853''45''8869''45'isGroup_3818 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsGroup_1074 Source #

d_'8853''45''8869''45'isAbelianGroup_3820 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 Source #

du_'8853''45''8869''45'isAbelianGroup_3820 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 Source #

d_'8853''45''8743''45'isRing_3822 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsRing_2740 Source #

du_'8853''45''8743''45'isRing_3822 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsRing_2740 Source #

d_'8853''45''8743''45'isCommutativeRing_3824 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_2888 Source #

du_'8853''45''8743''45'isCommutativeRing_3824 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_2888 Source #

d_'8853''45''8743''45'commutativeRing_3826 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_4126 Source #

du_'8853''45''8743''45'commutativeRing_3826 ∷ T_BooleanAlgebra_698 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_4126 Source #

d__'8853'__3828 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'691''45''8853'_3840 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'691''45''8853'_3840 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'737''45''8853'_3842 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'737''45''8853'_3842 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8853'_3844 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8743''45'distrib'45''8853'_3844 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8853'_3846 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8853'_3846 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8853'_3848 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8853'_3848 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'annihilates'45''172'_3850 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'annihilates'45''172'_3850 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'assoc_3852 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'assoc_3852 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'comm_3854 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'comm_3854 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'cong_3856 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'cong_3856 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'identity_3858 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8853''45'identity_3858 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8853''45'identity'691'_3860 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8853''45'identity'691'_3860 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8853''45'identity'737'_3862 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8853''45'identity'737'_3862 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8853''45'inverse_3864 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Σ_14 Source #

du_'8853''45'inverse_3864 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8853''45'inverse'691'_3866 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'691'_3866 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8853''45'inverse'737'_3868 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'737'_3868 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8853''45'isMagma_3870 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMagma_178 Source #

du_'8853''45'isMagma_3870 ∷ T_BooleanAlgebra_698 → T_IsMagma_178 Source #

d_'8853''45'isSemigroup_3872 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsSemigroup_488 Source #

du_'8853''45'isSemigroup_3872 ∷ T_BooleanAlgebra_698 → T_IsSemigroup_488 Source #

d_'8853''45''8743''45'commutativeRing_3874 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_CommutativeRing_4126 Source #

du_'8853''45''8743''45'commutativeRing_3874 ∷ T_BooleanAlgebra_698 → T_CommutativeRing_4126 Source #

d_'8853''45''8743''45'isCommutativeRing_3876 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsCommutativeRing_2888 Source #

du_'8853''45''8743''45'isCommutativeRing_3876 ∷ T_BooleanAlgebra_698 → T_IsCommutativeRing_2888 Source #

d_'8853''45''8743''45'isRing_3878 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsRing_2740 Source #

du_'8853''45''8743''45'isRing_3878 ∷ T_BooleanAlgebra_698 → T_IsRing_2740 Source #

d_'8853''45''8869''45'isAbelianGroup_3880 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsAbelianGroup_1172 Source #

du_'8853''45''8869''45'isAbelianGroup_3880 ∷ T_BooleanAlgebra_698 → T_IsAbelianGroup_1172 Source #

d_'8853''45''8869''45'isGroup_3882 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsGroup_1074 Source #

du_'8853''45''8869''45'isGroup_3882 ∷ T_BooleanAlgebra_698 → T_IsGroup_1074 Source #

d_'8853''45''8869''45'isMonoid_3884 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsMonoid_712 Source #

du_'8853''45''8869''45'isMonoid_3884 ∷ T_BooleanAlgebra_698 → T_IsMonoid_712 Source #

d_'8869''8777''8868'_3886 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny Source #

du_'8869''8777''8868'_3886 ∷ T_BooleanAlgebra_698 → AgdaAny Source #

d_'8868''8777''8869'_3888 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny Source #

du_'8868''8777''8869'_3888 ∷ T_BooleanAlgebra_698 → AgdaAny Source #