Documentation

d_Σ'45'assoc_22 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_58 Source #

du_Σ'45'assoc_22 :: T_Inverse_58 Source #

d_'215''45'comm_52 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 Source #

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

d_'215''45'identity'737'_60 :: T_Level_14 -> () -> T_Inverse_58 Source #

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

d_'215''45'identity'691'_68 :: T_Level_14 -> () -> T_Inverse_58 Source #

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

d_'215''45'identity_78 :: T_Level_14 -> T_Σ_14 Source #

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

d_'215''45'zero'737'_84 :: T_Level_14 -> () -> T_Inverse_58 Source #

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

d_'215''45'zero'691'_96 :: T_Level_14 -> () -> T_Inverse_58 Source #

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

d_'215''45'zero_108 :: T_Level_14 -> T_Σ_14 Source #

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

d_'8846''45'assoc_114 :: T_Level_14 -> () -> () -> () -> T_Inverse_58 Source #

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

d_'8846''45'comm_138 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 Source #

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

d_'8846''45'identity'737'_142 :: T_Level_14 -> () -> T_Inverse_58 Source #

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

d_'8846''45'identity'691'_150 :: T_Level_14 -> () -> T_Inverse_58 Source #

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

d_'8846''45'identity_158 :: T_Level_14 -> T_Σ_14 Source #

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

d_'215''45'distrib'737''45''8846'_164 :: T_Level_14 -> () -> () -> () -> 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_14 -> () -> () -> () -> 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_14 -> T_Σ_14 Source #

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

d_'215''45'isMagma_212 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsMagma_98 Source #

du_'215''45'isMagma_212 :: T_Symmetric'45'kind_250 -> T_IsMagma_98 Source #

d_'215''45'magma_220 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Magma_36 Source #

du_'215''45'magma_220 :: T_Symmetric'45'kind_250 -> T_Magma_36 Source #

d_'215''45'isSemigroup_230 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsSemigroup_206 Source #

du_'215''45'isSemigroup_230 :: T_Symmetric'45'kind_250 -> T_IsSemigroup_206 Source #

d_'215''45'semigroup_244 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Semigroup_206 Source #

du_'215''45'semigroup_244 :: T_Symmetric'45'kind_250 -> T_Semigroup_206 Source #

d_'215''45'isMonoid_254 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsMonoid_370 Source #

du_'215''45'isMonoid_254 :: T_Symmetric'45'kind_250 -> T_IsMonoid_370 Source #

d_'215''45'monoid_262 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Monoid_502 Source #

du_'215''45'monoid_262 :: T_Symmetric'45'kind_250 -> T_Monoid_502 Source #

d_'215''45'isCommutativeMonoid_272 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsCommutativeMonoid_420 Source #

du_'215''45'isCommutativeMonoid_272 :: T_Symmetric'45'kind_250 -> T_IsCommutativeMonoid_420 Source #

d_'215''45'commutativeMonoid_284 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_CommutativeMonoid_582 Source #

du_'215''45'commutativeMonoid_284 :: T_Symmetric'45'kind_250 -> T_CommutativeMonoid_582 Source #

d_'8846''45'isMagma_294 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsMagma_98 Source #

du_'8846''45'isMagma_294 :: T_Symmetric'45'kind_250 -> T_IsMagma_98 Source #

d_'8846''45'magma_302 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Magma_36 Source #

du_'8846''45'magma_302 :: T_Symmetric'45'kind_250 -> T_Magma_36 Source #

d_'8846''45'isSemigroup_312 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsSemigroup_206 Source #

du_'8846''45'isSemigroup_312 :: T_Symmetric'45'kind_250 -> T_IsSemigroup_206 Source #

d_'8846''45'semigroup_326 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Semigroup_206 Source #

du_'8846''45'semigroup_326 :: T_Symmetric'45'kind_250 -> T_Semigroup_206 Source #

d_'8846''45'isMonoid_336 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsMonoid_370 Source #

du_'8846''45'isMonoid_336 :: T_Symmetric'45'kind_250 -> T_IsMonoid_370 Source #

d_'8846''45'monoid_344 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Monoid_502 Source #

du_'8846''45'monoid_344 :: T_Symmetric'45'kind_250 -> T_Monoid_502 Source #

d_'8846''45'isCommutativeMonoid_354 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsCommutativeMonoid_420 Source #

du_'8846''45'isCommutativeMonoid_354 :: T_Symmetric'45'kind_250 -> T_IsCommutativeMonoid_420 Source #

d_'8846''45'commutativeMonoid_366 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_CommutativeMonoid_582 Source #

du_'8846''45'commutativeMonoid_366 :: T_Symmetric'45'kind_250 -> T_CommutativeMonoid_582 Source #

d_'215''45''8846''45'isCommutativeSemiring_376 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsCommutativeSemiring_1244 Source #

du_'215''45''8846''45'isCommutativeSemiring_376 :: T_Symmetric'45'kind_250 -> T_IsCommutativeSemiring_1244 Source #

d_'215''45''8846''45'commutativeSemiring_390 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_CommutativeSemiring_2036 Source #

du_'215''45''8846''45'commutativeSemiring_390 :: T_Symmetric'45'kind_250 -> T_CommutativeSemiring_2036 Source #

d_ΠΠ'8596'ΠΠ_416 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_58 Source #

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

d_'8707''8707''8596''8707''8707'_442 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_58 Source #

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

d_to_458 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 Source #

du_to_458 :: T_Σ_14 -> T_Σ_14 Source #

d_from_474 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 Source #

du_from_474 :: T_Σ_14 -> T_Σ_14 Source #

d_Π'8596'Π_498 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Inverse_58 Source #

du_Π'8596'Π_498 :: T_Inverse_58 Source #

d__'8594''45'cong'45''8660'__528 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> () -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (() -> (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_250 -> () -> () -> () -> () -> 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_250 -> () -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_A'8594'C'8660'B'8594'D_582 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (() -> (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_14 -> T_Level_14 -> () -> () -> 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_14 -> T_Level_14 -> (() -> (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_250 -> () -> () -> AgdaAny -> AgdaAny Source #

du_'172''45'cong_614 :: T_Symmetric'45'kind_250 -> AgdaAny -> AgdaAny Source #

d_Related'45'cong_640 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> () -> AgdaAny -> AgdaAny -> T_Equivalence_16 Source #

du_Related'45'cong_640 :: T_Symmetric'45'kind_250 -> AgdaAny -> AgdaAny -> T_Equivalence_16 Source #

d_True'8596'_672 :: T_Level_14 -> () -> 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''8594''8801'_704 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 Source #

d_Σ'45''8801''44''8801''8592''8801'_708 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T_Σ_14 Source #

du_Σ'45''8801''44''8801''8592''8801'_708 :: T_Σ_14 Source #

d_left'45'inverse'45'of_714 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 Source #

d_right'45'inverse'45'of_718 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T__'8801'__12 Source #

d_Σ'45''8801''44''8801''8596''8801'_722 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Inverse_58 Source #

du_Σ'45''8801''44''8801''8596''8801'_722 :: T_Inverse_58 Source #

d_'215''45''8801''44''8801''8594''8801'_740 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 Source #

d_'215''45''8801''44''8801''8592''8801'_742 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T_Σ_14 Source #

du_'215''45''8801''44''8801''8592''8801'_742 :: T_Σ_14 Source #

d_left'45'inverse'45'of_746 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 Source #

d_right'45'inverse'45'of_750 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T__'8801'__12 Source #

d_'215''45''8801''44''8801''8596''8801'_752 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Σ_14 -> T_Σ_14 -> T_Inverse_58 Source #

du_'215''45''8801''44''8801''8596''8801'_752 :: T_Inverse_58 Source #

d_'215''45''8801''215''8801''8596''8801''44''8801'_768 :: T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Inverse_58 Source #

du_'215''45''8801''215''8801''8596''8801''44''8801'_768 :: T_Inverse_58 Source #