{-# 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.Bundles.Raw 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.Primitive

-- Algebra.Bundles.Raw.RawSuccessorSet
d_RawSuccessorSet_10 :: p -> p -> ()
d_RawSuccessorSet_10 p
a0 p
a1 = ()
data T_RawSuccessorSet_10
  = C_RawSuccessorSet'46'constructor_89 (AgdaAny -> AgdaAny) AgdaAny
-- Algebra.Bundles.Raw.RawSuccessorSet.Carrier
d_Carrier_24 :: T_RawSuccessorSet_10 -> ()
d_Carrier_24 :: T_RawSuccessorSet_10 -> ()
d_Carrier_24 = T_RawSuccessorSet_10 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawSuccessorSet._≈_
d__'8776'__26 :: T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny -> ()
d__'8776'__26 :: T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny -> ()
d__'8776'__26 = T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawSuccessorSet.suc#
d_suc'35'_28 :: T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny
d_suc'35'_28 :: T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny
d_suc'35'_28 T_RawSuccessorSet_10
v0
  = case T_RawSuccessorSet_10 -> T_RawSuccessorSet_10
forall a b. a -> b
coe T_RawSuccessorSet_10
v0 of
      C_RawSuccessorSet'46'constructor_89 AgdaAny -> AgdaAny
v3 AgdaAny
v4 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v3
      T_RawSuccessorSet_10
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawSuccessorSet.zero#
d_zero'35'_30 :: T_RawSuccessorSet_10 -> AgdaAny
d_zero'35'_30 :: T_RawSuccessorSet_10 -> AgdaAny
d_zero'35'_30 T_RawSuccessorSet_10
v0
  = case T_RawSuccessorSet_10 -> T_RawSuccessorSet_10
forall a b. a -> b
coe T_RawSuccessorSet_10
v0 of
      C_RawSuccessorSet'46'constructor_89 AgdaAny -> AgdaAny
v3 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
      T_RawSuccessorSet_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawMagma
d_RawMagma_36 :: p -> p -> ()
d_RawMagma_36 p
a0 p
a1 = ()
newtype T_RawMagma_36
  = C_RawMagma'46'constructor_341 (AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Bundles.Raw.RawMagma.Carrier
d_Carrier_48 :: T_RawMagma_36 -> ()
d_Carrier_48 :: T_RawMagma_36 -> ()
d_Carrier_48 = T_RawMagma_36 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawMagma._≈_
d__'8776'__50 :: T_RawMagma_36 -> AgdaAny -> AgdaAny -> ()
d__'8776'__50 :: T_RawMagma_36 -> AgdaAny -> AgdaAny -> ()
d__'8776'__50 = T_RawMagma_36 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawMagma._∙_
d__'8729'__52 :: T_RawMagma_36 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__52 :: T_RawMagma_36 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__52 T_RawMagma_36
v0
  = case T_RawMagma_36 -> T_RawMagma_36
forall a b. a -> b
coe T_RawMagma_36
v0 of
      C_RawMagma'46'constructor_341 AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawMagma_36
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawMagma._≉_
d__'8777'__54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawMagma_36 -> AgdaAny -> AgdaAny -> ()
d__'8777'__54 :: () -> () -> T_RawMagma_36 -> AgdaAny -> AgdaAny -> ()
d__'8777'__54 = () -> () -> T_RawMagma_36 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawMonoid
d_RawMonoid_64 :: p -> p -> ()
d_RawMonoid_64 p
a0 p
a1 = ()
data T_RawMonoid_64
  = C_RawMonoid'46'constructor_745 (AgdaAny -> AgdaAny -> AgdaAny)
                                   AgdaAny
-- Algebra.Bundles.Raw.RawMonoid.Carrier
d_Carrier_78 :: T_RawMonoid_64 -> ()
d_Carrier_78 :: T_RawMonoid_64 -> ()
d_Carrier_78 = T_RawMonoid_64 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawMonoid._≈_
d__'8776'__80 :: T_RawMonoid_64 -> AgdaAny -> AgdaAny -> ()
d__'8776'__80 :: T_RawMonoid_64 -> AgdaAny -> AgdaAny -> ()
d__'8776'__80 = T_RawMonoid_64 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawMonoid._∙_
d__'8729'__82 :: T_RawMonoid_64 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__82 :: T_RawMonoid_64 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__82 T_RawMonoid_64
v0
  = case T_RawMonoid_64 -> T_RawMonoid_64
forall a b. a -> b
coe T_RawMonoid_64
v0 of
      C_RawMonoid'46'constructor_745 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawMonoid_64
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawMonoid.ε
d_ε_84 :: T_RawMonoid_64 -> AgdaAny
d_ε_84 :: T_RawMonoid_64 -> AgdaAny
d_ε_84 T_RawMonoid_64
v0
  = case T_RawMonoid_64 -> T_RawMonoid_64
forall a b. a -> b
coe T_RawMonoid_64
v0 of
      C_RawMonoid'46'constructor_745 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
      T_RawMonoid_64
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawMonoid.rawMagma
d_rawMagma_86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawMonoid_64 -> T_RawMagma_36
d_rawMagma_86 :: () -> () -> T_RawMonoid_64 -> T_RawMagma_36
d_rawMagma_86 ~()
v0 ~()
v1 T_RawMonoid_64
v2 = T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 T_RawMonoid_64
v2
du_rawMagma_86 :: T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 :: T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 T_RawMonoid_64
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
C_RawMagma'46'constructor_341 (T_RawMonoid_64 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__82 (T_RawMonoid_64 -> T_RawMonoid_64
forall a b. a -> b
coe T_RawMonoid_64
v0))
-- Algebra.Bundles.Raw.RawMonoid._._≉_
d__'8777'__90 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawMonoid_64 -> AgdaAny -> AgdaAny -> ()
d__'8777'__90 :: () -> () -> T_RawMonoid_64 -> AgdaAny -> AgdaAny -> ()
d__'8777'__90 = () -> () -> T_RawMonoid_64 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawGroup
d_RawGroup_96 :: p -> p -> ()
d_RawGroup_96 p
a0 p
a1 = ()
data T_RawGroup_96
  = C_RawGroup'46'constructor_1207 (AgdaAny -> AgdaAny -> AgdaAny)
                                   AgdaAny (AgdaAny -> AgdaAny)
-- Algebra.Bundles.Raw.RawGroup.Carrier
d_Carrier_112 :: T_RawGroup_96 -> ()
d_Carrier_112 :: T_RawGroup_96 -> ()
d_Carrier_112 = T_RawGroup_96 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawGroup._≈_
d__'8776'__114 :: T_RawGroup_96 -> AgdaAny -> AgdaAny -> ()
d__'8776'__114 :: T_RawGroup_96 -> AgdaAny -> AgdaAny -> ()
d__'8776'__114 = T_RawGroup_96 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawGroup._∙_
d__'8729'__116 :: T_RawGroup_96 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__116 :: T_RawGroup_96 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__116 T_RawGroup_96
v0
  = case T_RawGroup_96 -> T_RawGroup_96
forall a b. a -> b
coe T_RawGroup_96
v0 of
      C_RawGroup'46'constructor_1207 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny -> AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawGroup_96
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawGroup.ε
d_ε_118 :: T_RawGroup_96 -> AgdaAny
d_ε_118 :: T_RawGroup_96 -> AgdaAny
d_ε_118 T_RawGroup_96
v0
  = case T_RawGroup_96 -> T_RawGroup_96
forall a b. a -> b
coe T_RawGroup_96
v0 of
      C_RawGroup'46'constructor_1207 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny -> AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
      T_RawGroup_96
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawGroup._⁻¹
d__'8315''185'_120 :: T_RawGroup_96 -> AgdaAny -> AgdaAny
d__'8315''185'_120 :: T_RawGroup_96 -> AgdaAny -> AgdaAny
d__'8315''185'_120 T_RawGroup_96
v0
  = case T_RawGroup_96 -> T_RawGroup_96
forall a b. a -> b
coe T_RawGroup_96
v0 of
      C_RawGroup'46'constructor_1207 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny -> AgdaAny
v5 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v5
      T_RawGroup_96
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawGroup.rawMonoid
d_rawMonoid_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawGroup_96 -> T_RawMonoid_64
d_rawMonoid_122 :: () -> () -> T_RawGroup_96 -> T_RawMonoid_64
d_rawMonoid_122 ~()
v0 ~()
v1 T_RawGroup_96
v2 = T_RawGroup_96 -> T_RawMonoid_64
du_rawMonoid_122 T_RawGroup_96
v2
du_rawMonoid_122 :: T_RawGroup_96 -> T_RawMonoid_64
du_rawMonoid_122 :: T_RawGroup_96 -> T_RawMonoid_64
du_rawMonoid_122 T_RawGroup_96
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64
C_RawMonoid'46'constructor_745 (T_RawGroup_96 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__116 (T_RawGroup_96 -> T_RawGroup_96
forall a b. a -> b
coe T_RawGroup_96
v0))
      (T_RawGroup_96 -> AgdaAny
d_ε_118 (T_RawGroup_96 -> T_RawGroup_96
forall a b. a -> b
coe T_RawGroup_96
v0))
-- Algebra.Bundles.Raw.RawGroup._._≉_
d__'8777'__126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawGroup_96 -> AgdaAny -> AgdaAny -> ()
d__'8777'__126 :: () -> () -> T_RawGroup_96 -> AgdaAny -> AgdaAny -> ()
d__'8777'__126 = () -> () -> T_RawGroup_96 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawGroup._.rawMagma
d_rawMagma_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawGroup_96 -> T_RawMagma_36
d_rawMagma_128 :: () -> () -> T_RawGroup_96 -> T_RawMagma_36
d_rawMagma_128 ~()
v0 ~()
v1 T_RawGroup_96
v2 = T_RawGroup_96 -> T_RawMagma_36
du_rawMagma_128 T_RawGroup_96
v2
du_rawMagma_128 :: T_RawGroup_96 -> T_RawMagma_36
du_rawMagma_128 :: T_RawGroup_96 -> T_RawMagma_36
du_rawMagma_128 T_RawGroup_96
v0
  = (T_RawMonoid_64 -> T_RawMagma_36) -> AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 ((T_RawGroup_96 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawGroup_96 -> T_RawMonoid_64
du_rawMonoid_122 (T_RawGroup_96 -> AgdaAny
forall a b. a -> b
coe T_RawGroup_96
v0))
-- Algebra.Bundles.Raw.RawNearSemiring
d_RawNearSemiring_134 :: p -> p -> ()
d_RawNearSemiring_134 p
a0 p
a1 = ()
data T_RawNearSemiring_134
  = C_RawNearSemiring'46'constructor_1729 (AgdaAny ->
                                           AgdaAny -> AgdaAny)
                                          (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny
-- Algebra.Bundles.Raw.RawNearSemiring.Carrier
d_Carrier_150 :: T_RawNearSemiring_134 -> ()
d_Carrier_150 :: T_RawNearSemiring_134 -> ()
d_Carrier_150 = T_RawNearSemiring_134 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawNearSemiring._≈_
d__'8776'__152 :: T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> ()
d__'8776'__152 :: T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> ()
d__'8776'__152 = T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawNearSemiring._+_
d__'43'__154 ::
  T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__154 :: T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__154 T_RawNearSemiring_134
v0
  = case T_RawNearSemiring_134 -> T_RawNearSemiring_134
forall a b. a -> b
coe T_RawNearSemiring_134
v0 of
      C_RawNearSemiring'46'constructor_1729 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawNearSemiring_134
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawNearSemiring._*_
d__'42'__156 ::
  T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__156 :: T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__156 T_RawNearSemiring_134
v0
  = case T_RawNearSemiring_134 -> T_RawNearSemiring_134
forall a b. a -> b
coe T_RawNearSemiring_134
v0 of
      C_RawNearSemiring'46'constructor_1729 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawNearSemiring_134
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawNearSemiring.0#
d_0'35'_158 :: T_RawNearSemiring_134 -> AgdaAny
d_0'35'_158 :: T_RawNearSemiring_134 -> AgdaAny
d_0'35'_158 T_RawNearSemiring_134
v0
  = case T_RawNearSemiring_134 -> T_RawNearSemiring_134
forall a b. a -> b
coe T_RawNearSemiring_134
v0 of
      C_RawNearSemiring'46'constructor_1729 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
      T_RawNearSemiring_134
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawNearSemiring.+-rawMonoid
d_'43''45'rawMonoid_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawNearSemiring_134 -> T_RawMonoid_64
d_'43''45'rawMonoid_160 :: () -> () -> T_RawNearSemiring_134 -> T_RawMonoid_64
d_'43''45'rawMonoid_160 ~()
v0 ~()
v1 T_RawNearSemiring_134
v2 = T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 T_RawNearSemiring_134
v2
du_'43''45'rawMonoid_160 :: T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 :: T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 T_RawNearSemiring_134
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64
C_RawMonoid'46'constructor_745 (T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__154 (T_RawNearSemiring_134 -> T_RawNearSemiring_134
forall a b. a -> b
coe T_RawNearSemiring_134
v0))
      (T_RawNearSemiring_134 -> AgdaAny
d_0'35'_158 (T_RawNearSemiring_134 -> T_RawNearSemiring_134
forall a b. a -> b
coe T_RawNearSemiring_134
v0))
-- Algebra.Bundles.Raw.RawNearSemiring._._≉_
d__'8777'__164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> ()
d__'8777'__164 :: () -> () -> T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> ()
d__'8777'__164 = () -> () -> T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawNearSemiring._.rawMagma
d_rawMagma_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawNearSemiring_134 -> T_RawMagma_36
d_rawMagma_166 :: () -> () -> T_RawNearSemiring_134 -> T_RawMagma_36
d_rawMagma_166 ~()
v0 ~()
v1 T_RawNearSemiring_134
v2 = T_RawNearSemiring_134 -> T_RawMagma_36
du_rawMagma_166 T_RawNearSemiring_134
v2
du_rawMagma_166 :: T_RawNearSemiring_134 -> T_RawMagma_36
du_rawMagma_166 :: T_RawNearSemiring_134 -> T_RawMagma_36
du_rawMagma_166 T_RawNearSemiring_134
v0
  = (T_RawMonoid_64 -> T_RawMagma_36) -> AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 ((T_RawNearSemiring_134 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 (T_RawNearSemiring_134 -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134
v0))
-- Algebra.Bundles.Raw.RawNearSemiring.*-rawMagma
d_'42''45'rawMagma_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawNearSemiring_134 -> T_RawMagma_36
d_'42''45'rawMagma_168 :: () -> () -> T_RawNearSemiring_134 -> T_RawMagma_36
d_'42''45'rawMagma_168 ~()
v0 ~()
v1 T_RawNearSemiring_134
v2 = T_RawNearSemiring_134 -> T_RawMagma_36
du_'42''45'rawMagma_168 T_RawNearSemiring_134
v2
du_'42''45'rawMagma_168 :: T_RawNearSemiring_134 -> T_RawMagma_36
du_'42''45'rawMagma_168 :: T_RawNearSemiring_134 -> T_RawMagma_36
du_'42''45'rawMagma_168 T_RawNearSemiring_134
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
C_RawMagma'46'constructor_341 (T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__156 (T_RawNearSemiring_134 -> T_RawNearSemiring_134
forall a b. a -> b
coe T_RawNearSemiring_134
v0))
-- Algebra.Bundles.Raw.RawSemiring
d_RawSemiring_174 :: p -> p -> ()
d_RawSemiring_174 p
a0 p
a1 = ()
data T_RawSemiring_174
  = C_RawSemiring'46'constructor_2353 (AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny) AgdaAny AgdaAny
-- Algebra.Bundles.Raw.RawSemiring.Carrier
d_Carrier_192 :: T_RawSemiring_174 -> ()
d_Carrier_192 :: T_RawSemiring_174 -> ()
d_Carrier_192 = T_RawSemiring_174 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawSemiring._≈_
d__'8776'__194 :: T_RawSemiring_174 -> AgdaAny -> AgdaAny -> ()
d__'8776'__194 :: T_RawSemiring_174 -> AgdaAny -> AgdaAny -> ()
d__'8776'__194 = T_RawSemiring_174 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawSemiring._+_
d__'43'__196 :: T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__196 :: T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__196 T_RawSemiring_174
v0
  = case T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0 of
      C_RawSemiring'46'constructor_2353 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawSemiring_174
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawSemiring._*_
d__'42'__198 :: T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__198 :: T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__198 T_RawSemiring_174
v0
  = case T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0 of
      C_RawSemiring'46'constructor_2353 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawSemiring_174
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawSemiring.0#
d_0'35'_200 :: T_RawSemiring_174 -> AgdaAny
d_0'35'_200 :: T_RawSemiring_174 -> AgdaAny
d_0'35'_200 T_RawSemiring_174
v0
  = case T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0 of
      C_RawSemiring'46'constructor_2353 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
      T_RawSemiring_174
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawSemiring.1#
d_1'35'_202 :: T_RawSemiring_174 -> AgdaAny
d_1'35'_202 :: T_RawSemiring_174 -> AgdaAny
d_1'35'_202 T_RawSemiring_174
v0
  = case T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0 of
      C_RawSemiring'46'constructor_2353 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
      T_RawSemiring_174
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawSemiring.rawNearSemiring
d_rawNearSemiring_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawSemiring_174 -> T_RawNearSemiring_134
d_rawNearSemiring_204 :: () -> () -> T_RawSemiring_174 -> T_RawNearSemiring_134
d_rawNearSemiring_204 ~()
v0 ~()
v1 T_RawSemiring_174
v2 = T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 T_RawSemiring_174
v2
du_rawNearSemiring_204 ::
  T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 :: T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 T_RawSemiring_174
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_RawNearSemiring_134)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_RawNearSemiring_134
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_RawNearSemiring_134
C_RawNearSemiring'46'constructor_1729 (T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__196 (T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0))
      (T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__198 (T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0)) (T_RawSemiring_174 -> AgdaAny
d_0'35'_200 (T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0))
-- Algebra.Bundles.Raw.RawSemiring._._≉_
d__'8777'__208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawSemiring_174 -> AgdaAny -> AgdaAny -> ()
d__'8777'__208 :: () -> () -> T_RawSemiring_174 -> AgdaAny -> AgdaAny -> ()
d__'8777'__208 = () -> () -> T_RawSemiring_174 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawSemiring._.*-rawMagma
d_'42''45'rawMagma_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawSemiring_174 -> T_RawMagma_36
d_'42''45'rawMagma_210 :: () -> () -> T_RawSemiring_174 -> T_RawMagma_36
d_'42''45'rawMagma_210 ~()
v0 ~()
v1 T_RawSemiring_174
v2 = T_RawSemiring_174 -> T_RawMagma_36
du_'42''45'rawMagma_210 T_RawSemiring_174
v2
du_'42''45'rawMagma_210 :: T_RawSemiring_174 -> T_RawMagma_36
du_'42''45'rawMagma_210 :: T_RawSemiring_174 -> T_RawMagma_36
du_'42''45'rawMagma_210 T_RawSemiring_174
v0
  = (T_RawNearSemiring_134 -> T_RawMagma_36)
-> AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMagma_36
du_'42''45'rawMagma_168 ((T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (T_RawSemiring_174 -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174
v0))
-- Algebra.Bundles.Raw.RawSemiring._.rawMagma
d_rawMagma_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawSemiring_174 -> T_RawMagma_36
d_rawMagma_212 :: () -> () -> T_RawSemiring_174 -> T_RawMagma_36
d_rawMagma_212 ~()
v0 ~()
v1 T_RawSemiring_174
v2 = T_RawSemiring_174 -> T_RawMagma_36
du_rawMagma_212 T_RawSemiring_174
v2
du_rawMagma_212 :: T_RawSemiring_174 -> T_RawMagma_36
du_rawMagma_212 :: T_RawSemiring_174 -> T_RawMagma_36
du_rawMagma_212 T_RawSemiring_174
v0
  = let v1 :: t
v1 = (T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> t
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (T_RawSemiring_174 -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174
v0) in
    AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe ((T_RawMonoid_64 -> T_RawMagma_36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 ((T_RawNearSemiring_134 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Bundles.Raw.RawSemiring._.+-rawMonoid
d_'43''45'rawMonoid_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawSemiring_174 -> T_RawMonoid_64
d_'43''45'rawMonoid_214 :: () -> () -> T_RawSemiring_174 -> T_RawMonoid_64
d_'43''45'rawMonoid_214 ~()
v0 ~()
v1 T_RawSemiring_174
v2 = T_RawSemiring_174 -> T_RawMonoid_64
du_'43''45'rawMonoid_214 T_RawSemiring_174
v2
du_'43''45'rawMonoid_214 :: T_RawSemiring_174 -> T_RawMonoid_64
du_'43''45'rawMonoid_214 :: T_RawSemiring_174 -> T_RawMonoid_64
du_'43''45'rawMonoid_214 T_RawSemiring_174
v0
  = (T_RawNearSemiring_134 -> T_RawMonoid_64)
-> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe
      T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 ((T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (T_RawSemiring_174 -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174
v0))
-- Algebra.Bundles.Raw.RawSemiring.*-rawMonoid
d_'42''45'rawMonoid_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawSemiring_174 -> T_RawMonoid_64
d_'42''45'rawMonoid_216 :: () -> () -> T_RawSemiring_174 -> T_RawMonoid_64
d_'42''45'rawMonoid_216 ~()
v0 ~()
v1 T_RawSemiring_174
v2 = T_RawSemiring_174 -> T_RawMonoid_64
du_'42''45'rawMonoid_216 T_RawSemiring_174
v2
du_'42''45'rawMonoid_216 :: T_RawSemiring_174 -> T_RawMonoid_64
du_'42''45'rawMonoid_216 :: T_RawSemiring_174 -> T_RawMonoid_64
du_'42''45'rawMonoid_216 T_RawSemiring_174
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_RawMonoid_64
C_RawMonoid'46'constructor_745 (T_RawSemiring_174 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__198 (T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0))
      (T_RawSemiring_174 -> AgdaAny
d_1'35'_202 (T_RawSemiring_174 -> T_RawSemiring_174
forall a b. a -> b
coe T_RawSemiring_174
v0))
-- Algebra.Bundles.Raw.RawRingWithoutOne
d_RawRingWithoutOne_222 :: p -> p -> ()
d_RawRingWithoutOne_222 p
a0 p
a1 = ()
data T_RawRingWithoutOne_222
  = C_RawRingWithoutOne'46'constructor_3105 (AgdaAny ->
                                             AgdaAny -> AgdaAny)
                                            (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)
                                            AgdaAny
-- Algebra.Bundles.Raw.RawRingWithoutOne.Carrier
d_Carrier_240 :: T_RawRingWithoutOne_222 -> ()
d_Carrier_240 :: T_RawRingWithoutOne_222 -> ()
d_Carrier_240 = T_RawRingWithoutOne_222 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawRingWithoutOne._≈_
d__'8776'__242 ::
  T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> ()
d__'8776'__242 :: T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> ()
d__'8776'__242 = T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawRingWithoutOne._+_
d__'43'__244 ::
  T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__244 :: T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__244 T_RawRingWithoutOne_222
v0
  = case T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0 of
      C_RawRingWithoutOne'46'constructor_3105 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawRingWithoutOne_222
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRingWithoutOne._*_
d__'42'__246 ::
  T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__246 :: T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__246 T_RawRingWithoutOne_222
v0
  = case T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0 of
      C_RawRingWithoutOne'46'constructor_3105 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawRingWithoutOne_222
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRingWithoutOne.-_
d_'45'__248 :: T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny
d_'45'__248 :: T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny
d_'45'__248 T_RawRingWithoutOne_222
v0
  = case T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0 of
      C_RawRingWithoutOne'46'constructor_3105 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v5
      T_RawRingWithoutOne_222
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRingWithoutOne.0#
d_0'35'_250 :: T_RawRingWithoutOne_222 -> AgdaAny
d_0'35'_250 :: T_RawRingWithoutOne_222 -> AgdaAny
d_0'35'_250 T_RawRingWithoutOne_222
v0
  = case T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0 of
      C_RawRingWithoutOne'46'constructor_3105 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
      T_RawRingWithoutOne_222
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRingWithoutOne.+-rawGroup
d_'43''45'rawGroup_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRingWithoutOne_222 -> T_RawGroup_96
d_'43''45'rawGroup_252 :: () -> () -> T_RawRingWithoutOne_222 -> T_RawGroup_96
d_'43''45'rawGroup_252 ~()
v0 ~()
v1 T_RawRingWithoutOne_222
v2 = T_RawRingWithoutOne_222 -> T_RawGroup_96
du_'43''45'rawGroup_252 T_RawRingWithoutOne_222
v2
du_'43''45'rawGroup_252 :: T_RawRingWithoutOne_222 -> T_RawGroup_96
du_'43''45'rawGroup_252 :: T_RawRingWithoutOne_222 -> T_RawGroup_96
du_'43''45'rawGroup_252 T_RawRingWithoutOne_222
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_RawGroup_96)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_RawGroup_96
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> T_RawGroup_96
C_RawGroup'46'constructor_1207 (T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__244 (T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0))
      (T_RawRingWithoutOne_222 -> AgdaAny
d_0'35'_250 (T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0)) (T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny
d_'45'__248 (T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0))
-- Algebra.Bundles.Raw.RawRingWithoutOne._._≉_
d__'8777'__256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> ()
d__'8777'__256 :: () -> () -> T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> ()
d__'8777'__256 = () -> () -> T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawRingWithoutOne._.rawMagma
d_rawMagma_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRingWithoutOne_222 -> T_RawMagma_36
d_rawMagma_258 :: () -> () -> T_RawRingWithoutOne_222 -> T_RawMagma_36
d_rawMagma_258 ~()
v0 ~()
v1 T_RawRingWithoutOne_222
v2 = T_RawRingWithoutOne_222 -> T_RawMagma_36
du_rawMagma_258 T_RawRingWithoutOne_222
v2
du_rawMagma_258 :: T_RawRingWithoutOne_222 -> T_RawMagma_36
du_rawMagma_258 :: T_RawRingWithoutOne_222 -> T_RawMagma_36
du_rawMagma_258 T_RawRingWithoutOne_222
v0
  = let v1 :: t
v1 = (T_RawRingWithoutOne_222 -> T_RawGroup_96) -> AgdaAny -> t
forall a b. a -> b
coe T_RawRingWithoutOne_222 -> T_RawGroup_96
du_'43''45'rawGroup_252 (T_RawRingWithoutOne_222 -> AgdaAny
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0) in
    AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe ((T_RawMonoid_64 -> T_RawMagma_36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 ((T_RawGroup_96 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawGroup_96 -> T_RawMonoid_64
du_rawMonoid_122 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Bundles.Raw.RawRingWithoutOne._.rawMonoid
d_rawMonoid_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRingWithoutOne_222 -> T_RawMonoid_64
d_rawMonoid_260 :: () -> () -> T_RawRingWithoutOne_222 -> T_RawMonoid_64
d_rawMonoid_260 ~()
v0 ~()
v1 T_RawRingWithoutOne_222
v2 = T_RawRingWithoutOne_222 -> T_RawMonoid_64
du_rawMonoid_260 T_RawRingWithoutOne_222
v2
du_rawMonoid_260 :: T_RawRingWithoutOne_222 -> T_RawMonoid_64
du_rawMonoid_260 :: T_RawRingWithoutOne_222 -> T_RawMonoid_64
du_rawMonoid_260 T_RawRingWithoutOne_222
v0
  = (T_RawGroup_96 -> T_RawMonoid_64) -> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe T_RawGroup_96 -> T_RawMonoid_64
du_rawMonoid_122 ((T_RawRingWithoutOne_222 -> T_RawGroup_96) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawRingWithoutOne_222 -> T_RawGroup_96
du_'43''45'rawGroup_252 (T_RawRingWithoutOne_222 -> AgdaAny
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0))
-- Algebra.Bundles.Raw.RawRingWithoutOne.*-rawMagma
d_'42''45'rawMagma_262 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRingWithoutOne_222 -> T_RawMagma_36
d_'42''45'rawMagma_262 :: () -> () -> T_RawRingWithoutOne_222 -> T_RawMagma_36
d_'42''45'rawMagma_262 ~()
v0 ~()
v1 T_RawRingWithoutOne_222
v2 = T_RawRingWithoutOne_222 -> T_RawMagma_36
du_'42''45'rawMagma_262 T_RawRingWithoutOne_222
v2
du_'42''45'rawMagma_262 :: T_RawRingWithoutOne_222 -> T_RawMagma_36
du_'42''45'rawMagma_262 :: T_RawRingWithoutOne_222 -> T_RawMagma_36
du_'42''45'rawMagma_262 T_RawRingWithoutOne_222
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
C_RawMagma'46'constructor_341 (T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__246 (T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222
forall a b. a -> b
coe T_RawRingWithoutOne_222
v0))
-- Algebra.Bundles.Raw.RawRing
d_RawRing_268 :: p -> p -> ()
d_RawRing_268 p
a0 p
a1 = ()
data T_RawRing_268
  = C_RawRing'46'constructor_3857 (AgdaAny -> AgdaAny -> AgdaAny)
                                  (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) AgdaAny
                                  AgdaAny
-- Algebra.Bundles.Raw.RawRing.Carrier
d_Carrier_288 :: T_RawRing_268 -> ()
d_Carrier_288 :: T_RawRing_268 -> ()
d_Carrier_288 = T_RawRing_268 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawRing._≈_
d__'8776'__290 :: T_RawRing_268 -> AgdaAny -> AgdaAny -> ()
d__'8776'__290 :: T_RawRing_268 -> AgdaAny -> AgdaAny -> ()
d__'8776'__290 = T_RawRing_268 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawRing._+_
d__'43'__292 :: T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__292 :: T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__292 T_RawRing_268
v0
  = case T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0 of
      C_RawRing'46'constructor_3857 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawRing_268
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRing._*_
d__'42'__294 :: T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__294 :: T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__294 T_RawRing_268
v0
  = case T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0 of
      C_RawRing'46'constructor_3857 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawRing_268
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRing.-_
d_'45'__296 :: T_RawRing_268 -> AgdaAny -> AgdaAny
d_'45'__296 :: T_RawRing_268 -> AgdaAny -> AgdaAny
d_'45'__296 T_RawRing_268
v0
  = case T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0 of
      C_RawRing'46'constructor_3857 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v5
      T_RawRing_268
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRing.0#
d_0'35'_298 :: T_RawRing_268 -> AgdaAny
d_0'35'_298 :: T_RawRing_268 -> AgdaAny
d_0'35'_298 T_RawRing_268
v0
  = case T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0 of
      C_RawRing'46'constructor_3857 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
      T_RawRing_268
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRing.1#
d_1'35'_300 :: T_RawRing_268 -> AgdaAny
d_1'35'_300 :: T_RawRing_268 -> AgdaAny
d_1'35'_300 T_RawRing_268
v0
  = case T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0 of
      C_RawRing'46'constructor_3857 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7
      T_RawRing_268
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawRing.rawSemiring
d_rawSemiring_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawSemiring_174
d_rawSemiring_302 :: () -> () -> T_RawRing_268 -> T_RawSemiring_174
d_rawSemiring_302 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 T_RawRing_268
v2
du_rawSemiring_302 :: T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 :: T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 T_RawRing_268
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_RawSemiring_174)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_RawSemiring_174
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_RawSemiring_174
C_RawSemiring'46'constructor_2353 (T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__292 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0))
      (T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__294 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0)) (T_RawRing_268 -> AgdaAny
d_0'35'_298 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0))
      (T_RawRing_268 -> AgdaAny
d_1'35'_300 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0))
-- Algebra.Bundles.Raw.RawRing._._≉_
d__'8777'__306 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> AgdaAny -> AgdaAny -> ()
d__'8777'__306 :: () -> () -> T_RawRing_268 -> AgdaAny -> AgdaAny -> ()
d__'8777'__306 = () -> () -> T_RawRing_268 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawRing._.*-rawMagma
d_'42''45'rawMagma_308 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawMagma_36
d_'42''45'rawMagma_308 :: () -> () -> T_RawRing_268 -> T_RawMagma_36
d_'42''45'rawMagma_308 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawMagma_36
du_'42''45'rawMagma_308 T_RawRing_268
v2
du_'42''45'rawMagma_308 :: T_RawRing_268 -> T_RawMagma_36
du_'42''45'rawMagma_308 :: T_RawRing_268 -> T_RawMagma_36
du_'42''45'rawMagma_308 T_RawRing_268
v0
  = let v1 :: t
v1 = (T_RawRing_268 -> T_RawSemiring_174) -> AgdaAny -> t
forall a b. a -> b
coe T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 (T_RawRing_268 -> AgdaAny
forall a b. a -> b
coe T_RawRing_268
v0) in
    AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe
      ((T_RawNearSemiring_134 -> T_RawMagma_36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMagma_36
du_'42''45'rawMagma_168 ((T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Bundles.Raw.RawRing._.*-rawMonoid
d_'42''45'rawMonoid_310 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawMonoid_64
d_'42''45'rawMonoid_310 :: () -> () -> T_RawRing_268 -> T_RawMonoid_64
d_'42''45'rawMonoid_310 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawMonoid_64
du_'42''45'rawMonoid_310 T_RawRing_268
v2
du_'42''45'rawMonoid_310 :: T_RawRing_268 -> T_RawMonoid_64
du_'42''45'rawMonoid_310 :: T_RawRing_268 -> T_RawMonoid_64
du_'42''45'rawMonoid_310 T_RawRing_268
v0
  = (T_RawSemiring_174 -> T_RawMonoid_64) -> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawMonoid_64
du_'42''45'rawMonoid_216 ((T_RawRing_268 -> T_RawSemiring_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 (T_RawRing_268 -> AgdaAny
forall a b. a -> b
coe T_RawRing_268
v0))
-- Algebra.Bundles.Raw.RawRing._.rawMagma
d_rawMagma_312 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawMagma_36
d_rawMagma_312 :: () -> () -> T_RawRing_268 -> T_RawMagma_36
d_rawMagma_312 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawMagma_36
du_rawMagma_312 T_RawRing_268
v2
du_rawMagma_312 :: T_RawRing_268 -> T_RawMagma_36
du_rawMagma_312 :: T_RawRing_268 -> T_RawMagma_36
du_rawMagma_312 T_RawRing_268
v0
  = let v1 :: t
v1 = (T_RawRing_268 -> T_RawSemiring_174) -> AgdaAny -> t
forall a b. a -> b
coe T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 (T_RawRing_268 -> AgdaAny
forall a b. a -> b
coe T_RawRing_268
v0) in
    AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> t
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_RawMonoid_64 -> T_RawMagma_36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 ((T_RawNearSemiring_134 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Algebra.Bundles.Raw.RawRing._.+-rawMonoid
d_'43''45'rawMonoid_314 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawMonoid_64
d_'43''45'rawMonoid_314 :: () -> () -> T_RawRing_268 -> T_RawMonoid_64
d_'43''45'rawMonoid_314 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawMonoid_64
du_'43''45'rawMonoid_314 T_RawRing_268
v2
du_'43''45'rawMonoid_314 :: T_RawRing_268 -> T_RawMonoid_64
du_'43''45'rawMonoid_314 :: T_RawRing_268 -> T_RawMonoid_64
du_'43''45'rawMonoid_314 T_RawRing_268
v0
  = let v1 :: t
v1 = (T_RawRing_268 -> T_RawSemiring_174) -> AgdaAny -> t
forall a b. a -> b
coe T_RawRing_268 -> T_RawSemiring_174
du_rawSemiring_302 (T_RawRing_268 -> AgdaAny
forall a b. a -> b
coe T_RawRing_268
v0) in
    AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe
      ((T_RawNearSemiring_134 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 ((T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Bundles.Raw.RawRing.rawRingWithoutOne
d_rawRingWithoutOne_316 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawRingWithoutOne_222
d_rawRingWithoutOne_316 :: () -> () -> T_RawRing_268 -> T_RawRingWithoutOne_222
d_rawRingWithoutOne_316 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawRingWithoutOne_222
du_rawRingWithoutOne_316 T_RawRing_268
v2
du_rawRingWithoutOne_316 ::
  T_RawRing_268 -> T_RawRingWithoutOne_222
du_rawRingWithoutOne_316 :: T_RawRing_268 -> T_RawRingWithoutOne_222
du_rawRingWithoutOne_316 T_RawRing_268
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_RawRingWithoutOne_222)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_RawRingWithoutOne_222
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_RawRingWithoutOne_222
C_RawRingWithoutOne'46'constructor_3105 (T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__292 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0))
      (T_RawRing_268 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__294 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0)) (T_RawRing_268 -> AgdaAny -> AgdaAny
d_'45'__296 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0))
      (T_RawRing_268 -> AgdaAny
d_0'35'_298 (T_RawRing_268 -> T_RawRing_268
forall a b. a -> b
coe T_RawRing_268
v0))
-- Algebra.Bundles.Raw.RawRing._.+-rawGroup
d_'43''45'rawGroup_320 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawRing_268 -> T_RawGroup_96
d_'43''45'rawGroup_320 :: () -> () -> T_RawRing_268 -> T_RawGroup_96
d_'43''45'rawGroup_320 ~()
v0 ~()
v1 T_RawRing_268
v2 = T_RawRing_268 -> T_RawGroup_96
du_'43''45'rawGroup_320 T_RawRing_268
v2
du_'43''45'rawGroup_320 :: T_RawRing_268 -> T_RawGroup_96
du_'43''45'rawGroup_320 :: T_RawRing_268 -> T_RawGroup_96
du_'43''45'rawGroup_320 T_RawRing_268
v0
  = (T_RawRingWithoutOne_222 -> T_RawGroup_96)
-> AgdaAny -> T_RawGroup_96
forall a b. a -> b
coe
      T_RawRingWithoutOne_222 -> T_RawGroup_96
du_'43''45'rawGroup_252 ((T_RawRing_268 -> T_RawRingWithoutOne_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawRing_268 -> T_RawRingWithoutOne_222
du_rawRingWithoutOne_316 (T_RawRing_268 -> AgdaAny
forall a b. a -> b
coe T_RawRing_268
v0))
-- Algebra.Bundles.Raw.RawQuasigroup
d_RawQuasigroup_326 :: p -> p -> ()
d_RawQuasigroup_326 p
a0 p
a1 = ()
data T_RawQuasigroup_326
  = C_RawQuasigroup'46'constructor_4731 (AgdaAny ->
                                         AgdaAny -> AgdaAny)
                                        (AgdaAny -> AgdaAny -> AgdaAny)
                                        (AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Bundles.Raw.RawQuasigroup.Carrier
d_Carrier_342 :: T_RawQuasigroup_326 -> ()
d_Carrier_342 :: T_RawQuasigroup_326 -> ()
d_Carrier_342 = T_RawQuasigroup_326 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawQuasigroup._≈_
d__'8776'__344 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> ()
d__'8776'__344 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> ()
d__'8776'__344 = T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawQuasigroup._∙_
d__'8729'__346 ::
  T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__346 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__346 T_RawQuasigroup_326
v0
  = case T_RawQuasigroup_326 -> T_RawQuasigroup_326
forall a b. a -> b
coe T_RawQuasigroup_326
v0 of
      C_RawQuasigroup'46'constructor_4731 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawQuasigroup_326
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawQuasigroup._\\_
d__'92''92'__348 ::
  T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'92''92'__348 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'92''92'__348 T_RawQuasigroup_326
v0
  = case T_RawQuasigroup_326 -> T_RawQuasigroup_326
forall a b. a -> b
coe T_RawQuasigroup_326
v0 of
      C_RawQuasigroup'46'constructor_4731 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawQuasigroup_326
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawQuasigroup._//_
d__'47''47'__350 ::
  T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'47''47'__350 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'47''47'__350 T_RawQuasigroup_326
v0
  = case T_RawQuasigroup_326 -> T_RawQuasigroup_326
forall a b. a -> b
coe T_RawQuasigroup_326
v0 of
      C_RawQuasigroup'46'constructor_4731 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v5
      T_RawQuasigroup_326
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawQuasigroup.∙-rawMagma
d_'8729''45'rawMagma_352 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawQuasigroup_326 -> T_RawMagma_36
d_'8729''45'rawMagma_352 :: () -> () -> T_RawQuasigroup_326 -> T_RawMagma_36
d_'8729''45'rawMagma_352 ~()
v0 ~()
v1 T_RawQuasigroup_326
v2 = T_RawQuasigroup_326 -> T_RawMagma_36
du_'8729''45'rawMagma_352 T_RawQuasigroup_326
v2
du_'8729''45'rawMagma_352 :: T_RawQuasigroup_326 -> T_RawMagma_36
du_'8729''45'rawMagma_352 :: T_RawQuasigroup_326 -> T_RawMagma_36
du_'8729''45'rawMagma_352 T_RawQuasigroup_326
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
C_RawMagma'46'constructor_341 (T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__346 (T_RawQuasigroup_326 -> T_RawQuasigroup_326
forall a b. a -> b
coe T_RawQuasigroup_326
v0))
-- Algebra.Bundles.Raw.RawQuasigroup.\\-rawMagma
d_'92''92''45'rawMagma_354 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawQuasigroup_326 -> T_RawMagma_36
d_'92''92''45'rawMagma_354 :: () -> () -> T_RawQuasigroup_326 -> T_RawMagma_36
d_'92''92''45'rawMagma_354 ~()
v0 ~()
v1 T_RawQuasigroup_326
v2
  = T_RawQuasigroup_326 -> T_RawMagma_36
du_'92''92''45'rawMagma_354 T_RawQuasigroup_326
v2
du_'92''92''45'rawMagma_354 :: T_RawQuasigroup_326 -> T_RawMagma_36
du_'92''92''45'rawMagma_354 :: T_RawQuasigroup_326 -> T_RawMagma_36
du_'92''92''45'rawMagma_354 T_RawQuasigroup_326
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
C_RawMagma'46'constructor_341 (T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'92''92'__348 (T_RawQuasigroup_326 -> T_RawQuasigroup_326
forall a b. a -> b
coe T_RawQuasigroup_326
v0))
-- Algebra.Bundles.Raw.RawQuasigroup.//-rawMagma
d_'47''47''45'rawMagma_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawQuasigroup_326 -> T_RawMagma_36
d_'47''47''45'rawMagma_356 :: () -> () -> T_RawQuasigroup_326 -> T_RawMagma_36
d_'47''47''45'rawMagma_356 ~()
v0 ~()
v1 T_RawQuasigroup_326
v2
  = T_RawQuasigroup_326 -> T_RawMagma_36
du_'47''47''45'rawMagma_356 T_RawQuasigroup_326
v2
du_'47''47''45'rawMagma_356 :: T_RawQuasigroup_326 -> T_RawMagma_36
du_'47''47''45'rawMagma_356 :: T_RawQuasigroup_326 -> T_RawMagma_36
du_'47''47''45'rawMagma_356 T_RawQuasigroup_326
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_RawMagma_36
C_RawMagma'46'constructor_341 (T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny
d__'47''47'__350 (T_RawQuasigroup_326 -> T_RawQuasigroup_326
forall a b. a -> b
coe T_RawQuasigroup_326
v0))
-- Algebra.Bundles.Raw.RawQuasigroup._._≉_
d__'8777'__360 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> ()
d__'8777'__360 :: () -> () -> T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> ()
d__'8777'__360 = () -> () -> T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawLoop
d_RawLoop_366 :: p -> p -> ()
d_RawLoop_366 p
a0 p
a1 = ()
data T_RawLoop_366
  = C_RawLoop'46'constructor_5465 (AgdaAny -> AgdaAny -> AgdaAny)
                                  (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)
                                  AgdaAny
-- Algebra.Bundles.Raw.RawLoop.Carrier
d_Carrier_384 :: T_RawLoop_366 -> ()
d_Carrier_384 :: T_RawLoop_366 -> ()
d_Carrier_384 = T_RawLoop_366 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawLoop._≈_
d__'8776'__386 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> ()
d__'8776'__386 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> ()
d__'8776'__386 = T_RawLoop_366 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawLoop._∙_
d__'8729'__388 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__388 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__388 T_RawLoop_366
v0
  = case T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0 of
      C_RawLoop'46'constructor_5465 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawLoop_366
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawLoop._\\_
d__'92''92'__390 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'92''92'__390 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'92''92'__390 T_RawLoop_366
v0
  = case T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0 of
      C_RawLoop'46'constructor_5465 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawLoop_366
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawLoop._//_
d__'47''47'__392 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'47''47'__392 :: T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'47''47'__392 T_RawLoop_366
v0
  = case T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0 of
      C_RawLoop'46'constructor_5465 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v5
      T_RawLoop_366
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawLoop.ε
d_ε_394 :: T_RawLoop_366 -> AgdaAny
d_ε_394 :: T_RawLoop_366 -> AgdaAny
d_ε_394 T_RawLoop_366
v0
  = case T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0 of
      C_RawLoop'46'constructor_5465 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
      T_RawLoop_366
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawLoop.rawQuasigroup
d_rawQuasigroup_396 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawLoop_366 -> T_RawQuasigroup_326
d_rawQuasigroup_396 :: () -> () -> T_RawLoop_366 -> T_RawQuasigroup_326
d_rawQuasigroup_396 ~()
v0 ~()
v1 T_RawLoop_366
v2 = T_RawLoop_366 -> T_RawQuasigroup_326
du_rawQuasigroup_396 T_RawLoop_366
v2
du_rawQuasigroup_396 :: T_RawLoop_366 -> T_RawQuasigroup_326
du_rawQuasigroup_396 :: T_RawLoop_366 -> T_RawQuasigroup_326
du_rawQuasigroup_396 T_RawLoop_366
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RawQuasigroup_326)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_RawQuasigroup_326
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_RawQuasigroup_326
C_RawQuasigroup'46'constructor_4731 (T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__388 (T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0))
      (T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'92''92'__390 (T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0)) (T_RawLoop_366 -> AgdaAny -> AgdaAny -> AgdaAny
d__'47''47'__392 (T_RawLoop_366 -> T_RawLoop_366
forall a b. a -> b
coe T_RawLoop_366
v0))
-- Algebra.Bundles.Raw.RawLoop._._≉_
d__'8777'__400 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawLoop_366 -> AgdaAny -> AgdaAny -> ()
d__'8777'__400 :: () -> () -> T_RawLoop_366 -> AgdaAny -> AgdaAny -> ()
d__'8777'__400 = () -> () -> T_RawLoop_366 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawLoop._.//-rawMagma
d_'47''47''45'rawMagma_402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawLoop_366 -> T_RawMagma_36
d_'47''47''45'rawMagma_402 :: () -> () -> T_RawLoop_366 -> T_RawMagma_36
d_'47''47''45'rawMagma_402 ~()
v0 ~()
v1 T_RawLoop_366
v2
  = T_RawLoop_366 -> T_RawMagma_36
du_'47''47''45'rawMagma_402 T_RawLoop_366
v2
du_'47''47''45'rawMagma_402 :: T_RawLoop_366 -> T_RawMagma_36
du_'47''47''45'rawMagma_402 :: T_RawLoop_366 -> T_RawMagma_36
du_'47''47''45'rawMagma_402 T_RawLoop_366
v0
  = (T_RawQuasigroup_326 -> T_RawMagma_36) -> AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe
      T_RawQuasigroup_326 -> T_RawMagma_36
du_'47''47''45'rawMagma_356 ((T_RawLoop_366 -> T_RawQuasigroup_326) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawLoop_366 -> T_RawQuasigroup_326
du_rawQuasigroup_396 (T_RawLoop_366 -> AgdaAny
forall a b. a -> b
coe T_RawLoop_366
v0))
-- Algebra.Bundles.Raw.RawLoop._.\\-rawMagma
d_'92''92''45'rawMagma_404 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawLoop_366 -> T_RawMagma_36
d_'92''92''45'rawMagma_404 :: () -> () -> T_RawLoop_366 -> T_RawMagma_36
d_'92''92''45'rawMagma_404 ~()
v0 ~()
v1 T_RawLoop_366
v2
  = T_RawLoop_366 -> T_RawMagma_36
du_'92''92''45'rawMagma_404 T_RawLoop_366
v2
du_'92''92''45'rawMagma_404 :: T_RawLoop_366 -> T_RawMagma_36
du_'92''92''45'rawMagma_404 :: T_RawLoop_366 -> T_RawMagma_36
du_'92''92''45'rawMagma_404 T_RawLoop_366
v0
  = (T_RawQuasigroup_326 -> T_RawMagma_36) -> AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe
      T_RawQuasigroup_326 -> T_RawMagma_36
du_'92''92''45'rawMagma_354 ((T_RawLoop_366 -> T_RawQuasigroup_326) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawLoop_366 -> T_RawQuasigroup_326
du_rawQuasigroup_396 (T_RawLoop_366 -> AgdaAny
forall a b. a -> b
coe T_RawLoop_366
v0))
-- Algebra.Bundles.Raw.RawLoop._.∙-rawMagma
d_'8729''45'rawMagma_406 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawLoop_366 -> T_RawMagma_36
d_'8729''45'rawMagma_406 :: () -> () -> T_RawLoop_366 -> T_RawMagma_36
d_'8729''45'rawMagma_406 ~()
v0 ~()
v1 T_RawLoop_366
v2 = T_RawLoop_366 -> T_RawMagma_36
du_'8729''45'rawMagma_406 T_RawLoop_366
v2
du_'8729''45'rawMagma_406 :: T_RawLoop_366 -> T_RawMagma_36
du_'8729''45'rawMagma_406 :: T_RawLoop_366 -> T_RawMagma_36
du_'8729''45'rawMagma_406 T_RawLoop_366
v0
  = (T_RawQuasigroup_326 -> T_RawMagma_36) -> AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe T_RawQuasigroup_326 -> T_RawMagma_36
du_'8729''45'rawMagma_352 ((T_RawLoop_366 -> T_RawQuasigroup_326) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawLoop_366 -> T_RawQuasigroup_326
du_rawQuasigroup_396 (T_RawLoop_366 -> AgdaAny
forall a b. a -> b
coe T_RawLoop_366
v0))
-- Algebra.Bundles.Raw.RawKleeneAlgebra
d_RawKleeneAlgebra_412 :: p -> p -> ()
d_RawKleeneAlgebra_412 p
a0 p
a1 = ()
data T_RawKleeneAlgebra_412
  = C_RawKleeneAlgebra'46'constructor_6153 (AgdaAny ->
                                            AgdaAny -> AgdaAny)
                                           (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)
                                           AgdaAny AgdaAny
-- Algebra.Bundles.Raw.RawKleeneAlgebra.Carrier
d_Carrier_432 :: T_RawKleeneAlgebra_412 -> ()
d_Carrier_432 :: T_RawKleeneAlgebra_412 -> ()
d_Carrier_432 = T_RawKleeneAlgebra_412 -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawKleeneAlgebra._≈_
d__'8776'__434 ::
  T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> ()
d__'8776'__434 :: T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> ()
d__'8776'__434 = T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawKleeneAlgebra._+_
d__'43'__436 ::
  T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__436 :: T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__436 T_RawKleeneAlgebra_412
v0
  = case T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0 of
      C_RawKleeneAlgebra'46'constructor_6153 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3
      T_RawKleeneAlgebra_412
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawKleeneAlgebra._*_
d__'42'__438 ::
  T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__438 :: T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__438 T_RawKleeneAlgebra_412
v0
  = case T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0 of
      C_RawKleeneAlgebra'46'constructor_6153 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4
      T_RawKleeneAlgebra_412
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawKleeneAlgebra._⋆
d__'8902'_440 :: T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny
d__'8902'_440 :: T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny
d__'8902'_440 T_RawKleeneAlgebra_412
v0
  = case T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0 of
      C_RawKleeneAlgebra'46'constructor_6153 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v5
      T_RawKleeneAlgebra_412
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawKleeneAlgebra.0#
d_0'35'_442 :: T_RawKleeneAlgebra_412 -> AgdaAny
d_0'35'_442 :: T_RawKleeneAlgebra_412 -> AgdaAny
d_0'35'_442 T_RawKleeneAlgebra_412
v0
  = case T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0 of
      C_RawKleeneAlgebra'46'constructor_6153 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
      T_RawKleeneAlgebra_412
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawKleeneAlgebra.1#
d_1'35'_444 :: T_RawKleeneAlgebra_412 -> AgdaAny
d_1'35'_444 :: T_RawKleeneAlgebra_412 -> AgdaAny
d_1'35'_444 T_RawKleeneAlgebra_412
v0
  = case T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0 of
      C_RawKleeneAlgebra'46'constructor_6153 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7
      T_RawKleeneAlgebra_412
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Bundles.Raw.RawKleeneAlgebra.rawSemiring
d_rawSemiring_446 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawKleeneAlgebra_412 -> T_RawSemiring_174
d_rawSemiring_446 :: () -> () -> T_RawKleeneAlgebra_412 -> T_RawSemiring_174
d_rawSemiring_446 ~()
v0 ~()
v1 T_RawKleeneAlgebra_412
v2 = T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 T_RawKleeneAlgebra_412
v2
du_rawSemiring_446 :: T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 :: T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 T_RawKleeneAlgebra_412
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_RawSemiring_174)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_RawSemiring_174
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_RawSemiring_174
C_RawSemiring'46'constructor_2353 (T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> AgdaAny
d__'43'__436 (T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0))
      (T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> AgdaAny
d__'42'__438 (T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0)) (T_RawKleeneAlgebra_412 -> AgdaAny
d_0'35'_442 (T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0))
      (T_RawKleeneAlgebra_412 -> AgdaAny
d_1'35'_444 (T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0))
-- Algebra.Bundles.Raw.RawKleeneAlgebra._._≉_
d__'8777'__450 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> ()
d__'8777'__450 :: () -> () -> T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> ()
d__'8777'__450 = () -> () -> T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Bundles.Raw.RawKleeneAlgebra._.*-rawMagma
d_'42''45'rawMagma_452 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawKleeneAlgebra_412 -> T_RawMagma_36
d_'42''45'rawMagma_452 :: () -> () -> T_RawKleeneAlgebra_412 -> T_RawMagma_36
d_'42''45'rawMagma_452 ~()
v0 ~()
v1 T_RawKleeneAlgebra_412
v2 = T_RawKleeneAlgebra_412 -> T_RawMagma_36
du_'42''45'rawMagma_452 T_RawKleeneAlgebra_412
v2
du_'42''45'rawMagma_452 :: T_RawKleeneAlgebra_412 -> T_RawMagma_36
du_'42''45'rawMagma_452 :: T_RawKleeneAlgebra_412 -> T_RawMagma_36
du_'42''45'rawMagma_452 T_RawKleeneAlgebra_412
v0
  = let v1 :: t
v1 = (T_RawKleeneAlgebra_412 -> T_RawSemiring_174) -> AgdaAny -> t
forall a b. a -> b
coe T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 (T_RawKleeneAlgebra_412 -> AgdaAny
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0) in
    AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe
      ((T_RawNearSemiring_134 -> T_RawMagma_36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMagma_36
du_'42''45'rawMagma_168 ((T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Bundles.Raw.RawKleeneAlgebra._.*-rawMonoid
d_'42''45'rawMonoid_454 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawKleeneAlgebra_412 -> T_RawMonoid_64
d_'42''45'rawMonoid_454 :: () -> () -> T_RawKleeneAlgebra_412 -> T_RawMonoid_64
d_'42''45'rawMonoid_454 ~()
v0 ~()
v1 T_RawKleeneAlgebra_412
v2 = T_RawKleeneAlgebra_412 -> T_RawMonoid_64
du_'42''45'rawMonoid_454 T_RawKleeneAlgebra_412
v2
du_'42''45'rawMonoid_454 ::
  T_RawKleeneAlgebra_412 -> T_RawMonoid_64
du_'42''45'rawMonoid_454 :: T_RawKleeneAlgebra_412 -> T_RawMonoid_64
du_'42''45'rawMonoid_454 T_RawKleeneAlgebra_412
v0
  = (T_RawSemiring_174 -> T_RawMonoid_64) -> AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawMonoid_64
du_'42''45'rawMonoid_216 ((T_RawKleeneAlgebra_412 -> T_RawSemiring_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 (T_RawKleeneAlgebra_412 -> AgdaAny
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0))
-- Algebra.Bundles.Raw.RawKleeneAlgebra._.rawMagma
d_rawMagma_456 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawKleeneAlgebra_412 -> T_RawMagma_36
d_rawMagma_456 :: () -> () -> T_RawKleeneAlgebra_412 -> T_RawMagma_36
d_rawMagma_456 ~()
v0 ~()
v1 T_RawKleeneAlgebra_412
v2 = T_RawKleeneAlgebra_412 -> T_RawMagma_36
du_rawMagma_456 T_RawKleeneAlgebra_412
v2
du_rawMagma_456 :: T_RawKleeneAlgebra_412 -> T_RawMagma_36
du_rawMagma_456 :: T_RawKleeneAlgebra_412 -> T_RawMagma_36
du_rawMagma_456 T_RawKleeneAlgebra_412
v0
  = let v1 :: t
v1 = (T_RawKleeneAlgebra_412 -> T_RawSemiring_174) -> AgdaAny -> t
forall a b. a -> b
coe T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 (T_RawKleeneAlgebra_412 -> AgdaAny
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0) in
    AgdaAny -> T_RawMagma_36
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> t
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_RawMonoid_64 -> T_RawMagma_36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonoid_64 -> T_RawMagma_36
du_rawMagma_86 ((T_RawNearSemiring_134 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Algebra.Bundles.Raw.RawKleeneAlgebra._.+-rawMonoid
d_'43''45'rawMonoid_458 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_RawKleeneAlgebra_412 -> T_RawMonoid_64
d_'43''45'rawMonoid_458 :: () -> () -> T_RawKleeneAlgebra_412 -> T_RawMonoid_64
d_'43''45'rawMonoid_458 ~()
v0 ~()
v1 T_RawKleeneAlgebra_412
v2 = T_RawKleeneAlgebra_412 -> T_RawMonoid_64
du_'43''45'rawMonoid_458 T_RawKleeneAlgebra_412
v2
du_'43''45'rawMonoid_458 ::
  T_RawKleeneAlgebra_412 -> T_RawMonoid_64
du_'43''45'rawMonoid_458 :: T_RawKleeneAlgebra_412 -> T_RawMonoid_64
du_'43''45'rawMonoid_458 T_RawKleeneAlgebra_412
v0
  = let v1 :: t
v1 = (T_RawKleeneAlgebra_412 -> T_RawSemiring_174) -> AgdaAny -> t
forall a b. a -> b
coe T_RawKleeneAlgebra_412 -> T_RawSemiring_174
du_rawSemiring_446 (T_RawKleeneAlgebra_412 -> AgdaAny
forall a b. a -> b
coe T_RawKleeneAlgebra_412
v0) in
    AgdaAny -> T_RawMonoid_64
forall a b. a -> b
coe
      ((T_RawNearSemiring_134 -> T_RawMonoid_64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_RawNearSemiring_134 -> T_RawMonoid_64
du_'43''45'rawMonoid_160 ((T_RawSemiring_174 -> T_RawNearSemiring_134) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawSemiring_174 -> T_RawNearSemiring_134
du_rawNearSemiring_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))