Documentation

d_IsAbelianGroup_116 :: p -> p -> p -> p -> p -> p -> () #

d_IsCommutativeMonoid_128 :: p -> p -> p -> p -> p -> () #

d_IsCommutativeRing_130 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsCommutativeSemiring_134 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsGroup_140 :: p -> p -> p -> p -> p -> p -> () #

d_IsMagma_160 :: p -> p -> p -> p -> () #

d_IsMonoid_166 :: p -> p -> p -> p -> p -> () #

d_IsRing_182 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemigroup_188 :: p -> p -> p -> p -> () #

d_IsSemiring_192 :: p -> p -> p -> p -> p -> p -> p -> () #

d_comm_208 :: T_IsAbelianGroup_1132 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isGroup_230 :: T_IsAbelianGroup_1132 -> T_IsGroup_1036 #

d_comm_498 :: T_IsCommutativeMonoid_736 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMonoid_514 :: T_IsCommutativeMonoid_736 -> T_IsMonoid_686 #

d_'42''45'comm_544 :: T_IsCommutativeRing_2796 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRing_632 :: T_IsCommutativeRing_2796 -> T_IsRing_2650 #

d_'42''45'comm_698 :: T_IsCommutativeSemiring_1678 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isSemiring_768 :: T_IsCommutativeSemiring_1678 -> T_IsSemiring_1570 #

d_inverse_896 :: T_IsGroup_1036 -> T_Σ_14 #

d_isMonoid_910 :: T_IsGroup_1036 -> T_IsMonoid_686 #

d_'8315''185''45'cong_932 :: T_IsGroup_1036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence_1460 :: T_IsMagma_176 -> T_IsEquivalence_26 #

d_'8729''45'cong_1474 :: T_IsMagma_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_identity_1570 :: T_IsMonoid_686 -> T_Σ_14 #

d_isSemigroup_1582 :: T_IsMonoid_686 -> T_IsSemigroup_472 #

d_'42''45'assoc_2088 :: T_IsRing_2650 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'cong_2090 :: T_IsRing_2650 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'identity_2096 :: T_IsRing_2650 -> T_Σ_14 #

d_'43''45'isAbelianGroup_2124 :: T_IsRing_2650 -> T_IsAbelianGroup_1132 #

d_distrib_2154 :: T_IsRing_2650 -> T_Σ_14 #

d_assoc_2314 :: T_IsSemigroup_472 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagma_2318 :: T_IsSemigroup_472 -> T_IsMagma_176 #

d_isSemiringWithoutAnnihilatingZero_2432 :: T_IsSemiring_1570 -> T_IsSemiringWithoutAnnihilatingZero_1468 #

d_zero_2446 :: T_IsSemiring_1570 -> T_Σ_14 #

d__DistributesOver__2632 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d__DistributesOver'691'__2634 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d__DistributesOver'737'__2636 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Associative_2652 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Commutative_2656 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Congruent'8322'_2660 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Identity_2672 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Inverse_2676 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Involutive_2680 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny) -> () #

d_LeftIdentity_2698 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftInverse_2700 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftZero_2706 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightIdentity_2728 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightInverse_2730 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightZero_2736 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Zero_2756 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsBooleanAlgebra_2892 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_isDistributiveLattice_2914 :: T_IsBooleanAlgebra_3112 -> T_IsDistributiveLattice_3036 #

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

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

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

d_poset_3356 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Poset_314 #

du_poset_3356 :: T_BooleanAlgebra_682 -> T_Poset_314 #

d_'8743''45'idem_3358 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8743''45'idem_3358 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8743''45'isBand_3360 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsBand_508 #

du_'8743''45'isBand_3360 :: T_BooleanAlgebra_682 -> T_IsBand_508 #

d_'8743''45'isMagma_3362 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMagma_176 #

du_'8743''45'isMagma_3362 :: T_BooleanAlgebra_682 -> T_IsMagma_176 #

d_'8743''45'isOrderTheoreticJoinSemilattice_3364 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsJoinSemilattice_22 #

du_'8743''45'isOrderTheoreticJoinSemilattice_3364 :: T_BooleanAlgebra_682 -> T_IsJoinSemilattice_22 #

d_'8743''45'isOrderTheoreticMeetSemilattice_3366 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMeetSemilattice_180 #

du_'8743''45'isOrderTheoreticMeetSemilattice_3366 :: T_BooleanAlgebra_682 -> T_IsMeetSemilattice_180 #

d_'8743''45'isSemigroup_3368 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsSemigroup_472 #

du_'8743''45'isSemigroup_3368 :: T_BooleanAlgebra_682 -> T_IsSemigroup_472 #

d_'8743''45'isSemilattice_3370 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeBand_590 #

du_'8743''45'isSemilattice_3370 :: T_BooleanAlgebra_682 -> T_IsCommutativeBand_590 #

d_'8743''45'orderTheoreticJoinSemilattice_3372 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_JoinSemilattice_14 #

du_'8743''45'orderTheoreticJoinSemilattice_3372 :: T_BooleanAlgebra_682 -> T_JoinSemilattice_14 #

d_'8743''45'orderTheoreticMeetSemilattice_3374 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_MeetSemilattice_200 #

du_'8743''45'orderTheoreticMeetSemilattice_3374 :: T_BooleanAlgebra_682 -> T_MeetSemilattice_200 #

d_'8743''45'semilattice_3376 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Semilattice_10 #

du_'8743''45'semilattice_3376 :: T_BooleanAlgebra_682 -> T_Semilattice_10 #

d_'8743''45''8744''45'distributiveLattice_3378 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_DistributiveLattice_584 #

du_'8743''45''8744''45'distributiveLattice_3378 :: T_BooleanAlgebra_682 -> T_DistributiveLattice_584 #

d_'8743''45''8744''45'isDistributiveLattice_3380 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsDistributiveLattice_3036 #

du_'8743''45''8744''45'isDistributiveLattice_3380 :: T_BooleanAlgebra_682 -> T_IsDistributiveLattice_3036 #

d_'8743''45''8744''45'isLattice_3382 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsLattice_2962 #

du_'8743''45''8744''45'isLattice_3382 :: T_BooleanAlgebra_682 -> T_IsLattice_2962 #

d_'8743''45''8744''45'lattice_3384 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Lattice_500 #

du_'8743''45''8744''45'lattice_3384 :: T_BooleanAlgebra_682 -> T_Lattice_500 #

d_'8744''45'idem_3386 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8744''45'idem_3386 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8744''45'isBand_3388 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsBand_508 #

du_'8744''45'isBand_3388 :: T_BooleanAlgebra_682 -> T_IsBand_508 #

d_'8744''45'isMagma_3390 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMagma_176 #

du_'8744''45'isMagma_3390 :: T_BooleanAlgebra_682 -> T_IsMagma_176 #

d_'8743''45'isOrderTheoreticJoinSemilattice_3392 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsJoinSemilattice_22 #

du_'8743''45'isOrderTheoreticJoinSemilattice_3392 :: T_BooleanAlgebra_682 -> T_IsJoinSemilattice_22 #

d_'8743''45'isOrderTheoreticMeetSemilattice_3394 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMeetSemilattice_180 #

du_'8743''45'isOrderTheoreticMeetSemilattice_3394 :: T_BooleanAlgebra_682 -> T_IsMeetSemilattice_180 #

d_'8744''45'isSemigroup_3396 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsSemigroup_472 #

du_'8744''45'isSemigroup_3396 :: T_BooleanAlgebra_682 -> T_IsSemigroup_472 #

d_'8744''45'isSemilattice_3398 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeBand_590 #

du_'8744''45'isSemilattice_3398 :: T_BooleanAlgebra_682 -> T_IsCommutativeBand_590 #

d_'8743''45'orderTheoreticJoinSemilattice_3400 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_JoinSemilattice_14 #

du_'8743''45'orderTheoreticJoinSemilattice_3400 :: T_BooleanAlgebra_682 -> T_JoinSemilattice_14 #

d_'8743''45'orderTheoreticMeetSemilattice_3402 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_MeetSemilattice_200 #

du_'8743''45'orderTheoreticMeetSemilattice_3402 :: T_BooleanAlgebra_682 -> T_MeetSemilattice_200 #

d_'8744''45'semilattice_3404 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Semilattice_10 #

du_'8744''45'semilattice_3404 :: T_BooleanAlgebra_682 -> T_Semilattice_10 #

d_'8744''45''8743''45'isOrderTheoreticLattice_3406 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsLattice_340 #

du_'8744''45''8743''45'isOrderTheoreticLattice_3406 :: T_BooleanAlgebra_682 -> T_IsLattice_340 #

d_'8744''45''8743''45'orderTheoreticLattice_3408 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Lattice_386 #

du_'8744''45''8743''45'orderTheoreticLattice_3408 :: T_BooleanAlgebra_682 -> T_Lattice_386 #

d_'8743''45''8744''45'isBooleanAlgebra_3410 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsBooleanAlgebra_3112 #

du_'8743''45''8744''45'isBooleanAlgebra_3410 :: T_BooleanAlgebra_682 -> T_IsBooleanAlgebra_3112 #

d_'8743''45''8744''45'booleanAlgebra_3412 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_BooleanAlgebra_682 #

du_'8743''45''8744''45'booleanAlgebra_3412 :: T_BooleanAlgebra_682 -> T_BooleanAlgebra_682 #

