Documentation

d_Σ'45'assoc_32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Inverse_1960 Source #

du_Σ'45'assoc_32 ∷ T_Inverse_1960 Source #

d_'215''45'comm_42 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_1960 Source #

du_'215''45'comm_42 ∷ T_Inverse_1960 Source #

d_'215''45'identity'737'_50 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'215''45'identity'737'_50 ∷ T_Inverse_1960 Source #

d_'215''45'identity'691'_58 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'215''45'identity'691'_58 ∷ T_Inverse_1960 Source #

d_'215''45'identity_68 ∷ T_Level_18 → T_Σ_14 Source #

du_'215''45'identity_68 ∷ T_Σ_14 Source #

d_'215''45'zero'737'_74 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'215''45'zero'737'_74 ∷ T_Inverse_1960 Source #

d_'215''45'zero'691'_86 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'215''45'zero'691'_86 ∷ T_Inverse_1960 Source #

d_'215''45'zero_98 ∷ T_Level_18 → T_Σ_14 Source #

du_'215''45'zero_98 ∷ T_Σ_14 Source #

d_'8846''45'assoc_104 ∷ T_Level_18 → () → () → () → T_Inverse_1960 Source #

du_'8846''45'assoc_104 ∷ T_Inverse_1960 Source #

d_'8846''45'comm_124 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_1960 Source #

du_'8846''45'comm_124 ∷ T_Inverse_1960 Source #

d_'8846''45'identity'737'_128 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'8846''45'identity'737'_128 ∷ T_Inverse_1960 Source #

d_'8846''45'identity'691'_136 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'8846''45'identity'691'_136 ∷ T_Inverse_1960 Source #

d_'8846''45'identity_144 ∷ T_Level_18 → T_Σ_14 Source #

du_'8846''45'identity_144 ∷ T_Σ_14 Source #

d_'215''45'distrib'737''45''8846'_150 ∷ T_Level_18 → () → () → () → T_Inverse_1960 Source #

du_'215''45'distrib'737''45''8846'_150 ∷ T_Inverse_1960 Source #

d_'215''45'distrib'691''45''8846'_172 ∷ T_Level_18 → () → () → () → T_Inverse_1960 Source #

du_'215''45'distrib'691''45''8846'_172 ∷ T_Inverse_1960 Source #

d_'215''45'distrib'45''8846'_190 ∷ T_Level_18 → T_Σ_14 Source #

du_'215''45'distrib'45''8846'_190 ∷ T_Σ_14 Source #

d_'215''45'isMagma_198 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMagma_176 Source #

du_'215''45'isMagma_198 ∷ T_SymmetricKind_86 → T_IsMagma_176 Source #

d_'215''45'magma_206 ∷ T_SymmetricKind_86 → T_Level_18 → T_Magma_68 Source #

du_'215''45'magma_206 ∷ T_SymmetricKind_86 → T_Magma_68 Source #

d_'215''45'isSemigroup_216 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsSemigroup_472 Source #

du_'215''45'isSemigroup_216 ∷ T_SymmetricKind_86 → T_IsSemigroup_472 Source #

d_'215''45'semigroup_230 ∷ T_SymmetricKind_86 → T_Level_18 → T_Semigroup_536 Source #

du_'215''45'semigroup_230 ∷ T_SymmetricKind_86 → T_Semigroup_536 Source #

d_'215''45'isMonoid_240 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMonoid_686 Source #

du_'215''45'isMonoid_240 ∷ T_SymmetricKind_86 → T_IsMonoid_686 Source #

d_'215''45'monoid_248 ∷ T_SymmetricKind_86 → T_Level_18 → T_Monoid_882 Source #

du_'215''45'monoid_248 ∷ T_SymmetricKind_86 → T_Monoid_882 Source #

d_'215''45'isCommutativeMonoid_258 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsCommutativeMonoid_736 Source #

du_'215''45'isCommutativeMonoid_258 ∷ T_SymmetricKind_86 → T_IsCommutativeMonoid_736 Source #

d_'215''45'commutativeMonoid_270 ∷ T_SymmetricKind_86 → T_Level_18 → T_CommutativeMonoid_962 Source #

du_'215''45'commutativeMonoid_270 ∷ T_SymmetricKind_86 → T_CommutativeMonoid_962 Source #

d_'8846''45'isMagma_280 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMagma_176 Source #

du_'8846''45'isMagma_280 ∷ T_SymmetricKind_86 → T_IsMagma_176 Source #

d_'8846''45'magma_288 ∷ T_SymmetricKind_86 → T_Level_18 → T_Magma_68 Source #

du_'8846''45'magma_288 ∷ T_SymmetricKind_86 → T_Magma_68 Source #

d_'8846''45'isSemigroup_298 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsSemigroup_472 Source #

du_'8846''45'isSemigroup_298 ∷ T_SymmetricKind_86 → T_IsSemigroup_472 Source #

d_'8846''45'semigroup_312 ∷ T_SymmetricKind_86 → T_Level_18 → T_Semigroup_536 Source #

du_'8846''45'semigroup_312 ∷ T_SymmetricKind_86 → T_Semigroup_536 Source #

d_'8846''45'isMonoid_322 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMonoid_686 Source #

du_'8846''45'isMonoid_322 ∷ T_SymmetricKind_86 → T_IsMonoid_686 Source #

d_'8846''45'monoid_330 ∷ T_SymmetricKind_86 → T_Level_18 → T_Monoid_882 Source #

du_'8846''45'monoid_330 ∷ T_SymmetricKind_86 → T_Monoid_882 Source #

d_'8846''45'isCommutativeMonoid_340 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsCommutativeMonoid_736 Source #

du_'8846''45'isCommutativeMonoid_340 ∷ T_SymmetricKind_86 → T_IsCommutativeMonoid_736 Source #

d_'8846''45'commutativeMonoid_352 ∷ T_SymmetricKind_86 → T_Level_18 → T_CommutativeMonoid_962 Source #

du_'8846''45'commutativeMonoid_352 ∷ T_SymmetricKind_86 → T_CommutativeMonoid_962 Source #

d_'215''45''8846''45'isCommutativeSemiring_362 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsCommutativeSemiring_1678 Source #

du_'215''45''8846''45'isCommutativeSemiring_362 ∷ T_SymmetricKind_86 → T_IsCommutativeSemiring_1678 Source #

d_'215''45''8846''45'commutativeSemiring_376 ∷ T_SymmetricKind_86 → T_Level_18 → T_CommutativeSemiring_2446 Source #

du_'215''45''8846''45'commutativeSemiring_376 ∷ T_SymmetricKind_86 → T_CommutativeSemiring_2446 Source #

d_ΠΠ'8596'ΠΠ_402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Inverse_1960 Source #

du_ΠΠ'8596'ΠΠ_402 ∷ T_Inverse_1960 Source #

d_'8707''8707''8596''8707''8707'_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Inverse_1960 Source #

du_'8707''8707''8596''8707''8707'_428 ∷ T_Inverse_1960 Source #

d_to_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #

du_to_444 ∷ T_Σ_14 → T_Σ_14 Source #

d_from_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #

du_from_460 ∷ T_Σ_14 → T_Σ_14 Source #

d_Π'8596'Π_480 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Inverse_1960 Source #

du_Π'8596'Π_480 ∷ T_Inverse_1960 Source #

d_'8594''45'cong'45''8660'_486 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #

du_'8594''45'cong'45''8660'_486 ∷ T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #

d_'8594''45'cong'45''8596'_508 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → () → () → () → () → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #

du_'8594''45'cong'45''8596'_508 ∷ T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #

d_'8594''45'cong_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → T_SymmetricKind_86 → () → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_'8594''45'cong_544 ∷ T_SymmetricKind_86 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'cong'45''8660'_554 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 Source #

du_'172''45'cong'45''8660'_554 ∷ T_Equivalence_1714 → T_Equivalence_1714 Source #

d_'172''45'cong_564 ∷ T_Level_18 → T_Level_18 → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → T_SymmetricKind_86 → () → () → AgdaAny → AgdaAny Source #

du_'172''45'cong_564 ∷ T_SymmetricKind_86 → AgdaAny → AgdaAny Source #

d_Related'45'cong_574 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_SymmetricKind_86 → AgdaAny → AgdaAny → T_Equivalence_1714 Source #

du_Related'45'cong_574 ∷ () → () → () → () → T_SymmetricKind_86 → AgdaAny → AgdaAny → T_Equivalence_1714 Source #

d_True'8596'_606 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → T_Inverse_1960 Source #

du_True'8596'_606 ∷ T_Dec_20 → T_Inverse_1960 Source #