{-# 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.Relation.Binary.Pointwise 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Induction.WellFounded
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.Sum.Relation.Binary.Pointwise.Pointwise
d_Pointwise_70 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d_Pointwise_70 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 p
a10 p
a11 p
a12 p
a13 = ()
data T_Pointwise_70
  = C_inj'8321'_88 AgdaAny | C_inj'8322'_94 AgdaAny
-- Data.Sum.Relation.Binary.Pointwise.map
d_map_100 ::
  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 -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70
d_map_100 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_map_100 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~()
v8 ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 ~()
v12
          ~AgdaAny -> AgdaAny -> ()
v13 ~()
v14 ~AgdaAny -> AgdaAny -> ()
v15 ~AgdaAny -> AgdaAny
v16 ~AgdaAny -> AgdaAny
v17 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v18 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v19 T__'8846'__30
v20 T__'8846'__30
v21 T_Pointwise_70
v22
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_map_100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v18 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v19 T__'8846'__30
v20 T__'8846'__30
v21 T_Pointwise_70
v22
du_map_100 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70
du_map_100 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_map_100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
      C_inj'8321'_88 AgdaAny
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 AgdaAny
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 AgdaAny
v9
                      -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
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 AgdaAny
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 AgdaAny
v9
                      -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             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.Relation.Binary.Pointwise.drop-inj₁
d_drop'45'inj'8321'_114 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T_Pointwise_70 -> AgdaAny
d_drop'45'inj'8321'_114 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T_Pointwise_70
-> AgdaAny
d_drop'45'inj'8321'_114 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9
                        ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 ~AgdaAny
v12 ~AgdaAny
v13 T_Pointwise_70
v14
  = T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8321'_114 T_Pointwise_70
v14
du_drop'45'inj'8321'_114 :: T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8321'_114 :: T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8321'_114 T_Pointwise_70
v0
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v0 of
      C_inj'8321'_88 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
      T_Pointwise_70
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.drop-inj₂
d_drop'45'inj'8322'_122 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T_Pointwise_70 -> AgdaAny
d_drop'45'inj'8322'_122 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T_Pointwise_70
-> AgdaAny
d_drop'45'inj'8322'_122 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9
                        ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 ~AgdaAny
v12 ~AgdaAny
v13 T_Pointwise_70
v14
  = T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8322'_122 T_Pointwise_70
v14
du_drop'45'inj'8322'_122 :: T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8322'_122 :: T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8322'_122 T_Pointwise_70
v0
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v0 of
      C_inj'8322'_94 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
      T_Pointwise_70
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.⊎-refl
d_'8846''45'refl_126 ::
  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) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_70
d_'8846''45'refl_126 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T_Pointwise_70
d_'8846''45'refl_126 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 T__'8846'__30
v10
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70
du_'8846''45'refl_126 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 T__'8846'__30
v10
du_'8846''45'refl_126 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_70
du_'8846''45'refl_126 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70
du_'8846''45'refl_126 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T__'8846'__30
v2
  = 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 AgdaAny
v3
        -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v3
        -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3)
      T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.⊎-symmetric
d_'8846''45'symmetric_140 ::
  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) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70
d_'8846''45'symmetric_140 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'symmetric_140 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T__'8846'__30
v10
                          T__'8846'__30
v11 T_Pointwise_70
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'symmetric_140 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T__'8846'__30
v10 T__'8846'__30
v11 T_Pointwise_70
v12
du_'8846''45'symmetric_140 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70
du_'8846''45'symmetric_140 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'symmetric_140 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
      C_inj'8321'_88 AgdaAny
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 AgdaAny
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 AgdaAny
v9
                      -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
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 AgdaAny
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 AgdaAny
v9
                      -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             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.Relation.Binary.Pointwise.⊎-transitive
d_'8846''45'transitive_154 ::
  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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
d_'8846''45'transitive_154 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'transitive_154 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                           T__'8846'__30
v10 T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_70
v13 T_Pointwise_70
v14
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'transitive_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T__'8846'__30
v10 T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_70
v13 T_Pointwise_70
v14
du_'8846''45'transitive_154 ::
  (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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
du_'8846''45'transitive_154 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'transitive_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_70
v5 T_Pointwise_70
v6
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v5 of
      C_inj'8321'_88 AgdaAny
v9
        -> 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 AgdaAny
v10
               -> 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 AgdaAny
v11
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v6 of
                           C_inj'8321'_88 AgdaAny
v14
                             -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                                  MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v15
                                    -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v11 AgdaAny
v15 AgdaAny
v9 AgdaAny
v14)
                                  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
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
v9
        -> 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 AgdaAny
