{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Algebra.Structures.Biased where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Consequences.Setoid
import qualified MAlonzo.Code.Algebra.Structures

-- Algebra.Structures.Biased._._DistributesOver_
d__DistributesOver__18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d__DistributesOver__18 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d__DistributesOver__18 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._._DistributesOverʳ_
d__DistributesOver'691'__20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d__DistributesOver'691'__20 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d__DistributesOver'691'__20 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._._DistributesOverˡ_
d__DistributesOver'737'__22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d__DistributesOver'737'__22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d__DistributesOver'737'__22 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.Commutative
d_Commutative_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Commutative_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Commutative_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.Identity
d_Identity_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Identity_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Identity_50 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.LeftIdentity
d_LeftIdentity_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_LeftIdentity_64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_LeftIdentity_64 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.LeftZero
d_LeftZero_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_LeftZero_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_LeftZero_68 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.RightIdentity
d_RightIdentity_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_RightIdentity_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_RightIdentity_76 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.RightZero
d_RightZero_80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_RightZero_80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_RightZero_80 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.Zero
d_Zero_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Zero_84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Zero_84 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Structures.Biased._.IsAbelianGroup
d_IsAbelianGroup_88 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsAbelianGroup_88 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Algebra.Structures.Biased._.IsCommutativeMonoid
d_IsCommutativeMonoid_100 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeMonoid_100 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Algebra.Structures.Biased._.IsCommutativeSemiring
d_IsCommutativeSemiring_106 :: p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeSemiring_106 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Algebra.Structures.Biased._.IsMonoid
d_IsMonoid_120 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsMonoid_120 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Algebra.Structures.Biased._.IsRing
d_IsRing_124 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRing_124 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
-- Algebra.Structures.Biased._.IsSemigroup
d_IsSemigroup_128 :: p -> p -> p -> p -> p -> T_Level_18
d_IsSemigroup_128 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ
d_IsCommutativeMonoid'737'_1514 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeMonoid'737'_1514 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsCommutativeMonoid'737'_1514
  = C_IsCommutativeMonoid'737''46'constructor_18101 MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
                                                    (AgdaAny -> AgdaAny)
                                                    (AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ.isSemigroup
d_isSemigroup_1526 ::
  T_IsCommutativeMonoid'737'_1514 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_isSemigroup_1526 :: T_IsCommutativeMonoid'737'_1514 -> T_IsSemigroup_194
d_isSemigroup_1526 T_IsCommutativeMonoid'737'_1514
v0
  = case T_IsCommutativeMonoid'737'_1514 -> T_IsCommutativeMonoid'737'_1514
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v0 of
      C_IsCommutativeMonoid'737''46'constructor_18101 T_IsSemigroup_194
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 -> T_IsSemigroup_194 -> T_IsSemigroup_194
forall a b. a -> b
coe T_IsSemigroup_194
v1
      T_IsCommutativeMonoid'737'_1514
_ -> T_IsSemigroup_194
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ.identityˡ
d_identity'737'_1528 ::
  T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
d_identity'737'_1528 :: T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
d_identity'737'_1528 T_IsCommutativeMonoid'737'_1514
v0
  = case T_IsCommutativeMonoid'737'_1514 -> T_IsCommutativeMonoid'737'_1514
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v0 of
      C_IsCommutativeMonoid'737''46'constructor_18101 T_IsSemigroup_194
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2
      T_IsCommutativeMonoid'737'_1514
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ.comm
d_comm_1530 ::
  T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1530 :: T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1530 T_IsCommutativeMonoid'737'_1514
v0
  = case T_IsCommutativeMonoid'737'_1514 -> T_IsCommutativeMonoid'737'_1514
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v0 of
      C_IsCommutativeMonoid'737''46'constructor_18101 T_IsSemigroup_194
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsCommutativeMonoid'737'_1514
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ.identityʳ
d_identity'691'_1558 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
d_identity'691'_1558 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'737'_1514
-> AgdaAny
-> AgdaAny
d_identity'691'_1558 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'737'_1514
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
du_identity'691'_1558 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'737'_1514
v6
du_identity'691'_1558 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
du_identity'691'_1558 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
du_identity'691'_1558 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeMonoid'737'_1514
v2
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'id'737''8658'id'691'_172
      (let v3 :: T_IsSemigroup_194
v3 = T_IsCommutativeMonoid'737'_1514 -> T_IsSemigroup_194
d_isSemigroup_1526 (T_IsCommutativeMonoid'737'_1514 -> T_IsCommutativeMonoid'737'_1514
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
            ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1530 (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
      ((T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
d_identity'737'_1528 (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2))
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ.identity
d_identity_1560 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'737'_1514 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_identity_1560 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'737'_1514
-> T_Σ_14
d_identity_1560 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'737'_1514
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> T_Σ_14
du_identity_1560 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'737'_1514
v6
du_identity_1560 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'737'_1514 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_identity_1560 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> T_Σ_14
du_identity_1560 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeMonoid'737'_1514
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
d_identity'737'_1528 (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeMonoid'737'_1514
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny
du_identity'691'_1558 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2))
-- Algebra.Structures.Biased.IsCommutativeMonoidˡ.isCommutativeMonoid
d_isCommutativeMonoid_1562 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'737'_1514 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_isCommutativeMonoid_1562 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'737'_1514
-> T_IsCommutativeMonoid_406
d_isCommutativeMonoid_1562 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'737'_1514
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'737'_1514
-> T_IsCommutativeMonoid_406
du_isCommutativeMonoid_1562 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'737'_1514
v6
du_isCommutativeMonoid_1562 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'737'_1514 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
du_isCommutativeMonoid_1562 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'737'_1514
-> T_IsCommutativeMonoid_406
du_isCommutativeMonoid_1562 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeMonoid'737'_1514
v2
  = (T_IsMonoid_358
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe
      T_IsMonoid_358
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_9361
      ((T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
         ((T_IsCommutativeMonoid'737'_1514 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514 -> T_IsSemigroup_194
d_isSemigroup_1526 (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2))
         (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'737'_1514 -> T_Σ_14
du_identity_1560 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2)))
      ((T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1530 (T_IsCommutativeMonoid'737'_1514 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'737'_1514
v2))
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ
d_IsCommutativeMonoid'691'_1568 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeMonoid'691'_1568 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsCommutativeMonoid'691'_1568
  = C_IsCommutativeMonoid'691''46'constructor_19839 MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
                                                    (AgdaAny -> AgdaAny)
                                                    (AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ.isSemigroup
d_isSemigroup_1580 ::
  T_IsCommutativeMonoid'691'_1568 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_isSemigroup_1580 :: T_IsCommutativeMonoid'691'_1568 -> T_IsSemigroup_194
d_isSemigroup_1580 T_IsCommutativeMonoid'691'_1568
v0
  = case T_IsCommutativeMonoid'691'_1568 -> T_IsCommutativeMonoid'691'_1568
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v0 of
      C_IsCommutativeMonoid'691''46'constructor_19839 T_IsSemigroup_194
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 -> T_IsSemigroup_194 -> T_IsSemigroup_194
forall a b. a -> b
coe T_IsSemigroup_194
v1
      T_IsCommutativeMonoid'691'_1568
_ -> T_IsSemigroup_194
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ.identityʳ
d_identity'691'_1582 ::
  T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
d_identity'691'_1582 :: T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
d_identity'691'_1582 T_IsCommutativeMonoid'691'_1568
v0
  = case T_IsCommutativeMonoid'691'_1568 -> T_IsCommutativeMonoid'691'_1568
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v0 of
      C_IsCommutativeMonoid'691''46'constructor_19839 T_IsSemigroup_194
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2
      T_IsCommutativeMonoid'691'_1568
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ.comm
d_comm_1584 ::
  T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1584 :: T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1584 T_IsCommutativeMonoid'691'_1568
v0
  = case T_IsCommutativeMonoid'691'_1568 -> T_IsCommutativeMonoid'691'_1568
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v0 of
      C_IsCommutativeMonoid'691''46'constructor_19839 T_IsSemigroup_194
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsCommutativeMonoid'691'_1568
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ.identityˡ
d_identity'737'_1612 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
d_identity'737'_1612 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'691'_1568
-> AgdaAny
-> AgdaAny
d_identity'737'_1612 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'691'_1568
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
du_identity'737'_1612 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'691'_1568
v6
du_identity'737'_1612 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
du_identity'737'_1612 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
du_identity'737'_1612 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeMonoid'691'_1568
v2
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'id'691''8658'id'737'_178
      (let v3 :: T_IsSemigroup_194
v3 = T_IsCommutativeMonoid'691'_1568 -> T_IsSemigroup_194
d_isSemigroup_1580 (T_IsCommutativeMonoid'691'_1568 -> T_IsCommutativeMonoid'691'_1568
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
            ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1584 (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
      ((T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
d_identity'691'_1582 (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2))
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ.identity
d_identity_1614 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'691'_1568 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_identity_1614 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'691'_1568
-> T_Σ_14
d_identity_1614 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'691'_1568
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> T_Σ_14
du_identity_1614 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'691'_1568
v6
du_identity_1614 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'691'_1568 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_identity_1614 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> T_Σ_14
du_identity_1614 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeMonoid'691'_1568
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeMonoid'691'_1568
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
du_identity'737'_1612 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2))
      ((T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny
d_identity'691'_1582 (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2))
-- Algebra.Structures.Biased.IsCommutativeMonoidʳ.isCommutativeMonoid
d_isCommutativeMonoid_1616 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'691'_1568 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_isCommutativeMonoid_1616 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'691'_1568
-> T_IsCommutativeMonoid_406
d_isCommutativeMonoid_1616 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'691'_1568
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'691'_1568
-> T_IsCommutativeMonoid_406
du_isCommutativeMonoid_1616 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_IsCommutativeMonoid'691'_1568
v6
du_isCommutativeMonoid_1616 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeMonoid'691'_1568 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
du_isCommutativeMonoid_1616 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeMonoid'691'_1568
-> T_IsCommutativeMonoid_406
du_isCommutativeMonoid_1616 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeMonoid'691'_1568
v2
  = (T_IsMonoid_358
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe
      T_IsMonoid_358
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_9361
      ((T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
         ((T_IsCommutativeMonoid'691'_1568 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568 -> T_IsSemigroup_194
d_isSemigroup_1580 (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2))
         (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid'691'_1568 -> T_Σ_14
du_identity_1614 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2)))
      ((T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1584 (T_IsCommutativeMonoid'691'_1568 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoid'691'_1568
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ
d_IsCommutativeSemiring'737'_1626 :: p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeSemiring'737'_1626 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
data T_IsCommutativeSemiring'737'_1626
  = C_IsCommutativeSemiring'737''46'constructor_21625 MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
                                                      MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
                                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                                      (AgdaAny -> AgdaAny)
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.+-isCommutativeMonoid
d_'43''45'isCommutativeMonoid_1644 ::
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1644 :: T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1644 T_IsCommutativeSemiring'737'_1626
v0
  = case T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring'737'_1626
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v0 of
      C_IsCommutativeSemiring'737''46'constructor_21625 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v1
      T_IsCommutativeSemiring'737'_1626
_ -> T_IsCommutativeMonoid_406
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.*-isCommutativeMonoid
d_'42''45'isCommutativeMonoid_1646 ::
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 :: T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 T_IsCommutativeSemiring'737'_1626
v0
  = case T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring'737'_1626
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v0 of
      C_IsCommutativeSemiring'737''46'constructor_21625 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v2
      T_IsCommutativeSemiring'737'_1626
_ -> T_IsCommutativeMonoid_406
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.distribʳ
d_distrib'691'_1648 ::
  T_IsCommutativeSemiring'737'_1626 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'691'_1648 :: T_IsCommutativeSemiring'737'_1626
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'691'_1648 T_IsCommutativeSemiring'737'_1626
v0
  = case T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring'737'_1626
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v0 of
      C_IsCommutativeSemiring'737''46'constructor_21625 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsCommutativeSemiring'737'_1626
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.zeroˡ
d_zero'737'_1650 ::
  T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny
d_zero'737'_1650 :: T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny
d_zero'737'_1650 T_IsCommutativeSemiring'737'_1626
v0
  = case T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring'737'_1626
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v0 of
      C_IsCommutativeSemiring'737''46'constructor_21625 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v4
      T_IsCommutativeSemiring'737'_1626
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.*-CM.comm
d_comm_1698 ::
  T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1698 :: T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1698 T_IsCommutativeSemiring'737'_1626
v0
  = (T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
      ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v0))
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.distribˡ
d_distrib'737'_1736 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'737'_1626 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'737'_1736 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_distrib'737'_1736 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'737'_1626
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_distrib'737'_1736 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 T_IsCommutativeSemiring'737'_1626
v8
du_distrib'737'_1736 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  T_IsCommutativeSemiring'737'_1626 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib'737'_1736 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_distrib'737'_1736 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 T_IsCommutativeSemiring'737'_1626
v2
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'distr'691''8658'distr'737'_322
      (let v3 :: T_IsCommutativeMonoid_406
v3 = T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1644 (T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring'737'_1626
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: T_IsMonoid_358
v4
                = T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416 (T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v3) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsSemigroup_194
v5
                   = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5))))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
      ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
               ((T_IsCommutativeMonoid_406 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416
                  ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1644 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))))))
      ((T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
         ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2)))
      ((T_IsCommutativeSemiring'737'_1626
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'691'_1648 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.distrib
d_distrib_1738 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_distrib_1738 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> T_Σ_14
d_distrib_1738 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'737'_1626
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
-> T_Σ_14
du_distrib_1738 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 T_IsCommutativeSemiring'737'_1626
v8
du_distrib_1738 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_distrib_1738 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
-> T_Σ_14
du_distrib_1738 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 T_IsCommutativeSemiring'737'_1626
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'737'_1626
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_distrib'737'_1736 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))
      ((T_IsCommutativeSemiring'737'_1626
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'691'_1648 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.zeroʳ
d_zero'691'_1740 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny -> T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny
d_zero'691'_1740 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
d_zero'691'_1740 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'737'_1626
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
du_zero'691'_1740 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 T_IsCommutativeSemiring'737'_1626
v8
du_zero'691'_1740 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny
du_zero'691'_1740 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
du_zero'691'_1740 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeSemiring'737'_1626
v2
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'ze'737''8658'ze'691'_184
      (let v3 :: T_IsCommutativeMonoid_406
v3 = T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1644 (T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring'737'_1626
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: T_IsMonoid_358
v4
                = T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416 (T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v3) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsSemigroup_194
v5
                   = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5))))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
      ((T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
         ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ((T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny
d_zero'737'_1650 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.zero
d_zero_1742 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_zero_1742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> T_Σ_14
d_zero_1742 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'737'_1626
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeSemiring'737'_1626 -> T_Σ_14
du_zero_1742 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 T_IsCommutativeSemiring'737'_1626
v8
du_zero_1742 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_zero_1742 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeSemiring'737'_1626 -> T_Σ_14
du_zero_1742 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeSemiring'737'_1626
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> AgdaAny -> AgdaAny
d_zero'737'_1650 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeSemiring'737'_1626
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> AgdaAny
-> AgdaAny
du_zero'691'_1740 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringˡ.isCommutativeSemiring
d_isCommutativeSemiring_1744 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1344
d_isCommutativeSemiring_1744 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring_1344
d_isCommutativeSemiring_1744 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'737'_1626
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring_1344
du_isCommutativeSemiring_1744 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 T_IsCommutativeSemiring'737'_1626
v8
du_isCommutativeSemiring_1744 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeSemiring'737'_1626 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1344
du_isCommutativeSemiring_1744 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring_1344
du_isCommutativeSemiring_1744 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 T_IsCommutativeSemiring'737'_1626
v3
  = (T_IsSemiring_1238
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemiring_1344)
-> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1344
forall a b. a -> b
coe
      T_IsSemiring_1238
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemiring_1344
MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemiring'46'constructor_40675
      ((T_IsSemiringWithoutAnnihilatingZero_1142
 -> T_Σ_14 -> T_IsSemiring_1238)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsSemiringWithoutAnnihilatingZero_1142
-> T_Σ_14 -> T_IsSemiring_1238
MAlonzo.Code.Algebra.Structures.C_IsSemiring'46'constructor_37213
         ((T_IsCommutativeMonoid_406
 -> T_IsMonoid_358
 -> T_Σ_14
 -> T_IsSemiringWithoutAnnihilatingZero_1142)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsCommutativeMonoid_406
-> T_IsMonoid_358
-> T_Σ_14
-> T_IsSemiringWithoutAnnihilatingZero_1142
MAlonzo.Code.Algebra.Structures.C_IsSemiringWithoutAnnihilatingZero'46'constructor_33703
            ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1644 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v3))
            ((T_IsCommutativeMonoid_406 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416
               ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v3)))
            (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'737'_1626
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
-> T_Σ_14
du_distrib_1738 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v3)))
         (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeSemiring'737'_1626 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeSemiring'737'_1626 -> T_Σ_14
du_zero_1742 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v3)))
      ((T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
         ((T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1646 (T_IsCommutativeSemiring'737'_1626 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'737'_1626
v3)))
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ
d_IsCommutativeSemiring'691'_1754 :: p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeSemiring'691'_1754 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
data T_IsCommutativeSemiring'691'_1754
  = C_IsCommutativeSemiring'691''46'constructor_26987 MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
                                                      MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
                                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                                      (AgdaAny -> AgdaAny)
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.+-isCommutativeMonoid
d_'43''45'isCommutativeMonoid_1772 ::
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1772 :: T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1772 T_IsCommutativeSemiring'691'_1754
v0
  = case T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring'691'_1754
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v0 of
      C_IsCommutativeSemiring'691''46'constructor_26987 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v1
      T_IsCommutativeSemiring'691'_1754
_ -> T_IsCommutativeMonoid_406
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.*-isCommutativeMonoid
d_'42''45'isCommutativeMonoid_1774 ::
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 :: T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 T_IsCommutativeSemiring'691'_1754
v0
  = case T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring'691'_1754
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v0 of
      C_IsCommutativeSemiring'691''46'constructor_26987 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v2
      T_IsCommutativeSemiring'691'_1754
_ -> T_IsCommutativeMonoid_406
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.distribˡ
d_distrib'737'_1776 ::
  T_IsCommutativeSemiring'691'_1754 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'737'_1776 :: T_IsCommutativeSemiring'691'_1754
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'737'_1776 T_IsCommutativeSemiring'691'_1754
v0
  = case T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring'691'_1754
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v0 of
      C_IsCommutativeSemiring'691''46'constructor_26987 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsCommutativeSemiring'691'_1754
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.zeroʳ
d_zero'691'_1778 ::
  T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny
d_zero'691'_1778 :: T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny
d_zero'691'_1778 T_IsCommutativeSemiring'691'_1754
v0
  = case T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring'691'_1754
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v0 of
      C_IsCommutativeSemiring'691''46'constructor_26987 T_IsCommutativeMonoid_406
v1 T_IsCommutativeMonoid_406
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v4
      T_IsCommutativeSemiring'691'_1754
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.*-CM.comm
d_comm_1826 ::
  T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1826 :: T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_1826 T_IsCommutativeSemiring'691'_1754
v0
  = (T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
      ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v0))
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.distribʳ
d_distrib'691'_1864 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'691'_1754 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'691'_1864 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_distrib'691'_1864 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'691'_1754
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_distrib'691'_1864 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 T_IsCommutativeSemiring'691'_1754
v8
du_distrib'691'_1864 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  T_IsCommutativeSemiring'691'_1754 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib'691'_1864 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_distrib'691'_1864 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 T_IsCommutativeSemiring'691'_1754
v2
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'distr'737''8658'distr'691'_312
      (let v3 :: T_IsCommutativeMonoid_406
v3 = T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1772 (T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring'691'_1754
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: T_IsMonoid_358
v4
                = T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416 (T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v3) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsSemigroup_194
v5
                   = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5))))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
      ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
               ((T_IsCommutativeMonoid_406 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416
                  ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1772 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))))))
      ((T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
         ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2)))
      ((T_IsCommutativeSemiring'691'_1754
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'737'_1776 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.distrib
d_distrib_1866 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_distrib_1866 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> T_Σ_14
d_distrib_1866 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'691'_1754
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'691'_1754
-> T_Σ_14
du_distrib_1866 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 T_IsCommutativeSemiring'691'_1754
v8
du_distrib_1866 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_distrib_1866 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'691'_1754
-> T_Σ_14
du_distrib_1866 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 T_IsCommutativeSemiring'691'_1754
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_IsCommutativeSemiring'691'_1754
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib'737'_1776 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'691'_1754
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_distrib'691'_1864 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.zeroˡ
d_zero'737'_1868 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny -> T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny
d_zero'737'_1868 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
d_zero'737'_1868 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'691'_1754
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
du_zero'737'_1868 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 T_IsCommutativeSemiring'691'_1754
v8
du_zero'737'_1868 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny
du_zero'737'_1868 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
du_zero'737'_1868 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeSemiring'691'_1754
v2
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'ze'691''8658'ze'737'_190
      (let v3 :: T_IsCommutativeMonoid_406
v3 = T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1772 (T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring'691'_1754
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: T_IsMonoid_358
v4
                = T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416 (T_IsCommutativeMonoid_406 -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe T_IsCommutativeMonoid_406
v3) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsSemigroup_194
v5
                   = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5))))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
      ((T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
         ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ((T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny
d_zero'691'_1778 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.zero
d_zero_1870 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_zero_1870 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> T_Σ_14
d_zero_1870 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'691'_1754
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeSemiring'691'_1754 -> T_Σ_14
du_zero_1870 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 T_IsCommutativeSemiring'691'_1754
v8
du_zero_1870 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_zero_1870 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeSemiring'691'_1754 -> T_Σ_14
du_zero_1870 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_IsCommutativeSemiring'691'_1754
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeSemiring'691'_1754
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> AgdaAny
-> AgdaAny
du_zero'737'_1868 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))
      ((T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> AgdaAny -> AgdaAny
d_zero'691'_1778 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v2))
-- Algebra.Structures.Biased.IsCommutativeSemiringʳ.isCommutativeSemiring
d_isCommutativeSemiring_1872 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1344
d_isCommutativeSemiring_1872 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring_1344
d_isCommutativeSemiring_1872 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 ~AgdaAny
v7 T_IsCommutativeSemiring'691'_1754
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring_1344
du_isCommutativeSemiring_1872 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 T_IsCommutativeSemiring'691'_1754
v8
du_isCommutativeSemiring_1872 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsCommutativeSemiring'691'_1754 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1344
du_isCommutativeSemiring_1872 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'691'_1754
-> T_IsCommutativeSemiring_1344
du_isCommutativeSemiring_1872 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 T_IsCommutativeSemiring'691'_1754
v3
  = (T_IsSemiring_1238
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemiring_1344)
-> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring_1344
forall a b. a -> b
coe
      T_IsSemiring_1238
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeSemiring_1344
MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemiring'46'constructor_40675
      ((T_IsSemiringWithoutAnnihilatingZero_1142
 -> T_Σ_14 -> T_IsSemiring_1238)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsSemiringWithoutAnnihilatingZero_1142
-> T_Σ_14 -> T_IsSemiring_1238
MAlonzo.Code.Algebra.Structures.C_IsSemiring'46'constructor_37213
         ((T_IsCommutativeMonoid_406
 -> T_IsMonoid_358
 -> T_Σ_14
 -> T_IsSemiringWithoutAnnihilatingZero_1142)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsCommutativeMonoid_406
-> T_IsMonoid_358
-> T_Σ_14
-> T_IsSemiringWithoutAnnihilatingZero_1142
MAlonzo.Code.Algebra.Structures.C_IsSemiringWithoutAnnihilatingZero'46'constructor_33703
            ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'43''45'isCommutativeMonoid_1772 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v3))
            ((T_IsCommutativeMonoid_406 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCommutativeMonoid_406 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_416
               ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v3)))
            (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'691'_1754
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'691'_1754
-> T_Σ_14
du_distrib_1866 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v3)))
         (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeSemiring'691'_1754 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeSemiring'691'_1754 -> T_Σ_14
du_zero_1870 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v3)))
      ((T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_418
         ((T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754 -> T_IsCommutativeMonoid_406
d_'42''45'isCommutativeMonoid_1774 (T_IsCommutativeSemiring'691'_1754 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeSemiring'691'_1754
v3)))
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero
d_IsRingWithoutAnnihilatingZero_1884 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRingWithoutAnnihilatingZero_1884 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8
  = ()
data T_IsRingWithoutAnnihilatingZero_1884
  = C_IsRingWithoutAnnihilatingZero'46'constructor_32383 MAlonzo.Code.Algebra.Structures.T_IsAbelianGroup_662
                                                         MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
                                                         MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.+-isAbelianGroup
d_'43''45'isAbelianGroup_1902 ::
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Algebra.Structures.T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 :: T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 T_IsRingWithoutAnnihilatingZero_1884
v0
  = case T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v0 of
      C_IsRingWithoutAnnihilatingZero'46'constructor_32383 T_IsAbelianGroup_662
v1 T_IsMonoid_358
v2 T_Σ_14
v3
        -> T_IsAbelianGroup_662 -> T_IsAbelianGroup_662
forall a b. a -> b
coe T_IsAbelianGroup_662
v1
      T_IsRingWithoutAnnihilatingZero_1884
_ -> T_IsAbelianGroup_662
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.*-isMonoid
d_'42''45'isMonoid_1904 ::
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'42''45'isMonoid_1904 :: T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358
d_'42''45'isMonoid_1904 T_IsRingWithoutAnnihilatingZero_1884
v0
  = case T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v0 of
      C_IsRingWithoutAnnihilatingZero'46'constructor_32383 T_IsAbelianGroup_662
v1 T_IsMonoid_358
v2 T_Σ_14
v3
        -> T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v2
      T_IsRingWithoutAnnihilatingZero_1884
_ -> T_IsMonoid_358
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.distrib
d_distrib_1906 ::
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_distrib_1906 :: T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14
d_distrib_1906 T_IsRingWithoutAnnihilatingZero_1884
v0
  = case T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v0 of
      C_IsRingWithoutAnnihilatingZero'46'constructor_32383 T_IsAbelianGroup_662
v1 T_IsMonoid_358
v2 T_Σ_14
v3
        -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3
      T_IsRingWithoutAnnihilatingZero_1884
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.zeroˡ
d_zero'737'_2002 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny -> AgdaAny
d_zero'737'_2002 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
d_zero'737'_2002 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 ~AgdaAny
v8 T_IsRingWithoutAnnihilatingZero_1884
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
du_zero'737'_2002 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 T_IsRingWithoutAnnihilatingZero_1884
v9
du_zero'737'_2002 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny -> AgdaAny
du_zero'737'_2002 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
du_zero'737'_2002 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 T_IsRingWithoutAnnihilatingZero_1884
v4
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_assoc'43'distrib'691''43'id'691''43'inv'691''8658'ze'737'_364
      (let v5 :: T_IsAbelianGroup_662
v5 = T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v6 :: T_IsGroup_580
v6 = T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674 (T_IsAbelianGroup_662 -> T_IsAbelianGroup_662
forall a b. a -> b
coe T_IsAbelianGroup_662
v5) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v7 :: T_IsMonoid_358
v7
                   = T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> T_IsGroup_580
forall a b. a -> b
coe T_IsGroup_580
v6) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v8 :: T_IsSemigroup_194
v8
                      = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v7) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v8)))))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
      ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
               ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594
                  ((T_IsAbelianGroup_662 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674
                     ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4)))))))
      ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
               ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358
