{-# 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.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'_168
                    ((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'_168
                    ((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.⊎-antisymmetric
d_'8846''45'antisymmetric_278 ::
  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_278 :: ()
-> ()
-> ()
-> (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_278 ~()
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_278 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_278 ::
  (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_278 :: (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_278 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'_296 ::
  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'_296 :: ()
-> ()
-> ()
-> ()
-> ()
-> (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'_296 ~()
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'_296 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'_296 ::
  (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'_296 :: (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'_296 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'_314 ::
  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'_314 :: ()
-> ()
-> ()
-> ()
-> ()
-> (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'_314 ~()
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'_314 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'_314 ::
  (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'_314 :: (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'_314 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'_332 ::
  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'_332 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8846''45'respects'8322'_332 ~()
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'_332 T_Σ_14
v12 T_Σ_14
v13
du_'8846''45'respects'8322'_332 ::
  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'_332 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_332 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'_314 (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'_296 (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_342 ::
  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_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8846''45'isEquivalence_342 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_26
-> T_IsEquivalence_26
-> T_IsEquivalence_26
d_'8846''45'isEquivalence_342 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsEquivalence_26
v8 T_IsEquivalence_26
v9
  = T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_342 T_IsEquivalence_26
v8 T_IsEquivalence_26
v9
du_'8846''45'isEquivalence_342 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'8846''45'isEquivalence_342 :: T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_342 T_IsEquivalence_26
v0 T_IsEquivalence_26
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
      (((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_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
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_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isDecEquivalence
d_'8846''45'isDecEquivalence_352 ::
  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_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8846''45'isDecEquivalence_352 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
d_'8846''45'isDecEquivalence_352 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsDecEquivalence_44
v8
                                 T_IsDecEquivalence_44
v9
  = T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_352 T_IsDecEquivalence_44
v8 T_IsDecEquivalence_44
v9
du_'8846''45'isDecEquivalence_352 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_352 :: T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_352 T_IsDecEquivalence_44
v0 T_IsDecEquivalence_44
v1
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
      ((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_342
         ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
            (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
         ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
            (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
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_44 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
         ((T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isPreorder
d_'8846''45'isPreorder_362 ::
  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_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8846''45'isPreorder_362 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_IsPreorder_70
-> T_IsPreorder_70
d_'8846''45'isPreorder_362 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8 ~AgdaAny -> AgdaAny -> ()
v9
                           ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsPreorder_70
v12 T_IsPreorder_70
v13
  = T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_362 T_IsPreorder_70
v12 T_IsPreorder_70
v13
du_'8846''45'isPreorder_362 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_'8846''45'isPreorder_362 :: T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_362 T_IsPreorder_70
v0 T_IsPreorder_70
v1
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
      ((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_342
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
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_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
         ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isPartialOrder
d_'8846''45'isPartialOrder_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.Relation.Binary.Structures.T_IsPartialOrder_174 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8846''45'isPartialOrder_372 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_174
-> T_IsPartialOrder_174
-> T_IsPartialOrder_174
d_'8846''45'isPartialOrder_372 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~()
v7 ~()
v8
                               ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsPartialOrder_174
v12 T_IsPartialOrder_174
v13
  = T_IsPartialOrder_174
-> T_IsPartialOrder_174 -> T_IsPartialOrder_174
du_'8846''45'isPartialOrder_372 T_IsPartialOrder_174
v12 T_IsPartialOrder_174
v13
du_'8846''45'isPartialOrder_372 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_'8846''45'isPartialOrder_372 :: T_IsPartialOrder_174
-> T_IsPartialOrder_174 -> T_IsPartialOrder_174
du_'8846''45'isPartialOrder_372 T_IsPartialOrder_174
v0 T_IsPartialOrder_174
v1
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      ((T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_362
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0))
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
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_278
         ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0))
         ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-isStrictPartialOrder
d_'8846''45'isStrictPartialOrder_382 ::
  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_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'8846''45'isStrictPartialOrder_382 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_290
-> T_IsStrictPartialOrder_290
-> T_IsStrictPartialOrder_290
d_'8846''45'isStrictPartialOrder_382 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~()
v6
                                     ~()
v7 ~()
v8 ~AgdaAny -> AgdaAny -> ()
v9 ~()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsStrictPartialOrder_290
v12 T_IsStrictPartialOrder_290
v13
  = T_IsStrictPartialOrder_290
-> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
du_'8846''45'isStrictPartialOrder_382 T_IsStrictPartialOrder_290
v12 T_IsStrictPartialOrder_290
v13
du_'8846''45'isStrictPartialOrder_382 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
du_'8846''45'isStrictPartialOrder_382 :: T_IsStrictPartialOrder_290
-> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
du_'8846''45'isStrictPartialOrder_382 T_IsStrictPartialOrder_290
v0 T_IsStrictPartialOrder_290
v1
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
      ((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_342
         ((T_IsStrictPartialOrder_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
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_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_306 (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_306 (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
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'_332
         ((T_IsStrictPartialOrder_290 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-setoid
d_'8846''45'setoid_392 ::
  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_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8846''45'setoid_392 :: () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
d_'8846''45'setoid_392 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_Setoid_44
v5
  = T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du_'8846''45'setoid_392 T_Setoid_44
v4 T_Setoid_44
v5
du_'8846''45'setoid_392 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_'8846''45'setoid_392 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du_'8846''45'setoid_392 T_Setoid_44
v0 T_Setoid_44
v1
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
      ((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_342
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-decSetoid
d_'8846''45'decSetoid_402 ::
  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_84 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8846''45'decSetoid_402 :: ()
-> ()
-> ()
-> ()
-> T_DecSetoid_84
-> T_DecSetoid_84
-> T_DecSetoid_84
d_'8846''45'decSetoid_402 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_DecSetoid_84
v4 T_DecSetoid_84
v5
  = T_DecSetoid_84 -> T_DecSetoid_84 -> T_DecSetoid_84
du_'8846''45'decSetoid_402 T_DecSetoid_84
v4 T_DecSetoid_84
v5
du_'8846''45'decSetoid_402 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
du_'8846''45'decSetoid_402 :: T_DecSetoid_84 -> T_DecSetoid_84 -> T_DecSetoid_84
du_'8846''45'decSetoid_402 T_DecSetoid_84
v0 T_DecSetoid_84
v1
  = (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1389
      ((T_IsDecEquivalence_44
 -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_352
         ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
            (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0))
         ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
            (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-preorder
d_'8846''45'preorder_412 ::
  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_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8846''45'preorder_412 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Preorder_132
-> T_Preorder_132
-> T_Preorder_132
d_'8846''45'preorder_412 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 T_Preorder_132
v6 T_Preorder_132
v7
  = T_Preorder_132 -> T_Preorder_132 -> T_Preorder_132
du_'8846''45'preorder_412 T_Preorder_132
v6 T_Preorder_132
v7
du_'8846''45'preorder_412 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_'8846''45'preorder_412 :: T_Preorder_132 -> T_Preorder_132 -> T_Preorder_132
du_'8846''45'preorder_412 T_Preorder_132
v0 T_Preorder_132
v1
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
      ((T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_362
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v1)))
-- Data.Sum.Relation.Binary.Pointwise.⊎-poset
d_'8846''45'poset_422 ::
  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_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8846''45'poset_422 :: () -> () -> () -> T_Poset_314 -> T_Poset_314 -> T_Poset_314
d_'8846''45'poset_422 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 T_Poset_314
v4
  = T_Poset_314 -> T_Poset_314 -> T_Poset_314
du_'8846''45'poset_422 T_Poset_314
v3 T_Poset_314
v4
du_'8846''45'poset_422 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_'8846''45'poset_422 :: T_Poset_314 -> T_Poset_314 -> T_Poset_314
du_'8846''45'poset_422 T_Poset_314
v0 T_Poset_314
v1
  = (T_IsPartialOrder_174 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      ((T_IsPartialOrder_174
 -> T_IsPartialOrder_174 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174
-> T_IsPartialOrder_174 -> T_IsPartialOrder_174
du_'8846''45'isPartialOrder_372
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
            (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v1)))
-- Data.Sum.Relation.Binary.Pointwise._⊎ₛ_
d__'8846''8347'__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_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d__'8846''8347'__432 :: () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
d__'8846''8347'__432 ~()
v0 ~()
v1 ~()
v2 ~()
v3 = T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du__'8846''8347'__432
du__'8846''8347'__432 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du__'8846''8347'__432 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du__'8846''8347'__432 = (T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44)
-> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du_'8846''45'setoid_392
-- Data.Sum.Relation.Binary.Pointwise.Pointwise-≡⇒≡
d_Pointwise'45''8801''8658''8801'_434 ::
  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'_434 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_70
-> T__'8801'__12
d_Pointwise'45''8801''8658''8801'_434 = ()
-> ()
-> ()
-> ()
-> 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'_440 ::
  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'_440 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T__'8801'__12
-> T_Pointwise_70
d_'8801''8658'Pointwise'45''8801'_440 ~()
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'_440 T__'8846'__30
v4
du_'8801''8658'Pointwise'45''8801'_440 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_440 :: T__'8846'__30 -> T_Pointwise_70
du_'8801''8658'Pointwise'45''8801'_440 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'_446 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_Pointwise'45''8801''8596''8801'_446 :: () -> () -> () -> () -> T_Inverse_1960
d_Pointwise'45''8801''8596''8801'_446 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Inverse_1960
du_Pointwise'45''8801''8596''8801'_446
du_Pointwise'45''8801''8596''8801'_446 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Pointwise'45''8801''8596''8801'_446 :: T_Inverse_1960
du_Pointwise'45''8801''8596''8801'_446
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_1960)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      ((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'_440 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'_440 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))