v10
               -> 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 AgdaAny
v11
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v6 of
                           C_inj'8322'_94 AgdaAny
v14
                             -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                                  MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v15
                                    -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v10 AgdaAny
v11 AgdaAny
v15 AgdaAny
v9 AgdaAny
v14)
                                  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
             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.Relation.Binary.Pointwise.⊎-asymmetric
d_'8846''45'asymmetric_172 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 ->
  T_Pointwise_70 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8846''45'asymmetric_172 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Irrelevant_20
d_'8846''45'asymmetric_172 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Irrelevant_20
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise..extendedlambda0
d_'46'extendedlambda0_180 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T_Pointwise_70 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_180 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_70
-> T_Irrelevant_20
d_'46'extendedlambda0_180 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_70
-> T_Irrelevant_20
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise..extendedlambda1
d_'46'extendedlambda1_190 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T_Pointwise_70 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_190 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_70
-> T_Irrelevant_20
d_'46'extendedlambda1_190 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_70
-> T_Irrelevant_20
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise.⊎-substitutive
d_'8846''45'substitutive_194 ::
  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 ->
  () ->
  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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> AgdaAny -> AgdaAny
d_'8846''45'substitutive_194 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8846'__30 -> ())
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> AgdaAny
-> AgdaAny
d_'8846''45'substitutive_194 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~AgdaAny -> AgdaAny -> ()
v8 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                             (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T__'8846'__30 -> ()
v11 T__'8846'__30
v12 T__'8846'__30
v13 T_Pointwise_70
v14
  = ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8846'__30 -> ())
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> AgdaAny
-> AgdaAny
du_'8846''45'substitutive_194 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T__'8846'__30 -> ()
v11 T__'8846'__30
v12 T__'8846'__30
v13 T_Pointwise_70
v14
du_'8846''45'substitutive_194 ::
  ((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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> AgdaAny -> AgdaAny
du_'8846''45'substitutive_194 :: ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8846'__30 -> ())
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> AgdaAny
-> AgdaAny
du_'8846''45'substitutive_194 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30 -> ()
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_70
v5
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v5 of
      C_inj'8321'_88 AgdaAny
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 AgdaAny
v9
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10
                      -> ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
                           (\ AgdaAny
v11 ->
                              (T__'8846'__30 -> ()) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> ()
v2 ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)))
                           AgdaAny
v9 AgdaAny
v10 AgdaAny
v8
                    T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
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 AgdaAny
v9
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v10
                      -> ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
                           (\ AgdaAny
v11 ->
                              (T__'8846'__30 -> ()) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> ()
v2 ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)))
                           AgdaAny
v9 AgdaAny
v10 AgdaAny
v8
                    T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_70
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.⊎-decidable
d_'8846''45'decidable_212 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8846''45'decidable_212 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_20
d_'8846''45'decidable_212 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9
                          ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> T_Dec_20
