{-# 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.Data.Sum.Function.Setoid where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles

-- Data.Sum.Function.Setoid.inj₁ₛ
d_inj'8321''8347'_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_inj'8321''8347'_52 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Func_714
d_inj'8321''8347'_52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5
  = T_Func_714
du_inj'8321''8347'_52
du_inj'8321''8347'_52 :: MAlonzo.Code.Function.Bundles.T_Func_714
du_inj'8321''8347'_52 :: T_Func_714
du_inj'8321''8347'_52
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714)
-> Any -> (Any -> Any -> Any -> Any) -> T_Func_714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      ((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
      (\ Any
v0 Any
v1 Any
v2 ->
         (Any -> T_Pointwise_70) -> Any -> Any
forall a b. a -> b
coe
           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v2)
-- Data.Sum.Function.Setoid.inj₂ₛ
d_inj'8322''8347'_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_inj'8322''8347'_54 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Func_714
d_inj'8322''8347'_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5
  = T_Func_714
du_inj'8322''8347'_54
du_inj'8322''8347'_54 :: MAlonzo.Code.Function.Bundles.T_Func_714
du_inj'8322''8347'_54 :: T_Func_714
du_inj'8322''8347'_54
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714)
-> Any -> (Any -> Any -> Any -> Any) -> T_Func_714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      ((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
      (\ Any
v0 Any
v1 Any
v2 ->
         (Any -> T_Pointwise_70) -> Any -> Any
forall a b. a -> b
coe
           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v2)
-- Data.Sum.Function.Setoid.[_,_]ₛ
d_'91'_'44'_'93''8347'_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_'91'_'44'_'93''8347'_56 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Func_714
-> T_Func_714
-> T_Func_714
d_'91'_'44'_'93''8347'_56 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 T_Func_714
v9
                          T_Func_714
v10
  = T_Func_714 -> T_Func_714 -> T_Func_714
du_'91'_'44'_'93''8347'_56 T_Func_714
v9 T_Func_714
v10
du_'91'_'44'_'93''8347'_56 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_'91'_'44'_'93''8347'_56 :: T_Func_714 -> T_Func_714 -> T_Func_714
du_'91'_'44'_'93''8347'_56 T_Func_714
v0 T_Func_714
v1
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714)
-> Any -> Any -> T_Func_714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
         ((T_Func_714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v0))
         ((T_Func_714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v1)))
      ((T_Func_714
 -> T_Func_714
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Func_714
-> T_Func_714
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> Any
du_'46'extendedlambda0_66 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v0) (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v1))
-- Data.Sum.Function.Setoid._..extendedlambda0
d_'46'extendedlambda0_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  AgdaAny
d_'46'extendedlambda0_66 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Func_714
-> T_Func_714
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> Any
d_'46'extendedlambda0_66 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 T_Func_714
v9 T_Func_714
v10
                         T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_70
v13
  = T_Func_714
-> T_Func_714
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> Any
du_'46'extendedlambda0_66 T_Func_714
v9 T_Func_714
v10 T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_70
v13
du_'46'extendedlambda0_66 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  AgdaAny
du_'46'extendedlambda0_66 :: T_Func_714
-> T_Func_714
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> Any
du_'46'extendedlambda0_66 T_Func_714
v0 T_Func_714
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
      MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v7
        -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v9
                      -> (T_Func_714 -> Any -> Any -> Any -> Any)
-> T_Func_714 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_722 T_Func_714
v0 Any
v8 Any
v9 Any
v7
                    T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v7
        -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v9
                      -> (T_Func_714 -> Any -> Any -> Any -> Any)
-> T_Func_714 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_722 T_Func_714
v1 Any
v8 Any
v9 Any
v7
                    T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_70
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid.swapₛ
d_swap'8347'_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_swap'8347'_72 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Func_714
d_swap'8347'_72 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 = T_Func_714
du_swap'8347'_72
du_swap'8347'_72 :: MAlonzo.Code.Function.Bundles.T_Func_714
du_swap'8347'_72 :: T_Func_714
du_swap'8347'_72
  = (T_Func_714 -> T_Func_714 -> T_Func_714)
-> Any -> Any -> T_Func_714
forall a b. a -> b
coe
      T_Func_714 -> T_Func_714 -> T_Func_714
du_'91'_'44'_'93''8347'_56 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
du_inj'8322''8347'_54)
      (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
du_inj'8321''8347'_52)
-- Data.Sum.Function.Setoid.⊎-injective
d_'8846''45'injective_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'8846''45'injective_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'injective_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~Any -> Any -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~Any -> Any -> T_Level_18
v7 ~T_Level_18
v8 ~T_Level_18
v9
                         ~T_Level_18
