Documentation

d_Σ'45'assoc_32 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_1960 #

du_Σ'45'assoc_32 :: T_Inverse_1960 #

d_'215''45'comm_42 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Inverse_1960 #

du_'215''45'comm_42 :: T_Inverse_1960 #

d_'215''45'identity'737'_50 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'215''45'identity'737'_50 :: T_Inverse_1960 #

d_'215''45'identity'691'_58 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'215''45'identity'691'_58 :: T_Inverse_1960 #

d_'215''45'identity_68 :: T_Level_18 -> T_Σ_14 #

du_'215''45'identity_68 :: T_Σ_14 #

d_'215''45'zero'737'_74 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'215''45'zero'737'_74 :: T_Inverse_1960 #

d_'215''45'zero'691'_86 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'215''45'zero'691'_86 :: T_Inverse_1960 #

d_'215''45'zero_98 :: T_Level_18 -> T_Σ_14 #

du_'215''45'zero_98 :: T_Σ_14 #

d_'8846''45'assoc_104 :: T_Level_18 -> () -> () -> () -> T_Inverse_1960 #

du_'8846''45'assoc_104 :: T_Inverse_1960 #

d_'8846''45'comm_124 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Inverse_1960 #

du_'8846''45'comm_124 :: T_Inverse_1960 #

d_'8846''45'identity'737'_128 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'8846''45'identity'737'_128 :: T_Inverse_1960 #

d_'8846''45'identity'691'_136 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'8846''45'identity'691'_136 :: T_Inverse_1960 #

d_'8846''45'identity_144 :: T_Level_18 -> T_Σ_14 #

du_'8846''45'identity_144 :: T_Σ_14 #

d_'215''45'distrib'737''45''8846'_150 :: T_Level_18 -> () -> () -> () -> T_Inverse_1960 #

du_'215''45'distrib'737''45''8846'_150 :: T_Inverse_1960 #

d_'215''45'distrib'691''45''8846'_172 :: T_Level_18 -> () -> () -> () -> T_Inverse_1960 #

du_'215''45'distrib'691''45''8846'_172 :: T_Inverse_1960 #

d_'215''45'distrib'45''8846'_190 :: T_Level_18 -> T_Σ_14 #

du_'215''45'distrib'45''8846'_190 :: T_Σ_14 #

d_'215''45'isMagma_198 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMagma_176 #

du_'215''45'isMagma_198 :: T_SymmetricKind_86 -> T_IsMagma_176 #

d_'215''45'magma_206 :: T_SymmetricKind_86 -> T_Level_18 -> T_Magma_68 #

du_'215''45'magma_206 :: T_SymmetricKind_86 -> T_Magma_68 #

d_'215''45'isSemigroup_216 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsSemigroup_472 #

du_'215''45'isSemigroup_216 :: T_SymmetricKind_86 -> T_IsSemigroup_472 #

d_'215''45'semigroup_230 :: T_SymmetricKind_86 -> T_Level_18 -> T_Semigroup_536 #

du_'215''45'semigroup_230 :: T_SymmetricKind_86 -> T_Semigroup_536 #

d_'215''45'isMonoid_240 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMonoid_686 #

du_'215''45'isMonoid_240 :: T_SymmetricKind_86 -> T_IsMonoid_686 #

d_'215''45'monoid_248 :: T_SymmetricKind_86 -> T_Level_18 -> T_Monoid_882 #

du_'215''45'monoid_248 :: T_SymmetricKind_86 -> T_Monoid_882 #

d_'215''45'isCommutativeMonoid_258 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeMonoid_736 #

du_'215''45'isCommutativeMonoid_258 :: T_SymmetricKind_86 -> T_IsCommutativeMonoid_736 #

d_'215''45'commutativeMonoid_270 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeMonoid_962 #

du_'215''45'commutativeMonoid_270 :: T_SymmetricKind_86 -> T_CommutativeMonoid_962 #

d_'8846''45'isMagma_280 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMagma_176 #

du_'8846''45'isMagma_280 :: T_SymmetricKind_86 -> T_IsMagma_176 #

d_'8846''45'magma_288 :: T_SymmetricKind_86 -> T_Level_18 -> T_Magma_68 #

du_'8846''45'magma_288 :: T_SymmetricKind_86 -> T_Magma_68 #

d_'8846''45'isSemigroup_298 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsSemigroup_472 #

du_'8846''45'isSemigroup_298 :: T_SymmetricKind_86 -> T_IsSemigroup_472 #

d_'8846''45'semigroup_312 :: T_SymmetricKind_86 -> T_Level_18 -> T_Semigroup_536 #

du_'8846''45'semigroup_312 :: T_SymmetricKind_86 -> T_Semigroup_536 #

d_'8846''45'isMonoid_322 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMonoid_686 #

du_'8846''45'isMonoid_322 :: T_SymmetricKind_86 -> T_IsMonoid_686 #

d_'8846''45'monoid_330 :: T_SymmetricKind_86 -> T_Level_18 -> T_Monoid_882 #

du_'8846''45'monoid_330 :: T_SymmetricKind_86 -> T_Monoid_882 #

d_'8846''45'isCommutativeMonoid_340 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeMonoid_736 #

du_'8846''45'isCommutativeMonoid_340 :: T_SymmetricKind_86 -> T_IsCommutativeMonoid_736 #

d_'8846''45'commutativeMonoid_352 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeMonoid_962 #

du_'8846''45'commutativeMonoid_352 :: T_SymmetricKind_86 -> T_CommutativeMonoid_962 #

d_'215''45''8846''45'isCommutativeSemiring_362 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeSemiring_1678 #

du_'215''45''8846''45'isCommutativeSemiring_362 :: T_SymmetricKind_86 -> T_IsCommutativeSemiring_1678 #

d_'215''45''8846''45'commutativeSemiring_376 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeSemiring_2446 #

du_'215''45''8846''45'commutativeSemiring_376 :: T_SymmetricKind_86 -> T_CommutativeSemiring_2446 #

d_ΠΠ'8596'ΠΠ_402 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_1960 #

du_ΠΠ'8596'ΠΠ_402 :: T_Inverse_1960 #

d_'8707''8707''8596''8707''8707'_428 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_1960 #

du_'8707''8707''8596''8707''8707'_428 :: T_Inverse_1960 #

d_to_444 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #

du_to_444 :: T_Σ_14 -> T_Σ_14 #

d_from_460 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #

du_from_460 :: T_Σ_14 -> T_Σ_14 #

d_Π'8596'Π_480 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Inverse_1960 #

du_Π'8596'Π_480 :: T_Inverse_1960 #

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 #

du_'8594''45'cong'45''8660'_486 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

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 #

du_'8594''45'cong'45''8596'_508 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

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 #

du_'8594''45'cong_544 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'172''45'cong'45''8660'_554 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Equivalence_1714 -> T_Equivalence_1714 #

du_'172''45'cong'45''8660'_554 :: T_Equivalence_1714 -> T_Equivalence_1714 #

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 #

du_'172''45'cong_564 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny #

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 #

du_Related'45'cong_574 :: () -> () -> () -> () -> T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> T_Equivalence_1714 #

d_True'8596'_606 :: T_Level_18 -> () -> T_Dec_20 -> (AgdaAny -> AgdaAny -> T__'8801'__12) -> T_Inverse_1960 #

du_True'8596'_606 :: T_Dec_20 -> T_Inverse_1960 #