d_'42''45'isMonoid_1904 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4)))))
      ((T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_204
         ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
            ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594
               ((T_IsAbelianGroup_662 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674
                  ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))))))
      ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
         ((T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14
d_distrib_1906 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4)))
      (let v5 :: T_IsAbelianGroup_662
v5 = T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v6 :: T_IsGroup_580
v6 = T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674 (T_IsAbelianGroup_662 -> T_IsAbelianGroup_662
forall a b. a -> b
coe T_IsAbelianGroup_662
v5) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsMonoid_358 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_identity'691'_400
               ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> AgdaAny
forall a b. a -> b
coe T_IsGroup_580
v6)))))
      (let v5 :: T_IsAbelianGroup_662
v5 = T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsGroup_580 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsGroup_580 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_inverse'691'_642
            ((T_IsAbelianGroup_662 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674 (T_IsAbelianGroup_662 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroup_662
v5))))
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.zeroʳ
d_zero'691'_2004 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny -> AgdaAny
d_zero'691'_2004 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
d_zero'691'_2004 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 ~AgdaAny
v8 T_IsRingWithoutAnnihilatingZero_1884
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
du_zero'691'_2004 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 T_IsRingWithoutAnnihilatingZero_1884
v9
du_zero'691'_2004 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny -> AgdaAny
du_zero'691'_2004 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
du_zero'691'_2004 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 T_IsRingWithoutAnnihilatingZero_1884
v4
  = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Consequences.Setoid.du_assoc'43'distrib'737''43'id'691''43'inv'691''8658'ze'691'_376
      (let v5 :: T_IsAbelianGroup_662
v5 = T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v6 :: T_IsGroup_580
v6 = T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674 (T_IsAbelianGroup_662 -> T_IsAbelianGroup_662
forall a b. a -> b
coe T_IsAbelianGroup_662
v5) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v7 :: T_IsMonoid_358
v7
                   = T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> T_IsGroup_580
forall a b. a -> b
coe T_IsGroup_580
v6) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v8 :: T_IsSemigroup_194
v8
                      = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v7) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v8)))))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
      ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
               ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594
                  ((T_IsAbelianGroup_662 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674
                     ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4)))))))
      ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
               ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358
