{-# 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.Setoid
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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8729'__58 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Semigroup_206
v4 ~T_Semigroup_206
v5 = T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 T_Semigroup_206
v4
du__'8729'__58 ::
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 :: T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 T_Semigroup_206
v0
  = (T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__224 (T_Semigroup_206 -> AgdaAny
forall a b. a -> b
coe T_Semigroup_206
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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__60 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> 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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> (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_206
-> T_Semigroup_206
-> (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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> (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_206
-> T_Semigroup_206
-> (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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  (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_206
-> T_Semigroup_206
-> (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_206
-> T_Semigroup_206
-> (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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 -> ()
d_Morphism_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> T_Level_18
d_Morphism_144 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> 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_206 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsSemigroupMorphism'45'syntax_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemigroupMorphism'45'syntax_160 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_206
-> T_Semigroup_206
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.semigroup
d_semigroup_216 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_semigroup_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> T_Semigroup_206
d_semigroup_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Monoid_506
v4 ~T_Monoid_506
v5 = T_Monoid_506 -> T_Semigroup_206
du_semigroup_216 T_Monoid_506
v4
du_semigroup_216 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_semigroup_216 :: T_Monoid_506 -> T_Semigroup_206
du_semigroup_216 T_Monoid_506
v0
  = (T_Monoid_506 -> T_Semigroup_206) -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe T_Monoid_506 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.du_semigroup_566 (T_Monoid_506 -> AgdaAny
forall a b. a -> b
coe T_Monoid_506
v0)
-- Algebra.Morphism._.F.ε
d_ε_224 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 -> AgdaAny
d_ε_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> AgdaAny
d_ε_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Monoid_506
v4 ~T_Monoid_506
v5 = T_Monoid_506 -> AgdaAny
du_ε_224 T_Monoid_506
v4
du_ε_224 :: MAlonzo.Code.Algebra.Bundles.T_Monoid_506 -> AgdaAny
du_ε_224 :: T_Monoid_506 -> AgdaAny
du_ε_224 T_Monoid_506
v0 = (T_Monoid_506 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_506 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_528 (T_Monoid_506 -> AgdaAny
forall a b. a -> b
coe T_Monoid_506
v0)
-- Algebra.Morphism._.T.semigroup
d_semigroup_270 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_semigroup_270 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> T_Semigroup_206
d_semigroup_270 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Monoid_506
v4 T_Monoid_506
v5 = T_Monoid_506 -> T_Semigroup_206
du_semigroup_270 T_Monoid_506
v5
du_semigroup_270 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_semigroup_270 :: T_Monoid_506 -> T_Semigroup_206
du_semigroup_270 T_Monoid_506
v0
  = (T_Monoid_506 -> T_Semigroup_206) -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe T_Monoid_506 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.du_semigroup_566 (T_Monoid_506 -> AgdaAny
forall a b. a -> b
coe T_Monoid_506
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_288 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_288 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_288 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_290 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_290 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_290 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_292 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_292 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_292 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_294 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 -> ()
d_Morphism_294 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> T_Level_18
d_Morphism_294 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsMonoidMorphism
d_IsMonoidMorphism_298 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsMonoidMorphism_298 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsMonoidMorphism_298
  = C_IsMonoidMorphism'46'constructor_2137 T_IsSemigroupMorphism_148
                                           AgdaAny
-- Algebra.Morphism._.IsMonoidMorphism.sm-homo
d_sm'45'homo_306 ::
  T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 :: T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 T_IsMonoidMorphism_298
v0
  = case T_IsMonoidMorphism_298 -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsMonoidMorphism_298
v0 of
      C_IsMonoidMorphism'46'constructor_2137 T_IsSemigroupMorphism_148
v1 AgdaAny
v2 -> T_IsSemigroupMorphism_148 -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsSemigroupMorphism_148
v1
      T_IsMonoidMorphism_298
_ -> T_IsSemigroupMorphism_148
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsMonoidMorphism.ε-homo
d_ε'45'homo_308 :: T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308 :: T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308 T_IsMonoidMorphism_298
v0
  = case T_IsMonoidMorphism_298 -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsMonoidMorphism_298
v0 of
      C_IsMonoidMorphism'46'constructor_2137 T_IsSemigroupMorphism_148
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_IsMonoidMorphism_298
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsMonoidMorphism._.∙-homo
d_'8729''45'homo_312 ::
  T_IsMonoidMorphism_298 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_312 :: T_IsMonoidMorphism_298 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_312 T_IsMonoidMorphism_298
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 (T_IsMonoidMorphism_298 -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298
v0))
-- Algebra.Morphism._.IsMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_314 ::
  T_IsMonoidMorphism_298 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_314 :: T_IsMonoidMorphism_298 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_314 T_IsMonoidMorphism_298
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 (T_IsMonoidMorphism_298 -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298
v0))
-- Algebra.Morphism._.IsMonoidMorphism-syntax
d_IsMonoidMorphism'45'syntax_316 ::
  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_506 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsMonoidMorphism'45'syntax_316 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsMonoidMorphism'45'syntax_316 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_506
-> T_Monoid_506
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.monoid
d_monoid_376 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_monoid_376 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> T_Monoid_506
d_monoid_376 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_CommutativeMonoid_582
v4 ~T_CommutativeMonoid_582
v5 = T_CommutativeMonoid_582 -> T_Monoid_506
du_monoid_376 T_CommutativeMonoid_582
v4
du_monoid_376 ::
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_monoid_376 :: T_CommutativeMonoid_582 -> T_Monoid_506
du_monoid_376 T_CommutativeMonoid_582
v0
  = (T_CommutativeMonoid_582 -> T_Monoid_506)
-> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe T_CommutativeMonoid_582 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_650 (T_CommutativeMonoid_582 -> AgdaAny
forall a b. a -> b
coe T_CommutativeMonoid_582
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_444 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_monoid_444 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> T_Monoid_506
d_monoid_444 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_CommutativeMonoid_582
v4 T_CommutativeMonoid_582
v5 = T_CommutativeMonoid_582 -> T_Monoid_506
du_monoid_444 T_CommutativeMonoid_582
v5
du_monoid_444 ::
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_monoid_444 :: T_CommutativeMonoid_582 -> T_Monoid_506
du_monoid_444 T_CommutativeMonoid_582
v0
  = (T_CommutativeMonoid_582 -> T_Monoid_506)
-> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe T_CommutativeMonoid_582 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_650 (T_CommutativeMonoid_582 -> AgdaAny
forall a b. a -> b
coe T_CommutativeMonoid_582
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_472 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_472 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_472 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_474 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_474 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_474 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_476 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_476 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_476 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_478 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 -> ()
d_Morphism_478 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> T_Level_18
d_Morphism_478 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsCommutativeMonoidMorphism
d_IsCommutativeMonoidMorphism_482 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeMonoidMorphism_482 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsCommutativeMonoidMorphism_482
  = C_IsCommutativeMonoidMorphism'46'constructor_3701 T_IsMonoidMorphism_298
-- Algebra.Morphism._.IsCommutativeMonoidMorphism.mn-homo
d_mn'45'homo_488 ::
  T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298
d_mn'45'homo_488 :: T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298
d_mn'45'homo_488 T_IsCommutativeMonoidMorphism_482
v0
  = case T_IsCommutativeMonoidMorphism_482
-> T_IsCommutativeMonoidMorphism_482
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482
v0 of
      C_IsCommutativeMonoidMorphism'46'constructor_3701 T_IsMonoidMorphism_298
v1 -> T_IsMonoidMorphism_298 -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsMonoidMorphism_298
v1
      T_IsCommutativeMonoidMorphism_482
_ -> T_IsMonoidMorphism_298
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.sm-homo
d_sm'45'homo_492 ::
  T_IsCommutativeMonoidMorphism_482 -> T_IsSemigroupMorphism_148
d_sm'45'homo_492 :: T_IsCommutativeMonoidMorphism_482 -> T_IsSemigroupMorphism_148
d_sm'45'homo_492 T_IsCommutativeMonoidMorphism_482
v0
  = (T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298
d_mn'45'homo_488 (T_IsCommutativeMonoidMorphism_482 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482
v0))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.ε-homo
d_ε'45'homo_494 :: T_IsCommutativeMonoidMorphism_482 -> AgdaAny
d_ε'45'homo_494 :: T_IsCommutativeMonoidMorphism_482 -> AgdaAny
d_ε'45'homo_494 T_IsCommutativeMonoidMorphism_482
v0
  = (T_IsMonoidMorphism_298 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308 ((T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298
d_mn'45'homo_488 (T_IsCommutativeMonoidMorphism_482 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482
v0))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.∙-homo
d_'8729''45'homo_496 ::
  T_IsCommutativeMonoidMorphism_482 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_496 :: T_IsCommutativeMonoidMorphism_482 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_496 T_IsCommutativeMonoidMorphism_482
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298
d_mn'45'homo_488 (T_IsCommutativeMonoidMorphism_482 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482
v0)))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_498 ::
  T_IsCommutativeMonoidMorphism_482 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_498 :: T_IsCommutativeMonoidMorphism_482
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_498 T_IsCommutativeMonoidMorphism_482
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482 -> T_IsMonoidMorphism_298
d_mn'45'homo_488 (T_IsCommutativeMonoidMorphism_482 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_482
v0)))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism-syntax
d_IsCommutativeMonoidMorphism'45'syntax_500 ::
  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_582 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsCommutativeMonoidMorphism'45'syntax_500 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsCommutativeMonoidMorphism'45'syntax_500 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_582
-> T_CommutativeMonoid_582
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.commutativeMonoid
d_commutativeMonoid_534 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
d_commutativeMonoid_534 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> T_CommutativeMonoid_582
d_commutativeMonoid_534 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IdempotentCommutativeMonoid_674
v4 ~T_IdempotentCommutativeMonoid_674
v5
  = T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
du_commutativeMonoid_534 T_IdempotentCommutativeMonoid_674
v4
du_commutativeMonoid_534 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
du_commutativeMonoid_534 :: T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
du_commutativeMonoid_534 T_IdempotentCommutativeMonoid_674
v0
  = (T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582)
-> AgdaAny -> T_CommutativeMonoid_582
forall a b. a -> b
coe
      T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_746 (T_IdempotentCommutativeMonoid_674 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_674
v0)
-- Algebra.Morphism._.F.monoid
d_monoid_566 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_monoid_566 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> T_Monoid_506
d_monoid_566 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IdempotentCommutativeMonoid_674
v4 ~T_IdempotentCommutativeMonoid_674
v5 = T_IdempotentCommutativeMonoid_674 -> T_Monoid_506
du_monoid_566 T_IdempotentCommutativeMonoid_674
v4
du_monoid_566 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_monoid_566 :: T_IdempotentCommutativeMonoid_674 -> T_Monoid_506
du_monoid_566 T_IdempotentCommutativeMonoid_674
v0
  = (T_CommutativeMonoid_582 -> T_Monoid_506)
-> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      T_CommutativeMonoid_582 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_650
      ((T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_746 (T_IdempotentCommutativeMonoid_674 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_674
v0))
-- Algebra.Morphism._.T.commutativeMonoid
d_commutativeMonoid_608 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
d_commutativeMonoid_608 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> T_CommutativeMonoid_582
d_commutativeMonoid_608 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_674
v4 T_IdempotentCommutativeMonoid_674
v5
  = T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
du_commutativeMonoid_608 T_IdempotentCommutativeMonoid_674
v5
du_commutativeMonoid_608 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
du_commutativeMonoid_608 :: T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
du_commutativeMonoid_608 T_IdempotentCommutativeMonoid_674
v0
  = (T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582)
-> AgdaAny -> T_CommutativeMonoid_582
forall a b. a -> b
coe
      T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_746 (T_IdempotentCommutativeMonoid_674 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_674
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_640 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_monoid_640 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> T_Monoid_506
d_monoid_640 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_674
v4 T_IdempotentCommutativeMonoid_674
v5 = T_IdempotentCommutativeMonoid_674 -> T_Monoid_506
du_monoid_640 T_IdempotentCommutativeMonoid_674
v5
du_monoid_640 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_monoid_640 :: T_IdempotentCommutativeMonoid_674 -> T_Monoid_506
du_monoid_640 T_IdempotentCommutativeMonoid_674
v0
  = (T_CommutativeMonoid_582 -> T_Monoid_506)
-> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      T_CommutativeMonoid_582 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_650
      ((T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IdempotentCommutativeMonoid_674 -> T_CommutativeMonoid_582
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_746 (T_IdempotentCommutativeMonoid_674 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_674
v0))
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_668 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_668 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_668 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_670 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_670 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_670 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_672 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_672 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_672 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_674 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  ()
d_Morphism_674 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> T_Level_18
d_Morphism_674 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism
d_IsIdempotentCommutativeMonoidMorphism_678 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsIdempotentCommutativeMonoidMorphism_678 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6
  = ()
newtype T_IsIdempotentCommutativeMonoidMorphism_678
  = C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5357 T_IsMonoidMorphism_298
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism.mn-homo
d_mn'45'homo_684 ::
  T_IsIdempotentCommutativeMonoidMorphism_678 ->
  T_IsMonoidMorphism_298
d_mn'45'homo_684 :: T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsMonoidMorphism_298
d_mn'45'homo_684 T_IsIdempotentCommutativeMonoidMorphism_678
v0
  = case T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsIdempotentCommutativeMonoidMorphism_678
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
v0 of
      C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5357 T_IsMonoidMorphism_298
v1
        -> T_IsMonoidMorphism_298 -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsMonoidMorphism_298
v1
      T_IsIdempotentCommutativeMonoidMorphism_678
_ -> T_IsMonoidMorphism_298
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.sm-homo
d_sm'45'homo_688 ::
  T_IsIdempotentCommutativeMonoidMorphism_678 ->
  T_IsSemigroupMorphism_148
d_sm'45'homo_688 :: T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsSemigroupMorphism_148
d_sm'45'homo_688 T_IsIdempotentCommutativeMonoidMorphism_678
v0
  = (T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsIdempotentCommutativeMonoidMorphism_678
 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsMonoidMorphism_298
d_mn'45'homo_684 (T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.ε-homo
d_ε'45'homo_690 ::
  T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
d_ε'45'homo_690 :: T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
d_ε'45'homo_690 T_IsIdempotentCommutativeMonoidMorphism_678
v0
  = (T_IsMonoidMorphism_298 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308 ((T_IsIdempotentCommutativeMonoidMorphism_678
 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsMonoidMorphism_298
d_mn'45'homo_684 (T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.∙-homo
d_'8729''45'homo_692 ::
  T_IsIdempotentCommutativeMonoidMorphism_678 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_692 :: T_IsIdempotentCommutativeMonoidMorphism_678
-> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_692 T_IsIdempotentCommutativeMonoidMorphism_678
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsIdempotentCommutativeMonoidMorphism_678
 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsMonoidMorphism_298
d_mn'45'homo_684 (T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
v0)))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_694 ::
  T_IsIdempotentCommutativeMonoidMorphism_678 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_694 :: T_IsIdempotentCommutativeMonoidMorphism_678
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_694 T_IsIdempotentCommutativeMonoidMorphism_678
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsIdempotentCommutativeMonoidMorphism_678
 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsMonoidMorphism_298
d_mn'45'homo_684 (T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
v0)))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism.isCommutativeMonoidMorphism
d_isCommutativeMonoidMorphism_696 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  (AgdaAny -> AgdaAny) ->
  T_IsIdempotentCommutativeMonoidMorphism_678 ->
  T_IsCommutativeMonoidMorphism_482
d_isCommutativeMonoidMorphism_696 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsCommutativeMonoidMorphism_482
d_isCommutativeMonoidMorphism_696 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_674
v4 ~T_IdempotentCommutativeMonoid_674
v5 ~AgdaAny -> AgdaAny
v6 T_IsIdempotentCommutativeMonoidMorphism_678
v7
  = T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsCommutativeMonoidMorphism_482
du_isCommutativeMonoidMorphism_696 T_IsIdempotentCommutativeMonoidMorphism_678
v7
du_isCommutativeMonoidMorphism_696 ::
  T_IsIdempotentCommutativeMonoidMorphism_678 ->
  T_IsCommutativeMonoidMorphism_482
du_isCommutativeMonoidMorphism_696 :: T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsCommutativeMonoidMorphism_482
du_isCommutativeMonoidMorphism_696 T_IsIdempotentCommutativeMonoidMorphism_678
v0
  = (T_IsMonoidMorphism_298 -> T_IsCommutativeMonoidMorphism_482)
-> AgdaAny -> T_IsCommutativeMonoidMorphism_482
forall a b. a -> b
coe
      T_IsMonoidMorphism_298 -> T_IsCommutativeMonoidMorphism_482
C_IsCommutativeMonoidMorphism'46'constructor_3701
      ((T_IsIdempotentCommutativeMonoidMorphism_678
 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
-> T_IsMonoidMorphism_298
d_mn'45'homo_684 (T_IsIdempotentCommutativeMonoidMorphism_678 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_678
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism-syntax
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_698 ::
  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_674 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_674 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_698 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_698 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_674
-> T_IdempotentCommutativeMonoid_674
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F._⁻¹
d__'8315''185'_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_Group_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 -> AgdaAny -> AgdaAny
d__'8315''185'_720 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> AgdaAny
-> AgdaAny
d__'8315''185'_720 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_890
v4 ~T_Group_890
v5 = T_Group_890 -> AgdaAny -> AgdaAny
du__'8315''185'_720 T_Group_890
v4
du__'8315''185'_720 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_890 -> AgdaAny -> AgdaAny
du__'8315''185'_720 :: T_Group_890 -> AgdaAny -> AgdaAny
du__'8315''185'_720 T_Group_890
v0
  = (T_Group_890 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v0)
-- Algebra.Morphism._.F.monoid
d_monoid_758 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_monoid_758 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> T_Monoid_506
d_monoid_758 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_890
v4 ~T_Group_890
v5 = T_Group_890 -> T_Monoid_506
du_monoid_758 T_Group_890
v4
du_monoid_758 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_monoid_758 :: T_Group_890 -> T_Monoid_506
du_monoid_758 T_Group_890
v0
  = (T_Group_890 -> T_Monoid_506) -> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe T_Group_890 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_972 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_834 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_monoid_834 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> T_Monoid_506
d_monoid_834 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Group_890
v4 T_Group_890
v5 = T_Group_890 -> T_Monoid_506
du_monoid_834 T_Group_890
v5
du_monoid_834 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_monoid_834 :: T_Group_890 -> T_Monoid_506
du_monoid_834 T_Group_890
v0
  = (T_Group_890 -> T_Monoid_506) -> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe T_Group_890 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_972 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_870 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_870 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_870 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_872 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_872 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_872 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_874 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_874 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_874 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_876 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 -> ()
d_Morphism_876 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> T_Level_18
d_Morphism_876 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsGroupMorphism
d_IsGroupMorphism_880 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsGroupMorphism_880 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsGroupMorphism_880
  = C_IsGroupMorphism'46'constructor_7461 T_IsMonoidMorphism_298
-- Algebra.Morphism._.IsGroupMorphism.mn-homo
d_mn'45'homo_886 :: T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 :: T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 T_IsGroupMorphism_880
v0
  = case T_IsGroupMorphism_880 -> T_IsGroupMorphism_880
forall a b. a -> b
coe T_IsGroupMorphism_880
v0 of
      C_IsGroupMorphism'46'constructor_7461 T_IsMonoidMorphism_298
v1 -> T_IsMonoidMorphism_298 -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsMonoidMorphism_298
v1
      T_IsGroupMorphism_880
_ -> T_IsMonoidMorphism_298
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsGroupMorphism._.sm-homo
d_sm'45'homo_890 ::
  T_IsGroupMorphism_880 -> T_IsSemigroupMorphism_148
d_sm'45'homo_890 :: T_IsGroupMorphism_880 -> T_IsSemigroupMorphism_148
d_sm'45'homo_890 T_IsGroupMorphism_880
v0
  = (T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
v0))
-- Algebra.Morphism._.IsGroupMorphism._.ε-homo
d_ε'45'homo_892 :: T_IsGroupMorphism_880 -> AgdaAny
d_ε'45'homo_892 :: T_IsGroupMorphism_880 -> AgdaAny
d_ε'45'homo_892 T_IsGroupMorphism_880
v0
  = (T_IsMonoidMorphism_298 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
v0))
-- Algebra.Morphism._.IsGroupMorphism._.∙-homo
d_'8729''45'homo_894 ::
  T_IsGroupMorphism_880 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_894 :: T_IsGroupMorphism_880 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_894 T_IsGroupMorphism_880
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
v0)))
-- Algebra.Morphism._.IsGroupMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_896 ::
  T_IsGroupMorphism_880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_896 :: T_IsGroupMorphism_880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_896 T_IsGroupMorphism_880
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
v0)))
-- Algebra.Morphism._.IsGroupMorphism.⁻¹-homo
d_'8315''185''45'homo_898 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_880 -> AgdaAny -> AgdaAny
d_'8315''185''45'homo_898 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_880
-> AgdaAny
-> AgdaAny
d_'8315''185''45'homo_898 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_890
v4 T_Group_890
v5 AgdaAny -> AgdaAny
v6 T_IsGroupMorphism_880
v7 AgdaAny
v8
  = T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_880
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_898 T_Group_890
v4 T_Group_890
v5 AgdaAny -> AgdaAny
v6 T_IsGroupMorphism_880
v7 AgdaAny
v8
du_'8315''185''45'homo_898 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_880 -> AgdaAny -> AgdaAny
du_'8315''185''45'homo_898 :: T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_880
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_898 T_Group_890
v0 T_Group_890
v1 AgdaAny -> AgdaAny
v2 T_IsGroupMorphism_880
v3 AgdaAny
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> T_IsGroup_580
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsGroup_580
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsGroup_580
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.du_unique'737''45''8315''185'_648
      (T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__912 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
      (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
      (T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
      (T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny
v2 ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
v0 AgdaAny
v4))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4)
      (T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            (let v5 :: T_IsGroup_580
v5 = T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v6 :: T_IsMonoid_358
v6
                      = T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> T_IsGroup_580
forall a b. a -> b
coe T_IsGroup_580
v5) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v7 :: T_IsSemigroup_194
v7
                         = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v6) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                        ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v7))))))
            ((T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__912 T_Group_890
v1
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2 ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
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_890 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__912 T_Group_890
v0
                  ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
v0 AgdaAny
v4) AgdaAny
v4))
            (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               (let v5 :: T_IsGroup_580
v5 = T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v6 :: T_IsMonoid_358
v6
                         = T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> T_IsGroup_580
forall a b. a -> b
coe T_IsGroup_580
v5) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (let v7 :: T_IsSemigroup_194
v7
                            = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v6) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                           ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v7))))))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  ((T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__912 T_Group_890
v0
                     ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
v0 AgdaAny
v4) AgdaAny
v4))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v0)))
               (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
               ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                  (let v5 :: T_IsGroup_580
v5 = T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (let v6 :: T_IsMonoid_358
v6
                            = T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> T_IsGroup_580
forall a b. a -> b
coe T_IsGroup_580
v5) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (let v7 :: T_IsSemigroup_194
v7
                               = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368 (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v6) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                              ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v7))))))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v0)))
                  (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
                  (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1))
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                     ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                        ((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_580
v5 = T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v1) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (let v6 :: T_IsMonoid_358
v6
                                     = T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594 (T_IsGroup_580 -> T_IsGroup_580
forall a b. a -> b
coe T_IsGroup_580
v5) in
                               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 (let v7 :: T_IsSemigroup_194
v7
                                        = T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
                                            (T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v6) in
                                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                                       ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                          T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                                          (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v7))))))))
                     ((T_Group_890 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v1)))
                  (T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
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_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
v3)))
                  ((T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Group_890 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__912 T_Group_890
v0
                     ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
v0 AgdaAny
v4) AgdaAny
v4)
                  (T_Group_890 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_914 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
v0))
                  ((T_IsGroup_580 -> AgdaAny -> AgdaAny)
-> T_IsGroup_580 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsGroup_580 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_inverse'737'_640
                     (T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> T_Group_890
forall a b. a -> b
coe T_Group_890
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_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                     T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                     ((T_IsMonoid_358 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMonoid_358 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_368
                        ((T_IsGroup_580 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsGroup_580 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.d_isMonoid_594
                           ((T_Group_890 -> T_IsGroup_580) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> T_IsGroup_580
MAlonzo.Code.Algebra.Bundles.d_isGroup_918 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v1))))))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  (let v5 :: b
v5
                         = let v5 :: t
v5
                                 = (T_Group_890 -> T_Monoid_506) -> AgdaAny -> t
forall a b. a -> b
coe T_Group_890 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_972 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v0) in
                           AgdaAny -> b
forall a b. a -> b
coe ((T_Monoid_506 -> T_Semigroup_206) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_506 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.du_semigroup_566 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__224 AgdaAny
forall a. a
v5
                        ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
v0 AgdaAny
v4) AgdaAny
v4)))
               ((T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Semigroup_206 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__224
                  (let v5 :: t
v5
                         = (T_Group_890 -> T_Monoid_506) -> AgdaAny -> t
forall a b. a -> b
coe T_Group_890 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_monoid_972 (T_Group_890 -> AgdaAny
forall a b. a -> b
coe T_Group_890
v1) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_Monoid_506 -> T_Semigroup_206) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_506 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.du_semigroup_566 (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_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
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_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306 ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 (T_IsGroupMorphism_880 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880
v3)))
                  ((T_Group_890 -> AgdaAny -> AgdaAny)
-> T_Group_890 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_890 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_916 T_Group_890
v0 AgdaAny
v4) AgdaAny
v4))))
-- Algebra.Morphism._.IsGroupMorphism-syntax
d_IsGroupMorphism'45'syntax_926 ::
  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_890 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsGroupMorphism'45'syntax_926 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsGroupMorphism'45'syntax_926 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.group