v10 ~Any -> Any -> T_Level_18
v11 ~T_Level_18
v12 ~T_Level_18
v13 ~T_Level_18
v14 ~Any -> Any -> T_Level_18
v15 ~Any -> Any
v16 ~Any -> Any
v17 Any -> Any -> Any -> Any
v18 Any -> Any -> Any -> Any
v19 T__'8846'__30
v20 T__'8846'__30
v21 T_Pointwise_70
v22
  = (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'injective_78 Any -> Any -> Any -> Any
v18 Any -> Any -> Any -> Any
v19 T__'8846'__30
v20 T__'8846'__30
v21 T_Pointwise_70
v22
du_'8846''45'injective_78 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'8846''45'injective_78 :: (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'injective_78 Any -> Any -> Any -> Any
v0 Any -> Any -> Any -> Any
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
        -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v6
               -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
                    MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88
                           ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v0 Any
v5 Any
v6 Any
v9)
                    T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
        -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v6
               -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
                    MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94
                           ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v1 Any
v5 Any
v6 Any
v9)
                    T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid.⊎-strictlySurjective
d_'8846''45'strictlySurjective_104 ::
  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.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8846''45'strictlySurjective_104 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T_Σ_14)
-> (Any -> T_Σ_14)
-> T__'8846'__30
-> T_Σ_14
d_'8846''45'strictlySurjective_104 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7
                                   ~T_Level_18
