Documentation

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

du_Σ'45'assoc_32 ∷ T_Inverse_2122 Source #

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

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

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

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

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

du_'215''45'identity'691'_58 ∷ T_Inverse_2122 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_2122 Source #

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

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

du_'215''45'zero'691'_86 ∷ T_Inverse_2122 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_2122 Source #

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

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

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

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

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

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

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

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

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

d_Σ'45'distrib'737''45''8846'_154 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_2122 Source #

du_Σ'45'distrib'737''45''8846'_154 ∷ T_Inverse_2122 Source #

d_Σ'45'distrib'691''45''8846'_174 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (T__'8846'__30 → ()) → T_Inverse_2122 Source #

du_Σ'45'distrib'691''45''8846'_174 ∷ T_Inverse_2122 Source #

d_'215''45'distrib'737''45''8846'_188 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 Source #

du_'215''45'distrib'737''45''8846'_188 ∷ T_Inverse_2122 Source #

d_'215''45'distrib'737''45''8846''8242'_192 ∷ T_Level_18 → () → () → () → T_Inverse_2122 Source #

du_'215''45'distrib'737''45''8846''8242'_192 ∷ T_Inverse_2122 Source #

d_'215''45'distrib'691''45''8846'_196 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 Source #

du_'215''45'distrib'691''45''8846'_196 ∷ T_Inverse_2122 Source #

d_'215''45'distrib'691''45''8846''8242'_200 ∷ T_Level_18 → () → () → () → T_Inverse_2122 Source #

du_'215''45'distrib'691''45''8846''8242'_200 ∷ T_Inverse_2122 Source #

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

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

d_'215''45'isMagma_214 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMagma_178 Source #

du_'215''45'isMagma_214 ∷ T_SymmetricKind_86 → T_IsMagma_178 Source #

d_'215''45'magma_222 ∷ T_SymmetricKind_86 → T_Level_18 → T_Magma_74 Source #

du_'215''45'magma_222 ∷ T_SymmetricKind_86 → T_Magma_74 Source #

d_'215''45'isSemigroup_232 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsSemigroup_488 Source #

du_'215''45'isSemigroup_232 ∷ T_SymmetricKind_86 → T_IsSemigroup_488 Source #

d_'215''45'semigroup_246 ∷ T_SymmetricKind_86 → T_Level_18 → T_Semigroup_558 Source #

du_'215''45'semigroup_246 ∷ T_SymmetricKind_86 → T_Semigroup_558 Source #

d_'215''45'isMonoid_256 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMonoid_712 Source #

du_'215''45'isMonoid_256 ∷ T_SymmetricKind_86 → T_IsMonoid_712 Source #

d_'215''45'monoid_264 ∷ T_SymmetricKind_86 → T_Level_18 → T_Monoid_914 Source #

du_'215''45'monoid_264 ∷ T_SymmetricKind_86 → T_Monoid_914 Source #

d_'215''45'isCommutativeMonoid_274 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsCommutativeMonoid_764 Source #

du_'215''45'isCommutativeMonoid_274 ∷ T_SymmetricKind_86 → T_IsCommutativeMonoid_764 Source #

d_'215''45'commutativeMonoid_286 ∷ T_SymmetricKind_86 → T_Level_18 → T_CommutativeMonoid_996 Source #

du_'215''45'commutativeMonoid_286 ∷ T_SymmetricKind_86 → T_CommutativeMonoid_996 Source #

d_'8846''45'isMagma_296 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMagma_178 Source #

du_'8846''45'isMagma_296 ∷ T_SymmetricKind_86 → T_IsMagma_178 Source #

d_'8846''45'magma_304 ∷ T_SymmetricKind_86 → T_Level_18 → T_Magma_74 Source #

du_'8846''45'magma_304 ∷ T_SymmetricKind_86 → T_Magma_74 Source #

d_'8846''45'isSemigroup_314 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsSemigroup_488 Source #

du_'8846''45'isSemigroup_314 ∷ T_SymmetricKind_86 → T_IsSemigroup_488 Source #

d_'8846''45'semigroup_328 ∷ T_SymmetricKind_86 → T_Level_18 → T_Semigroup_558 Source #

du_'8846''45'semigroup_328 ∷ T_SymmetricKind_86 → T_Semigroup_558 Source #

d_'8846''45'isMonoid_338 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsMonoid_712 Source #

du_'8846''45'isMonoid_338 ∷ T_SymmetricKind_86 → T_IsMonoid_712 Source #

d_'8846''45'monoid_346 ∷ T_SymmetricKind_86 → T_Level_18 → T_Monoid_914 Source #

du_'8846''45'monoid_346 ∷ T_SymmetricKind_86 → T_Monoid_914 Source #

d_'8846''45'isCommutativeMonoid_356 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsCommutativeMonoid_764 Source #

du_'8846''45'isCommutativeMonoid_356 ∷ T_SymmetricKind_86 → T_IsCommutativeMonoid_764 Source #

d_'8846''45'commutativeMonoid_368 ∷ T_SymmetricKind_86 → T_Level_18 → T_CommutativeMonoid_996 Source #

du_'8846''45'commutativeMonoid_368 ∷ T_SymmetricKind_86 → T_CommutativeMonoid_996 Source #

d_'215''45''8846''45'isCommutativeSemiring_378 ∷ T_SymmetricKind_86 → T_Level_18 → T_IsCommutativeSemiring_1750 Source #

du_'215''45''8846''45'isCommutativeSemiring_378 ∷ T_SymmetricKind_86 → T_IsCommutativeSemiring_1750 Source #

d_'215''45''8846''45'commutativeSemiring_392 ∷ T_SymmetricKind_86 → T_Level_18 → T_CommutativeSemiring_2524 Source #

du_'215''45''8846''45'commutativeSemiring_392 ∷ T_SymmetricKind_86 → T_CommutativeSemiring_2524 Source #

d_ΠΠ'8596'ΠΠ_418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Inverse_2122 Source #

du_ΠΠ'8596'ΠΠ_418 ∷ T_Inverse_2122 Source #

d_'8707''8707''8596''8707''8707'_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Inverse_2122 Source #

du_'8707''8707''8596''8707''8707'_444 ∷ T_Inverse_2122 Source #

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

du_to_460 ∷ T_Σ_14 → T_Σ_14 Source #

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

du_from_476 ∷ T_Σ_14 → T_Σ_14 Source #

d_Π'8596'Π_496 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Inverse_2122 Source #

du_Π'8596'Π_496 ∷ T_Inverse_2122 Source #

d_'8594''45'cong'45''8660'_502 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #

du_'8594''45'cong'45''8660'_502 ∷ T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #

d_'8594''45'cong'45''8596'_524 ∷ 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_2122 → T_Inverse_2122 → T_Inverse_2122 Source #

du_'8594''45'cong'45''8596'_524 ∷ T_Inverse_2122 → T_Inverse_2122 → T_Inverse_2122 Source #

d_'8594''45'cong_560 ∷ 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_560 ∷ T_SymmetricKind_86 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'cong'45''8660'_570 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Equivalence_1858 Source #

du_'172''45'cong'45''8660'_570 ∷ T_Equivalence_1858 → T_Equivalence_1858 Source #

d_'172''45'cong_580 ∷ 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_580 ∷ T_SymmetricKind_86 → AgdaAny → AgdaAny Source #

d_Related'45'cong_590 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_SymmetricKind_86 → AgdaAny → AgdaAny → T_Equivalence_1858 Source #

du_Related'45'cong_590 ∷ () → () → () → () → T_SymmetricKind_86 → AgdaAny → AgdaAny → T_Equivalence_1858 Source #

d_'8707''45''8801'_618 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Inverse_2122 Source #

du_'8707''45''8801'_618 ∷ AgdaAny → T_Inverse_2122 Source #

d_'46'extendedlambda2_626 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Σ_14 → AgdaAny Source #

du_'46'extendedlambda2_626 ∷ T_Σ_14 → AgdaAny Source #

d_'46'extendedlambda3_630 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Σ_14 → T__'8801'__12 Source #