Documentation

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

d_IsCommutativeMonoid_128 ∷ p → p → p → p → p → () Source #

d_IsCommutativeRing_130 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring_134 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroup_140 ∷ p → p → p → p → p → p → () Source #

d_IsMagma_160 ∷ p → p → p → p → () Source #

d_IsMonoid_166 ∷ p → p → p → p → p → () Source #

d_IsRing_182 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemigroup_188 ∷ p → p → p → p → () Source #

d_IsSemiring_192 ∷ p → p → p → p → p → p → p → () Source #

d_comm_208 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroup_230 ∷ T_IsAbelianGroup_1132 → T_IsGroup_1036 Source #

d_comm_498 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoid_514 ∷ T_IsCommutativeMonoid_736 → T_IsMonoid_686 Source #

d_'42''45'comm_544 ∷ T_IsCommutativeRing_2796 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRing_632 ∷ T_IsCommutativeRing_2796 → T_IsRing_2650 Source #

d_'42''45'comm_698 ∷ T_IsCommutativeSemiring_1678 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemiring_768 ∷ T_IsCommutativeSemiring_1678 → T_IsSemiring_1570 Source #

d_inverse_896 ∷ T_IsGroup_1036 → T_Σ_14 Source #

d_isMonoid_910 ∷ T_IsGroup_1036 → T_IsMonoid_686 Source #

d_'8315''185''45'cong_932 ∷ T_IsGroup_1036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_1460 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1474 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_1570 ∷ T_IsMonoid_686 → T_Σ_14 Source #

d_isSemigroup_1582 ∷ T_IsMonoid_686 → T_IsSemigroup_472 Source #

d_'42''45'assoc_2088 ∷ T_IsRing_2650 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_2090 ∷ T_IsRing_2650 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'identity_2096 ∷ T_IsRing_2650 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_2124 ∷ T_IsRing_2650 → T_IsAbelianGroup_1132 Source #

d_distrib_2154 ∷ T_IsRing_2650 → T_Σ_14 Source #

d_assoc_2314 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_2318 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_isSemiringWithoutAnnihilatingZero_2432 ∷ T_IsSemiring_1570 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #

d_zero_2446 ∷ T_IsSemiring_1570 → T_Σ_14 Source #

d__DistributesOver__2632 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__2634 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__2636 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_2652 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_2656 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_2660 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_2672 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_2676 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Involutive_2680 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_2698 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_2700 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_2706 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_2728 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_2730 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_2736 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Zero_2756 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsBooleanAlgebra_2892 ∷ p → p → p → p → p → p → p → p → () Source #

d_isDistributiveLattice_2914 ∷ T_IsBooleanAlgebra_3112 → T_IsDistributiveLattice_3036 Source #

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

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

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

d_poset_3356 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Poset_314 Source #

du_poset_3356 ∷ T_BooleanAlgebra_682 → T_Poset_314 Source #

d_'8743''45'idem_3358 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_3358 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'isBand_3360 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsBand_508 Source #

du_'8743''45'isBand_3360 ∷ T_BooleanAlgebra_682 → T_IsBand_508 Source #

d_'8743''45'isMagma_3362 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMagma_176 Source #

du_'8743''45'isMagma_3362 ∷ T_BooleanAlgebra_682 → T_IsMagma_176 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_3364 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_3364 ∷ T_BooleanAlgebra_682 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_3366 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMeetSemilattice_180 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_3366 ∷ T_BooleanAlgebra_682 → T_IsMeetSemilattice_180 Source #

d_'8743''45'isSemigroup_3368 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsSemigroup_472 Source #

du_'8743''45'isSemigroup_3368 ∷ T_BooleanAlgebra_682 → T_IsSemigroup_472 Source #

d_'8743''45'isSemilattice_3370 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeBand_590 Source #

du_'8743''45'isSemilattice_3370 ∷ T_BooleanAlgebra_682 → T_IsCommutativeBand_590 Source #

d_'8743''45'orderTheoreticJoinSemilattice_3372 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_3372 ∷ T_BooleanAlgebra_682 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_3374 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_MeetSemilattice_200 Source #

du_'8743''45'orderTheoreticMeetSemilattice_3374 ∷ T_BooleanAlgebra_682 → T_MeetSemilattice_200 Source #

d_'8743''45'semilattice_3376 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Semilattice_10 Source #

du_'8743''45'semilattice_3376 ∷ T_BooleanAlgebra_682 → T_Semilattice_10 Source #

d_'8743''45''8744''45'distributiveLattice_3378 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_DistributiveLattice_584 Source #

du_'8743''45''8744''45'distributiveLattice_3378 ∷ T_BooleanAlgebra_682 → T_DistributiveLattice_584 Source #

d_'8743''45''8744''45'isDistributiveLattice_3380 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsDistributiveLattice_3036 Source #

du_'8743''45''8744''45'isDistributiveLattice_3380 ∷ T_BooleanAlgebra_682 → T_IsDistributiveLattice_3036 Source #

d_'8743''45''8744''45'isLattice_3382 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsLattice_2962 Source #

du_'8743''45''8744''45'isLattice_3382 ∷ T_BooleanAlgebra_682 → T_IsLattice_2962 Source #

d_'8743''45''8744''45'lattice_3384 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Lattice_500 Source #

du_'8743''45''8744''45'lattice_3384 ∷ T_BooleanAlgebra_682 → T_Lattice_500 Source #

d_'8744''45'idem_3386 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_3386 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'isBand_3388 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsBand_508 Source #

du_'8744''45'isBand_3388 ∷ T_BooleanAlgebra_682 → T_IsBand_508 Source #

d_'8744''45'isMagma_3390 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMagma_176 Source #

du_'8744''45'isMagma_3390 ∷ T_BooleanAlgebra_682 → T_IsMagma_176 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_3392 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_3392 ∷ T_BooleanAlgebra_682 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_3394 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMeetSemilattice_180 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_3394 ∷ T_BooleanAlgebra_682 → T_IsMeetSemilattice_180 Source #

d_'8744''45'isSemigroup_3396 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsSemigroup_472 Source #

du_'8744''45'isSemigroup_3396 ∷ T_BooleanAlgebra_682 → T_IsSemigroup_472 Source #

d_'8744''45'isSemilattice_3398 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeBand_590 Source #

du_'8744''45'isSemilattice_3398 ∷ T_BooleanAlgebra_682 → T_IsCommutativeBand_590 Source #

d_'8743''45'orderTheoreticJoinSemilattice_3400 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_3400 ∷ T_BooleanAlgebra_682 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_3402 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_MeetSemilattice_200 Source #

du_'8743''45'orderTheoreticMeetSemilattice_3402 ∷ T_BooleanAlgebra_682 → T_MeetSemilattice_200 Source #

d_'8744''45'semilattice_3404 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Semilattice_10 Source #

du_'8744''45'semilattice_3404 ∷ T_BooleanAlgebra_682 → T_Semilattice_10 Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_3406 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsLattice_340 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_3406 ∷ T_BooleanAlgebra_682 → T_IsLattice_340 Source #

d_'8744''45''8743''45'orderTheoreticLattice_3408 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Lattice_386 Source #

du_'8744''45''8743''45'orderTheoreticLattice_3408 ∷ T_BooleanAlgebra_682 → T_Lattice_386 Source #

d_'8743''45''8744''45'isBooleanAlgebra_3410 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsBooleanAlgebra_3112 Source #

du_'8743''45''8744''45'isBooleanAlgebra_3410 ∷ T_BooleanAlgebra_682 → T_IsBooleanAlgebra_3112 Source #

d_'8743''45''8744''45'booleanAlgebra_3412 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_BooleanAlgebra_682 Source #

du_'8743''45''8744''45'booleanAlgebra_3412 ∷ T_BooleanAlgebra_682 → T_BooleanAlgebra_682 Source #

d_'8743''45'identity'691'_3414 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'identity'691'_3414 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'identity'737'_3418 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'identity'737'_3418 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'identity_3420 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8743''45'identity_3420 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8744''45'identity'691'_3422 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'identity'691'_3422 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'identity'737'_3426 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'identity'737'_3426 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'identity_3428 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8744''45'identity_3428 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8743''45'zero'691'_3430 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'zero'691'_3430 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'zero'737'_3434 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8743''45'zero'737'_3434 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8743''45'zero_3436 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8743''45'zero_3436 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8744''45'zero'691'_3440 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'zero'691'_3440 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'zero'737'_3444 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8744''45'zero'737'_3444 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8744''45'zero_3446 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8744''45'zero_3446 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8744''45''8869''45'isMonoid_3448 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMonoid_686 Source #

du_'8744''45''8869''45'isMonoid_3448 ∷ T_BooleanAlgebra_682 → T_IsMonoid_686 Source #

d_'8743''45''8868''45'isMonoid_3450 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMonoid_686 Source #

du_'8743''45''8868''45'isMonoid_3450 ∷ T_BooleanAlgebra_682 → T_IsMonoid_686 Source #

d_'8744''45''8869''45'isCommutativeMonoid_3452 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeMonoid_736 Source #

du_'8744''45''8869''45'isCommutativeMonoid_3452 ∷ T_BooleanAlgebra_682 → T_IsCommutativeMonoid_736 Source #

d_'8743''45''8868''45'isCommutativeMonoid_3454 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeMonoid_736 Source #

du_'8743''45''8868''45'isCommutativeMonoid_3454 ∷ T_BooleanAlgebra_682 → T_IsCommutativeMonoid_736 Source #

d_'8744''45''8743''45'isSemiring_3456 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsSemiring_1570 Source #

du_'8744''45''8743''45'isSemiring_3456 ∷ T_BooleanAlgebra_682 → T_IsSemiring_1570 Source #

d_'8743''45''8744''45'isSemiring_3458 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsSemiring_1570 Source #

du_'8743''45''8744''45'isSemiring_3458 ∷ T_BooleanAlgebra_682 → T_IsSemiring_1570 Source #

d_'8744''45''8743''45'isCommutativeSemiring_3460 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeSemiring_1678 Source #

du_'8744''45''8743''45'isCommutativeSemiring_3460 ∷ T_BooleanAlgebra_682 → T_IsCommutativeSemiring_1678 Source #

d_'8743''45''8744''45'isCommutativeSemiring_3462 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeSemiring_1678 Source #

du_'8743''45''8744''45'isCommutativeSemiring_3462 ∷ T_BooleanAlgebra_682 → T_IsCommutativeSemiring_1678 Source #

d_'8744''45''8743''45'commutativeSemiring_3464 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_CommutativeSemiring_2446 Source #

du_'8744''45''8743''45'commutativeSemiring_3464 ∷ T_BooleanAlgebra_682 → T_CommutativeSemiring_2446 Source #

d_'8743''45''8744''45'commutativeSemiring_3466 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_CommutativeSemiring_2446 Source #

du_'8743''45''8744''45'commutativeSemiring_3466 ∷ T_BooleanAlgebra_682 → T_CommutativeSemiring_2446 Source #

d_lemma_3472 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lemma_3472 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869''8777''8868'_3482 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny Source #

du_'8869''8777''8868'_3482 ∷ T_BooleanAlgebra_682 → AgdaAny Source #

d_'8868''8777''8869'_3484 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny Source #

du_'8868''8777''8869'_3484 ∷ T_BooleanAlgebra_682 → AgdaAny Source #

d_'172''45'involutive_3486 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'172''45'involutive_3486 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_deMorgan'8321'_3494 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_deMorgan'8321'_3494 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_3504 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_3504 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_3506 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_3506 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_3508 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_3508 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_deMorgan'8322'_3514 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_deMorgan'8322'_3514 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8853'__3530 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

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

d_helper_3540 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_helper_3540 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'cong_3546 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'cong_3546 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'comm_3560 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'comm_3560 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'737''45''8853'_3570 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'737''45''8853'_3570 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_lem_3584 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem_3584 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'691''45''8853'_3594 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'691''45''8853'_3594 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'annihilates'45''172'_3604 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'annihilates'45''172'_3604 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'identity'737'_3610 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'identity'737'_3610 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'identity'691'_3614 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'identity'691'_3614 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'identity_3616 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8853''45'identity_3616 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8853''45'inverse'737'_3618 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'737'_3618 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'inverse'691'_3622 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'691'_3622 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'inverse_3624 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8853''45'inverse_3624 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8743''45'distrib'737''45''8853'_3626 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8853'_3626 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_3638 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_3638 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_3640 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_3640 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_3642 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_3642 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'691''45''8853'_3644 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8853'_3644 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_lemma'8322'_3656 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lemma'8322'_3656 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'assoc_3666 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'assoc_3666 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_3678 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_3678 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322''8242'_3680 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322''8242'_3680 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_3682 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_3682 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_3684 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_3684 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8324''8242'_3686 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8324''8242'_3686 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8324'_3688 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8324'_3688 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8325'_3690 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8325'_3690 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'isMagma_3692 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 Source #

du_'8853''45'isMagma_3692 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 Source #

d_'8853''45'isSemigroup_3694 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 Source #

du_'8853''45'isSemigroup_3694 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 Source #

d_'8853''45''8869''45'isMonoid_3696 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMonoid_686 Source #

du_'8853''45''8869''45'isMonoid_3696 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMonoid_686 Source #

d_'8853''45''8869''45'isGroup_3698 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsGroup_1036 Source #

du_'8853''45''8869''45'isGroup_3698 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsGroup_1036 Source #

d_'8853''45''8869''45'isAbelianGroup_3700 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 Source #

du_'8853''45''8869''45'isAbelianGroup_3700 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 Source #

d_'8853''45''8743''45'isRing_3702 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsRing_2650 Source #

du_'8853''45''8743''45'isRing_3702 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsRing_2650 Source #

d_'8853''45''8743''45'isCommutativeRing_3704 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_2796 Source #

du_'8853''45''8743''45'isCommutativeRing_3704 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_2796 Source #

d_'8853''45''8743''45'commutativeRing_3706 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_4016 Source #

du_'8853''45''8743''45'commutativeRing_3706 ∷ T_BooleanAlgebra_682 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_4016 Source #

d__'8853'__3708 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'691''45''8853'_3720 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'691''45''8853'_3720 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'737''45''8853'_3722 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'737''45''8853'_3722 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8853'_3724 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8743''45'distrib'45''8853'_3724 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8853'_3726 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8853'_3726 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8853'_3728 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8853'_3728 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'annihilates'45''172'_3730 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'annihilates'45''172'_3730 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'assoc_3732 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'assoc_3732 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'comm_3734 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'comm_3734 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'cong_3736 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'cong_3736 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'identity_3738 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8853''45'identity_3738 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8853''45'identity'691'_3740 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8853''45'identity'691'_3740 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8853''45'identity'737'_3742 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8853''45'identity'737'_3742 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8853''45'inverse_3744 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_Σ_14 Source #

du_'8853''45'inverse_3744 ∷ T_BooleanAlgebra_682 → T_Σ_14 Source #

d_'8853''45'inverse'691'_3746 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'691'_3746 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8853''45'inverse'737'_3748 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'737'_3748 ∷ T_BooleanAlgebra_682 → AgdaAny → AgdaAny Source #

d_'8853''45'isMagma_3750 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMagma_176 Source #

du_'8853''45'isMagma_3750 ∷ T_BooleanAlgebra_682 → T_IsMagma_176 Source #

d_'8853''45'isSemigroup_3752 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsSemigroup_472 Source #

du_'8853''45'isSemigroup_3752 ∷ T_BooleanAlgebra_682 → T_IsSemigroup_472 Source #

d_'8853''45''8743''45'commutativeRing_3754 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_CommutativeRing_4016 Source #

du_'8853''45''8743''45'commutativeRing_3754 ∷ T_BooleanAlgebra_682 → T_CommutativeRing_4016 Source #

d_'8853''45''8743''45'isCommutativeRing_3756 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsCommutativeRing_2796 Source #

du_'8853''45''8743''45'isCommutativeRing_3756 ∷ T_BooleanAlgebra_682 → T_IsCommutativeRing_2796 Source #

d_'8853''45''8743''45'isRing_3758 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsRing_2650 Source #

du_'8853''45''8743''45'isRing_3758 ∷ T_BooleanAlgebra_682 → T_IsRing_2650 Source #

d_'8853''45''8869''45'isAbelianGroup_3760 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsAbelianGroup_1132 Source #

du_'8853''45''8869''45'isAbelianGroup_3760 ∷ T_BooleanAlgebra_682 → T_IsAbelianGroup_1132 Source #

d_'8853''45''8869''45'isGroup_3762 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsGroup_1036 Source #

du_'8853''45''8869''45'isGroup_3762 ∷ T_BooleanAlgebra_682 → T_IsGroup_1036 Source #

d_'8853''45''8869''45'isMonoid_3764 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_682 → T_IsMonoid_686 Source #

du_'8853''45''8869''45'isMonoid_3764 ∷ T_BooleanAlgebra_682 → T_IsMonoid_686 Source #