d_group_968 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890
d_group_968 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> T_Group_890
d_group_968 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_AbelianGroup_990
v4 ~T_AbelianGroup_990
v5 = T_AbelianGroup_990 -> T_Group_890
du_group_968 T_AbelianGroup_990
v4
du_group_968 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890
du_group_968 :: T_AbelianGroup_990 -> T_Group_890
du_group_968 T_AbelianGroup_990
v0
  = (T_AbelianGroup_990 -> T_Group_890) -> AgdaAny -> T_Group_890
forall a b. a -> b
coe T_AbelianGroup_990 -> T_Group_890
MAlonzo.Code.Algebra.Bundles.du_group_1080 (T_AbelianGroup_990 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_990
v0)
-- Algebra.Morphism._.T.group
d_group_1062 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890
d_group_1062 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> T_Group_890
d_group_1062 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_AbelianGroup_990
v4 T_AbelianGroup_990
v5 = T_AbelianGroup_990 -> T_Group_890
du_group_1062 T_AbelianGroup_990
v5
du_group_1062 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_890
du_group_1062 :: T_AbelianGroup_990 -> T_Group_890
du_group_1062 T_AbelianGroup_990
v0
  = (T_AbelianGroup_990 -> T_Group_890) -> AgdaAny -> T_Group_890