d_'8743''45'identity'691'_3414 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8743''45'identity'691'_3414 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8743''45'identity'737'_3418 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8743''45'identity'737'_3418 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8743''45'identity_3420 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8743''45'identity_3420 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8744''45'identity'691'_3422 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8744''45'identity'691'_3422 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8744''45'identity'737'_3426 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8744''45'identity'737'_3426 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8744''45'identity_3428 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8744''45'identity_3428 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8743''45'zero'691'_3430 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8743''45'zero'691'_3430 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8743''45'zero'737'_3434 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8743''45'zero'737'_3434 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8743''45'zero_3436 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8743''45'zero_3436 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8744''45'zero'691'_3440 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8744''45'zero'691'_3440 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8744''45'zero'737'_3444 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8744''45'zero'737'_3444 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8744''45'zero_3446 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8744''45'zero_3446 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8744''45''8869''45'isMonoid_3448 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMonoid_686 #

du_'8744''45''8869''45'isMonoid_3448 :: T_BooleanAlgebra_682 -> T_IsMonoid_686 #

d_'8743''45''8868''45'isMonoid_3450 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMonoid_686 #

du_'8743''45''8868''45'isMonoid_3450 :: T_BooleanAlgebra_682 -> T_IsMonoid_686 #

d_'8744''45''8869''45'isCommutativeMonoid_3452 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeMonoid_736 #

du_'8744''45''8869''45'isCommutativeMonoid_3452 :: T_BooleanAlgebra_682 -> T_IsCommutativeMonoid_736 #

d_'8743''45''8868''45'isCommutativeMonoid_3454 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeMonoid_736 #

du_'8743''45''8868''45'isCommutativeMonoid_3454 :: T_BooleanAlgebra_682 -> T_IsCommutativeMonoid_736 #

d_'8744''45''8743''45'isSemiring_3456 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsSemiring_1570 #

du_'8744''45''8743''45'isSemiring_3456 :: T_BooleanAlgebra_682 -> T_IsSemiring_1570 #

d_'8743''45''8744''45'isSemiring_3458 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsSemiring_1570 #

du_'8743''45''8744''45'isSemiring_3458 :: T_BooleanAlgebra_682 -> T_IsSemiring_1570 #

d_'8744''45''8743''45'isCommutativeSemiring_3460 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeSemiring_1678 #

du_'8744''45''8743''45'isCommutativeSemiring_3460 :: T_BooleanAlgebra_682 -> T_IsCommutativeSemiring_1678 #

d_'8743''45''8744''45'isCommutativeSemiring_3462 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeSemiring_1678 #

du_'8743''45''8744''45'isCommutativeSemiring_3462 :: T_BooleanAlgebra_682 -> T_IsCommutativeSemiring_1678 #

d_'8744''45''8743''45'commutativeSemiring_3464 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_CommutativeSemiring_2446 #

du_'8744''45''8743''45'commutativeSemiring_3464 :: T_BooleanAlgebra_682 -> T_CommutativeSemiring_2446 #

d_'8743''45''8744''45'commutativeSemiring_3466 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_CommutativeSemiring_2446 #

du_'8743''45''8744''45'commutativeSemiring_3466 :: T_BooleanAlgebra_682 -> T_CommutativeSemiring_2446 #

d_lemma_3472 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lemma_3472 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8869''8777''8868'_3482 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny #

du_'8869''8777''8868'_3482 :: T_BooleanAlgebra_682 -> AgdaAny #

d_'8868''8777''8869'_3484 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny #

du_'8868''8777''8869'_3484 :: T_BooleanAlgebra_682 -> AgdaAny #

d_'172''45'involutive_3486 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'172''45'involutive_3486 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_deMorgan'8321'_3494 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_deMorgan'8321'_3494 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8321'_3504 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8321'_3504 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8323'_3506 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8323'_3506 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8322'_3508 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8322'_3508 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_deMorgan'8322'_3514 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_deMorgan'8322'_3514 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8853'__3530 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

du__'8853'__3530 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_helper_3540 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8853''45'cong_3546 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'comm_3560 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8853''45'comm_3560 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'172''45'distrib'737''45''8853'_3570 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem_3584 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem_3584 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'172''45'distrib'691''45''8853'_3594 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8853''45'annihilates'45''172'_3604 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'identity'737'_3610 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8853''45'identity'737'_3610 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8853''45'identity'691'_3614 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8853''45'identity'691'_3614 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8853''45'identity_3616 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 #

du_'8853''45'identity_3616 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 #

d_'8853''45'inverse'737'_3618 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8853''45'inverse'737'_3618 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8853''45'inverse'691'_3622 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_'8853''45'inverse'691'_3622 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_'8853''45'inverse_3624 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 #

du_'8853''45'inverse_3624 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 #

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 #

du_'8743''45'distrib'737''45''8853'_3626 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8322'_3638 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8322'_3638 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8321'_3640 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8321'_3640 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8323'_3642 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8323'_3642 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_'8743''45'distrib'691''45''8853'_3644 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'distrib'45''8853'_3646 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 #

du_'8743''45'distrib'45''8853'_3646 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 #

d_lemma'8322'_3656 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lemma'8322'_3656 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'assoc_3666 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8853''45'assoc_3666 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8321'_3678 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8321'_3678 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8322''8242'_3680 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8322''8242'_3680 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8322'_3682 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8322'_3682 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8323'_3684 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8323'_3684 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8324''8242'_3686 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8324''8242'_3686 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8324'_3688 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8324'_3688 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_lem'8325'_3690 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_lem'8325'_3690 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'isMagma_3692 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 #

du_'8853''45'isMagma_3692 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 #

d_'8853''45'isSemigroup_3694 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472 #

du_'8853''45'isSemigroup_3694 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472 #

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 #

du_'8853''45''8869''45'isMonoid_3696 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMonoid_686 #

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 #

du_'8853''45''8869''45'isGroup_3698 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsGroup_1036 #

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 #

du_'8853''45''8869''45'isAbelianGroup_3700 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsAbelianGroup_1132 #

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 #

du_'8853''45''8743''45'isRing_3702 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsRing_2650 #

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 #

du_'8853''45''8743''45'isCommutativeRing_3704 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeRing_2796 #

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 #

du_'8853''45''8743''45'commutativeRing_3706 :: T_BooleanAlgebra_682 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_CommutativeRing_4016 #

d__'8853'__3708 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'172''45'distrib'691''45''8853'_3720 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'172''45'distrib'691''45''8853'_3720 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'172''45'distrib'737''45''8853'_3722 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'172''45'distrib'737''45''8853'_3722 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'distrib'45''8853'_3724 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8743''45'distrib'45''8853'_3724 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8743''45'distrib'691''45''8853'_3726 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'distrib'691''45''8853'_3726 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'distrib'737''45''8853'_3728 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8743''45'distrib'737''45''8853'_3728 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'annihilates'45''172'_3730 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8853''45'annihilates'45''172'_3730 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'assoc_3732 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8853''45'assoc_3732 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'comm_3734 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8853''45'comm_3734 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'cong_3736 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8853''45'cong_3736 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8853''45'identity_3738 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8853''45'identity_3738 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8853''45'identity'691'_3740 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8853''45'identity'691'_3740 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8853''45'identity'737'_3742 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8853''45'identity'737'_3742 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8853''45'inverse_3744 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_Σ_14 #

du_'8853''45'inverse_3744 :: T_BooleanAlgebra_682 -> T_Σ_14 #

d_'8853''45'inverse'691'_3746 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8853''45'inverse'691'_3746 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8853''45'inverse'737'_3748 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

du_'8853''45'inverse'737'_3748 :: T_BooleanAlgebra_682 -> AgdaAny -> AgdaAny #

d_'8853''45'isMagma_3750 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMagma_176 #

du_'8853''45'isMagma_3750 :: T_BooleanAlgebra_682 -> T_IsMagma_176 #

d_'8853''45'isSemigroup_3752 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsSemigroup_472 #

du_'8853''45'isSemigroup_3752 :: T_BooleanAlgebra_682 -> T_IsSemigroup_472 #

d_'8853''45''8743''45'commutativeRing_3754 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_CommutativeRing_4016 #

du_'8853''45''8743''45'commutativeRing_3754 :: T_BooleanAlgebra_682 -> T_CommutativeRing_4016 #

d_'8853''45''8743''45'isCommutativeRing_3756 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsCommutativeRing_2796 #

du_'8853''45''8743''45'isCommutativeRing_3756 :: T_BooleanAlgebra_682 -> T_IsCommutativeRing_2796 #

d_'8853''45''8743''45'isRing_3758 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsRing_2650 #

du_'8853''45''8743''45'isRing_3758 :: T_BooleanAlgebra_682 -> T_IsRing_2650 #

d_'8853''45''8869''45'isAbelianGroup_3760 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsAbelianGroup_1132 #

du_'8853''45''8869''45'isAbelianGroup_3760 :: T_BooleanAlgebra_682 -> T_IsAbelianGroup_1132 #

d_'8853''45''8869''45'isGroup_3762 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsGroup_1036 #

du_'8853''45''8869''45'isGroup_3762 :: T_BooleanAlgebra_682 -> T_IsGroup_1036 #

d_'8853''45''8869''45'isMonoid_3764 :: T_Level_18 -> T_Level_18 -> T_BooleanAlgebra_682 -> T_IsMonoid_686 #

du_'8853''45''8869''45'isMonoid_3764 :: T_BooleanAlgebra_682 -> T_IsMonoid_686 #