v8 ~Any -> Any -> T_Level_18
v9 ~T_Level_18
v10 ~Any -> Any -> T_Level_18
v11 ~Any -> Any
v12 ~Any -> Any
v13 Any -> T_Σ_14
v14 Any -> T_Σ_14
v15
  = (Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14
du_'8846''45'strictlySurjective_104 Any -> T_Σ_14
v14 Any -> T_Σ_14
v15
du_'8846''45'strictlySurjective_104 ::
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8846''45'strictlySurjective_104 :: (Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14
du_'8846''45'strictlySurjective_104 Any -> T_Σ_14
v0 Any -> T_Σ_14
v1
  = ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> Any -> Any -> T__'8846'__30 -> T_Σ_14
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 ->
            ((Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              (Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
              ((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    (Any -> T_Pointwise_70) -> Any
forall a b. a -> b
coe
                      Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88))
              ((Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Σ_14
v0 Any
v2)))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 ->
            ((Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              (Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
              ((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    (Any -> T_Pointwise_70) -> Any
forall a b. a -> b
coe
                      Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94))
              ((Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Σ_14
v1 Any
v2)))
-- Data.Sum.Function.Setoid.⊎-surjective
d_'8846''45'surjective_114 ::
  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.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8846''45'surjective_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T_Σ_14)
-> (Any -> T_Σ_14)
-> T__'8846'__30
-> T_Σ_14
d_'8846''45'surjective_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~Any -> Any -> T_Level_18
v9
                           ~T_Level_18
v10 ~Any -> Any -> T_Level_18
v11 ~T_Level_18
v12 ~Any -> Any -> T_Level_18
v13 ~T_Level_18
v14 ~Any -> Any -> T_Level_18
v15 ~Any -> Any
v16 ~Any -> Any
v17 Any -> T_Σ_14
v18 Any -> T_Σ_14
v19
  = (Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14
du_'8846''45'surjective_114 Any -> T_Σ_14
v18 Any -> T_Σ_14
v19
du_'8846''45'surjective_114 ::
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8846''45'surjective_114 :: (Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14
du_'8846''45'surjective_114 Any -> T_Σ_14
v0 Any -> T_Σ_14
v1
  = ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> Any -> Any -> T__'8846'__30 -> T_Σ_14
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 ->
            ((Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> Any -> (Any -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
              (Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
              ((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
              (\ Any
v3 Any
v4 Any
v5 Any
v6 -> ((Any -> Any -> Any)
 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe (Any -> Any -> Any)
-> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70
du_'46'extendedlambda0_120 Any
v4 Any
v5 Any
v6)
              ((Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Σ_14
v0 Any
v2)))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 ->
            ((Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> Any -> (Any -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
              (Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
              ((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
              (\ Any
v3 Any
v4 Any
v5 Any
v6 -> ((Any -> Any -> Any)
 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe (Any -> Any -> Any)
-> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70
du_'46'extendedlambda1_126 Any
v4 Any
v5 Any
v6)
              ((Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Σ_14
v1 Any
v2)))
-- Data.Sum.Function.Setoid..extendedlambda0
d_'46'extendedlambda0_120 ::
  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.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'46'extendedlambda0_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T_Σ_14)
-> (Any -> T_Σ_14)
-> Any
-> Any
-> (Any -> Any -> Any)
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'46'extendedlambda0_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~Any -> Any -> T_Level_18
v9
                          ~T_Level_18
v10 ~Any -> Any -> T_Level_18
v11 ~T_Level_18
v12 ~Any -> Any -> T_Level_18
v13 ~T_Level_18
v14 ~Any -> Any -> T_Level_18
v15 ~Any -> Any
v16 ~Any -> Any
v17 ~Any -> T_Σ_14
v18 ~Any -> T_Σ_14
v19 ~Any
v20 ~Any
v21 Any -> Any -> Any
v22 T__'8846'__30
v23
                          T_Pointwise_70
v24
  = (Any -> Any -> Any)
-> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70
du_'46'extendedlambda0_120 Any -> Any -> Any
v22 T__'8846'__30
v23 T_Pointwise_70
v24
du_'46'extendedlambda0_120 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'46'extendedlambda0_120 :: (Any -> Any -> Any)
-> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70
du_'46'extendedlambda0_120 Any -> Any -> Any
v0 T__'8846'__30
v1 T_Pointwise_70
v2
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v2 of
      MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v5
        -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v1 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v6
               -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                    Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88
                    ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
v0 Any
v6 Any
v5)
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid..extendedlambda1
d_'46'extendedlambda1_126 ::
  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.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'46'extendedlambda1_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> T_Level_18
-> (Any -> Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T_Σ_14)
-> (Any -> T_Σ_14)
-> Any
-> Any
-> (Any -> Any -> Any)
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'46'extendedlambda1_126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~Any -> Any -> T_Level_18
v9
                          ~T_Level_18
v10 ~Any -> Any -> T_Level_18
v11 ~T_Level_18
v12 ~Any -> Any -> T_Level_18
v13 ~T_Level_18
v14 ~Any -> Any -> T_Level_18
v15 ~Any -> Any
v16 ~Any -> Any
v17 ~Any -> T_Σ_14
v18 ~Any -> T_Σ_14
v19 ~Any
v20 ~Any
v21 Any -> Any -> Any
v22 T__'8846'__30
v23
                          T_Pointwise_70
v24
  = (Any -> Any -> Any)
-> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70
du_'46'extendedlambda1_126 Any -> Any -> Any
v22 T__'8846'__30
v23 T_Pointwise_70
v24
du_'46'extendedlambda1_126 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'46'extendedlambda1_126 :: (Any -> Any -> Any)
-> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70
du_'46'extendedlambda1_126 Any -> Any -> Any
v0 T__'8846'__30
v1 T_Pointwise_70
v2
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v2 of
      MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v5
        -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v1 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v6
               -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                    Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94
                    ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
v0 Any
v6 Any
v5)
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid._⊎-function_
d__'8846''45'function__132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d__'8846''45'function__132 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Func_714
-> T_Func_714
-> T_Func_714
d__'8846''45'function__132 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                           ~T_Level_18
v10 ~T_Setoid_44
v11 T_Func_714
v12 T_Func_714
v13
  = T_Func_714 -> T_Func_714 -> T_Func_714
du__'8846''45'function__132 T_Func_714
v12 T_Func_714
v13
du__'8846''45'function__132 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du__'8846''45'function__132 :: T_Func_714 -> T_Func_714 -> T_Func_714
du__'8846''45'function__132 T_Func_714
v0 T_Func_714
v1
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714)
-> Any -> Any -> T_Func_714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Func_714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v0))
         ((T_Func_714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Func_714 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_722 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v0))
         ((T_Func_714 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Func_714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_722 (T_Func_714 -> Any
forall a b. a -> b
coe T_Func_714
v1)))
-- Data.Sum.Function.Setoid._⊎-equivalence_
d__'8846''45'equivalence__142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d__'8846''45'equivalence__142 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Equivalence_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
d__'8846''45'equivalence__142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8
                              ~T_Level_18
v9 ~T_Level_18
v10 ~T_Setoid_44
v11 T_Equivalence_1714
v12 T_Equivalence_1714
v13
  = T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8846''45'equivalence__142 T_Equivalence_1714
v12 T_Equivalence_1714
v13
du__'8846''45'equivalence__142 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du__'8846''45'equivalence__142 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8846''45'equivalence__142 T_Equivalence_1714
v0 T_Equivalence_1714
v1
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Equivalence_1714)
-> Any -> Any -> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.C_Equivalence'46'constructor_25797
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Equivalence_1714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1724 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v0))
         ((T_Equivalence_1714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1724 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v1)))
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Equivalence_1714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1726 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v0))
         ((T_Equivalence_1714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1726 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Equivalence_1714 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1728 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v0))
         ((T_Equivalence_1714 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1728 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Equivalence_1714 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1730 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v0))
         ((T_Equivalence_1714 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1730 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v1)))
-- Data.Sum.Function.Setoid._⊎-injection_
d__'8846''45'injection__152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d__'8846''45'injection__152 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Injection_776
-> T_Injection_776
-> T_Injection_776
d__'8846''45'injection__152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                            ~T_Level_18
v10 ~T_Setoid_44
v11 T_Injection_776
v12 T_Injection_776
v13
  = T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8846''45'injection__152 T_Injection_776
v12 T_Injection_776
v13
du__'8846''45'injection__152 ::
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du__'8846''45'injection__152 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8846''45'injection__152 T_Injection_776
v0 T_Injection_776
v1
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Injection_776)
-> Any -> Any -> Any -> T_Injection_776
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Injection_776
MAlonzo.Code.Function.Bundles.C_Injection'46'constructor_8675
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Injection_776 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_784 (T_Injection_776 -> Any
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_784 (T_Injection_776 -> Any
forall a b. a -> b
coe T_Injection_776
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Injection_776 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_786 (T_Injection_776 -> Any
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_786 (T_Injection_776 -> Any
forall a b. a -> b
coe T_Injection_776
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'injective_78
         ((T_Injection_776 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_injective_788 (T_Injection_776 -> Any
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_injective_788 (T_Injection_776 -> Any
forall a b. a -> b
coe T_Injection_776
v1)))
-- Data.Sum.Function.Setoid._⊎-surjection_
d__'8846''45'surjection__162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d__'8846''45'surjection__162 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
d__'8846''45'surjection__162 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8
                             ~T_Level_18
v9 ~T_Level_18
v10 ~T_Setoid_44
v11 T_Surjection_846
v12 T_Surjection_846
v13
  = T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8846''45'surjection__162 T_Surjection_846
v12 T_Surjection_846
v13
du__'8846''45'surjection__162 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du__'8846''45'surjection__162 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8846''45'surjection__162 T_Surjection_846
v0 T_Surjection_846
v1
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> T_Σ_14)
 -> T_Surjection_846)
-> Any -> Any -> Any -> T_Surjection_846
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> T_Σ_14)
-> T_Surjection_846
MAlonzo.Code.Function.Bundles.C_Surjection'46'constructor_11197
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Surjection_846 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Surjection_846 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> Any
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Surjection_846 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> Any
forall a b. a -> b
coe T_Surjection_846
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Surjection_846 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Surjection_846 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_856 (T_Surjection_846 -> Any
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Surjection_846 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_856 (T_Surjection_846 -> Any
forall a b. a -> b
coe T_Surjection_846
v1)))
      (((Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14
du_'8846''45'surjective_114
         ((T_Surjection_846 -> Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_Surjection_846 -> Any -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_858 (T_Surjection_846 -> Any
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_Surjection_846 -> Any -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_858 (T_Surjection_846 -> Any
forall a b. a -> b
coe T_Surjection_846
v1)))
-- Data.Sum.Function.Setoid._⊎-bijection_
d__'8846''45'bijection__172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d__'8846''45'bijection__172 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
d__'8846''45'bijection__172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                            ~T_Level_18
v10 ~T_Setoid_44
v11 T_Bijection_926
v12 T_Bijection_926
v13
  = T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'8846''45'bijection__172 T_Bijection_926
v12 T_Bijection_926
v13
du__'8846''45'bijection__172 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du__'8846''45'bijection__172 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'8846''45'bijection__172 T_Bijection_926
v0 T_Bijection_926
v1
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Bijection_926)
-> Any -> Any -> Any -> T_Bijection_926
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Bijection_926
MAlonzo.Code.Function.Bundles.C_Bijection'46'constructor_15277
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Bijection_926 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v0))
         ((T_Bijection_926 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Bijection_926 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_936 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v0))
         ((T_Bijection_926 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_936 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v1)))
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
         (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'injective_78
            ((T_Bijection_926 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_injective_940 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v0))
            ((T_Bijection_926 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_injective_940 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v1)))
         (((Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
            (Any -> T_Σ_14) -> (Any -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14
du_'8846''45'surjective_114
            ((T_Bijection_926 -> Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> T_Σ_14
MAlonzo.Code.Function.Bundles.du_surjective_942 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v0))
            ((T_Bijection_926 -> Any -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> T_Σ_14
MAlonzo.Code.Function.Bundles.du_surjective_942 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v1))))
-- Data.Sum.Function.Setoid._⊎-leftInverse_
d__'8846''45'leftInverse__182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d__'8846''45'leftInverse__182 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_LeftInverse_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
d__'8846''45'leftInverse__182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8
                              ~T_Level_18
v9 ~T_Level_18
v10 ~T_Setoid_44
v11 T_LeftInverse_1792
v12 T_LeftInverse_1792
v13
  = T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8846''45'leftInverse__182 T_LeftInverse_1792
v12 T_LeftInverse_1792
v13
du__'8846''45'leftInverse__182 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du__'8846''45'leftInverse__182 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8846''45'leftInverse__182 T_LeftInverse_1792
v0 T_LeftInverse_1792
v1
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_LeftInverse_1792)
-> Any -> Any -> Any -> Any -> Any -> T_LeftInverse_1792
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.C_LeftInverse'46'constructor_29775
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_LeftInverse_1792 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1804 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1804 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v1)))
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_LeftInverse_1792 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1806 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1806 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_LeftInverse_1792 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1808 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1808 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_LeftInverse_1792 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1810 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1810 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v1)))
      ((T_LeftInverse_1792
 -> T_LeftInverse_1792
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792
-> T_LeftInverse_1792
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_192 (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v0) (T_LeftInverse_1792 -> Any
forall a b. a -> b
coe T_LeftInverse_1792
v1))
-- Data.Sum.Function.Setoid._..extendedlambda2
d_'46'extendedlambda2_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'46'extendedlambda2_192 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_LeftInverse_1792
-> T_LeftInverse_1792
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'46'extendedlambda2_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                          ~T_Level_18
v10 ~T_Setoid_44
v11 T_LeftInverse_1792
v12 T_LeftInverse_1792
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
  = T_LeftInverse_1792
-> T_LeftInverse_1792
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_192 T_LeftInverse_1792
v12 T_LeftInverse_1792
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
du_'46'extendedlambda2_192 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'46'extendedlambda2_192 :: T_LeftInverse_1792
-> T_LeftInverse_1792
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_192 T_LeftInverse_1792
v0 T_LeftInverse_1792
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88
                           ((T_LeftInverse_1792 -> Any -> Any -> Any -> Any)
-> T_LeftInverse_1792 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_inverse'737'_1812 T_LeftInverse_1792
v0 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94
                           ((T_LeftInverse_1792 -> Any -> Any -> Any -> Any)
-> T_LeftInverse_1792 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_1792 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_inverse'737'_1812 T_LeftInverse_1792
v1 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid._⊎-rightInverse_
d__'8846''45'rightInverse__198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d__'8846''45'rightInverse__198 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
d__'8846''45'rightInverse__198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8
                               ~T_Level_18
v9 ~T_Level_18
v10 ~T_Setoid_44
v11 T_RightInverse_1880
v12 T_RightInverse_1880
v13
  = T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8846''45'rightInverse__198 T_RightInverse_1880
v12 T_RightInverse_1880
v13
du__'8846''45'rightInverse__198 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du__'8846''45'rightInverse__198 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8846''45'rightInverse__198 T_RightInverse_1880
v0 T_RightInverse_1880
v1
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_RightInverse_1880)
-> Any -> Any -> Any -> Any -> Any -> T_RightInverse_1880
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.C_RightInverse'46'constructor_34573
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_RightInverse_1880 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v1)))
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_RightInverse_1880 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_RightInverse_1880 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1896 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1896 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_RightInverse_1880 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v1)))
      ((T_RightInverse_1880
 -> T_RightInverse_1880
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880
-> T_RightInverse_1880
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_208 (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v0) (T_RightInverse_1880 -> Any
forall a b. a -> b
coe T_RightInverse_1880
v1))
-- Data.Sum.Function.Setoid._..extendedlambda2
d_'46'extendedlambda2_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'46'extendedlambda2_208 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_RightInverse_1880
-> T_RightInverse_1880
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'46'extendedlambda2_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                          ~T_Level_18
v10 ~T_Setoid_44
v11 T_RightInverse_1880
v12 T_RightInverse_1880
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
  = T_RightInverse_1880
-> T_RightInverse_1880
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_208 T_RightInverse_1880
v12 T_RightInverse_1880
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
du_'46'extendedlambda2_208 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'46'extendedlambda2_208 :: T_RightInverse_1880
-> T_RightInverse_1880
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_208 T_RightInverse_1880
v0 T_RightInverse_1880
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88
                           ((T_RightInverse_1880 -> Any -> Any -> Any -> Any)
-> T_RightInverse_1880 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 T_RightInverse_1880
v0 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94
                           ((T_RightInverse_1880 -> Any -> Any -> Any -> Any)
-> T_RightInverse_1880 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 T_RightInverse_1880
v1 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid._⊎-inverse_
d__'8846''45'inverse__214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d__'8846''45'inverse__214 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Inverse_1960
-> T_Inverse_1960
d__'8846''45'inverse__214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                          ~T_Level_18
v10 ~T_Setoid_44
v11 T_Inverse_1960
v12 T_Inverse_1960
v13
  = T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8846''45'inverse__214 T_Inverse_1960
v12 T_Inverse_1960
v13
du__'8846''45'inverse__214 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du__'8846''45'inverse__214 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8846''45'inverse__214 T_Inverse_1960
v0 T_Inverse_1960
v1
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> T_Inverse_1960)
-> Any -> Any -> Any -> Any -> Any -> T_Inverse_1960
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v1)))
      (((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
         ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v1)))
      (((Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_map_100
         ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v1)))
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
         ((T_Inverse_1960
 -> T_Inverse_1960
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_224 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0) (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v1))
         ((T_Inverse_1960
 -> T_Inverse_1960
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda3_230 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0) (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v1)))
-- Data.Sum.Function.Setoid._..extendedlambda2
d_'46'extendedlambda2_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'46'extendedlambda2_224 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'46'extendedlambda2_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                          ~T_Level_18
v10 ~T_Setoid_44
v11 T_Inverse_1960
v12 T_Inverse_1960
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
  = T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_224 T_Inverse_1960
