{-# 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.List.Relation.Binary.Lex 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Binary.Lex.Core
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.List.Relation.Binary.Lex._._≋_
d__'8779'__28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'8779'__28 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
d__'8779'__28 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
-- Data.List.Relation.Binary.Lex._._<_
d__'60'__30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'60'__30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
d__'60'__30 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
-- Data.List.Relation.Binary.Lex._.²-this
d_'172''8804''45'this_40 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'172''8804''45'this_40 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T_Lex_32
-> T_Irrelevant_20
d_'172''8804''45'this_40 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T_Lex_32
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex._.²-next
d_'172''8804''45'next_64 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'172''8804''45'next_64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> T_Irrelevant_20)
-> (T_Lex_32 -> T_Irrelevant_20)
-> T_Lex_32
-> T_Irrelevant_20
d_'172''8804''45'next_64 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> T_Irrelevant_20)
-> (T_Lex_32 -> T_Irrelevant_20)
-> T_Lex_32
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex._.antisymmetric
d_antisymmetric_78 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_antisymmetric_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
d_antisymmetric_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 [AgdaAny]
v10 [AgdaAny]
v11
  = [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
du_antisymmetric_78 [AgdaAny]
v10 [AgdaAny]
v11
du_antisymmetric_78 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_antisymmetric_78 :: [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
du_antisymmetric_78 [AgdaAny]
v0 [AgdaAny]
v1 = ([AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
du_as_90 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
-- Data.List.Relation.Binary.Lex._._.as
d_as_90 ::
  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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_as_90 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
d_as_90 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~[AgdaAny]
v10 ~[AgdaAny]
v11 [AgdaAny]
v12 [AgdaAny]
v13
        T_Lex_32
v14 T_Lex_32
v15
  = [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
du_as_90 [AgdaAny]
v12 [AgdaAny]
v13 T_Lex_32
v14 T_Lex_32
v15
du_as_90 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_as_90 :: [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
du_as_90 [AgdaAny]
v0 [AgdaAny]
v1 T_Lex_32
v2 T_Lex_32
v3
  = case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v2 of
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42 AgdaAny
v4
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v3)
             (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe
                T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v8
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.du_'8869''45'elim_14)
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v8 T_Lex_32
v9
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
             (:) AgdaAny
v10 [AgdaAny]
v11
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
                    (:) AgdaAny
v12 [AgdaAny]
v13
                      -> case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v3 of
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v18
                             -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.du_'8869''45'elim_14
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v18 T_Lex_32
v19
                             -> (AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
                                  AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                  AgdaAny
v8 (([AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
du_as_90 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v11) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v9) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v19))
                           T_Lex_32
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Lex_32
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._.toSum
d_toSum_124 ::
  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] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_124 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T__'8846'__30
d_toSum_124 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~[AgdaAny]
v9 ~[AgdaAny]
v10 T_Lex_32
v11
  = T_Lex_32 -> T__'8846'__30
du_toSum_124 T_Lex_32
v11
du_toSum_124 ::
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_124 :: T_Lex_32 -> T__'8846'__30
du_toSum_124 T_Lex_32
v0
  = case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v0 of
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v5
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
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
v5)
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v5 T_Lex_32
v6
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
             AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
             ((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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v6))
      T_Lex_32
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._.transitive
d_transitive_132 ::
  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.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_transitive_132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
d_transitive_132 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsEquivalence_26
v7 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 [AgdaAny]
v12
  = T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_transitive_132 T_IsEquivalence_26
v7 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 [AgdaAny]
v12
du_transitive_132 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_transitive_132 :: T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_transitive_132 T_IsEquivalence_26
v0 T_Σ_14
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 [AgdaAny]
v5
  = (T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
forall a b. a -> b
coe
      T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_trans_144 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5)
-- Data.List.Relation.Binary.Lex._._.trans
d_trans_144 ::
  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.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_trans_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
d_trans_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsEquivalence_26
v7 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~[AgdaAny]
v10 ~[AgdaAny]
v11 ~[AgdaAny]
v12 [AgdaAny]
v13
            [AgdaAny]
v14 [AgdaAny]
v15 T_Lex_32
v16 T_Lex_32
v17
  = T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_trans_144 T_IsEquivalence_26
v7 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 [AgdaAny]
v13 [AgdaAny]
v14 [AgdaAny]
v15 T_Lex_32
v16 T_Lex_32
v17
du_trans_144 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_trans_144 :: T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_trans_144 T_IsEquivalence_26
v0 T_Σ_14
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 [AgdaAny]
v5 T_Lex_32
v6 T_Lex_32
v7
  = case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v6 of
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42 AgdaAny
v8
        -> case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v7 of
             MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42 AgdaAny
v9
               -> T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v6
             T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48
               -> T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48
             T_Lex_32
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v7)
             (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48)
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v12
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             (:) AgdaAny
v13 [AgdaAny]
v14
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
                    (:) AgdaAny
v15 [AgdaAny]
v16
                      -> case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v7 of
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v21
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v5 of
                                  (:) AgdaAny
v22 [AgdaAny]
v23
                                    -> (AgdaAny -> T_Lex_32) -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60
                                         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v13 AgdaAny
v15 AgdaAny
v22 AgdaAny
v12 AgdaAny
v21)
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v21 T_Lex_32
v22
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v5 of
                                  (:) AgdaAny
v23 [AgdaAny]
v24
                                    -> (AgdaAny -> T_Lex_32) -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60
                                         ((T_Σ_14 -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                            T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 T_Σ_14
v1 AgdaAny
v13 AgdaAny
v15 AgdaAny
v23
                                            AgdaAny
v21 AgdaAny
v12)
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Lex_32
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v12 T_Lex_32
v13
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             (:) AgdaAny
v14 [AgdaAny]
v15
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
                    (:) AgdaAny
v16 [AgdaAny]
v17
                      -> case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v7 of
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v22
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v5 of
                                  (:) AgdaAny
v23 [AgdaAny]
v24
                                    -> (AgdaAny -> T_Lex_32) -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60
                                         ((T_Σ_14 -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                            T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v23 AgdaAny
v16 AgdaAny
v14
                                            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 T_IsEquivalence_26
v0
                                               AgdaAny
v14 AgdaAny
v16 AgdaAny
v12)
                                            AgdaAny
v22)
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v22 T_Lex_32
v23
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v5 of
                                  (:) AgdaAny
v24 [AgdaAny]
v25
                                    -> (AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> 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
v0
                                            AgdaAny
v14 AgdaAny
v16 AgdaAny
v24 AgdaAny
v12 AgdaAny
v22)
                                         ((T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                            T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_trans_144 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v15)
                                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v17) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v25) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v13) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v23))
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Lex_32
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Lex_32
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._.respects₂
d_respects'8322'_180 ::
  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.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_respects'8322'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> T_Σ_14