v12 AgdaAny -> AgdaAny -> T_Dec_20
v13 T__'8846'__30
v14 T__'8846'__30
v15
  = (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_20
du_'8846''45'decidable_212 AgdaAny -> AgdaAny -> T_Dec_20
v12 AgdaAny -> AgdaAny -> T_Dec_20
v13 T__'8846'__30
v14 T__'8846'__30
v15
du_'8846''45'decidable_212 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8846''45'decidable_212 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_20
du_'8846''45'decidable_212 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 T__'8846'__30
v2 T__'8846'__30
v3
  = 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 AgdaAny
v4
        -> 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 AgdaAny
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
                    ((AgdaAny -> T_Pointwise_70) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88) ((T_Pointwise_70 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8321'_114) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v4 AgdaAny
v5)
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T__'8846'__30
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v4
        -> 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 AgdaAny
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
                    ((AgdaAny -> T_Pointwise_70) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94) ((T_Pointwise_70 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Pointwise_70 -> AgdaAny
du_drop'45'inj'8322'_122) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v4 AgdaAny
v5)
             T__'8846'__30
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.⊎-reflexive
d_'8846''45'reflexive_246 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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 ->
  T_Pointwise_70 -> T_Pointwise_70
d_'8846''45'reflexive_246 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'reflexive_246 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8 ~AgdaAny -> AgdaAny -> ()
v9
                          ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'reflexive_246 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16
du_'8846''45'reflexive_246 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70
du_'8846''45'reflexive_246 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'reflexive_246 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
      C_inj'8321'_88 AgdaAny
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 AgdaAny
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 AgdaAny
v9
                      -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
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 AgdaAny
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 AgdaAny
v9
                      -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
                    T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
             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.Relation.Binary.Pointwise.⊎-irreflexive
d_'8846''45'irreflexive_260 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 ->
  T_Pointwise_70 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8846''45'irreflexive_260 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Irrelevant_20
d_'8846''45'irreflexive_260 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Irrelevant_20
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise.⊎-wellFounded
d_'8846''45'wellFounded_278 ::
  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 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  (AgdaAny -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_'8846''45'wellFounded_278 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> T_Acc_42
d_'8846''45'wellFounded_278 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> T_Acc_42
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise._.⊎-acc₁
d_'8846''45'acc'8321'_296 ::
  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 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  (AgdaAny -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  AgdaAny ->
  MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_'8846''45'acc'8321'_296 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> AgdaAny
-> T_Acc_42
-> T__'8846'__30
-> T_Pointwise_70
-> T_Acc_42
d_'8846''45'acc'8321'_296 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> AgdaAny
-> T_Acc_42
-> T__'8846'__30
-> T_Pointwise_70
-> T_Acc_42
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise._.⊎-acc₂
d_'8846''45'acc'8322'_304 ::
  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 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  (AgdaAny -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  AgdaAny ->
  MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_'8846''45'acc'8322'_304 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> AgdaAny
-> T_Acc_42
-> T__'8846'__30
-> T_Pointwise_70
-> T_Acc_42
d_'8846''45'acc'8322'_304 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> AgdaAny
-> T_Acc_42
-> T__'8846'__30
-> T_Pointwise_70
-> T_Acc_42
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise._.⊎-acc
d_'8846''45'acc_312 ::
  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 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  (AgdaAny -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_'8846''45'acc_312 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Acc_42
d_'8846''45'acc_312 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Acc_42)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Acc_42
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise.⊎-antisymmetric
d_'8846''45'antisymmetric_318 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
d_'8846''45'antisymmetric_318 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'antisymmetric_318 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8
                              ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16 T_Pointwise_70
v17
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'antisymmetric_318 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_70
v16 T_Pointwise_70
v17
du_'8846''45'antisymmetric_318 ::
  (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 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
du_'8846''45'antisymmetric_318 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'antisymmetric_318 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_70
v4 T_Pointwise_70
v5
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v4 of
      C_inj'8321'_88 AgdaAny
v8
        -> 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 AgdaAny
v9
               -> 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 AgdaAny
v10
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v5 of
                           C_inj'8321'_88 AgdaAny
v13 -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v9 AgdaAny
v10 AgdaAny
v8 AgdaAny
v13)
                           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
      C_inj'8322'_94 AgdaAny
v8
        -> 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 AgdaAny
v9
               -> 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 AgdaAny
v10
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v5 of
                           C_inj'8322'_94 AgdaAny
v13 -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v9 AgdaAny
v10 AgdaAny
v8 AgdaAny
v13)
                           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
      T_Pointwise_70
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.⊎-respectsˡ
d_'8846''45'respects'737'_336 ::
  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 ->
  () ->
  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 -> 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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
d_'8846''45'respects'737'_336 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'respects'737'_336 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
                              ~()
v9 ~()
v10 ~()
v11 ~()
v12 ~AgdaAny -> AgdaAny -> ()
v13 ~()
v14 ~AgdaAny -> AgdaAny -> ()
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 T__'8846'__30
v18 T__'8846'__30
v19 T__'8846'__30
v20 T_Pointwise_70
v21 T_Pointwise_70
v22
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'respects'737'_336 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 T__'8846'__30
v18 T__'8846'__30
v19 T__'8846'__30
v20 T_Pointwise_70
v21 T_Pointwise_70
v22
du_'8846''45'respects'737'_336 ::
  (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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
du_'8846''45'respects'737'_336 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'respects'737'_336 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_70
v5 T_Pointwise_70
v6
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v5 of
      C_inj'8321'_88 AgdaAny
v9
        -> 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 AgdaAny
v10
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v6 of
                           C_inj'8321'_88 AgdaAny
v14
                             -> 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 AgdaAny
v15
                                    -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
                                  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
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
v9
        -> 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 AgdaAny
v10
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v6 of
                           C_inj'8322'_94 AgdaAny
v14
                             -> 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 AgdaAny
v15
                                    -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
                                  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
             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.Relation.Binary.Pointwise.⊎-respectsʳ
d_'8846''45'respects'691'_354 ::
  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 ->
  () ->
  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 -> 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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
d_'8846''45'respects'691'_354 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
d_'8846''45'respects'691'_354 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
                              ~()
v9 ~()
v10 ~()
v11 ~()
v12 ~AgdaAny -> AgdaAny -> ()
v13 ~()
v14 ~AgdaAny -> AgdaAny -> ()
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 T__'8846'__30
v18 T__'8846'__30
v19 T__'8846'__30
v20 T_Pointwise_70
v21 T_Pointwise_70
v22
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'respects'691'_354 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 T__'8846'__30
v18 T__'8846'__30
v19 T__'8846'__30
v20 T_Pointwise_70
v21 T_Pointwise_70
v22
du_'8846''45'respects'691'_354 ::
  (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.Base.T__'8846'__30 ->
  T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70
du_'8846''45'respects'691'_354 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'respects'691'_354 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_70
v5 T_Pointwise_70
v6
  = case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v5 of
      C_inj'8321'_88 AgdaAny
v9
        -> 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 AgdaAny
v10
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v6 of
                           C_inj'8321'_88 AgdaAny
v14
                             -> 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 AgdaAny
v15
                                    -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8321'_88 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
                                  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
             T__'8846'__30
_ -> T_Pointwise_70
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_inj'8322'_94 AgdaAny
v9
        -> 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 AgdaAny
v10
               -> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
                    MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
                      -> case T_Pointwise_70 -> T_Pointwise_70
forall a b. a -> b
coe T_Pointwise_70
v6 of
                           C_inj'8322'_94 AgdaAny
v14
                             -> 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 AgdaAny
v15
                                    -> (AgdaAny -> T_Pointwise_70) -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe AgdaAny -> T_Pointwise_70
C_inj'8322'_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
                                  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
             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.Relation.Binary.Pointwise.⊎-respects₂
d_'8846''45'respects'8322'_372 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8846''45'respects'8322'_372 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8846''45'respects'8322'_372 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8
                               ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_Σ_14
v12 T_Σ_14
v13
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_372 T_Σ_14
v12 T_Σ_14
v13
du_'8846''45'respects'8322'_372 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8846''45'respects'8322'_372 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_372 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                    (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'respects'691'_354 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                    (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'respects'737'_336 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Sum.Relation.Binary.Pointwise.⊎-isEquivalence
d_'8846''45'isEquivalence_382 ::
  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.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_'8846''45'isEquivalence_382 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_28
-> T_IsEquivalence_28
-> T_IsEquivalence_28
d_'8846''45'isEquivalence_382 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsEquivalence_28
v8 T_IsEquivalence_28
v9
  = T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'8846''45'isEquivalence_382 T_IsEquivalence_28
v8 T_IsEquivalence_28
v9
du_'8846''45'isEquivalence_382 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_'8846''45'isEquivalence_382 :: T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'8846''45'isEquivalence_382 T_IsEquivalence_28
v0 T_IsEquivalence_28
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70
du_'8846''45'refl_126
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'symmetric_140
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'transitive_154
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0))
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isDecEquivalence
d_'8846''45'isDecEquivalence_392 ::
  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.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
d_'8846''45'isDecEquivalence_392 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_48
-> T_IsDecEquivalence_48
-> T_IsDecEquivalence_48
d_'8846''45'isDecEquivalence_392 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsDecEquivalence_48
v8
                                 T_IsDecEquivalence_48
v9
  = T_IsDecEquivalence_48
-> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_'8846''45'isDecEquivalence_392 T_IsDecEquivalence_48
v8 T_IsDecEquivalence_48
v9
du_'8846''45'isDecEquivalence_392 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
du_'8846''45'isDecEquivalence_392 :: T_IsDecEquivalence_48
-> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_'8846''45'isDecEquivalence_392 T_IsDecEquivalence_48
v0 T_IsDecEquivalence_48
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_48)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_48
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Structures.C_constructor_70
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'8846''45'isEquivalence_382
         ((T_IsDecEquivalence_48 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_54
            (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v0))
         ((T_IsDecEquivalence_48 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_54
            (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v1)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_20
du_'8846''45'decidable_212
         ((T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__56 (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v0))
         ((T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__56 (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isPreorder
d_'8846''45'isPreorder_402 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_'8846''45'isPreorder_402 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_76
-> T_IsPreorder_76
-> T_IsPreorder_76
d_'8846''45'isPreorder_402 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8 ~AgdaAny -> AgdaAny -> ()
v9
                           ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsPreorder_76
v12 T_IsPreorder_76
v13
  = T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'8846''45'isPreorder_402 T_IsPreorder_76
v12 T_IsPreorder_76
v13
du_'8846''45'isPreorder_402 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_'8846''45'isPreorder_402 :: T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'8846''45'isPreorder_402 T_IsPreorder_76
v0 T_IsPreorder_76
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'8846''45'isEquivalence_382
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'reflexive_246
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'transitive_154
         ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
         ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isPartialOrder
d_'8846''45'isPartialOrder_412 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_'8846''45'isPartialOrder_412 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_248
-> T_IsPartialOrder_248
-> T_IsPartialOrder_248
d_'8846''45'isPartialOrder_412 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8
                               ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsPartialOrder_248
v12 T_IsPartialOrder_248
v13
  = T_IsPartialOrder_248
-> T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_'8846''45'isPartialOrder_412 T_IsPartialOrder_248
v12 T_IsPartialOrder_248
v13
du_'8846''45'isPartialOrder_412 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_'8846''45'isPartialOrder_412 :: T_IsPartialOrder_248
-> T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_'8846''45'isPartialOrder_412 T_IsPartialOrder_248
v0 T_IsPartialOrder_248
v1
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      ((T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'8846''45'isPreorder_402
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v0))
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'antisymmetric_318
         ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v0))
         ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isStrictPartialOrder
d_'8846''45'isStrictPartialOrder_422 ::
  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 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_'8846''45'isStrictPartialOrder_422 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370
d_'8846''45'isStrictPartialOrder_422 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6
                                     ~()
v7 ~()
v8 ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsStrictPartialOrder_370
v12 T_IsStrictPartialOrder_370
v13
  = T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'8846''45'isStrictPartialOrder_422 T_IsStrictPartialOrder_370
v12 T_IsStrictPartialOrder_370
v13
du_'8846''45'isStrictPartialOrder_422 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
du_'8846''45'isStrictPartialOrder_422 :: T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'8846''45'isStrictPartialOrder_422 T_IsStrictPartialOrder_370
v0 T_IsStrictPartialOrder_370
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.C_constructor_412
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'8846''45'isEquivalence_382
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T__'8846'__30
 -> T__'8846'__30
 -> T__'8846'__30
 -> T_Pointwise_70
 -> T_Pointwise_70
 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T_Pointwise_70
-> T_Pointwise_70
du_'8846''45'transitive_154
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v1)))
      ((T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_372
         ((T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-setoid
d_'8846''45'setoid_432 ::
  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.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_'8846''45'setoid_432 :: () -> () -> () -> () -> T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
d_'8846''45'setoid_432 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_46
v4 T_Setoid_46
v5
  = T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du_'8846''45'setoid_432 T_Setoid_46
v4 T_Setoid_46
v5
du_'8846''45'setoid_432 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_'8846''45'setoid_432 :: T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du_'8846''45'setoid_432 T_Setoid_46
v0 T_Setoid_46
v1
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'8846''45'isEquivalence_382
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-decSetoid
d_'8846''45'decSetoid_442 ::
  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.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
d_'8846''45'decSetoid_442 :: ()
-> ()
-> ()
-> ()
-> T_DecSetoid_90
-> T_DecSetoid_90
-> T_DecSetoid_90
d_'8846''45'decSetoid_442 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_DecSetoid_90
v4 T_DecSetoid_90
v5
  = T_DecSetoid_90 -> T_DecSetoid_90 -> T_DecSetoid_90
du_'8846''45'decSetoid_442 T_DecSetoid_90
v4 T_DecSetoid_90
v5
du_'8846''45'decSetoid_442 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
du_'8846''45'decSetoid_442 :: T_DecSetoid_90 -> T_DecSetoid_90 -> T_DecSetoid_90
du_'8846''45'decSetoid_442 T_DecSetoid_90
v0 T_DecSetoid_90
v1
  = (T_IsDecEquivalence_48 -> T_DecSetoid_90)
-> AgdaAny -> T_DecSetoid_90
forall a b. a -> b
coe
      T_IsDecEquivalence_48 -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_134
      ((T_IsDecEquivalence_48
 -> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_48
-> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_'8846''45'isDecEquivalence_392
         ((T_DecSetoid_90 -> T_IsDecEquivalence_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_90 -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_106
            (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v0))
         ((T_DecSetoid_90 -> T_IsDecEquivalence_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_90 -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_106
            (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-preorder
d_'8846''45'preorder_452 ::
  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 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_'8846''45'preorder_452 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Preorder_142
-> T_Preorder_142
-> T_Preorder_142
d_'8846''45'preorder_452 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 T_Preorder_142
v6 T_Preorder_142
v7
  = T_Preorder_142 -> T_Preorder_142 -> T_Preorder_142
du_'8846''45'preorder_452 T_Preorder_142
v6 T_Preorder_142
v7
du_'8846''45'preorder_452 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_'8846''45'preorder_452 :: T_Preorder_142 -> T_Preorder_142 -> T_Preorder_142
du_'8846''45'preorder_452 T_Preorder_142
v0 T_Preorder_142
v1
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'8846''45'isPreorder_402
         ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0))
         ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-poset
d_'8846''45'poset_462 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_'8846''45'poset_462 :: () -> () -> () -> T_Poset_492 -> T_Poset_492 -> T_Poset_492
d_'8846''45'poset_462 ~()
v0 ~()
v1 ~()
v2 T_Poset_492
v3 T_Poset_492
v4
  = T_Poset_492 -> T_Poset_492 -> T_Poset_492
du_'8846''45'poset_462 T_Poset_492
v3 T_Poset_492
v4
du_'8846''45'poset_462 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_'8846''45'poset_462 :: T_Poset_492 -> T_Poset_492 -> T_Poset_492
du_'8846''45'poset_462 T_Poset_492
v0 T_Poset_492
v1
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      ((T_IsPartialOrder_248
 -> T_IsPartialOrder_248 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248
-> T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_'8846''45'isPartialOrder_412
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
            (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v1)))
-- Data.Sum.Relation.Binary.Pointwise._⊎ₛ_
d__'8846''8347'__472 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d__'8846''8347'__472 :: () -> () -> () -> () -> T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
d__'8846''8347'__472 ~()
v0 ~()
v1 ~()
v2 ~()
v3 = T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du__'8846''8347'__472
du__'8846''8347'__472 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du__'8846''8347'__472 :: T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du__'8846''8347'__472 = (T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46)
-> T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du_'8846''45'setoid_432
-- Data.Sum.Relation.Binary.Pointwise.Pointwise-≡⇒≡
d_Pointwise'45''8801''8658''8801'_474 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  T_Pointwise_70 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_Pointwise'45''8801''8658''8801'_474 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T__'8801'__12
d_Pointwise'45''8801''8658''8801'_474 = ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T__'8801'__12
forall a. a
erased
-- Data.Sum.Relation.Binary.Pointwise.≡⇒Pointwise-≡
d_'8801''8658'Pointwise'45''8801'_480 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T_Pointwise_70
d_'8801''8658'Pointwise'45''8801'_480 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T__'8801'__12
-> T_Pointwise_70
d_'8801''8658'Pointwise'45''8801'_480 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T__'8846'__30
v4 ~T__'8846'__30
v5 ~T__'8801'__12
v6
  = T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_480 T__'8846'__30
v4
du_'8801''8658'Pointwise'45''8801'_480 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_480 :: T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_480 T__'8846'__30
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_70
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70
du_'8846''45'refl_126 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v0)
-- Data.Sum.Relation.Binary.Pointwise.Pointwise-≡↔≡
d_Pointwise'45''8801''8596''8801'_486 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Pointwise'45''8801''8596''8801'_486 :: () -> () -> () -> () -> T_Inverse_2122
d_Pointwise'45''8801''8596''8801'_486 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Inverse_2122
du_Pointwise'45''8801''8596''8801'_486
du_Pointwise'45''8801''8596''8801'_486 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Pointwise'45''8801''8596''8801'_486 :: T_Inverse_2122
du_Pointwise'45''8801''8596''8801'_486
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_2122)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_2122
MAlonzo.Code.Function.Bundles.C_constructor_2220 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> (T__'8846'__30 -> T_Pointwise_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_480 AgdaAny
v0)
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 ->
               (T__'8846'__30 -> T_Pointwise_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_480 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))