v12 T_Inverse_1960
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
du_'46'extendedlambda2_224 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'46'extendedlambda2_224 :: T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda2_224 T_Inverse_1960
v0 T_Inverse_1960
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88
                           ((T_Inverse_1960 -> Any -> Any -> Any -> Any)
-> T_Inverse_1960 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'737'_1982 T_Inverse_1960
v0 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94
                           ((T_Inverse_1960 -> Any -> Any -> Any -> Any)
-> T_Inverse_1960 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'737'_1982 T_Inverse_1960
v1 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid._..extendedlambda3
d_'46'extendedlambda3_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
d_'46'extendedlambda3_230 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'46'extendedlambda3_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Level_18
v9
                          ~T_Level_18
v10 ~T_Setoid_44
v11 T_Inverse_1960
v12 T_Inverse_1960
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
  = T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda3_230 T_Inverse_1960
v12 T_Inverse_1960
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
du_'46'extendedlambda3_230 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70 ->
  MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_70
du_'46'extendedlambda3_230 :: T_Inverse_1960
-> T_Inverse_1960
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'46'extendedlambda3_230 T_Inverse_1960
v0 T_Inverse_1960
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_88
                           ((T_Inverse_1960 -> Any -> Any -> Any -> Any)
-> T_Inverse_1960 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'691'_1984 T_Inverse_1960
v0 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
        -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
             MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94 Any
v8
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v9
                      -> (Any -> T_Pointwise_70) -> Any -> T_Pointwise_70
forall a b. a -> b
coe
                           Any -> T_Pointwise_70
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_94
                           ((T_Inverse_1960 -> Any -> Any -> Any -> Any)
-> T_Inverse_1960 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'691'_1984 T_Inverse_1960
v1 Any
v5 Any
v9 Any
v8)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Function.Setoid._⊎-left-inverse_
d__'8846''45'left'45'inverse__236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d__'8846''45'left'45'inverse__236 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_LeftInverse_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
d__'8846''45'left'45'inverse__236 T_Level_18
v0 T_Level_18
v1 T_Setoid_44
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_44
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_44
v8 T_Level_18
v9 T_Level_18
v10
                                  T_Setoid_44
v11 T_LeftInverse_1792
v12 T_LeftInverse_1792
v13
  = (T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792)
-> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
forall a b. a -> b
coe T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8846''45'leftInverse__182 T_LeftInverse_1792
v12 T_LeftInverse_1792
v13