{-# 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.Equality.Setoid where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary

-- Data.List.Relation.Binary.Equality.Setoid._.AllPairs
d_AllPairs_20 :: p -> p -> p -> p -> ()
d_AllPairs_20 p
a0 p
a1 p
a2 p
a3 = ()
-- Data.List.Relation.Binary.Equality.Setoid._≋_
d__'8779'__58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] -> [AgdaAny] -> ()
d__'8779'__58 :: () -> () -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> ()
d__'8779'__58 = () -> () -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> ()
forall a. a
erased
-- Data.List.Relation.Binary.Equality.Setoid.≋-refl
d_'8779''45'refl_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8779''45'refl_60 :: () -> () -> T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48
d_'8779''45'refl_60 ~()
v0 ~()
v1 T_Setoid_44
v2 [AgdaAny]
v3 = T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48
du_'8779''45'refl_60 T_Setoid_44
v2 [AgdaAny]
v3
du_'8779''45'refl_60 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8779''45'refl_60 :: T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48
du_'8779''45'refl_60 T_Setoid_44
v0 [AgdaAny]
v1
  = ((AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_refl_30
      ((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_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)))
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
-- Data.List.Relation.Binary.Equality.Setoid.≋-reflexive
d_'8779''45'reflexive_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8779''45'reflexive_62 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T__'8801'__12
-> T_Pointwise_48
d_'8779''45'reflexive_62 ~()
v0 ~()
v1 T_Setoid_44
v2 [AgdaAny]
v3 ~[AgdaAny]
v4 ~T__'8801'__12
v5
  = T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48
du_'8779''45'reflexive_62 T_Setoid_44
v2 [AgdaAny]
v3
du_'8779''45'reflexive_62 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8779''45'reflexive_62 :: T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48
du_'8779''45'reflexive_62 T_Setoid_44
v0 [AgdaAny]
v1
  = (T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe T_Setoid_44 -> [AgdaAny] -> T_Pointwise_48
du_'8779''45'refl_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
-- Data.List.Relation.Binary.Equality.Setoid.≋-sym
d_'8779''45'sym_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8779''45'sym_64 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_'8779''45'sym_64 ~()
v0 ~()
v1 T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4 = T_Setoid_44
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'8779''45'sym_64 T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4
du_'8779''45'sym_64 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8779''45'sym_64 :: T_Setoid_44
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'8779''45'sym_64 T_Setoid_44
v0 [AgdaAny]
v1 [AgdaAny]
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_symmetric_40
      ((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_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)))
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Relation.Binary.Equality.Setoid.≋-trans
d_'8779''45'trans_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8779''45'trans_66 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'8779''45'trans_66 ~()
v0 ~()
v1 T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4 [AgdaAny]
v5
  = T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_'8779''45'trans_66 T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4 [AgdaAny]
v5
du_'8779''45'trans_66 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8779''45'trans_66 :: T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_'8779''45'trans_66 T_Setoid_44
v0 [AgdaAny]
v1 [AgdaAny]
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_transitive_50
      ((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_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)))
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Relation.Binary.Equality.Setoid.≋-isEquivalence
d_'8779''45'isEquivalence_68 ::
  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.Structures.T_IsEquivalence_26
d_'8779''45'isEquivalence_68 :: () -> () -> T_Setoid_44 -> T_IsEquivalence_26
d_'8779''45'isEquivalence_68 ~()
v0 ~()
v1 T_Setoid_44
v2
  = T_Setoid_44 -> T_IsEquivalence_26
du_'8779''45'isEquivalence_68 T_Setoid_44
v2
du_'8779''45'isEquivalence_68 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'8779''45'isEquivalence_68 :: T_Setoid_44 -> T_IsEquivalence_26
du_'8779''45'isEquivalence_68 T_Setoid_44
v0
  = (T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
      ((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))
-- Data.List.Relation.Binary.Equality.Setoid.≋-setoid
d_'8779''45'setoid_70 ::
  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
d_'8779''45'setoid_70 :: () -> () -> T_Setoid_44 -> T_Setoid_44
d_'8779''45'setoid_70 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Setoid_44
du_'8779''45'setoid_70 T_Setoid_44
v2
du_'8779''45'setoid_70 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_'8779''45'setoid_70 :: T_Setoid_44 -> T_Setoid_44
du_'8779''45'setoid_70 T_Setoid_44
v0
  = (T_Setoid_44 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_setoid_176
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
-- Data.List.Relation.Binary.Equality.Setoid.Unique-resp-≋
d_Unique'45'resp'45''8779'_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
  MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
d_Unique'45'resp'45''8779'_72 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
d_Unique'45'resp'45''8779'_72 ~()
v0 ~()
v1 T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4
  = T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
du_Unique'45'resp'45''8779'_72 T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4
du_Unique'45'resp'45''8779'_72 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
  MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
du_Unique'45'resp'45''8779'_72 :: T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
du_Unique'45'resp'45''8779'_72 T_Setoid_44
v0 [AgdaAny]
v1 [AgdaAny]
v2
  = (T_Σ_14
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_AllPairs_20
 -> T_AllPairs_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
forall a b. a -> b
coe
      T_Σ_14
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_AllPairs'45'resp'45'Pointwise_228
      ((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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
               AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny
v7
                 ((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_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                    AgdaAny
v3 AgdaAny
v5 AgdaAny
v4 AgdaAny
v8
                    ((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_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                       AgdaAny
v4 AgdaAny
v5 AgdaAny
v6))))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
               AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny
v7
                 ((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_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                    AgdaAny
v4 AgdaAny
v5 AgdaAny
v3 AgdaAny
v6 AgdaAny
v8))))
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Relation.Binary.Equality.Setoid.≋-length
d_'8779''45'length_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8779''45'length_78 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T__'8801'__12
d_'8779''45'length_78 = ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T__'8801'__12
forall a. a
erased
-- Data.List.Relation.Binary.Equality.Setoid._._≋′_
d__'8779''8242'__94 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] -> [AgdaAny] -> ()
d__'8779''8242'__94 :: T_Setoid_44
-> () -> () -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> ()
d__'8779''8242'__94 = T_Setoid_44
-> () -> () -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> ()
forall a. a
erased
-- Data.List.Relation.Binary.Equality.Setoid._.map⁺
d_map'8314'_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (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.Pointwise.Base.T_Pointwise_48
d_map'8314'_102 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_map'8314'_102 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 ~AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 [AgdaAny]
v8 [AgdaAny]
v9 T_Pointwise_48
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8314'_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 [AgdaAny]
v8 [AgdaAny]
v9 T_Pointwise_48
v10
du_map'8314'_102 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_map'8314'_102 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8314'_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 T_Pointwise_48
v3
  = ([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_map'8314'_382
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.du_map_120
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v3))
-- Data.List.Relation.Binary.Equality.Setoid.foldr⁺
d_foldr'8314'_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (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 ->
  AgdaAny
d_foldr'8314'_130 :: ()
-> ()
-> T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> AgdaAny
d_foldr'8314'_130 ~()
v0 ~()
v1 ~T_Setoid_44
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 T_Pointwise_48
v11
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> AgdaAny
du_foldr'8314'_130 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 T_Pointwise_48
v11
du_foldr'8314'_130 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (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 ->
  AgdaAny
du_foldr'8314'_130 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> AgdaAny
du_foldr'8314'_130 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 T_Pointwise_48
v8
  = ([AgdaAny]
 -> [AgdaAny]
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Pointwise_48
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> AgdaAny
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_foldr'8314'_434
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v8)
-- Data.List.Relation.Binary.Equality.Setoid.++⁺
d_'43''43''8314'_146 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'43''43''8314'_146 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'43''43''8314'_146 ~()
v0 ~()
v1 ~T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4 ~[AgdaAny]
v5 ~[AgdaAny]
v6
  = [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''8314'_146 [AgdaAny]
v3 [AgdaAny]
v4
du_'43''43''8314'_146 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'43''43''8314'_146 :: [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''8314'_146 [AgdaAny]
v0 [AgdaAny]
v1
  = ([AgdaAny]
 -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_'43''43''8314'_290
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
-- Data.List.Relation.Binary.Equality.Setoid.++-cancelˡ
d_'43''43''45'cancel'737'_154 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'43''43''45'cancel'737'_154 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_'43''43''45'cancel'737'_154 ~()
v0 ~()
v1 ~T_Setoid_44
v2 [AgdaAny]
v3 ~[AgdaAny]
v4 ~[AgdaAny]
v5
  = [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'737'_154 [AgdaAny]
v3
du_'43''43''45'cancel'737'_154 ::
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'43''43''45'cancel'737'_154 :: [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'737'_154 [AgdaAny]
v0
  = ([AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_'43''43''45'cancel'737'_302
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
-- Data.List.Relation.Binary.Equality.Setoid.++-cancelʳ
d_'43''43''45'cancel'691'_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'43''43''45'cancel'691'_164 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_'43''43''45'cancel'691'_164 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~[AgdaAny]
v3
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'691'_164
du_'43''43''45'cancel'691'_164 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'43''43''45'cancel'691'_164 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'691'_164
  = ([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_'43''43''45'cancel'691'_316
-- Data.List.Relation.Binary.Equality.Setoid.concat⁺
d_concat'8314'_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [[AgdaAny]] ->
  [[AgdaAny]] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_concat'8314'_170 :: ()
-> ()
-> T_Setoid_44
-> [[AgdaAny]]
-> [[AgdaAny]]
-> T_Pointwise_48
-> T_Pointwise_48
d_concat'8314'_170 ~()
v0 ~()
v1 ~T_Setoid_44
v2 [[AgdaAny]]
v3 [[AgdaAny]]
v4 = [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48
du_concat'8314'_170 [[AgdaAny]]
v3 [[AgdaAny]]
v4
du_concat'8314'_170 ::
  [[AgdaAny]] ->
  [[AgdaAny]] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_concat'8314'_170 :: [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48
du_concat'8314'_170 [[AgdaAny]]
v0 [[AgdaAny]]
v1
  = ([[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
      [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_concat'8314'_350
      ([[AgdaAny]] -> AgdaAny
forall a b. a -> b
coe [[AgdaAny]]
v0) ([[AgdaAny]] -> AgdaAny
forall a b. a -> b
coe [[AgdaAny]]
v1)
-- Data.List.Relation.Binary.Equality.Setoid.tabulate⁺
d_tabulate'8314'_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  Integer ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny) ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny) ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_tabulate'8314'_180 :: ()
-> ()
-> T_Setoid_44
-> Integer
-> (T_Fin_6 -> AgdaAny)
-> (T_Fin_6 -> AgdaAny)
-> (T_Fin_6 -> AgdaAny)
-> T_Pointwise_48
d_tabulate'8314'_180 ~()
v0 ~()
v1 ~T_Setoid_44
v2 Integer
v3 ~T_Fin_6 -> AgdaAny
v4 ~T_Fin_6 -> AgdaAny
v5
  = Integer -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48
du_tabulate'8314'_180 Integer
v3
du_tabulate'8314'_180 ::
  Integer ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_tabulate'8314'_180 :: Integer -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48
du_tabulate'8314'_180 Integer
v0
  = (Integer -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48)
-> AgdaAny -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48
forall a b. a -> b
coe
      Integer -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_tabulate'8314'_258
      (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0)
-- Data.List.Relation.Binary.Equality.Setoid.tabulate⁻
d_tabulate'8315'_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  Integer ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny) ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny
d_tabulate'8315'_190 :: ()
-> ()
-> T_Setoid_44
-> Integer
-> (T_Fin_6 -> AgdaAny)
-> (T_Fin_6 -> AgdaAny)
-> T_Pointwise_48
-> T_Fin_6
-> AgdaAny
d_tabulate'8315'_190 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~Integer
v3 ~T_Fin_6 -> AgdaAny
v4 ~T_Fin_6 -> AgdaAny
v5
  = T_Pointwise_48 -> T_Fin_6 -> AgdaAny
du_tabulate'8315'_190
du_tabulate'8315'_190 ::
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> AgdaAny
du_tabulate'8315'_190 :: T_Pointwise_48 -> T_Fin_6 -> AgdaAny
du_tabulate'8315'_190
  = (T_Pointwise_48 -> T_Fin_6 -> AgdaAny)
-> T_Pointwise_48 -> T_Fin_6 -> AgdaAny
forall a b. a -> b
coe
      T_Pointwise_48 -> T_Fin_6 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_tabulate'8315'_274
-- Data.List.Relation.Binary.Equality.Setoid._.filter⁺
d_filter'8314'_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_filter'8314'_208 :: ()
-> ()
-> T_Setoid_44
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_filter'8314'_208 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~AgdaAny -> ()
v4 AgdaAny -> T_Dec_32
v5 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9
  = (AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_filter'8314'_208 AgdaAny -> T_Dec_32
v5 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9
du_filter'8314'_208 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_filter'8314'_208 :: (AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_filter'8314'_208 AgdaAny -> T_Dec_32
v0 [AgdaAny]
v1 [AgdaAny]
v2 T_Pointwise_48
v3
  = ((AgdaAny -> T_Dec_32)
 -> (AgdaAny -> T_Dec_32)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
forall a b. a -> b
coe
      (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_filter'8314'_480
      ((AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0) ((AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v3)
-- Data.List.Relation.Binary.Equality.Setoid.ʳ++⁺
d_'691''43''43''8314'_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'691''43''43''8314'_220 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'691''43''43''8314'_220 ~()
v0 ~()
v1 ~T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4 ~[AgdaAny]
v5 ~[AgdaAny]
v6
  = [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'691''43''43''8314'_220 [AgdaAny]
v3 [AgdaAny]
v4
du_'691''43''43''8314'_220 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'691''43''43''8314'_220 :: [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'691''43''43''8314'_220 [AgdaAny]
v0 [AgdaAny]
v1
  = ([AgdaAny]
 -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_'691''43''43''8314'_366
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
-- Data.List.Relation.Binary.Equality.Setoid.reverse⁺
d_reverse'8314'_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_reverse'8314'_226 :: ()
-> ()
-> T_Setoid_44
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_reverse'8314'_226 ~()
v0 ~()
v1 ~T_Setoid_44
v2 [AgdaAny]
v3 [AgdaAny]
v4 = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_reverse'8314'_226 [AgdaAny]
v3 [AgdaAny]
v4
du_reverse'8314'_226 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_reverse'8314'_226 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_reverse'8314'_226 [AgdaAny]
v0 [AgdaAny]
v1
  = ([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_reverse'8314'_372
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)