d_'42''45'isMonoid_1904 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4)))))
      ((T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_204
         ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
            ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594
               ((T_IsAbelianGroup_662 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674
                  ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))))))
      ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
         ((T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14
d_distrib_1906 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4)))
      (let v5 :: T_IsAbelianGroup_662
v5 = T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v6 :: T_IsGroup_580
v6 = T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674 (T_IsAbelianGroup_662 -> T_IsAbelianGroup_662
forall a b. a -> b
coe T_IsAbelianGroup_662
v5) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsMonoid_358 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMonoid_358 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_identity'691'_400
               ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> AgdaAny
forall a b. a -> b
coe T_IsGroup_580
v6)))))
      (let v5 :: T_IsAbelianGroup_662
v5 = T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRingWithoutAnnihilatingZero_1884
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsGroup_580 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsGroup_580 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_inverse'691'_642
            ((T_IsAbelianGroup_662 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroup_662 -> T_IsGroup_580
MAlonzo.Code.Algebra.Structures.d_isGroup_674 (T_IsAbelianGroup_662 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroup_662
v5))))
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.zero
d_zero_2006 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_zero_2006 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_Σ_14
d_zero_2006 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 ~AgdaAny
v8 T_IsRingWithoutAnnihilatingZero_1884
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_Σ_14
du_zero_2006 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 T_IsRingWithoutAnnihilatingZero_1884
v9
du_zero_2006 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_zero_2006 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_Σ_14
du_zero_2006 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 T_IsRingWithoutAnnihilatingZero_1884
v4
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsRingWithoutAnnihilatingZero_1884
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
du_zero'737'_2002 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsRingWithoutAnnihilatingZero_1884
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> AgdaAny
-> AgdaAny
du_zero'691'_2004 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))
-- Algebra.Structures.Biased.IsRingWithoutAnnihilatingZero.isRing
d_isRing_2008 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Algebra.Structures.T_IsRing_1584
d_isRing_2008 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRing_1584
d_isRing_2008 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 ~AgdaAny
v8 T_IsRingWithoutAnnihilatingZero_1884
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRing_1584
du_isRing_2008 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 T_IsRingWithoutAnnihilatingZero_1884
v9
du_isRing_2008 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T_IsRingWithoutAnnihilatingZero_1884 ->
  MAlonzo.Code.Algebra.Structures.T_IsRing_1584
du_isRing_2008 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_IsRing_1584
du_isRing_2008 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 T_IsRingWithoutAnnihilatingZero_1884
v4
  = (T_IsAbelianGroup_662
 -> T_IsMonoid_358 -> T_Σ_14 -> T_Σ_14 -> T_IsRing_1584)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRing_1584
forall a b. a -> b
coe
      T_IsAbelianGroup_662
-> T_IsMonoid_358 -> T_Σ_14 -> T_Σ_14 -> T_IsRing_1584
MAlonzo.Code.Algebra.Structures.C_IsRing'46'constructor_48413
      ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsAbelianGroup_662
d_'43''45'isAbelianGroup_1902 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))
      ((T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_IsMonoid_358
d_'42''45'isMonoid_1904 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))
      ((T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884 -> T_Σ_14
d_distrib_1906 (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsRingWithoutAnnihilatingZero_1884
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsRingWithoutAnnihilatingZero_1884
-> T_Σ_14
du_zero_2006 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (T_IsRingWithoutAnnihilatingZero_1884 -> AgdaAny
forall a b. a -> b
coe T_IsRingWithoutAnnihilatingZero_1884
v4))