d_respects'8322'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsEquivalence_26
v7 T_Σ_14
v8
  = T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_respects'8322'_180 T_IsEquivalence_26
v7 T_Σ_14
v8
du_respects'8322'_180 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_respects'8322'_180 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_respects'8322'_180 T_IsEquivalence_26
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (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
             ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'185'_200 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
             ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'178'_218 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._._.resp¹
d_resp'185'_200 ::
  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.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_resp'185'_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
d_resp'185'_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsEquivalence_26
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 [AgdaAny]
v12
                T_Pointwise_48
v13 T_Lex_32
v14
  = T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'185'_200 T_IsEquivalence_26
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v10 [AgdaAny]
v11 [AgdaAny]
v12 T_Pointwise_48
v13 T_Lex_32
v14
du_resp'185'_200 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_resp'185'_200 :: T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'185'_200 T_IsEquivalence_26
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 [AgdaAny]
v2 [AgdaAny]
v3 [AgdaAny]
v4 T_Pointwise_48
v5 T_Lex_32
v6
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v5 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v6
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v11 T_Pointwise_48
v12
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             (:) AgdaAny
v13 [AgdaAny]
v14
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
                    (:) AgdaAny
v15 [AgdaAny]
v16
                      -> case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v6 of
                           T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48
                             -> T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v21
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                                  (:) AgdaAny
v22 [AgdaAny]
v23
                                    -> (AgdaAny -> T_Lex_32) -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60
                                         ((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
v22 AgdaAny
v13 AgdaAny
v15 AgdaAny
v11 AgdaAny
v21)
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v21 T_Lex_32
v22
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                                  (:) AgdaAny
v23 [AgdaAny]
v24
                                    -> (AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> 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
v0
                                            AgdaAny
v23 AgdaAny
v13 AgdaAny
v15 AgdaAny
v21 AgdaAny
v11)
                                         ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                            T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'185'_200 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v24) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14)
                                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v16) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v12) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v22))
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Lex_32
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._._.resp²
d_resp'178'_218 ::
  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.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_resp'178'_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
d_resp'178'_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsEquivalence_26
v7 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 [AgdaAny]
v12
                T_Pointwise_48
v13 T_Lex_32
v14
  = T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'178'_218 T_IsEquivalence_26
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 [AgdaAny]
v12 T_Pointwise_48
v13 T_Lex_32
v14
du_resp'178'_218 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_resp'178'_218 :: T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'178'_218 T_IsEquivalence_26
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 [AgdaAny]
v2 [AgdaAny]
v3 [AgdaAny]
v4 T_Pointwise_48
v5 T_Lex_32
v6
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v5 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v6
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v11 T_Pointwise_48
v12
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             (:) AgdaAny
v13 [AgdaAny]
v14
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
                    (:) AgdaAny
v15 [AgdaAny]
v16
                      -> case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v6 of
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v21
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                                  (:) AgdaAny
v22 [AgdaAny]
v23
                                    -> (AgdaAny -> T_Lex_32) -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60
                                         ((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
v22 AgdaAny
v13 AgdaAny
v15 AgdaAny
v11 AgdaAny
v21)
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v21 T_Lex_32
v22
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                                  (:) AgdaAny
v23 [AgdaAny]
v24
                                    -> (AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                                         AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> 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
v0
                                            AgdaAny
v15 AgdaAny
v13 AgdaAny
v23
                                            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 T_IsEquivalence_26
v0
                                               AgdaAny
v13 AgdaAny
v15 AgdaAny
v11)
                                            AgdaAny
v21)
                                         ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                            T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Lex_32
du_resp'178'_218 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v24) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14)
                                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v16) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v12) (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
v22))
                                  [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Lex_32
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._.[]<[]-⇔
d_'91''93''60''91''93''45''8660'_234 ::
  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.Function.Bundles.T_Equivalence_1714
d_'91''93''60''91''93''45''8660'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Equivalence_1714
d_'91''93''60''91''93''45''8660'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6
  = T_Equivalence_1714
du_'91''93''60''91''93''45''8660'_234
du_'91''93''60''91''93''45''8660'_234 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'91''93''60''91''93''45''8660'_234 :: T_Equivalence_1714
du_'91''93''60''91''93''45''8660'_234
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      ((AgdaAny -> T_Lex_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42)
      ((T_Lex_32 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Lex_32 -> AgdaAny
du_'46'extendedlambda0_236)
-- Data.List.Relation.Binary.Lex._..extendedlambda0
d_'46'extendedlambda0_236 ::
  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.Data.List.Relation.Binary.Lex.Core.T_Lex_32 -> AgdaAny
d_'46'extendedlambda0_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Lex_32
-> AgdaAny
d_'46'extendedlambda0_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_Lex_32
v7
  = T_Lex_32 -> AgdaAny
du_'46'extendedlambda0_236 T_Lex_32
v7
du_'46'extendedlambda0_236 ::
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 -> AgdaAny
du_'46'extendedlambda0_236 :: T_Lex_32 -> AgdaAny
du_'46'extendedlambda0_236 T_Lex_32
v0
  = case T_Lex_32 -> T_Lex_32
forall a b. a -> b
coe T_Lex_32
v0 of
      MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42 AgdaAny
v1
        -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Lex_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex._.∷<∷-⇔
d_'8759''60''8759''45''8660'_248 ::
  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] -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8759''60''8759''45''8660'_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T_Equivalence_1714
d_'8759''60''8759''45''8660'_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny
v7
                                 ~AgdaAny
v8 ~[AgdaAny]
v9 ~[AgdaAny]
v10
  = T_Equivalence_1714
du_'8759''60''8759''45''8660'_248
du_'8759''60''8759''45''8660'_248 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8759''60''8759''45''8660'_248 :: T_Equivalence_1714
du_'8759''60''8759''45''8660'_248
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
         ((AgdaAny -> T_Lex_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60)
         (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244
            ((AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74)))
      ((T_Lex_32 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe T_Lex_32 -> T__'8846'__30
du_toSum_124)
-- Data.List.Relation.Binary.Lex._._.decidable
d_decidable_260 ::
  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) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decidable_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Dec_20
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
d_decidable_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_Dec_20
v7 AgdaAny -> AgdaAny -> T_Dec_20
v8 AgdaAny -> AgdaAny -> T_Dec_20
v9 [AgdaAny]
v10 [AgdaAny]
v11
  = T_Dec_20
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_decidable_260 T_Dec_20
v7 AgdaAny -> AgdaAny -> T_Dec_20
v8 AgdaAny -> AgdaAny -> T_Dec_20
v9 [AgdaAny]
v10 [AgdaAny]
v11
du_decidable_260 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_decidable_260 :: T_Dec_20
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_decidable_260 T_Dec_20
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2 [AgdaAny]
v3 [AgdaAny]
v4
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
             []
               -> (T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
                    T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.du_map_18
                    (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
du_'91''93''60''91''93''45''8660'_234) T_Dec_20
v0
             (:) AgdaAny
v5 [AgdaAny]
v6
               -> (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_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                       (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48))
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v5 [AgdaAny]
v6
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
             []
               -> (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)
             (:) AgdaAny
v7 [AgdaAny]
v8
               -> (T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.du_map_18
                    (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
du_'8759''60''8759''45''8660'_248)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'8846''45'dec__86
                       ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v2 AgdaAny
v5 AgdaAny
v7)
                       ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                          ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v5 AgdaAny
v7)
                          ((T_Dec_20
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Dec_20
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_decidable_260 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v8))))
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError