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

-- Algebra.Morphism.Definitions._.Homomorphic₀
d_Homomorphic'8320'_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_32 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism.Definitions._.Homomorphic₁
d_Homomorphic'8321'_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_34 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_34 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism.Definitions._.Homomorphic₂
d_Homomorphic'8322'_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_36 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism.Definitions._.Morphism
d_Morphism_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Morphism_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
d_Morphism_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F._∙_
d__'8729'__58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8729'__58 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Semigroup_558
v4 ~T_Semigroup_558
v5 = T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 T_Semigroup_558
v4
du__'8729'__58 ::
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 :: T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8729'__58 T_Semigroup_558
v0
  = (T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__576 (T_Semigroup_558 -> AgdaAny
forall a b. a -> b
coe T_Semigroup_558
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_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__60 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> 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_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> (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_558
-> T_Semigroup_558
-> (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_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> (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_558
-> T_Semigroup_558
-> (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_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  (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_558
-> T_Semigroup_558
-> (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_558
-> T_Semigroup_558
-> (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_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 -> ()
d_Morphism_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> T_Level_18
d_Morphism_144 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> 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_constructor_160 (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_constructor_160 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_constructor_160 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_162 ::
  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_558 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsSemigroupMorphism'45'syntax_162 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemigroupMorphism'45'syntax_162 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Semigroup_558
-> T_Semigroup_558
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.semigroup
d_semigroup_220 ::
  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_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_semigroup_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> T_Semigroup_558
d_semigroup_220 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Monoid_914
v4 ~T_Monoid_914
v5 = T_Monoid_914 -> T_Semigroup_558
du_semigroup_220 T_Monoid_914
v4
du_semigroup_220 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_semigroup_220 :: T_Monoid_914 -> T_Semigroup_558
du_semigroup_220 T_Monoid_914
v0
  = (T_Monoid_914 -> T_Semigroup_558) -> AgdaAny -> T_Semigroup_558
forall a b. a -> b
coe T_Monoid_914 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.du_semigroup_976 (T_Monoid_914 -> AgdaAny
forall a b. a -> b
coe T_Monoid_914
v0)
-- Algebra.Morphism._.F.ε
d_ε_230 ::
  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_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 -> AgdaAny
d_ε_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> AgdaAny
d_ε_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Monoid_914
v4 ~T_Monoid_914
v5 = T_Monoid_914 -> AgdaAny
du_ε_230 T_Monoid_914
v4
du_ε_230 :: MAlonzo.Code.Algebra.Bundles.T_Monoid_914 -> AgdaAny
du_ε_230 :: T_Monoid_914 -> AgdaAny
du_ε_230 T_Monoid_914
v0 = (T_Monoid_914 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_914 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_936 (T_Monoid_914 -> AgdaAny
forall a b. a -> b
coe T_Monoid_914
v0)
-- Algebra.Morphism._.T.semigroup
d_semigroup_278 ::
  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_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_semigroup_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> T_Semigroup_558
d_semigroup_278 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Monoid_914
v4 T_Monoid_914
v5 = T_Monoid_914 -> T_Semigroup_558
du_semigroup_278 T_Monoid_914
v5
du_semigroup_278 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_semigroup_278 :: T_Monoid_914 -> T_Semigroup_558
du_semigroup_278 T_Monoid_914
v0
  = (T_Monoid_914 -> T_Semigroup_558) -> AgdaAny -> T_Semigroup_558
forall a b. a -> b
coe T_Monoid_914 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.du_semigroup_976 (T_Monoid_914 -> AgdaAny
forall a b. a -> b
coe T_Monoid_914
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_298 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_300 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_300 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_300 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_302 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_304 ::
  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_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 -> ()
d_Morphism_304 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> T_Level_18
d_Morphism_304 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsMonoidMorphism
d_IsMonoidMorphism_308 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsMonoidMorphism_308 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsMonoidMorphism_308
  = C_constructor_326 T_IsSemigroupMorphism_148 AgdaAny
-- Algebra.Morphism._.IsMonoidMorphism.sm-homo
d_sm'45'homo_316 ::
  T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 :: T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 T_IsMonoidMorphism_308
v0
  = case T_IsMonoidMorphism_308 -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsMonoidMorphism_308
v0 of
      C_constructor_326 T_IsSemigroupMorphism_148
v1 AgdaAny
v2 -> T_IsSemigroupMorphism_148 -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsSemigroupMorphism_148
v1
      T_IsMonoidMorphism_308
_ -> T_IsSemigroupMorphism_148
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsMonoidMorphism.ε-homo
d_ε'45'homo_318 :: T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318 :: T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318 T_IsMonoidMorphism_308
v0
  = case T_IsMonoidMorphism_308 -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsMonoidMorphism_308
v0 of
      C_constructor_326 T_IsSemigroupMorphism_148
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_IsMonoidMorphism_308
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsMonoidMorphism._.∙-homo
d_'8729''45'homo_322 ::
  T_IsMonoidMorphism_308 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_322 :: T_IsMonoidMorphism_308 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_322 T_IsMonoidMorphism_308
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 (T_IsMonoidMorphism_308 -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308
v0))
-- Algebra.Morphism._.IsMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_324 ::
  T_IsMonoidMorphism_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_324 :: T_IsMonoidMorphism_308 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_324 T_IsMonoidMorphism_308
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 (T_IsMonoidMorphism_308 -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308
v0))
-- Algebra.Morphism._.IsMonoidMorphism-syntax
d_IsMonoidMorphism'45'syntax_328 ::
  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_914 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsMonoidMorphism'45'syntax_328 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsMonoidMorphism'45'syntax_328 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Monoid_914
-> T_Monoid_914
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.monoid
d_monoid_390 ::
  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_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_monoid_390 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> T_Monoid_914
d_monoid_390 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_CommutativeMonoid_996
v4 ~T_CommutativeMonoid_996
v5 = T_CommutativeMonoid_996 -> T_Monoid_914
du_monoid_390 T_CommutativeMonoid_996
v4
du_monoid_390 ::
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_monoid_390 :: T_CommutativeMonoid_996 -> T_Monoid_914
du_monoid_390 T_CommutativeMonoid_996
v0
  = (T_CommutativeMonoid_996 -> T_Monoid_914)
-> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe T_CommutativeMonoid_996 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1066 (T_CommutativeMonoid_996 -> AgdaAny
forall a b. a -> b
coe T_CommutativeMonoid_996
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_462 ::
  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_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_monoid_462 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> T_Monoid_914
d_monoid_462 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_CommutativeMonoid_996
v4 T_CommutativeMonoid_996
v5 = T_CommutativeMonoid_996 -> T_Monoid_914
du_monoid_462 T_CommutativeMonoid_996
v5
du_monoid_462 ::
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_monoid_462 :: T_CommutativeMonoid_996 -> T_Monoid_914
du_monoid_462 T_CommutativeMonoid_996
v0
  = (T_CommutativeMonoid_996 -> T_Monoid_914)
-> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe T_CommutativeMonoid_996 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1066 (T_CommutativeMonoid_996 -> AgdaAny
forall a b. a -> b
coe T_CommutativeMonoid_996
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_492 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_492 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_492 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_494 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_494 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_494 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_496 ::
  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_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_496 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_496 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_498 ::
  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_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 -> ()
d_Morphism_498 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> T_Level_18
d_Morphism_498 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsCommutativeMonoidMorphism
d_IsCommutativeMonoidMorphism_502 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCommutativeMonoidMorphism_502 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsCommutativeMonoidMorphism_502
  = C_constructor_520 T_IsMonoidMorphism_308
-- Algebra.Morphism._.IsCommutativeMonoidMorphism.mn-homo
d_mn'45'homo_508 ::
  T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308
d_mn'45'homo_508 :: T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308
d_mn'45'homo_508 T_IsCommutativeMonoidMorphism_502
v0
  = case T_IsCommutativeMonoidMorphism_502
-> T_IsCommutativeMonoidMorphism_502
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502
v0 of
      C_constructor_520 T_IsMonoidMorphism_308
v1 -> T_IsMonoidMorphism_308 -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsMonoidMorphism_308
v1
      T_IsCommutativeMonoidMorphism_502
_ -> T_IsMonoidMorphism_308
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.sm-homo
d_sm'45'homo_512 ::
  T_IsCommutativeMonoidMorphism_502 -> T_IsSemigroupMorphism_148
d_sm'45'homo_512 :: T_IsCommutativeMonoidMorphism_502 -> T_IsSemigroupMorphism_148
d_sm'45'homo_512 T_IsCommutativeMonoidMorphism_502
v0
  = (T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308
d_mn'45'homo_508 (T_IsCommutativeMonoidMorphism_502 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502
v0))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.ε-homo
d_ε'45'homo_514 :: T_IsCommutativeMonoidMorphism_502 -> AgdaAny
d_ε'45'homo_514 :: T_IsCommutativeMonoidMorphism_502 -> AgdaAny
d_ε'45'homo_514 T_IsCommutativeMonoidMorphism_502
v0
  = (T_IsMonoidMorphism_308 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318 ((T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308
d_mn'45'homo_508 (T_IsCommutativeMonoidMorphism_502 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502
v0))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.∙-homo
d_'8729''45'homo_516 ::
  T_IsCommutativeMonoidMorphism_502 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_516 :: T_IsCommutativeMonoidMorphism_502 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_516 T_IsCommutativeMonoidMorphism_502
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308
d_mn'45'homo_508 (T_IsCommutativeMonoidMorphism_502 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502
v0)))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_518 ::
  T_IsCommutativeMonoidMorphism_502 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_518 :: T_IsCommutativeMonoidMorphism_502
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_518 T_IsCommutativeMonoidMorphism_502
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502 -> T_IsMonoidMorphism_308
d_mn'45'homo_508 (T_IsCommutativeMonoidMorphism_502 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeMonoidMorphism_502
v0)))
-- Algebra.Morphism._.IsCommutativeMonoidMorphism-syntax
d_IsCommutativeMonoidMorphism'45'syntax_522 ::
  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_996 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsCommutativeMonoidMorphism'45'syntax_522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsCommutativeMonoidMorphism'45'syntax_522 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_CommutativeMonoid_996
-> T_CommutativeMonoid_996
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.commutativeMonoid
d_commutativeMonoid_560 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
d_commutativeMonoid_560 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> T_CommutativeMonoid_996
d_commutativeMonoid_560 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IdempotentCommutativeMonoid_1186
v4 ~T_IdempotentCommutativeMonoid_1186
v5
  = T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
du_commutativeMonoid_560 T_IdempotentCommutativeMonoid_1186
v4
du_commutativeMonoid_560 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
du_commutativeMonoid_560 :: T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
du_commutativeMonoid_560 T_IdempotentCommutativeMonoid_1186
v0
  = (T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996)
-> AgdaAny -> T_CommutativeMonoid_996
forall a b. a -> b
coe
      T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1266 (T_IdempotentCommutativeMonoid_1186 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1186
v0)
-- Algebra.Morphism._.F.monoid
d_monoid_602 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_monoid_602 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> T_Monoid_914
d_monoid_602 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IdempotentCommutativeMonoid_1186
v4 ~T_IdempotentCommutativeMonoid_1186
v5 = T_IdempotentCommutativeMonoid_1186 -> T_Monoid_914
du_monoid_602 T_IdempotentCommutativeMonoid_1186
v4
du_monoid_602 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_monoid_602 :: T_IdempotentCommutativeMonoid_1186 -> T_Monoid_914
du_monoid_602 T_IdempotentCommutativeMonoid_1186
v0
  = (T_CommutativeMonoid_996 -> T_Monoid_914)
-> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      T_CommutativeMonoid_996 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1066
      ((T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1266 (T_IdempotentCommutativeMonoid_1186 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1186
v0))
-- Algebra.Morphism._.T.commutativeMonoid
d_commutativeMonoid_650 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
d_commutativeMonoid_650 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> T_CommutativeMonoid_996
d_commutativeMonoid_650 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_1186
v4 T_IdempotentCommutativeMonoid_1186
v5
  = T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
du_commutativeMonoid_650 T_IdempotentCommutativeMonoid_1186
v5
du_commutativeMonoid_650 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
du_commutativeMonoid_650 :: T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
du_commutativeMonoid_650 T_IdempotentCommutativeMonoid_1186
v0
  = (T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996)
-> AgdaAny -> T_CommutativeMonoid_996
forall a b. a -> b
coe
      T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1266 (T_IdempotentCommutativeMonoid_1186 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1186
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_692 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_monoid_692 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> T_Monoid_914
d_monoid_692 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_1186
v4 T_IdempotentCommutativeMonoid_1186
v5 = T_IdempotentCommutativeMonoid_1186 -> T_Monoid_914
du_monoid_692 T_IdempotentCommutativeMonoid_1186
v5
du_monoid_692 ::
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_monoid_692 :: T_IdempotentCommutativeMonoid_1186 -> T_Monoid_914
du_monoid_692 T_IdempotentCommutativeMonoid_1186
v0
  = (T_CommutativeMonoid_996 -> T_Monoid_914)
-> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      T_CommutativeMonoid_996 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1066
      ((T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IdempotentCommutativeMonoid_1186 -> T_CommutativeMonoid_996
MAlonzo.Code.Algebra.Bundles.du_commutativeMonoid_1266 (T_IdempotentCommutativeMonoid_1186 -> AgdaAny
forall a b. a -> b
coe T_IdempotentCommutativeMonoid_1186
v0))
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_722 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_722 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_722 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_724 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_724 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_724 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_726 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_726 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_726 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_728 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  ()
d_Morphism_728 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> T_Level_18
d_Morphism_728 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism
d_IsIdempotentCommutativeMonoidMorphism_732 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsIdempotentCommutativeMonoidMorphism_732 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6
  = ()
newtype T_IsIdempotentCommutativeMonoidMorphism_732
  = C_constructor_752 T_IsMonoidMorphism_308
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism.mn-homo
d_mn'45'homo_738 ::
  T_IsIdempotentCommutativeMonoidMorphism_732 ->
  T_IsMonoidMorphism_308
d_mn'45'homo_738 :: T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsMonoidMorphism_308
d_mn'45'homo_738 T_IsIdempotentCommutativeMonoidMorphism_732
v0
  = case T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsIdempotentCommutativeMonoidMorphism_732
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
v0 of
      C_constructor_752 T_IsMonoidMorphism_308
v1 -> T_IsMonoidMorphism_308 -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsMonoidMorphism_308
v1
      T_IsIdempotentCommutativeMonoidMorphism_732
_ -> T_IsMonoidMorphism_308
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.sm-homo
d_sm'45'homo_742 ::
  T_IsIdempotentCommutativeMonoidMorphism_732 ->
  T_IsSemigroupMorphism_148
d_sm'45'homo_742 :: T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsSemigroupMorphism_148
d_sm'45'homo_742 T_IsIdempotentCommutativeMonoidMorphism_732
v0
  = (T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsIdempotentCommutativeMonoidMorphism_732
 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsMonoidMorphism_308
d_mn'45'homo_738 (T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.ε-homo
d_ε'45'homo_744 ::
  T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
d_ε'45'homo_744 :: T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
d_ε'45'homo_744 T_IsIdempotentCommutativeMonoidMorphism_732
v0
  = (T_IsMonoidMorphism_308 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318 ((T_IsIdempotentCommutativeMonoidMorphism_732
 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsMonoidMorphism_308
d_mn'45'homo_738 (T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.∙-homo
d_'8729''45'homo_746 ::
  T_IsIdempotentCommutativeMonoidMorphism_732 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_746 :: T_IsIdempotentCommutativeMonoidMorphism_732
-> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_746 T_IsIdempotentCommutativeMonoidMorphism_732
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsIdempotentCommutativeMonoidMorphism_732
 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsMonoidMorphism_308
d_mn'45'homo_738 (T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
v0)))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_748 ::
  T_IsIdempotentCommutativeMonoidMorphism_732 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_748 :: T_IsIdempotentCommutativeMonoidMorphism_732
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_748 T_IsIdempotentCommutativeMonoidMorphism_732
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsIdempotentCommutativeMonoidMorphism_732
 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsMonoidMorphism_308
d_mn'45'homo_738 (T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
v0)))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism.isCommutativeMonoidMorphism
d_isCommutativeMonoidMorphism_750 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  (AgdaAny -> AgdaAny) ->
  T_IsIdempotentCommutativeMonoidMorphism_732 ->
  T_IsCommutativeMonoidMorphism_502
d_isCommutativeMonoidMorphism_750 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsCommutativeMonoidMorphism_502
d_isCommutativeMonoidMorphism_750 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_IdempotentCommutativeMonoid_1186
v4 ~T_IdempotentCommutativeMonoid_1186
v5 ~AgdaAny -> AgdaAny
v6 T_IsIdempotentCommutativeMonoidMorphism_732
v7
  = T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsCommutativeMonoidMorphism_502
du_isCommutativeMonoidMorphism_750 T_IsIdempotentCommutativeMonoidMorphism_732
v7
du_isCommutativeMonoidMorphism_750 ::
  T_IsIdempotentCommutativeMonoidMorphism_732 ->
  T_IsCommutativeMonoidMorphism_502
du_isCommutativeMonoidMorphism_750 :: T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsCommutativeMonoidMorphism_502
du_isCommutativeMonoidMorphism_750 T_IsIdempotentCommutativeMonoidMorphism_732
v0
  = (T_IsMonoidMorphism_308 -> T_IsCommutativeMonoidMorphism_502)
-> AgdaAny -> T_IsCommutativeMonoidMorphism_502
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsCommutativeMonoidMorphism_502
C_constructor_520 ((T_IsIdempotentCommutativeMonoidMorphism_732
 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
-> T_IsMonoidMorphism_308
d_mn'45'homo_738 (T_IsIdempotentCommutativeMonoidMorphism_732 -> AgdaAny
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoidMorphism_732
v0))
-- Algebra.Morphism._.IsIdempotentCommutativeMonoidMorphism-syntax
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_754 ::
  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_1186 ->
  MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1186 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_754 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsIdempotentCommutativeMonoidMorphism'45'syntax_754 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IdempotentCommutativeMonoid_1186
-> T_IdempotentCommutativeMonoid_1186
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F._⁻¹
d__'8315''185'_780 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 -> AgdaAny -> AgdaAny
d__'8315''185'_780 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> AgdaAny
-> AgdaAny
d__'8315''185'_780 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_1564
v4 ~T_Group_1564
v5 = T_Group_1564 -> AgdaAny -> AgdaAny
du__'8315''185'_780 T_Group_1564
v4
du__'8315''185'_780 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 -> AgdaAny -> AgdaAny
du__'8315''185'_780 :: T_Group_1564 -> AgdaAny -> AgdaAny
du__'8315''185'_780 T_Group_1564
v0
  = (T_Group_1564 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v0)
-- Algebra.Morphism._.F.monoid
d_monoid_828 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_monoid_828 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> T_Monoid_914
d_monoid_828 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_1564
v4 ~T_Group_1564
v5 = T_Group_1564 -> T_Monoid_914
du_monoid_828 T_Group_1564
v4
du_monoid_828 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_monoid_828 :: T_Group_1564 -> T_Monoid_914
du_monoid_828 T_Group_1564
v0
  = (T_Group_1564 -> T_Monoid_914) -> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe T_Group_1564 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1656 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v0)
-- Algebra.Morphism._.T.monoid
d_monoid_920 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_monoid_920 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> T_Monoid_914
d_monoid_920 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Group_1564
v4 T_Group_1564
v5 = T_Group_1564 -> T_Monoid_914
du_monoid_920 T_Group_1564
v5
du_monoid_920 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_monoid_920 :: T_Group_1564 -> T_Monoid_914
du_monoid_920 T_Group_1564
v0
  = (T_Group_1564 -> T_Monoid_914) -> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe T_Group_1564 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1656 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_958 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_958 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_958 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_960 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_960 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_960 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_962 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_962 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_962 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_964 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 -> ()
d_Morphism_964 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> T_Level_18
d_Morphism_964 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsGroupMorphism
d_IsGroupMorphism_968 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsGroupMorphism_968 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsGroupMorphism_968
  = C_constructor_1030 T_IsMonoidMorphism_308
-- Algebra.Morphism._.IsGroupMorphism.mn-homo
d_mn'45'homo_974 :: T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 :: T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 T_IsGroupMorphism_968
v0
  = case T_IsGroupMorphism_968 -> T_IsGroupMorphism_968
forall a b. a -> b
coe T_IsGroupMorphism_968
v0 of
      C_constructor_1030 T_IsMonoidMorphism_308
v1 -> T_IsMonoidMorphism_308 -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsMonoidMorphism_308
v1
      T_IsGroupMorphism_968
_ -> T_IsMonoidMorphism_308
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsGroupMorphism._.sm-homo
d_sm'45'homo_978 ::
  T_IsGroupMorphism_968 -> T_IsSemigroupMorphism_148
d_sm'45'homo_978 :: T_IsGroupMorphism_968 -> T_IsSemigroupMorphism_148
d_sm'45'homo_978 T_IsGroupMorphism_968
v0
  = (T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
v0))
-- Algebra.Morphism._.IsGroupMorphism._.ε-homo
d_ε'45'homo_980 :: T_IsGroupMorphism_968 -> AgdaAny
d_ε'45'homo_980 :: T_IsGroupMorphism_968 -> AgdaAny
d_ε'45'homo_980 T_IsGroupMorphism_968
v0
  = (T_IsMonoidMorphism_308 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
v0))
-- Algebra.Morphism._.IsGroupMorphism._.∙-homo
d_'8729''45'homo_982 ::
  T_IsGroupMorphism_968 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_982 :: T_IsGroupMorphism_968 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_982 T_IsGroupMorphism_968
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
v0)))
-- Algebra.Morphism._.IsGroupMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_984 ::
  T_IsGroupMorphism_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_984 :: T_IsGroupMorphism_968 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_984 T_IsGroupMorphism_968
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
v0)))
-- Algebra.Morphism._.IsGroupMorphism.⁻¹-homo
d_'8315''185''45'homo_986 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_968 -> AgdaAny -> AgdaAny
d_'8315''185''45'homo_986 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_968
-> AgdaAny
-> AgdaAny
d_'8315''185''45'homo_986 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Group_1564
v4 T_Group_1564
v5 AgdaAny -> AgdaAny
v6 T_IsGroupMorphism_968
v7 AgdaAny
v8
  = T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_968
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_986 T_Group_1564
v4 T_Group_1564
v5 AgdaAny -> AgdaAny
v6 T_IsGroupMorphism_968
v7 AgdaAny
v8
du_'8315''185''45'homo_986 ::
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_968 -> AgdaAny -> AgdaAny
du_'8315''185''45'homo_986 :: T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_968
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_986 T_Group_1564
v0 T_Group_1564
v1 AgdaAny -> AgdaAny
v2 T_IsGroupMorphism_968
v3 AgdaAny
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> T_IsGroup_1074
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsGroup_1074
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsGroup_1074
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.du_unique'737''45''8315''185'_1152
      (T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1586 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
      (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
      (T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
      (T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny
v2 ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
         (\ AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 ->
            (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v7)
         ((T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1586 T_Group_1564
v1
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> AgdaAny
v2 ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4))
         (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                        ((T_IsMonoid_712 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMonoid_712 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_722
                           ((T_IsGroup_1074 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsGroup_1074 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.d_isMonoid_1088
                              ((T_Group_1564 -> T_IsGroup_1074) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1))))))))
            ((T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1586 T_Group_1564
v1
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2 ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
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_1564 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1586 T_Group_1564
v0
                  ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4) AgdaAny
v4))
            (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                        ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                           ((T_IsMonoid_712 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsMonoid_712 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_722
                              ((T_IsGroup_1074 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsGroup_1074 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.d_isMonoid_1088
                                 ((T_Group_1564 -> T_IsGroup_1074) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1))))))))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  ((T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1586 T_Group_1564
v0
                     ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4) AgdaAny
v4))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v0)))
               (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                     ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                        ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                           ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                              ((T_IsMonoid_712 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsMonoid_712 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_722
                                 ((T_IsGroup_1074 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_IsGroup_1074 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.d_isMonoid_1088
                                    ((T_Group_1564 -> T_IsGroup_1074) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1))))))))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v0)))
                  (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
                  (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v1))
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                     (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                        ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                           ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                              ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                                 ((T_IsMonoid_712 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_IsMonoid_712 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_722
                                    ((T_IsGroup_1074 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       T_IsGroup_1074 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.d_isMonoid_1088
                                       ((T_Group_1564 -> T_IsGroup_1074) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                          T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592
                                          (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1))))))))
                     ((T_Group_1564 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1)))
                  (T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
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_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
v3)))
                  ((T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Group_1564 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__1586 T_Group_1564
v0
                     ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4) AgdaAny
v4)
                  (T_Group_1564 -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d_ε_1588 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v0))
                  ((T_IsGroup_1074 -> AgdaAny -> AgdaAny)
-> T_IsGroup_1074 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsGroup_1074 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_inverse'737'_1144
                     (T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592 (T_Group_1564 -> T_Group_1564
forall a b. a -> b
coe T_Group_1564
v0)) AgdaAny
v4)))
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
               (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsMonoid_712 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMonoid_712 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_722
                        ((T_IsGroup_1074 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsGroup_1074 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.d_isMonoid_1088
                           ((T_Group_1564 -> T_IsGroup_1074) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> T_IsGroup_1074
MAlonzo.Code.Algebra.Bundles.d_isGroup_1592 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1))))))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  (let v5 :: AgdaAny
v5
                         = let v5 :: AgdaAny
v5
                                 = (T_Group_1564 -> T_Monoid_914) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1656 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v0) in
                           AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_Monoid_914 -> T_Semigroup_558) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_914 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.du_semigroup_976 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__576 AgdaAny
v5
                        ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4) AgdaAny
v4)))
               ((T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Semigroup_558 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8729'__576
                  (let v5 :: AgdaAny
v5
                         = (T_Group_1564 -> T_Monoid_914) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_monoid_1656 (T_Group_1564 -> AgdaAny
forall a b. a -> b
coe T_Group_1564
v1) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_Monoid_914 -> T_Semigroup_558) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monoid_914 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.du_semigroup_976 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     AgdaAny -> AgdaAny
v2 ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
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_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316 ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 (T_IsGroupMorphism_968 -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968
v3)))
                  ((T_Group_1564 -> AgdaAny -> AgdaAny)
-> T_Group_1564 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Group_1564 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8315''185'_1590 T_Group_1564
v0 AgdaAny
v4) AgdaAny
v4))))
-- Algebra.Morphism._.IsGroupMorphism-syntax
d_IsGroupMorphism'45'syntax_1032 ::
  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_1564 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsGroupMorphism'45'syntax_1032 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsGroupMorphism'45'syntax_1032 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.group
d_group_1074 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564
d_group_1074 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> T_Group_1564
d_group_1074 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_AbelianGroup_1682
v4 ~T_AbelianGroup_1682
v5 = T_AbelianGroup_1682 -> T_Group_1564
du_group_1074 T_AbelianGroup_1682
v4
du_group_1074 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564
du_group_1074 :: T_AbelianGroup_1682 -> T_Group_1564
du_group_1074 T_AbelianGroup_1682
v0
  = (T_AbelianGroup_1682 -> T_Group_1564) -> AgdaAny -> T_Group_1564
forall a b. a -> b
coe T_AbelianGroup_1682 -> T_Group_1564
MAlonzo.Code.Algebra.Bundles.du_group_1778 (T_AbelianGroup_1682 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1682
v0)
-- Algebra.Morphism._.T.group
d_group_1178 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564
d_group_1178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> T_Group_1564
d_group_1178 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_AbelianGroup_1682
v4 T_AbelianGroup_1682
v5 = T_AbelianGroup_1682 -> T_Group_1564
du_group_1178 T_AbelianGroup_1682
v5
du_group_1178 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_Group_1564
du_group_1178 :: T_AbelianGroup_1682 -> T_Group_1564
du_group_1178 T_AbelianGroup_1682
v0
  = (T_AbelianGroup_1682 -> T_Group_1564) -> AgdaAny -> T_Group_1564
forall a b. a -> b
coe T_AbelianGroup_1682 -> T_Group_1564
MAlonzo.Code.Algebra.Bundles.du_group_1778 (T_AbelianGroup_1682 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1682
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_1260 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_1260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_1260 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_1262 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_1262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_1262 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_1264 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_1264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_1264 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_1266 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 -> ()
d_Morphism_1266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> T_Level_18
d_Morphism_1266 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsAbelianGroupMorphism
d_IsAbelianGroupMorphism_1270 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsAbelianGroupMorphism_1270 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_IsAbelianGroupMorphism_1270
  = C_constructor_1292 T_IsGroupMorphism_968
-- Algebra.Morphism._.IsAbelianGroupMorphism.gp-homo
d_gp'45'homo_1276 ::
  T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 :: T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 T_IsAbelianGroupMorphism_1270
v0
  = case T_IsAbelianGroupMorphism_1270 -> T_IsAbelianGroupMorphism_1270
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v0 of
      C_constructor_1292 T_IsGroupMorphism_968
v1 -> T_IsGroupMorphism_968 -> T_IsGroupMorphism_968
forall a b. a -> b
coe T_IsGroupMorphism_968
v1
      T_IsAbelianGroupMorphism_1270
_ -> T_IsGroupMorphism_968
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsAbelianGroupMorphism._.mn-homo
d_mn'45'homo_1280 ::
  T_IsAbelianGroupMorphism_1270 -> T_IsMonoidMorphism_308
d_mn'45'homo_1280 :: T_IsAbelianGroupMorphism_1270 -> T_IsMonoidMorphism_308
d_mn'45'homo_1280 T_IsAbelianGroupMorphism_1270
v0
  = (T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 ((T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 (T_IsAbelianGroupMorphism_1270 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v0))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.sm-homo
d_sm'45'homo_1282 ::
  T_IsAbelianGroupMorphism_1270 -> T_IsSemigroupMorphism_148
d_sm'45'homo_1282 :: T_IsAbelianGroupMorphism_1270 -> T_IsSemigroupMorphism_148
d_sm'45'homo_1282 T_IsAbelianGroupMorphism_1270
v0
  = (T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> T_IsSemigroupMorphism_148
forall a b. a -> b
coe
      T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316
      ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 ((T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 (T_IsAbelianGroupMorphism_1270 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v0)))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.ε-homo
d_ε'45'homo_1284 :: T_IsAbelianGroupMorphism_1270 -> AgdaAny
d_ε'45'homo_1284 :: T_IsAbelianGroupMorphism_1270 -> AgdaAny
d_ε'45'homo_1284 T_IsAbelianGroupMorphism_1270
v0
  = (T_IsMonoidMorphism_308 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsMonoidMorphism_308 -> AgdaAny
d_ε'45'homo_318
      ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 ((T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 (T_IsAbelianGroupMorphism_1270 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v0)))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.⁻¹-homo
d_'8315''185''45'homo_1286 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  (AgdaAny -> AgdaAny) ->
  T_IsAbelianGroupMorphism_1270 -> AgdaAny -> AgdaAny
d_'8315''185''45'homo_1286 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1270
-> AgdaAny
-> AgdaAny
d_'8315''185''45'homo_1286 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_AbelianGroup_1682
v4 T_AbelianGroup_1682
v5 AgdaAny -> AgdaAny
v6 T_IsAbelianGroupMorphism_1270
v7
  = T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1270
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_1286 T_AbelianGroup_1682
v4 T_AbelianGroup_1682
v5 AgdaAny -> AgdaAny
v6 T_IsAbelianGroupMorphism_1270
v7
du_'8315''185''45'homo_1286 ::
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  (AgdaAny -> AgdaAny) ->
  T_IsAbelianGroupMorphism_1270 -> AgdaAny -> AgdaAny
du_'8315''185''45'homo_1286 :: T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> T_IsAbelianGroupMorphism_1270
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_1286 T_AbelianGroup_1682
v0 T_AbelianGroup_1682
v1 AgdaAny -> AgdaAny
v2 T_IsAbelianGroupMorphism_1270
v3
  = (T_Group_1564
 -> T_Group_1564
 -> (AgdaAny -> AgdaAny)
 -> T_IsGroupMorphism_968
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Group_1564
-> T_Group_1564
-> (AgdaAny -> AgdaAny)
-> T_IsGroupMorphism_968
-> AgdaAny
-> AgdaAny
du_'8315''185''45'homo_986
      ((T_AbelianGroup_1682 -> T_Group_1564) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1682 -> T_Group_1564
MAlonzo.Code.Algebra.Bundles.du_group_1778 (T_AbelianGroup_1682 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1682
v0))
      ((T_AbelianGroup_1682 -> T_Group_1564) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1682 -> T_Group_1564
MAlonzo.Code.Algebra.Bundles.du_group_1778 (T_AbelianGroup_1682 -> AgdaAny
forall a b. a -> b
coe T_AbelianGroup_1682
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      ((T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 (T_IsAbelianGroupMorphism_1270 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v3))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.∙-homo
d_'8729''45'homo_1288 ::
  T_IsAbelianGroupMorphism_1270 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_1288 :: T_IsAbelianGroupMorphism_1270 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'homo_1288 T_IsAbelianGroupMorphism_1270
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316
         ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 ((T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 (T_IsAbelianGroupMorphism_1270 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v0))))
-- Algebra.Morphism._.IsAbelianGroupMorphism._.⟦⟧-cong
d_'10214''10215''45'cong_1290 ::
  T_IsAbelianGroupMorphism_1270 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_1290 :: T_IsAbelianGroupMorphism_1270
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'10214''10215''45'cong_1290 T_IsAbelianGroupMorphism_1270
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_308 -> T_IsSemigroupMorphism_148)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMonoidMorphism_308 -> T_IsSemigroupMorphism_148
d_sm'45'homo_316
         ((T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsGroupMorphism_968 -> T_IsMonoidMorphism_308
d_mn'45'homo_974 ((T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270 -> T_IsGroupMorphism_968
d_gp'45'homo_1276 (T_IsAbelianGroupMorphism_1270 -> AgdaAny
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v0))))
-- Algebra.Morphism._.IsAbelianGroupMorphism-syntax
d_IsAbelianGroupMorphism'45'syntax_1294 ::
  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_1682 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsAbelianGroupMorphism'45'syntax_1294 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsAbelianGroupMorphism'45'syntax_1294 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_AbelianGroup_1682
-> T_AbelianGroup_1682
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.F.*-monoid
d_'42''45'monoid_1346 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'42''45'monoid_1346 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> T_Monoid_914
d_'42''45'monoid_1346 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Ring_3908
v4 ~T_Ring_3908
v5
  = T_Ring_3908 -> T_Monoid_914
du_'42''45'monoid_1346 T_Ring_3908
v4
du_'42''45'monoid_1346 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'42''45'monoid_1346 :: T_Ring_3908 -> T_Monoid_914
du_'42''45'monoid_1346 T_Ring_3908
v0
  = let v1 :: AgdaAny
v1
          = (T_Ring_3908 -> T_Semiring_2356) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ring_3908 -> T_Semiring_2356
MAlonzo.Code.Algebra.Bundles.du_semiring_4060 (T_Ring_3908 -> AgdaAny
forall a b. a -> b
coe T_Ring_3908
v0) in
    AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      ((T_SemiringWithoutAnnihilatingZero_2204 -> T_Monoid_914)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SemiringWithoutAnnihilatingZero_2204 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_'42''45'monoid_2338
         ((T_Semiring_2356 -> T_SemiringWithoutAnnihilatingZero_2204)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semiring_2356 -> T_SemiringWithoutAnnihilatingZero_2204
MAlonzo.Code.Algebra.Bundles.du_semiringWithoutAnnihilatingZero_2474
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
-- Algebra.Morphism._.F.+-abelianGroup
d_'43''45'abelianGroup_1354 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682
d_'43''45'abelianGroup_1354 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> T_AbelianGroup_1682
d_'43''45'abelianGroup_1354 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Ring_3908
v4 ~T_Ring_3908
v5
  = T_Ring_3908 -> T_AbelianGroup_1682
du_'43''45'abelianGroup_1354 T_Ring_3908
v4
du_'43''45'abelianGroup_1354 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682
du_'43''45'abelianGroup_1354 :: T_Ring_3908 -> T_AbelianGroup_1682
du_'43''45'abelianGroup_1354 T_Ring_3908
v0
  = (T_Ring_3908 -> T_AbelianGroup_1682)
-> AgdaAny -> T_AbelianGroup_1682
forall a b. a -> b
coe
      T_Ring_3908 -> T_AbelianGroup_1682
MAlonzo.Code.Algebra.Bundles.du_'43''45'abelianGroup_4056 (T_Ring_3908 -> AgdaAny
forall a b. a -> b
coe T_Ring_3908
v0)
-- Algebra.Morphism._.T.*-monoid
d_'42''45'monoid_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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'42''45'monoid_1528 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> T_Monoid_914
d_'42''45'monoid_1528 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Ring_3908
v4 T_Ring_3908
v5
  = T_Ring_3908 -> T_Monoid_914
du_'42''45'monoid_1528 T_Ring_3908
v5
du_'42''45'monoid_1528 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'42''45'monoid_1528 :: T_Ring_3908 -> T_Monoid_914
du_'42''45'monoid_1528 T_Ring_3908
v0
  = let v1 :: AgdaAny
v1
          = (T_Ring_3908 -> T_Semiring_2356) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ring_3908 -> T_Semiring_2356
MAlonzo.Code.Algebra.Bundles.du_semiring_4060 (T_Ring_3908 -> AgdaAny
forall a b. a -> b
coe T_Ring_3908
v0) in
    AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      ((T_SemiringWithoutAnnihilatingZero_2204 -> T_Monoid_914)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SemiringWithoutAnnihilatingZero_2204 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.du_'42''45'monoid_2338
         ((T_Semiring_2356 -> T_SemiringWithoutAnnihilatingZero_2204)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semiring_2356 -> T_SemiringWithoutAnnihilatingZero_2204
MAlonzo.Code.Algebra.Bundles.du_semiringWithoutAnnihilatingZero_2474
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
-- Algebra.Morphism._.T.+-abelianGroup
d_'43''45'abelianGroup_1536 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682
d_'43''45'abelianGroup_1536 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> T_AbelianGroup_1682
d_'43''45'abelianGroup_1536 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Ring_3908
v4 T_Ring_3908
v5
  = T_Ring_3908 -> T_AbelianGroup_1682
du_'43''45'abelianGroup_1536 T_Ring_3908
v5
du_'43''45'abelianGroup_1536 ::
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1682
du_'43''45'abelianGroup_1536 :: T_Ring_3908 -> T_AbelianGroup_1682
du_'43''45'abelianGroup_1536 T_Ring_3908
v0
  = (T_Ring_3908 -> T_AbelianGroup_1682)
-> AgdaAny -> T_AbelianGroup_1682
forall a b. a -> b
coe
      T_Ring_3908 -> T_AbelianGroup_1682
MAlonzo.Code.Algebra.Bundles.du_'43''45'abelianGroup_4056 (T_Ring_3908 -> AgdaAny
forall a b. a -> b
coe T_Ring_3908
v0)
-- Algebra.Morphism._._.Homomorphic₀
d_Homomorphic'8320'_1678 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d_Homomorphic'8320'_1678 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_Homomorphic'8320'_1678 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₁
d_Homomorphic'8321'_1680 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8321'_1680 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8321'_1680 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Homomorphic₂
d_Homomorphic'8322'_1682 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_1682 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Homomorphic'8322'_1682 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._._.Morphism
d_Morphism_1684 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 -> ()
d_Morphism_1684 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> T_Level_18
d_Morphism_1684 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> T_Level_18
forall a. a
erased
-- Algebra.Morphism._.IsRingMorphism
d_IsRingMorphism_1688 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRingMorphism_1688 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_IsRingMorphism_1688
  = C_constructor_1700 T_IsAbelianGroupMorphism_1270
                       T_IsMonoidMorphism_308
-- Algebra.Morphism._.IsRingMorphism.+-abgp-homo
d_'43''45'abgp'45'homo_1696 ::
  T_IsRingMorphism_1688 -> T_IsAbelianGroupMorphism_1270
d_'43''45'abgp'45'homo_1696 :: T_IsRingMorphism_1688 -> T_IsAbelianGroupMorphism_1270
d_'43''45'abgp'45'homo_1696 T_IsRingMorphism_1688
v0
  = case T_IsRingMorphism_1688 -> T_IsRingMorphism_1688
forall a b. a -> b
coe T_IsRingMorphism_1688
v0 of
      C_constructor_1700 T_IsAbelianGroupMorphism_1270
v1 T_IsMonoidMorphism_308
v2 -> T_IsAbelianGroupMorphism_1270 -> T_IsAbelianGroupMorphism_1270
forall a b. a -> b
coe T_IsAbelianGroupMorphism_1270
v1
      T_IsRingMorphism_1688
_ -> T_IsAbelianGroupMorphism_1270
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsRingMorphism.*-mn-homo
d_'42''45'mn'45'homo_1698 ::
  T_IsRingMorphism_1688 -> T_IsMonoidMorphism_308
d_'42''45'mn'45'homo_1698 :: T_IsRingMorphism_1688 -> T_IsMonoidMorphism_308
d_'42''45'mn'45'homo_1698 T_IsRingMorphism_1688
v0
  = case T_IsRingMorphism_1688 -> T_IsRingMorphism_1688
forall a b. a -> b
coe T_IsRingMorphism_1688
v0 of
      C_constructor_1700 T_IsAbelianGroupMorphism_1270
v1 T_IsMonoidMorphism_308
v2 -> T_IsMonoidMorphism_308 -> T_IsMonoidMorphism_308
forall a b. a -> b
coe T_IsMonoidMorphism_308
v2
      T_IsRingMorphism_1688
_ -> T_IsMonoidMorphism_308
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Morphism._.IsRingMorphism-syntax
d_IsRingMorphism'45'syntax_1702 ::
  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_3908 ->
  MAlonzo.Code.Algebra.Bundles.T_Ring_3908 ->
  (AgdaAny -> AgdaAny) -> ()
d_IsRingMorphism'45'syntax_1702 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> T_Level_18
d_IsRingMorphism'45'syntax_1702 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Ring_3908
-> T_Ring_3908
-> (AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased