{-# 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.Morphism 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
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Algebra.Morphism.Definitions._.Homomorphic₀
d_Homomorphic'8320'_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_32 = T_Level_18
-> T_Level_18
-> 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.Morphism.Definitions._.Homomorphic₁
d_Homomorphic'8321'_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_34 :: T_Level_18
-> T_Level_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_Homomorphic'8321'_34 = T_Level_18
-> T_Level_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.Morphism.Definitions._.Homomorphic₂
d_Homomorphic'8322'_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_36 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism.Definitions._.Morphism
d_Morphism_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Morphism_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
d_Morphism_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F._∙_
d__'8729'__58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8729'__58 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Semigroup_536
v4 ~T_Semigroup_536
v5 = T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 T_Semigroup_536
v4
du__'8729'__58 ::
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 T_Semigroup_536
v0
  = (T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__554 (T_Semigroup_536 -> AgdaAny
forall a b. a -> b
coe T_Semigroup_536
v0)
-- Algebra.Morphism._.F._≈_
d__'8776'__60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__60 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_138 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_140 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_142 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 -> ()
d_Morphism_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> T_Level_18
d_Morphism_144 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsSemigroupMorphism
d_IsSemigroupMorphism_148 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsSemigroupMorphism_148 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsSemigroupMorphism_148
  = C_IsSemigroupMorphism'46'constructor_1081 (AgdaAny ->
                                               AgdaAny -> AgdaAny -> AgdaAny)
                                              (AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Morphism._.IsSemigroupMorphism.⟦⟧-cong
d_'10214''10215''45'cong_156 ::
  T_IsSemigroupMorphism_148 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156 :: T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156 T_IsSemigroupMorphism_148
v0
  = case T_IsSemigroupMorphism_148 -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsSemigroupMorphism_148
v0 of
      C_IsSemigroupMorphism'46'constructor_1081 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
      T_IsSemigroupMorphism_148
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsSemigroupMorphism.∙-homo
d_'8729''45'homo_158 ::
  T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158 :: T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158 T_IsSemigroupMorphism_148
v0
  = case T_IsSemigroupMorphism_148 -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsSemigroupMorphism_148
v0 of
      C_IsSemigroupMorphism'46'constructor_1081 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2
      T_IsSemigroupMorphism_148
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsSemigroupMorphism-syntax
d_IsSemigroupMorphism'45'syntax_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsSemigroupMorphism'45'syntax_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemigroupMorphism'45'syntax_160 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_536
-> T_Semigroup_536
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.semigroup
d_semigroup_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_semigroup_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> T_Semigroup_536
d_semigroup_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Monoid_882
v4 ~T_Monoid_882
v5 = T_Monoid_882 -> T_Semigroup_536
du_semigroup_218 T_Monoid_882
v4
du_semigroup_218 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_semigroup_218 :: T_Monoid_882 -> T_Semigroup_536
du_semigroup_218 T_Monoid_882
v0
  = (T_Monoid_882 -> T_Semigroup_536) -> AgdaAny -> T_Semigroup_536
forall a b. a -> b
coe T_Monoid_882 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.du_semigroup_944 (T_Monoid_882 -> AgdaAny
forall a b. a -> b
coe T_Monoid_882
v0)
-- Algebra.Morphism._.F.ε
d_ε_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 -> AgdaAny
d_ε_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> AgdaAny
d_ε_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Monoid_882
v4 ~T_Monoid_882
v5 = T_Monoid_882 -> AgdaAny
du_ε_228 T_Monoid_882
v4
du_ε_228 :: MAlonzo.Code.Algebra.Bundles.T_Monoid_882 -> AgdaAny
du_ε_228 :: T_Monoid_882 -> AgdaAny
du_ε_228 T_Monoid_882
v0 = (T_Monoid_882 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_882 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_904 (T_Monoid_882 -> AgdaAny
forall a b. a -> b
coe T_Monoid_882
v0)
-- Algebra.Morphism._.T.semigroup
d_semigroup_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_semigroup_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> T_Semigroup_536
d_semigroup_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Monoid_882
v4 T_Monoid_882
v5 = T_Monoid_882 -> T_Semigroup_536
du_semigroup_276 T_Monoid_882
v5
du_semigroup_276 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_semigroup_276 :: T_Monoid_882 -> T_Semigroup_536
du_semigroup_276 T_Monoid_882
v0
  = (T_Monoid_882 -> T_Semigroup_536) -> AgdaAny -> T_Semigroup_536
forall a b. a -> b
coe T_Monoid_882 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.du_semigroup_944 (T_Monoid_882 -> AgdaAny
forall a b. a -> b
coe T_Monoid_882
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_296 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_296 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_298 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_300 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_300 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_300 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 -> ()
d_Morphism_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> T_Level_18
d_Morphism_302 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsMonoidMorphism
d_IsMonoidMorphism_306 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsMonoidMorphism_306 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsMonoidMorphism_306
  = C_IsMonoidMorphism'46'constructor_2139 T_IsSemigroupMorphism_148
                                           AgdaAny
-- Algebra.Morphism._.IsMonoidMorphism.sm-homo
d_sm'45'homo_314 ::
  T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 :: T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 T_IsMonoidMorphism_306
v0
  = case T_IsMonoidMorphism_306 -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsMonoidMorphism_306
v0 of
      C_IsMonoidMorphism'46'constructor_2139 T_IsSemigroupMorphism_148
v1 AgdaAny
v2 -> T_IsSemigroupMorphism_148 -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsSemigroupMorphism_148
v1
      T_IsMonoidMorphism_306
_ -> T_IsSemigroupMorphism_148
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsMonoidMorphism.ε-homo
d_ε'45'homo_316 :: T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316 :: T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316 T_IsMonoidMorphism_306
v0
  = case T_IsMonoidMorphism_306 -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsMonoidMorphism_306
v0 of
      C_IsMonoidMorphism'46'constructor_2139 T_IsSemigroupMorphism_148
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_IsMonoidMorphism_306
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsMonoidMorphism._.∙-homo
d_'8729''45'homo_320 ::
  T_IsMonoidMorphism_306 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_320 :: T_IsMonoidMorphism_306 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_320 T_IsMonoidMorphism_306
v0
  = (T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158 ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 (T_IsMonoidMorphism_306 -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306
v0))
-- Algebra.Morphism._.IsMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_322 ::
  T_IsMonoidMorphism_306 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_322 :: T_IsMonoidMorphism_306 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_322 T_IsMonoidMorphism_306
v0
  = (T_IsSemigroupMorphism_148
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156 ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 (T_IsMonoidMorphism_306 -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306
v0))
-- Algebra.Morphism._.IsMonoidMorphism-syntax
d_IsMonoidMorphism'45'syntax_324 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsMonoidMorphism'45'syntax_324 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsMonoidMorphism'45'syntax_324 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_882
-> T_Monoid_882
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.monoid
d_monoid_386 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_monoid_386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> T_Monoid_882
d_monoid_386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_CommutativeMonoid_962
v4 ~T_CommutativeMonoid_962
v5 = T_CommutativeMonoid_962 -> T_Monoid_882
du_monoid_386 T_CommutativeMonoid_962
v4
du_monoid_386 ::
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_monoid_386 :: T_CommutativeMonoid_962 -> T_Monoid_882
du_monoid_386 T_CommutativeMonoid_962
v0
  = (T_CommutativeMonoid_962 -> T_Monoid_882)
-> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe T_CommutativeMonoid_962 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1032 (T_CommutativeMonoid_962 -> AgdaAny
forall a b. a -> b
coe T_CommutativeMonoid_962
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_458 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_monoid_458 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> T_Monoid_882
d_monoid_458 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_CommutativeMonoid_962
v4 T_CommutativeMonoid_962
v5 = T_CommutativeMonoid_962 -> T_Monoid_882
du_monoid_458 T_CommutativeMonoid_962
v5
du_monoid_458 ::
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_monoid_458 :: T_CommutativeMonoid_962 -> T_Monoid_882
du_monoid_458 T_CommutativeMonoid_962
v0
  = (T_CommutativeMonoid_962 -> T_Monoid_882)
-> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe T_CommutativeMonoid_962 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1032 (T_CommutativeMonoid_962 -> AgdaAny
forall a b. a -> b
coe T_CommutativeMonoid_962
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_488 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_488 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_488 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_490 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_490 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_490 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_492 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_492 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_492 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_494 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 -> ()
d_Morphism_494 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> T_Level_18
d_Morphism_494 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsCommutativeMonoidMorphism
d_IsCommutativeMonoidMorphism_498 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeMonoidMorphism_498 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsCommutativeMonoidMorphism_498
  = C_IsCommutativeMonoidMorphism'46'constructor_3705 T_IsMonoidMorphism_306
-- Algebra.Morphism._.IsCommutativeMonoidMorphism.mn-homo
d_mn'45'homo_504 ::
  T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306
d_mn'45'homo_504 :: T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306
d_mn'45'homo_504 T_IsCommutativeMonoidMorphism_498
v0
  = case T_IsCommutativeMonoidMorphism_498
-> T_IsCommutativeMonoidMorphism_498
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498
v0 of
      C_IsCommutativeMonoidMorphism'46'constructor_3705 T_IsMonoidMorphism_306
v1 -> T_IsMonoidMorphism_306 -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsMonoidMorphism_306
v1
      T_IsCommutativeMonoidMorphism_498
_ -> T_IsMonoidMorphism_306
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.sm-homo
d_sm'45'homo_508 ::
  T_IsCommutativeMonoidMorphism_498 -> T_IsSemigroupMorphism_148
d_sm'45'homo_508 :: T_IsCommutativeMonoidMorphism_498 -> T_IsSemigroupMorphism_148
d_sm'45'homo_508 T_IsCommutativeMonoidMorphism_498
v0
  = (T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306
d_mn'45'homo_504 (T_IsCommutativeMonoidMorphism_498 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498
v0))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.ε-homo
d_ε'45'homo_510 :: T_IsCommutativeMonoidMorphism_498 -> AgdaAny
d_ε'45'homo_510 :: T_IsCommutativeMonoidMorphism_498 -> AgdaAny
d_ε'45'homo_510 T_IsCommutativeMonoidMorphism_498
v0
  = (T_IsMonoidMorphism_306 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316 ((T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306
d_mn'45'homo_504 (T_IsCommutativeMonoidMorphism_498 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498
v0))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.∙-homo
d_'8729''45'homo_512 ::
  T_IsCommutativeMonoidMorphism_498 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_512 :: T_IsCommutativeMonoidMorphism_498 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_512 T_IsCommutativeMonoidMorphism_498
v0
  = (T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306
d_mn'45'homo_504 (T_IsCommutativeMonoidMorphism_498 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498
v0)))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_514 ::
  T_IsCommutativeMonoidMorphism_498 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_514 :: T_IsCommutativeMonoidMorphism_498
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_514 T_IsCommutativeMonoidMorphism_498
v0
  = (T_IsSemigroupMorphism_148
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306
d_mn'45'homo_504 (T_IsCommutativeMonoidMorphism_498 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_498
v0)))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism-syntax
d_IsCommutativeMonoidMorphism'45'syntax_516 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsCommutativeMonoidMorphism'45'syntax_516 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsCommutativeMonoidMorphism'45'syntax_516 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_962
-> T_CommutativeMonoid_962
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.commutativeMonoid
d_commutativeMonoid_554 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
d_commutativeMonoid_554 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> T_CommutativeMonoid_962
d_commutativeMonoid_554 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IdempotentCommutativeMonoid_1148
v4 ~T_IdempotentCommutativeMonoid_1148
v5
  = T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
du_commutativeMonoid_554 T_IdempotentCommutativeMonoid_1148
v4
du_commutativeMonoid_554 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
du_commutativeMonoid_554 :: T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
du_commutativeMonoid_554 T_IdempotentCommutativeMonoid_1148
v0
  = (T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962)
-> AgdaAny -> T_CommutativeMonoid_962
forall a b. a -> b
coe
      T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1228 (T_IdempotentCommutativeMonoid_1148 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1148
v0)
-- Algebra.Morphism._.F.monoid
d_monoid_596 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_monoid_596 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> T_Monoid_882
d_monoid_596 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IdempotentCommutativeMonoid_1148
v4 ~T_IdempotentCommutativeMonoid_1148
v5 = T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882
du_monoid_596 T_IdempotentCommutativeMonoid_1148
v4
du_monoid_596 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_monoid_596 :: T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882
du_monoid_596 T_IdempotentCommutativeMonoid_1148
v0
  = (T_CommutativeMonoid_962 -> T_Monoid_882)
-> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      T_CommutativeMonoid_962 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1032
      ((T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1228 (T_IdempotentCommutativeMonoid_1148 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1148
v0))
-- Algebra.Morphism._.T.commutativeMonoid
d_commutativeMonoid_644 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
d_commutativeMonoid_644 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> T_CommutativeMonoid_962
d_commutativeMonoid_644 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_1148
v4 T_IdempotentCommutativeMonoid_1148
v5
  = T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
du_commutativeMonoid_644 T_IdempotentCommutativeMonoid_1148
v5
du_commutativeMonoid_644 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
du_commutativeMonoid_644 :: T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
du_commutativeMonoid_644 T_IdempotentCommutativeMonoid_1148
v0
  = (T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962)
-> AgdaAny -> T_CommutativeMonoid_962
forall a b. a -> b
coe
      T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1228 (T_IdempotentCommutativeMonoid_1148 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1148
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_686 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_monoid_686 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> T_Monoid_882
d_monoid_686 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_1148
v4 T_IdempotentCommutativeMonoid_1148
v5 = T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882
du_monoid_686 T_IdempotentCommutativeMonoid_1148
v5
du_monoid_686 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_monoid_686 :: T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882
du_monoid_686 T_IdempotentCommutativeMonoid_1148
v0
  = (T_CommutativeMonoid_962 -> T_Monoid_882)
-> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      T_CommutativeMonoid_962 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1032
      ((T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1228 (T_IdempotentCommutativeMonoid_1148 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1148
v0))
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_716 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_716 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_716 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_718 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_718 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_718 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_720 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_720 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_720 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_722 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  ()
d_Morphism_722 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> T_Level_18
d_Morphism_722 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism
d_IsIdempotentCommutativeMonoidMorphism_726 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsIdempotentCommutativeMonoidMorphism_726 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6
  = ()
newtype T_IsIdempotentCommutativeMonoidMorphism_726
  = C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5361 T_IsMonoidMorphism_306
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism.mn-homo
d_mn'45'homo_732 ::
  T_IsIdempotentCommutativeMonoidMorphism_726 ->
  T_IsMonoidMorphism_306
d_mn'45'homo_732 :: T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsMonoidMorphism_306
d_mn'45'homo_732 T_IsIdempotentCommutativeMonoidMorphism_726
v0
  = case T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsIdempotentCommutativeMonoidMorphism_726
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
v0 of
      C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5361 T_IsMonoidMorphism_306
v1
        -> T_IsMonoidMorphism_306 -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsMonoidMorphism_306
v1
      T_IsIdempotentCommutativeMonoidMorphism_726
_ -> T_IsMonoidMorphism_306
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.sm-homo
d_sm'45'homo_736 ::
  T_IsIdempotentCommutativeMonoidMorphism_726 ->
  T_IsSemigroupMorphism_148
d_sm'45'homo_736 :: T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsSemigroupMorphism_148
d_sm'45'homo_736 T_IsIdempotentCommutativeMonoidMorphism_726
v0
  = (T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsIdempotentCommutativeMonoidMorphism_726
 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsMonoidMorphism_306
d_mn'45'homo_732 (T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.ε-homo
d_ε'45'homo_738 ::
  T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
d_ε'45'homo_738 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
d_ε'45'homo_738 T_IsIdempotentCommutativeMonoidMorphism_726
v0
  = (T_IsMonoidMorphism_306 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316 ((T_IsIdempotentCommutativeMonoidMorphism_726
 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsMonoidMorphism_306
d_mn'45'homo_732 (T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.∙-homo
d_'8729''45'homo_740 ::
  T_IsIdempotentCommutativeMonoidMorphism_726 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_740 :: T_IsIdempotentCommutativeMonoidMorphism_726
-> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_740 T_IsIdempotentCommutativeMonoidMorphism_726
v0
  = (T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsIdempotentCommutativeMonoidMorphism_726
 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsMonoidMorphism_306
d_mn'45'homo_732 (T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
v0)))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_742 ::
  T_IsIdempotentCommutativeMonoidMorphism_726 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_742 :: T_IsIdempotentCommutativeMonoidMorphism_726
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_742 T_IsIdempotentCommutativeMonoidMorphism_726
v0
  = (T_IsSemigroupMorphism_148
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsIdempotentCommutativeMonoidMorphism_726
 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsMonoidMorphism_306
d_mn'45'homo_732 (T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
v0)))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism.isCommutativeMonoidMorphism
d_isCommutativeMonoidMorphism_744 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  (AgdaAny -> AgdaAny) ->
  T_IsIdempotentCommutativeMonoidMorphism_726 ->
  T_IsCommutativeMonoidMorphism_498
d_isCommutativeMonoidMorphism_744 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsCommutativeMonoidMorphism_498
d_isCommutativeMonoidMorphism_744 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_1148
v4 ~T_IdempotentCommutativeMonoid_1148
v5 ~AgdaAny -> AgdaAny
v6 T_IsIdempotentCommutativeMonoidMorphism_726
v7
  = T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsCommutativeMonoidMorphism_498
du_isCommutativeMonoidMorphism_744 T_IsIdempotentCommutativeMonoidMorphism_726
v7
du_isCommutativeMonoidMorphism_744 ::
  T_IsIdempotentCommutativeMonoidMorphism_726 ->
  T_IsCommutativeMonoidMorphism_498
du_isCommutativeMonoidMorphism_744 :: T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsCommutativeMonoidMorphism_498
du_isCommutativeMonoidMorphism_744 T_IsIdempotentCommutativeMonoidMorphism_726
v0
  = (T_IsMonoidMorphism_306 -> T_IsCommutativeMonoidMorphism_498)
-> AgdaAny -> T_IsCommutativeMonoidMorphism_498
forall a b. a -> b
coe
      T_IsMonoidMorphism_306 -> T_IsCommutativeMonoidMorphism_498
C_IsCommutativeMonoidMorphism'46'constructor_3705
      ((T_IsIdempotentCommutativeMonoidMorphism_726
 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
-> T_IsMonoidMorphism_306
d_mn'45'homo_732 (T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_726
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism-syntax
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_746 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_746 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_746 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1148
-> T_IdempotentCommutativeMonoid_1148
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F._⁻¹
d__'8315''185'_772 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 -> AgdaAny -> AgdaAny
d__'8315''185'_772 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> AgdaAny
-> AgdaAny
d__'8315''185'_772 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_1520
v4 ~T_Group_1520
v5 = T_Group_1520 -> AgdaAny -> AgdaAny
du__'8315''185'_772 T_Group_1520
v4
du__'8315''185'_772 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 -> AgdaAny -> AgdaAny
du__'8315''185'_772 :: T_Group_1520 -> AgdaAny -> AgdaAny
du__'8315''185'_772 T_Group_1520
v0
  = (T_Group_1520 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v0)
-- Algebra.Morphism._.F.monoid
d_monoid_820 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_monoid_820 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> T_Monoid_882
d_monoid_820 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_1520
v4 ~T_Group_1520
v5 = T_Group_1520 -> T_Monoid_882
du_monoid_820 T_Group_1520
v4
du_monoid_820 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_monoid_820 :: T_Group_1520 -> T_Monoid_882
du_monoid_820 T_Group_1520
v0
  = (T_Group_1520 -> T_Monoid_882) -> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe T_Group_1520 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1612 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_912 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_monoid_912 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> T_Monoid_882
d_monoid_912 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Group_1520
v4 T_Group_1520
v5 = T_Group_1520 -> T_Monoid_882
du_monoid_912 T_Group_1520
v5
du_monoid_912 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_monoid_912 :: T_Group_1520 -> T_Monoid_882
du_monoid_912 T_Group_1520
v0
  = (T_Group_1520 -> T_Monoid_882) -> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe T_Group_1520 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1612 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_950 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_950 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_950 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_952 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_952 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_952 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_954 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_954 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_954 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_956 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 -> ()
d_Morphism_956 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> T_Level_18
d_Morphism_956 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsGroupMorphism
d_IsGroupMorphism_960 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsGroupMorphism_960 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsGroupMorphism_960
  = C_IsGroupMorphism'46'constructor_7465 T_IsMonoidMorphism_306
-- Algebra.Morphism._.IsGroupMorphism.mn-homo
d_mn'45'homo_966 :: T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 :: T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 T_IsGroupMorphism_960
v0
  = case T_IsGroupMorphism_960 -> T_IsGroupMorphism_960
forall a b. a -> b
coe T_IsGroupMorphism_960
v0 of
      C_IsGroupMorphism'46'constructor_7465 T_IsMonoidMorphism_306
v1 -> T_IsMonoidMorphism_306 -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsMonoidMorphism_306
v1
      T_IsGroupMorphism_960
_ -> T_IsMonoidMorphism_306
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsGroupMorphism._.sm-homo
d_sm'45'homo_970 ::
  T_IsGroupMorphism_960 -> T_IsSemigroupMorphism_148
d_sm'45'homo_970 :: T_IsGroupMorphism_960 -> T_IsSemigroupMorphism_148
d_sm'45'homo_970 T_IsGroupMorphism_960
v0
  = (T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v0))
-- Algebra.Morphism._.IsGroupMorphism._.ε-homo
d_ε'45'homo_972 :: T_IsGroupMorphism_960 -> AgdaAny
d_ε'45'homo_972 :: T_IsGroupMorphism_960 -> AgdaAny
d_ε'45'homo_972 T_IsGroupMorphism_960
v0
  = (T_IsMonoidMorphism_306 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v0))
-- Algebra.Morphism._.IsGroupMorphism._.∙-homo
d_'8729''45'homo_974 ::
  T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_974 :: T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_974 T_IsGroupMorphism_960
v0
  = (T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v0)))
-- Algebra.Morphism._.IsGroupMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_976 ::
  T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_976 :: T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_976 T_IsGroupMorphism_960
v0
  = (T_IsSemigroupMorphism_148
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v0)))
-- Algebra.Morphism._.IsGroupMorphism.⁻¹-homo
d_'8315''185''45'homo_978 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny
d_'8315''185''45'homo_978 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_960
-> AgdaAny
-> AgdaAny
d_'8315''185''45'homo_978 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_1520
v4 T_Group_1520
v5 AgdaAny -> AgdaAny
v6 T_IsGroupMorphism_960
v7 AgdaAny
v8
  = T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_960
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_978 T_Group_1520
v4 T_Group_1520
v5 AgdaAny -> AgdaAny
v6 T_IsGroupMorphism_960
v7 AgdaAny
v8
du_'8315''185''45'homo_978 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny
du_'8315''185''45'homo_978 :: T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_960
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_978 T_Group_1520
v0 T_Group_1520
v1 AgdaAny -> AgdaAny
v2 T_IsGroupMorphism_960
v3 AgdaAny
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> T_IsGroup_1036
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsGroup_1036
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsGroup_1036
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.du_unique'737''45''8315''185'_1114
      (T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1542 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
      (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
      (T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
      (T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny
v2 ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
         (\ AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 ->
            (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v7)
         ((T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1542 T_Group_1520
v1
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> AgdaAny
v2 ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4))
         (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
         (((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
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                  ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                     (let v5 :: T_IsGroup_1036
v5 = T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (let v6 :: T_IsMonoid_686
v6
                               = T_IsGroup_1036 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.d_isMonoid_1050 (T_IsGroup_1036 -> T_IsGroup_1036
forall a b. a -> b
coe T_IsGroup_1036
v5) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (let v7 :: T_IsSemigroup_472
v7
                                  = T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (T_IsMonoid_686 -> T_IsMonoid_686
forall a b. a -> b
coe T_IsMonoid_686
v6) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              ((T_IsMagma_176 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsMagma_176 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_200
                                 ((T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480 (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v7)))))))))
            ((T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1542 T_Group_1520
v1
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2 ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> AgdaAny
v2
               ((T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1542 T_Group_1520
v0
                  ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4) AgdaAny
v4))
            (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
            (((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
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                     ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                        (let v5 :: T_IsGroup_1036
v5 = T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (let v6 :: T_IsMonoid_686
v6
                                  = T_IsGroup_1036 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.d_isMonoid_1050 (T_IsGroup_1036 -> T_IsGroup_1036
forall a b. a -> b
coe T_IsGroup_1036
v5) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (let v7 :: T_IsSemigroup_472
v7
                                     = T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (T_IsMonoid_686 -> T_IsMonoid_686
forall a b. a -> b
coe T_IsMonoid_686
v6) in
                               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 ((T_IsMagma_176 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_IsMagma_176 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_200
                                    ((T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480
                                       (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v7)))))))))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  ((T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1542 T_Group_1520
v0
                     ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4) AgdaAny
v4))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v0)))
               (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
               (((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
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                     ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                           (let v5 :: T_IsGroup_1036
v5 = T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (let v6 :: T_IsMonoid_686
v6
                                     = T_IsGroup_1036 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.d_isMonoid_1050 (T_IsGroup_1036 -> T_IsGroup_1036
forall a b. a -> b
coe T_IsGroup_1036
v5) in
                               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 (let v7 :: T_IsSemigroup_472
v7
                                        = T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
                                            (T_IsMonoid_686 -> T_IsMonoid_686
forall a b. a -> b
coe T_IsMonoid_686
v6) in
                                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    ((T_IsMagma_176 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       T_IsMagma_176 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_200
                                       ((T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                          T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480
                                          (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v7)))))))))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v0)))
                  (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
                  (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1))
                  (let v5 :: AgdaAny -> AgdaAny
v5
                         = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                             ((T_Setoid_44 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                                T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                                (let v5 :: T_IsGroup_1036
v5 = T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v1) in
                                 AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   (let v6 :: T_IsMonoid_686
v6
                                          = T_IsGroup_1036 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.d_isMonoid_1050
                                              (T_IsGroup_1036 -> T_IsGroup_1036
forall a b. a -> b
coe T_IsGroup_1036
v5) in
                                    AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                      (let v7 :: T_IsSemigroup_472
v7
                                             = T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
                                                 (T_IsMonoid_686 -> T_IsMonoid_686
forall a b. a -> b
coe T_IsMonoid_686
v6) in
                                       AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                         ((T_IsMagma_176 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            T_IsMagma_176 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_200
                                            ((T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480
                                               (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v7))))))) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                        (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                           ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v5))
                        ((T_Group_1520 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v1))))
                  (T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v3))))
               ((T_IsSemigroupMorphism_148
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroupMorphism_148
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156
                  (T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v3)))
                  ((T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Group_1520 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1542 T_Group_1520
v0
                     ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4) AgdaAny
v4)
                  (T_Group_1520 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1544 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v0))
                  ((T_IsGroup_1036 -> AgdaAny -> AgdaAny)
-> T_IsGroup_1036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsGroup_1036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_inverse'737'_1106
                     (T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> T_Group_1520
forall a b. a -> b
coe T_Group_1520
v0)) AgdaAny
v4)))
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               (T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
                  ((T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
                     T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480
                     ((T_IsMonoid_686 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
                        ((T_IsGroup_1036 -> T_IsMonoid_686) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsGroup_1036 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.d_isMonoid_1050
                           ((T_Group_1520 -> T_IsGroup_1036) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> T_IsGroup_1036
MAlonzo.Code.Algebra.Bundles.d_isGroup_1548 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v1))))))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  (let v5 :: b
v5
                         = let v5 :: t
v5
                                 = (T_Group_1520 -> T_Monoid_882) -> AgdaAny -> t
forall a b. a -> b
coe T_Group_1520 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1612 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v0) in
                           AgdaAny -> b
forall a b. a -> b
coe ((T_Monoid_882 -> T_Semigroup_536) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_882 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.du_semigroup_944 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__554 AgdaAny
forall a. a
v5
                        ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4) AgdaAny
v4)))
               ((T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__554
                  (let v5 :: t
v5
                         = (T_Group_1520 -> T_Monoid_882) -> AgdaAny -> t
forall a b. a -> b
coe T_Group_1520 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_monoid_1612 (T_Group_1520 -> AgdaAny
forall a b. a -> b
coe T_Group_1520
v1) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_Monoid_882 -> T_Semigroup_536) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_882 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.du_semigroup_944 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     AgdaAny -> AgdaAny
v2 ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4))
               ((T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158
                  (T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314 ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 (T_IsGroupMorphism_960 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960
v3)))
                  ((T_Group_1520 -> AgdaAny -> AgdaAny)
-> T_Group_1520 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1520 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1546 T_Group_1520
v0 AgdaAny
v4) AgdaAny
v4))))
-- Algebra.Morphism._.IsGroupMorphism-syntax
d_IsGroupMorphism'45'syntax_1022 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsGroupMorphism'45'syntax_1022 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsGroupMorphism'45'syntax_1022 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.group
d_group_1064 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520
d_group_1064 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> T_Group_1520
d_group_1064 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_AbelianGroup_1636
v4 ~T_AbelianGroup_1636
v5 = T_AbelianGroup_1636 -> T_Group_1520
du_group_1064 T_AbelianGroup_1636
v4
du_group_1064 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520
du_group_1064 :: T_AbelianGroup_1636 -> T_Group_1520
du_group_1064 T_AbelianGroup_1636
v0
  = (T_AbelianGroup_1636 -> T_Group_1520) -> AgdaAny -> T_Group_1520
forall a b. a -> b
coe T_AbelianGroup_1636 -> T_Group_1520
MAlonzo.Code.Algebra.Bundles.du_group_1732 (T_AbelianGroup_1636 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1636
v0)
-- Algebra.Morphism._.T.group
d_group_1168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520
d_group_1168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> T_Group_1520
d_group_1168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_AbelianGroup_1636
v4 T_AbelianGroup_1636
v5 = T_AbelianGroup_1636 -> T_Group_1520
du_group_1168 T_AbelianGroup_1636
v5
du_group_1168 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1520
du_group_1168 :: T_AbelianGroup_1636 -> T_Group_1520
du_group_1168 T_AbelianGroup_1636
v0
  = (T_AbelianGroup_1636 -> T_Group_1520) -> AgdaAny -> T_Group_1520
forall a b. a -> b
coe T_AbelianGroup_1636 -> T_Group_1520
MAlonzo.Code.Algebra.Bundles.du_group_1732 (T_AbelianGroup_1636 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1636
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_1250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_1250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_1250 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_1252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_1252 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_1252 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_1254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_1254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_1254 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_1256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 -> ()
d_Morphism_1256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> T_Level_18
d_Morphism_1256 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsAbelianGroupMorphism
d_IsAbelianGroupMorphism_1260 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsAbelianGroupMorphism_1260 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsAbelianGroupMorphism_1260
  = C_IsAbelianGroupMorphism'46'constructor_11939 T_IsGroupMorphism_960
-- Algebra.Morphism._.IsAbelianGroupMorphism.gp-homo
d_gp'45'homo_1266 ::
  T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 :: T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 T_IsAbelianGroupMorphism_1260
v0
  = case T_IsAbelianGroupMorphism_1260 -> T_IsAbelianGroupMorphism_1260
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v0 of
      C_IsAbelianGroupMorphism'46'constructor_11939 T_IsGroupMorphism_960
v1 -> T_IsGroupMorphism_960 -> T_IsGroupMorphism_960
forall a b. a -> b
coe T_IsGroupMorphism_960
v1
      T_IsAbelianGroupMorphism_1260
_ -> T_IsGroupMorphism_960
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsAbelianGroupMorphism._.mn-homo
d_mn'45'homo_1270 ::
  T_IsAbelianGroupMorphism_1260 -> T_IsMonoidMorphism_306
d_mn'45'homo_1270 :: T_IsAbelianGroupMorphism_1260 -> T_IsMonoidMorphism_306
d_mn'45'homo_1270 T_IsAbelianGroupMorphism_1260
v0
  = (T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 ((T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 (T_IsAbelianGroupMorphism_1260 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v0))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.sm-homo
d_sm'45'homo_1272 ::
  T_IsAbelianGroupMorphism_1260 -> T_IsSemigroupMorphism_148
d_sm'45'homo_1272 :: T_IsAbelianGroupMorphism_1260 -> T_IsSemigroupMorphism_148
d_sm'45'homo_1272 T_IsAbelianGroupMorphism_1260
v0
  = (T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe
      T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314
      ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 ((T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 (T_IsAbelianGroupMorphism_1260 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v0)))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.ε-homo
d_ε'45'homo_1274 :: T_IsAbelianGroupMorphism_1260 -> AgdaAny
d_ε'45'homo_1274 :: T_IsAbelianGroupMorphism_1260 -> AgdaAny
d_ε'45'homo_1274 T_IsAbelianGroupMorphism_1260
v0
  = (T_IsMonoidMorphism_306 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsMonoidMorphism_306 -> AgdaAny
d_ε'45'homo_316
      ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 ((T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 (T_IsAbelianGroupMorphism_1260 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v0)))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.⁻¹-homo
d_'8315''185''45'homo_1276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  (AgdaAny -> AgdaAny) ->
  T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny
d_'8315''185''45'homo_1276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1260
-> AgdaAny
-> AgdaAny
d_'8315''185''45'homo_1276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_AbelianGroup_1636
v4 T_AbelianGroup_1636
v5 AgdaAny -> AgdaAny
v6 T_IsAbelianGroupMorphism_1260
v7
  = T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1260
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_1276 T_AbelianGroup_1636
v4 T_AbelianGroup_1636
v5 AgdaAny -> AgdaAny
v6 T_IsAbelianGroupMorphism_1260
v7
du_'8315''185''45'homo_1276 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  (AgdaAny -> AgdaAny) ->
  T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny
du_'8315''185''45'homo_1276 :: T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1260
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_1276 T_AbelianGroup_1636
v0 T_AbelianGroup_1636
v1 AgdaAny -> AgdaAny
v2 T_IsAbelianGroupMorphism_1260
v3
  = (T_Group_1520
 -> T_Group_1520
 -> (AgdaAny -> AgdaAny)
 -> T_IsGroupMorphism_960
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Group_1520
-> T_Group_1520
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_960
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_978
      ((T_AbelianGroup_1636 -> T_Group_1520) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1636 -> T_Group_1520
MAlonzo.Code.Algebra.Bundles.du_group_1732 (T_AbelianGroup_1636 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1636
v0))
      ((T_AbelianGroup_1636 -> T_Group_1520) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1636 -> T_Group_1520
MAlonzo.Code.Algebra.Bundles.du_group_1732 (T_AbelianGroup_1636 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1636
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      ((T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 (T_IsAbelianGroupMorphism_1260 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v3))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.∙-homo
d_'8729''45'homo_1278 ::
  T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_1278 :: T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_1278 T_IsAbelianGroupMorphism_1260
v0
  = (T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_158
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314
         ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 ((T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 (T_IsAbelianGroupMorphism_1260 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v0))))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_1280 ::
  T_IsAbelianGroupMorphism_1260 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_1280 :: T_IsAbelianGroupMorphism_1260
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_1280 T_IsAbelianGroupMorphism_1260
v0
  = (T_IsSemigroupMorphism_148
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsSemigroupMorphism_148
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_156
      ((T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148
d_sm'45'homo_314
         ((T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306
d_mn'45'homo_966 ((T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960
d_gp'45'homo_1266 (T_IsAbelianGroupMorphism_1260 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v0))))
-- Algebra.Morphism._.IsAbelianGroupMorphism-syntax
d_IsAbelianGroupMorphism'45'syntax_1282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsAbelianGroupMorphism'45'syntax_1282 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsAbelianGroupMorphism'45'syntax_1282 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1636
-> T_AbelianGroup_1636
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.*-monoid
d_'42''45'monoid_1334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'42''45'monoid_1334 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> T_Monoid_882
d_'42''45'monoid_1334 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Ring_3800
v4 ~T_Ring_3800
v5
  = T_Ring_3800 -> T_Monoid_882
du_'42''45'monoid_1334 T_Ring_3800
v4
du_'42''45'monoid_1334 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'42''45'monoid_1334 :: T_Ring_3800 -> T_Monoid_882
du_'42''45'monoid_1334 T_Ring_3800
v0
  = let v1 :: t
v1
          = (T_Ring_3800 -> T_Semiring_2280) -> AgdaAny -> t
forall a b. a -> b
coe T_Ring_3800 -> T_Semiring_2280
MAlonzo.Code.Algebra.Bundles.du_semiring_3952 (T_Ring_3800 -> AgdaAny
forall a b. a -> b
coe T_Ring_3800
v0) in
    AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      ((T_SemiringWithoutAnnihilatingZero_2130 -> T_Monoid_882)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SemiringWithoutAnnihilatingZero_2130 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_'42''45'monoid_2264
         ((T_Semiring_2280 -> T_SemiringWithoutAnnihilatingZero_2130)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semiring_2280 -> T_SemiringWithoutAnnihilatingZero_2130
MAlonzo.Code.Algebra.Bundles.du_semiringWithoutAnnihilatingZero_2398
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Morphism._.F.+-abelianGroup
d_'43''45'abelianGroup_1342 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636
d_'43''45'abelianGroup_1342 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> T_AbelianGroup_1636
d_'43''45'abelianGroup_1342 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Ring_3800
v4 ~T_Ring_3800
v5
  = T_Ring_3800 -> T_AbelianGroup_1636
du_'43''45'abelianGroup_1342 T_Ring_3800
v4
du_'43''45'abelianGroup_1342 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636
du_'43''45'abelianGroup_1342 :: T_Ring_3800 -> T_AbelianGroup_1636
du_'43''45'abelianGroup_1342 T_Ring_3800
v0
  = (T_Ring_3800 -> T_AbelianGroup_1636)
-> AgdaAny -> T_AbelianGroup_1636
forall a b. a -> b
coe
      T_Ring_3800 -> T_AbelianGroup_1636
MAlonzo.Code.Algebra.Bundles.du_'43''45'abelianGroup_3948 (T_Ring_3800 -> AgdaAny
forall a b. a -> b
coe T_Ring_3800
v0)
-- Algebra.Morphism._.T.*-monoid
d_'42''45'monoid_1516 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'42''45'monoid_1516 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> T_Monoid_882
d_'42''45'monoid_1516 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Ring_3800
v4 T_Ring_3800
v5
  = T_Ring_3800 -> T_Monoid_882
du_'42''45'monoid_1516 T_Ring_3800
v5
du_'42''45'monoid_1516 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'42''45'monoid_1516 :: T_Ring_3800 -> T_Monoid_882
du_'42''45'monoid_1516 T_Ring_3800
v0
  = let v1 :: t
v1
          = (T_Ring_3800 -> T_Semiring_2280) -> AgdaAny -> t
forall a b. a -> b
coe T_Ring_3800 -> T_Semiring_2280
MAlonzo.Code.Algebra.Bundles.du_semiring_3952 (T_Ring_3800 -> AgdaAny
forall a b. a -> b
coe T_Ring_3800
v0) in
    AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      ((T_SemiringWithoutAnnihilatingZero_2130 -> T_Monoid_882)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SemiringWithoutAnnihilatingZero_2130 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.du_'42''45'monoid_2264
         ((T_Semiring_2280 -> T_SemiringWithoutAnnihilatingZero_2130)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semiring_2280 -> T_SemiringWithoutAnnihilatingZero_2130
MAlonzo.Code.Algebra.Bundles.du_semiringWithoutAnnihilatingZero_2398
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Morphism._.T.+-abelianGroup
d_'43''45'abelianGroup_1524 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636
d_'43''45'abelianGroup_1524 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> T_AbelianGroup_1636
d_'43''45'abelianGroup_1524 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Ring_3800
v4 T_Ring_3800
v5
  = T_Ring_3800 -> T_AbelianGroup_1636
du_'43''45'abelianGroup_1524 T_Ring_3800
v5
du_'43''45'abelianGroup_1524 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636
du_'43''45'abelianGroup_1524 :: T_Ring_3800 -> T_AbelianGroup_1636
du_'43''45'abelianGroup_1524 T_Ring_3800
v0
  = (T_Ring_3800 -> T_AbelianGroup_1636)
-> AgdaAny -> T_AbelianGroup_1636
forall a b. a -> b
coe
      T_Ring_3800 -> T_AbelianGroup_1636
MAlonzo.Code.Algebra.Bundles.du_'43''45'abelianGroup_3948 (T_Ring_3800 -> AgdaAny
forall a b. a -> b
coe T_Ring_3800
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_1666 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_1666 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_1666 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_1668 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_1668 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_1668 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_1670 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_1670 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_1670 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_1672 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 -> ()
d_Morphism_1672 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> T_Level_18
d_Morphism_1672 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsRingMorphism
d_IsRingMorphism_1676 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRingMorphism_1676 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsRingMorphism_1676
  = C_IsRingMorphism'46'constructor_13939 T_IsAbelianGroupMorphism_1260
                                          T_IsMonoidMorphism_306
-- Algebra.Morphism._.IsRingMorphism.+-abgp-homo
d_'43''45'abgp'45'homo_1684 ::
  T_IsRingMorphism_1676 -> T_IsAbelianGroupMorphism_1260
d_'43''45'abgp'45'homo_1684 :: T_IsRingMorphism_1676 -> T_IsAbelianGroupMorphism_1260
d_'43''45'abgp'45'homo_1684 T_IsRingMorphism_1676
v0
  = case T_IsRingMorphism_1676 -> T_IsRingMorphism_1676
forall a b. a -> b
coe T_IsRingMorphism_1676
v0 of
      C_IsRingMorphism'46'constructor_13939 T_IsAbelianGroupMorphism_1260
v1 T_IsMonoidMorphism_306
v2 -> T_IsAbelianGroupMorphism_1260 -> T_IsAbelianGroupMorphism_1260
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1260
v1
      T_IsRingMorphism_1676
_ -> T_IsAbelianGroupMorphism_1260
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsRingMorphism.*-mn-homo
d_'42''45'mn'45'homo_1686 ::
  T_IsRingMorphism_1676 -> T_IsMonoidMorphism_306
d_'42''45'mn'45'homo_1686 :: T_IsRingMorphism_1676 -> T_IsMonoidMorphism_306
d_'42''45'mn'45'homo_1686 T_IsRingMorphism_1676
v0
  = case T_IsRingMorphism_1676 -> T_IsRingMorphism_1676
forall a b. a -> b
coe T_IsRingMorphism_1676
v0 of
      C_IsRingMorphism'46'constructor_13939 T_IsAbelianGroupMorphism_1260
v1 T_IsMonoidMorphism_306
v2 -> T_IsMonoidMorphism_306 -> T_IsMonoidMorphism_306
forall a b. a -> b
coe T_IsMonoidMorphism_306
v2
      T_IsRingMorphism_1676
_ -> T_IsMonoidMorphism_306
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsRingMorphism-syntax
d_IsRingMorphism'45'syntax_1688 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3800 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsRingMorphism'45'syntax_1688 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsRingMorphism'45'syntax_1688 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3800
-> T_Ring_3800
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased