Documentation

d_Σ'45'assoc_22 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Inverse_58 Source #

du_Σ'45'assoc_22 ∷ T_Inverse_58 Source #

d_'215''45'comm_52 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 Source #

du_'215''45'comm_52 ∷ T_Inverse_58 Source #

d_'215''45'identity'737'_60 ∷ T_Level_18 → () → T_Inverse_58 Source #

du_'215''45'identity'737'_60 ∷ T_Inverse_58 Source #

d_'215''45'identity'691'_68 ∷ T_Level_18 → () → T_Inverse_58 Source #

du_'215''45'identity'691'_68 ∷ T_Inverse_58 Source #

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

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

d_'215''45'zero'737'_84 ∷ T_Level_18 → () → T_Inverse_58 Source #

du_'215''45'zero'737'_84 ∷ T_Inverse_58 Source #

d_'215''45'zero'691'_96 ∷ T_Level_18 → () → T_Inverse_58 Source #

du_'215''45'zero'691'_96 ∷ T_Inverse_58 Source #

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

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

d_'8846''45'assoc_114 ∷ T_Level_18 → () → () → () → T_Inverse_58 Source #

du_'8846''45'assoc_114 ∷ T_Inverse_58 Source #

d_'8846''45'comm_138 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 Source #

du_'8846''45'comm_138 ∷ T_Inverse_58 Source #

d_'8846''45'identity'737'_142 ∷ T_Level_18 → () → T_Inverse_58 Source #

du_'8846''45'identity'737'_142 ∷ T_Inverse_58 Source #

d_'8846''45'identity'691'_150 ∷ T_Level_18 → () → T_Inverse_58 Source #

du_'8846''45'identity'691'_150 ∷ T_Inverse_58 Source #

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

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

d_'215''45'distrib'737''45''8846'_164 ∷ T_Level_18 → () → () → () → T_Inverse_58 Source #

du_'215''45'distrib'737''45''8846'_164 ∷ T_Inverse_58 Source #

d_'215''45'distrib'691''45''8846'_186 ∷ T_Level_18 → () → () → () → T_Inverse_58 Source #

du_'215''45'distrib'691''45''8846'_186 ∷ T_Inverse_58 Source #

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

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

d_'215''45'isMagma_212 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsMagma_86 Source #

du_'215''45'isMagma_212 ∷ T_Symmetric'45'kind_142 → T_IsMagma_86 Source #

d_'215''45'magma_220 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Magma_36 Source #

du_'215''45'magma_220 ∷ T_Symmetric'45'kind_142 → T_Magma_36 Source #

d_'215''45'isSemigroup_230 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsSemigroup_194 Source #

du_'215''45'isSemigroup_230 ∷ T_Symmetric'45'kind_142 → T_IsSemigroup_194 Source #

d_'215''45'semigroup_244 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Semigroup_206 Source #

du_'215''45'semigroup_244 ∷ T_Symmetric'45'kind_142 → T_Semigroup_206 Source #

d_'215''45'isMonoid_254 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsMonoid_358 Source #

du_'215''45'isMonoid_254 ∷ T_Symmetric'45'kind_142 → T_IsMonoid_358 Source #

d_'215''45'monoid_262 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Monoid_506 Source #

du_'215''45'monoid_262 ∷ T_Symmetric'45'kind_142 → T_Monoid_506 Source #

d_'215''45'isCommutativeMonoid_272 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsCommutativeMonoid_406 Source #

du_'215''45'isCommutativeMonoid_272 ∷ T_Symmetric'45'kind_142 → T_IsCommutativeMonoid_406 Source #

d_'215''45'commutativeMonoid_284 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_CommutativeMonoid_582 Source #

du_'215''45'commutativeMonoid_284 ∷ T_Symmetric'45'kind_142 → T_CommutativeMonoid_582 Source #

d_'8846''45'isMagma_294 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsMagma_86 Source #

du_'8846''45'isMagma_294 ∷ T_Symmetric'45'kind_142 → T_IsMagma_86 Source #

d_'8846''45'magma_302 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Magma_36 Source #

du_'8846''45'magma_302 ∷ T_Symmetric'45'kind_142 → T_Magma_36 Source #

d_'8846''45'isSemigroup_312 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsSemigroup_194 Source #

du_'8846''45'isSemigroup_312 ∷ T_Symmetric'45'kind_142 → T_IsSemigroup_194 Source #

d_'8846''45'semigroup_326 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Semigroup_206 Source #

du_'8846''45'semigroup_326 ∷ T_Symmetric'45'kind_142 → T_Semigroup_206 Source #

d_'8846''45'isMonoid_336 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsMonoid_358 Source #

du_'8846''45'isMonoid_336 ∷ T_Symmetric'45'kind_142 → T_IsMonoid_358 Source #

d_'8846''45'monoid_344 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Monoid_506 Source #

du_'8846''45'monoid_344 ∷ T_Symmetric'45'kind_142 → T_Monoid_506 Source #

d_'8846''45'isCommutativeMonoid_354 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsCommutativeMonoid_406 Source #

du_'8846''45'isCommutativeMonoid_354 ∷ T_Symmetric'45'kind_142 → T_IsCommutativeMonoid_406 Source #

d_'8846''45'commutativeMonoid_366 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_CommutativeMonoid_582 Source #

du_'8846''45'commutativeMonoid_366 ∷ T_Symmetric'45'kind_142 → T_CommutativeMonoid_582 Source #

d_'215''45''8846''45'isCommutativeSemiring_376 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsCommutativeSemiring_1344 Source #

du_'215''45''8846''45'isCommutativeSemiring_376 ∷ T_Symmetric'45'kind_142 → T_IsCommutativeSemiring_1344 Source #

d_'215''45''8846''45'commutativeSemiring_390 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_CommutativeSemiring_2094 Source #

du_'215''45''8846''45'commutativeSemiring_390 ∷ T_Symmetric'45'kind_142 → T_CommutativeSemiring_2094 Source #

d_ΠΠ'8596'ΠΠ_416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Inverse_58 Source #

du_ΠΠ'8596'ΠΠ_416 ∷ T_Inverse_58 Source #

d_'8707''8707''8596''8707''8707'_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Inverse_58 Source #

du_'8707''8707''8596''8707''8707'_442 ∷ T_Inverse_58 Source #

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

du_to_458 ∷ T_Σ_14 → T_Σ_14 Source #

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

du_from_474 ∷ T_Σ_14 → T_Σ_14 Source #

d_Π'8596'Π_498 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Inverse_58 Source #

du_Π'8596'Π_498 ∷ T_Inverse_58 Source #

d__'8594''45'cong'45''8660'__528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 Source #

du__'8594''45'cong'45''8660'__528 ∷ T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 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_Symmetric'45'kind_142 → () → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_'8594''45'cong_560 ∷ (() → (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_Symmetric'45'kind_142 → () → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

d_A'8594'C'8660'B'8594'D_582 ∷ 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_58 → T_Inverse_58 → T_Equivalence_16 Source #

du_A'8594'C'8660'B'8594'D_582 ∷ T_Inverse_58 → T_Inverse_58 → T_Equivalence_16 Source #

d_'172''45'cong'45''8660'_600 ∷ T_Level_18 → T_Level_18 → () → () → T_Equivalence_16 → T_Equivalence_16 Source #

du_'172''45'cong'45''8660'_600 ∷ T_Equivalence_16 → T_Equivalence_16 Source #

d_'172''45'cong_614 ∷ 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_Symmetric'45'kind_142 → () → () → AgdaAny → AgdaAny Source #

du_'172''45'cong_614 ∷ T_Symmetric'45'kind_142 → AgdaAny → AgdaAny Source #

d_Related'45'cong_640 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → AgdaAny → AgdaAny → T_Equivalence_16 Source #

du_Related'45'cong_640 ∷ T_Symmetric'45'kind_142 → AgdaAny → AgdaAny → T_Equivalence_16 Source #

d_True'8596'_672 ∷ T_Level_18 → () → T_Dec_32 → (AgdaAny → AgdaAny → T__'8801'__12) → T_Inverse_58 Source #

du_True'8596'_672 ∷ T_Dec_32 → T_Inverse_58 Source #

d_Σ'45''8801''44''8801''8596''8801'_700 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Inverse_58 Source #

du_Σ'45''8801''44''8801''8596''8801'_700 ∷ T_Inverse_58 Source #

d_to_716 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_from_724 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #

du_from_724 ∷ T_Σ_14 Source #

d_left'45'inverse'45'of_734 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_right'45'inverse'45'of_742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #

d_'215''45''8801''44''8801''8596''8801'_756 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T_Inverse_58 Source #

du_'215''45''8801''44''8801''8596''8801'_756 ∷ T_Inverse_58 Source #

d_to_770 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_from_776 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #

du_from_776 ∷ T_Σ_14 Source #

d_left'45'inverse'45'of_784 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_right'45'inverse'45'of_792 ∷ T_Level_18 → T_Level_18 → () → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #

d_'215''45''8801''215''8801''8596''8801''44''8801'_808 ∷ T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → T_Σ_14 → T_Inverse_58 Source #

du_'215''45''8801''215''8801''8596''8801''44''8801'_808 ∷ T_Inverse_58 Source #

d_to_820 ∷ T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_from_822 ∷ T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #

du_from_822 ∷ T__'8801'__12 → T_Σ_14 Source #

d_from'8728'to_826 ∷ T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_to'8728'from_830 ∷ T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #

d_'215''45'CommutativeMonoid_832 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_CommutativeMonoid_582 Source #

d_'8846''45'CommutativeMonoid_834 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_CommutativeMonoid_582 Source #

d_'215''8846''45'CommutativeSemiring_836 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_CommutativeSemiring_2094 Source #