forall a b. a -> b
coe T_AbelianGroup_990 -> T_Group_890
MAlonzo.Code.Algebra.Bundles.du_group_1080 (T_AbelianGroup_990 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_990
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_1134 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_1134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_1134 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_1136 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_1136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_1136 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_1138 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_1138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_1138 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_1140 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 -> ()
d_Morphism_1140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> T_Level_18
d_Morphism_1140 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsAbelianGroupMorphism
d_IsAbelianGroupMorphism_1144 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsAbelianGroupMorphism_1144 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsAbelianGroupMorphism_1144
  = C_IsAbelianGroupMorphism'46'constructor_11199 T_IsGroupMorphism_880
-- Algebra.Morphism._.IsAbelianGroupMorphism.gp-homo
d_gp'45'homo_1150 ::
  T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 :: T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 T_IsAbelianGroupMorphism_1144
v0
  = case T_IsAbelianGroupMorphism_1144 -> T_IsAbelianGroupMorphism_1144
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v0 of
      C_IsAbelianGroupMorphism'46'constructor_11199 T_IsGroupMorphism_880
v1 -> T_IsGroupMorphism_880 -> T_IsGroupMorphism_880
forall a b. a -> b
coe T_IsGroupMorphism_880
v1
      T_IsAbelianGroupMorphism_1144
_ -> T_IsGroupMorphism_880
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsAbelianGroupMorphism._.mn-homo
d_mn'45'homo_1154 ::
  T_IsAbelianGroupMorphism_1144 -> T_IsMonoidMorphism_298
d_mn'45'homo_1154 :: T_IsAbelianGroupMorphism_1144 -> T_IsMonoidMorphism_298
d_mn'45'homo_1154 T_IsAbelianGroupMorphism_1144
v0
  = (T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 ((T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 (T_IsAbelianGroupMorphism_1144 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v0))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.sm-homo
d_sm'45'homo_1156 ::
  T_IsAbelianGroupMorphism_1144 -> T_IsSemigroupMorphism_148
d_sm'45'homo_1156 :: T_IsAbelianGroupMorphism_1144 -> T_IsSemigroupMorphism_148
d_sm'45'homo_1156 T_IsAbelianGroupMorphism_1144
v0
  = (T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe
      T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306
      ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 ((T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 (T_IsAbelianGroupMorphism_1144 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v0)))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.ε-homo
d_ε'45'homo_1158 :: T_IsAbelianGroupMorphism_1144 -> AgdaAny
d_ε'45'homo_1158 :: T_IsAbelianGroupMorphism_1144 -> AgdaAny
d_ε'45'homo_1158 T_IsAbelianGroupMorphism_1144
v0
  = (T_IsMonoidMorphism_298 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsMonoidMorphism_298 -> AgdaAny
d_ε'45'homo_308
      ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 ((T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 (T_IsAbelianGroupMorphism_1144 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v0)))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.⁻¹-homo
d_'8315''185''45'homo_1160 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  (AgdaAny -> AgdaAny) ->
  T_IsAbelianGroupMorphism_1144 -> AgdaAny -> AgdaAny
d_'8315''185''45'homo_1160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1144
-> AgdaAny
-> AgdaAny
d_'8315''185''45'homo_1160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_AbelianGroup_990
v4 T_AbelianGroup_990
v5 AgdaAny -> AgdaAny
v6 T_IsAbelianGroupMorphism_1144
v7
  = T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1144
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_1160 T_AbelianGroup_990
v4 T_AbelianGroup_990
v5 AgdaAny -> AgdaAny
v6 T_IsAbelianGroupMorphism_1144
v7
du_'8315''185''45'homo_1160 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  (AgdaAny -> AgdaAny) ->
  T_IsAbelianGroupMorphism_1144 -> AgdaAny -> AgdaAny
du_'8315''185''45'homo_1160 :: T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1144
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_1160 T_AbelianGroup_990
v0 T_AbelianGroup_990
v1 AgdaAny -> AgdaAny
v2 T_IsAbelianGroupMorphism_1144
v3
  = (T_Group_890
 -> T_Group_890
 -> (AgdaAny -> AgdaAny)
 -> T_IsGroupMorphism_880
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Group_890
-> T_Group_890
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_880
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_898
      ((T_AbelianGroup_990 -> T_Group_890) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_990 -> T_Group_890
MAlonzo.Code.Algebra.Bundles.du_group_1080 (T_AbelianGroup_990 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_990
v0))
      ((T_AbelianGroup_990 -> T_Group_890) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_990 -> T_Group_890
MAlonzo.Code.Algebra.Bundles.du_group_1080 (T_AbelianGroup_990 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_990
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      ((T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 (T_IsAbelianGroupMorphism_1144 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v3))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.∙-homo
d_'8729''45'homo_1162 ::
  T_IsAbelianGroupMorphism_1144 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_1162 :: T_IsAbelianGroupMorphism_1144 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_1162 T_IsAbelianGroupMorphism_1144
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306
         ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 ((T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 (T_IsAbelianGroupMorphism_1144 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v0))))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_1164 ::
  T_IsAbelianGroupMorphism_1144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_1164 :: T_IsAbelianGroupMorphism_1144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_1164 T_IsAbelianGroupMorphism_1144
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_298 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMonoidMorphism_298 -> T_IsSemigroupMorphism_148
d_sm'45'homo_306
         ((T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_880 -> T_IsMonoidMorphism_298
d_mn'45'homo_886 ((T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144 -> T_IsGroupMorphism_880
d_gp'45'homo_1150 (T_IsAbelianGroupMorphism_1144 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v0))))
-- Algebra.Morphism._.IsAbelianGroupMorphism-syntax
d_IsAbelianGroupMorphism'45'syntax_1166 ::
  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_990 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsAbelianGroupMorphism'45'syntax_1166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsAbelianGroupMorphism'45'syntax_1166 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_990
-> T_AbelianGroup_990
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.*-monoid
d_'42''45'monoid_1218 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'42''45'monoid_1218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> T_Monoid_506
d_'42''45'monoid_1218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Ring_2514
v4 ~T_Ring_2514
v5
  = T_Ring_2514 -> T_Monoid_506
du_'42''45'monoid_1218 T_Ring_2514
v4
du_'42''45'monoid_1218 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'42''45'monoid_1218 :: T_Ring_2514 -> T_Monoid_506
du_'42''45'monoid_1218 T_Ring_2514
v0
  = let v1 :: t
v1
          = (T_Ring_2514 -> T_Semiring_1932) -> AgdaAny -> t
forall a b. a -> b
coe T_Ring_2514 -> T_Semiring_1932
MAlonzo.Code.Algebra.Bundles.du_semiring_2656 (T_Ring_2514 -> AgdaAny
forall a b. a -> b
coe T_Ring_2514
v0) in
    AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      ((T_SemiringWithoutAnnihilatingZero_1786 -> T_Monoid_506)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SemiringWithoutAnnihilatingZero_1786 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_'42''45'monoid_1916
         ((T_Semiring_1932 -> T_SemiringWithoutAnnihilatingZero_1786)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semiring_1932 -> T_SemiringWithoutAnnihilatingZero_1786
MAlonzo.Code.Algebra.Bundles.du_semiringWithoutAnnihilatingZero_2048
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Morphism._.F.+-abelianGroup
d_'43''45'abelianGroup_1226 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990
d_'43''45'abelianGroup_1226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> T_AbelianGroup_990
d_'43''45'abelianGroup_1226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Ring_2514
v4 ~T_Ring_2514
v5
  = T_Ring_2514 -> T_AbelianGroup_990
du_'43''45'abelianGroup_1226 T_Ring_2514
v4
du_'43''45'abelianGroup_1226 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990
du_'43''45'abelianGroup_1226 :: T_Ring_2514 -> T_AbelianGroup_990
du_'43''45'abelianGroup_1226 T_Ring_2514
v0
  = (T_Ring_2514 -> T_AbelianGroup_990)
-> AgdaAny -> T_AbelianGroup_990
forall a b. a -> b
coe
      T_Ring_2514 -> T_AbelianGroup_990
MAlonzo.Code.Algebra.Bundles.du_'43''45'abelianGroup_2654 (T_Ring_2514 -> AgdaAny
forall a b. a -> b
coe T_Ring_2514
v0)
-- Algebra.Morphism._.T.*-monoid
d_'42''45'monoid_1378 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'42''45'monoid_1378 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> T_Monoid_506
d_'42''45'monoid_1378 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Ring_2514
v4 T_Ring_2514
v5
  = T_Ring_2514 -> T_Monoid_506
du_'42''45'monoid_1378 T_Ring_2514
v5
du_'42''45'monoid_1378 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'42''45'monoid_1378 :: T_Ring_2514 -> T_Monoid_506
du_'42''45'monoid_1378 T_Ring_2514
v0
  = let v1 :: t
v1
          = (T_Ring_2514 -> T_Semiring_1932) -> AgdaAny -> t
forall a b. a -> b
coe T_Ring_2514 -> T_Semiring_1932
MAlonzo.Code.Algebra.Bundles.du_semiring_2656 (T_Ring_2514 -> AgdaAny
forall a b. a -> b
coe T_Ring_2514
v0) in
    AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      ((T_SemiringWithoutAnnihilatingZero_1786 -> T_Monoid_506)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SemiringWithoutAnnihilatingZero_1786 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.du_'42''45'monoid_1916
         ((T_Semiring_1932 -> T_SemiringWithoutAnnihilatingZero_1786)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semiring_1932 -> T_SemiringWithoutAnnihilatingZero_1786
MAlonzo.Code.Algebra.Bundles.du_semiringWithoutAnnihilatingZero_2048
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Morphism._.T.+-abelianGroup
d_'43''45'abelianGroup_1386 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990
d_'43''45'abelianGroup_1386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> T_AbelianGroup_990
d_'43''45'abelianGroup_1386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Ring_2514
v4 T_Ring_2514
v5
  = T_Ring_2514 -> T_AbelianGroup_990
du_'43''45'abelianGroup_1386 T_Ring_2514
v5
du_'43''45'abelianGroup_1386 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_990
du_'43''45'abelianGroup_1386 :: T_Ring_2514 -> T_AbelianGroup_990
du_'43''45'abelianGroup_1386 T_Ring_2514
v0
  = (T_Ring_2514 -> T_AbelianGroup_990)
-> AgdaAny -> T_AbelianGroup_990
forall a b. a -> b
coe
      T_Ring_2514 -> T_AbelianGroup_990
MAlonzo.Code.Algebra.Bundles.du_'43''45'abelianGroup_2654 (T_Ring_2514 -> AgdaAny
forall a b. a -> b
coe T_Ring_2514
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_1506 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_1506 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_1506 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_1508 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_1508 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_1508 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_1510 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_1510 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_1510 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_1512 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 -> ()
d_Morphism_1512 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> T_Level_18
d_Morphism_1512 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsRingMorphism
d_IsRingMorphism_1516 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRingMorphism_1516 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsRingMorphism_1516
  = C_IsRingMorphism'46'constructor_13379 T_IsAbelianGroupMorphism_1144
                                          T_IsMonoidMorphism_298
-- Algebra.Morphism._.IsRingMorphism.+-abgp-homo
d_'43''45'abgp'45'homo_1524 ::
  T_IsRingMorphism_1516 -> T_IsAbelianGroupMorphism_1144
d_'43''45'abgp'45'homo_1524 :: T_IsRingMorphism_1516 -> T_IsAbelianGroupMorphism_1144
d_'43''45'abgp'45'homo_1524 T_IsRingMorphism_1516
v0
  = case T_IsRingMorphism_1516 -> T_IsRingMorphism_1516
forall a b. a -> b
coe T_IsRingMorphism_1516
v0 of
      C_IsRingMorphism'46'constructor_13379 T_IsAbelianGroupMorphism_1144
v1 T_IsMonoidMorphism_298
v2 -> T_IsAbelianGroupMorphism_1144 -> T_IsAbelianGroupMorphism_1144
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1144
v1
      T_IsRingMorphism_1516
_ -> T_IsAbelianGroupMorphism_1144
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsRingMorphism.*-mn-homo
d_'42''45'mn'45'homo_1526 ::
  T_IsRingMorphism_1516 -> T_IsMonoidMorphism_298
d_'42''45'mn'45'homo_1526 :: T_IsRingMorphism_1516 -> T_IsMonoidMorphism_298
d_'42''45'mn'45'homo_1526 T_IsRingMorphism_1516
v0
  = case T_IsRingMorphism_1516 -> T_IsRingMorphism_1516
forall a b. a -> b
coe T_IsRingMorphism_1516
v0 of
      C_IsRingMorphism'46'constructor_13379 T_IsAbelianGroupMorphism_1144
v1 T_IsMonoidMorphism_298
v2 -> T_IsMonoidMorphism_298 -> T_IsMonoidMorphism_298
forall a b. a -> b
coe T_IsMonoidMorphism_298
v2
      T_IsRingMorphism_1516
_ -> T_IsMonoidMorphism_298
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsRingMorphism-syntax
d_IsRingMorphism'45'syntax_1528 ::
  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_2514 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_2514 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsRingMorphism'45'syntax_1528 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsRingMorphism'45'syntax_1528 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_2514
-> T_Ring_2514
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased