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

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.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.Base
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.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core

-- Data.List.Relation.Binary.Pointwise.isEquivalence
d_isEquivalence_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsEquivalence_26
d_isEquivalence_56 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_56 T_IsEquivalence_26
v4
du_isEquivalence_56 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_56 :: T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_56 T_IsEquivalence_26
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48)
-> AgdaAny -> AgdaAny
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_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> 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.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_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny
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_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
-- Data.List.Relation.Binary.Pointwise.isDecEquivalence
d_isDecEquivalence_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
d_isDecEquivalence_76 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsDecEquivalence_44
v4
  = T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_isDecEquivalence_76 T_IsDecEquivalence_44
v4
du_isDecEquivalence_76 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_isDecEquivalence_76 :: T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_isDecEquivalence_76 T_IsDecEquivalence_44
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_56
         ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
            (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
         ((T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0)))
-- Data.List.Relation.Binary.Pointwise.isPreorder
d_isPreorder_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPreorder_70
-> T_IsPreorder_70
d_isPreorder_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsPreorder_70
v6 = T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_100 T_IsPreorder_70
v6
du_isPreorder_100 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_100 :: T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_100 T_IsPreorder_70
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_56
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
      (((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.Properties.du_reflexive_28
         (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny
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_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
-- Data.List.Relation.Binary.Pointwise.isPartialOrder
d_isPartialOrder_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_isPartialOrder_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPartialOrder_174
-> T_IsPartialOrder_174
d_isPartialOrder_142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsPartialOrder_174
v6
  = T_IsPartialOrder_174 -> T_IsPartialOrder_174
du_isPartialOrder_142 T_IsPartialOrder_174
v6
du_isPartialOrder_142 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_isPartialOrder_142 :: T_IsPartialOrder_174 -> T_IsPartialOrder_174
du_isPartialOrder_142 T_IsPartialOrder_174
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      ((T_IsPreorder_70 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_100
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (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_antisymmetric_64
         ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0)))
-- Data.List.Relation.Binary.Pointwise.setoid
d_setoid_188 ::
  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_setoid_188 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44
d_setoid_188 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Setoid_44
du_setoid_188 T_Setoid_44
v2
du_setoid_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_setoid_188 :: T_Setoid_44 -> T_Setoid_44
du_setoid_188 T_Setoid_44
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
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.Pointwise.decSetoid
d_decSetoid_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_decSetoid_192 :: T_Level_18 -> T_Level_18 -> T_DecSetoid_84 -> T_DecSetoid_84
d_decSetoid_192 ~T_Level_18
v0 ~T_Level_18
v1 T_DecSetoid_84
v2 = T_DecSetoid_84 -> T_DecSetoid_84
du_decSetoid_192 T_DecSetoid_84
v2
du_decSetoid_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
du_decSetoid_192 :: T_DecSetoid_84 -> T_DecSetoid_84
du_decSetoid_192 T_DecSetoid_84
v0
  = (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1389
      ((T_IsDecEquivalence_44 -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_isDecEquivalence_76
         ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
            (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0)))
-- Data.List.Relation.Binary.Pointwise.preorder
d_preorder_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_196 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_preorder_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_Preorder_132
du_preorder_196 T_Preorder_132
v3
du_preorder_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_196 :: T_Preorder_132 -> T_Preorder_132
du_preorder_196 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
      ((T_IsPreorder_70 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_100
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Data.List.Relation.Binary.Pointwise.poset
d_poset_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_poset_200 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_Poset_314
d_poset_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 = T_Poset_314 -> T_Poset_314
du_poset_200 T_Poset_314
v3
du_poset_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_poset_200 :: T_Poset_314 -> T_Poset_314
du_poset_200 T_Poset_314
v0
  = (T_IsPartialOrder_174 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      ((T_IsPartialOrder_174 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174 -> T_IsPartialOrder_174
du_isPartialOrder_142
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
            (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
-- Data.List.Relation.Binary.Pointwise.All-resp-Pointwise
d_All'45'resp'45'Pointwise_206 ::
  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] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_All'45'resp'45'Pointwise_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_All_44
-> T_All_44
d_All'45'resp'45'Pointwise_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9
                               T_All_44
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_All_44 -> T_All_44
du_All'45'resp'45'Pointwise_206 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9 T_All_44
v10
du_All'45'resp'45'Pointwise_206 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_All'45'resp'45'Pointwise_206 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_All_44 -> T_All_44
du_All'45'resp'45'Pointwise_206 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 T_Pointwise_48
v3 T_All_44
v4
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v3 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v4)
             (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50)
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v9 T_Pointwise_48
v10
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v11 [AgdaAny]
v12
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                    (:) AgdaAny
v13 [AgdaAny]
v14
                      -> case T_All_44 -> T_All_44
forall a b. a -> b
coe T_All_44
v4 of
                           MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 AgdaAny
v17 T_All_44
v18
                             -> (AgdaAny -> T_All_44 -> T_All_44) -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
                                  AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
                                  ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v11 AgdaAny
v13 AgdaAny
v9 AgdaAny
v17)
                                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_All_44
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_All_44 -> T_All_44
du_All'45'resp'45'Pointwise_206 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14)
                                     (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v10) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v18))
                           T_All_44
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Any-resp-Pointwise
d_Any'45'resp'45'Pointwise_222 ::
  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] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
d_Any'45'resp'45'Pointwise_222 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Any_34
-> T_Any_34
d_Any'45'resp'45'Pointwise_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9
                               T_Any_34
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Any_34 -> T_Any_34
du_Any'45'resp'45'Pointwise_222 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9 T_Any_34
v10
du_Any'45'resp'45'Pointwise_222 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
du_Any'45'resp'45'Pointwise_222 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Any_34 -> T_Any_34
du_Any'45'resp'45'Pointwise_222 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 T_Pointwise_48
v3 T_Any_34
v4
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v3 of
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v9 T_Pointwise_48
v10
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v11 [AgdaAny]
v12
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                    (:) AgdaAny
v13 [AgdaAny]
v14
                      -> case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v4 of
                           MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 AgdaAny
v17
                             -> (AgdaAny -> T_Any_34) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
                                  AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                                  ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v11 AgdaAny
v13 AgdaAny
v9 AgdaAny
v17)
                           MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 T_Any_34
v17
                             -> (T_Any_34 -> T_Any_34) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
                                  T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54
                                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Any_34
 -> T_Any_34)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Any_34 -> T_Any_34
du_Any'45'resp'45'Pointwise_222 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14)
                                     (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v10) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v17))
                           T_Any_34
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.AllPairs-resp-Pointwise
d_AllPairs'45'resp'45'Pointwise_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  [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_AllPairs'45'resp'45'Pointwise_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
d_AllPairs'45'resp'45'Pointwise_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_Σ_14
v6 [AgdaAny]
v7
                                    [AgdaAny]
v8 T_Pointwise_48
v9 T_AllPairs_20
v10
  = T_Σ_14
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
du_AllPairs'45'resp'45'Pointwise_240 T_Σ_14
v6 [AgdaAny]
v7 [AgdaAny]
v8 T_Pointwise_48
v9 T_AllPairs_20
v10
du_AllPairs'45'resp'45'Pointwise_240 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  [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_AllPairs'45'resp'45'Pointwise_240 :: T_Σ_14
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
du_AllPairs'45'resp'45'Pointwise_240 T_Σ_14
v0 [AgdaAny]
v1 [AgdaAny]
v2 T_Pointwise_48
v3 T_AllPairs_20
v4
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v3 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_AllPairs_20
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_AllPairs_20 -> AgdaAny
forall a b. a -> b
coe T_AllPairs_20
v4)
             (T_AllPairs_20 -> AgdaAny
forall a b. a -> b
coe
                T_AllPairs_20
MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22)
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v9 T_Pointwise_48
v10
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v11 [AgdaAny]
v12
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                    (:) AgdaAny
v13 [AgdaAny]
v14
                      -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                             -> case T_AllPairs_20 -> T_AllPairs_20
forall a b. a -> b
coe T_AllPairs_20
v4 of
                                  MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 T_All_44
v19 T_AllPairs_20
v20
                                    -> (T_All_44 -> T_AllPairs_20 -> T_AllPairs_20)
-> AgdaAny -> AgdaAny -> T_AllPairs_20
forall a b. a -> b
coe
                                         T_All_44 -> T_AllPairs_20 -> T_AllPairs_20
MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28
                                         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_All_44
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_All_44 -> T_All_44
du_All'45'resp'45'Pointwise_206 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15 AgdaAny
v13) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12)
                                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v10)
                                            (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
                                               ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v21 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16 AgdaAny
v21 AgdaAny
v11 AgdaAny
v13 AgdaAny
v9)) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12)
                                               (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v19)))
                                         ((T_Σ_14
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_AllPairs_20
 -> T_AllPairs_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            T_Σ_14
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_AllPairs_20
-> T_AllPairs_20
du_AllPairs'45'resp'45'Pointwise_240 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12)
                                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v10) (T_AllPairs_20 -> AgdaAny
forall a b. a -> b
coe T_AllPairs_20
v20))
                                  T_AllPairs_20
_ -> T_AllPairs_20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> T_AllPairs_20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_AllPairs_20
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_AllPairs_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_AllPairs_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Pointwise-length
d_Pointwise'45'length_256 ::
  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.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_Pointwise'45'length_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T__'8801'__12
d_Pointwise'45'length_256 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T__'8801'__12
forall a. a
erased
-- Data.List.Relation.Binary.Pointwise.tabulate⁺
d_tabulate'8314'_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  Integer ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_tabulate'8314'_270 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> Integer
-> (T_Fin_10 -> AgdaAny)
-> (T_Fin_10 -> AgdaAny)
-> (T_Fin_10 -> AgdaAny)
-> T_Pointwise_48
d_tabulate'8314'_270 ~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 Integer
v6 ~T_Fin_10 -> AgdaAny
v7 ~T_Fin_10 -> AgdaAny
v8 T_Fin_10 -> AgdaAny
v9
  = Integer -> (T_Fin_10 -> AgdaAny) -> T_Pointwise_48
du_tabulate'8314'_270 Integer
v6 T_Fin_10 -> AgdaAny
v9
du_tabulate'8314'_270 ::
  Integer ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_tabulate'8314'_270 :: Integer -> (T_Fin_10 -> AgdaAny) -> T_Pointwise_48
du_tabulate'8314'_270 Integer
v0 T_Fin_10 -> AgdaAny
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
             T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
             ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                ((T_Fin_10 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> AgdaAny
v1 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                ((Integer -> (T_Fin_10 -> AgdaAny) -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Integer -> (T_Fin_10 -> AgdaAny) -> T_Pointwise_48
du_tabulate'8314'_270 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                   ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                      (\ AgdaAny
v3 -> (T_Fin_10 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> AgdaAny
v1 ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16 AgdaAny
v3)))))
-- Data.List.Relation.Binary.Pointwise.tabulate⁻
d_tabulate'8315'_286 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  Integer ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
d_tabulate'8315'_286 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> Integer
-> (T_Fin_10 -> AgdaAny)
-> (T_Fin_10 -> AgdaAny)
-> T_Pointwise_48
-> T_Fin_10
-> AgdaAny
d_tabulate'8315'_286 ~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 ~Integer
v6 ~T_Fin_10 -> AgdaAny
v7 ~T_Fin_10 -> AgdaAny
v8 T_Pointwise_48
v9 T_Fin_10
v10
  = T_Pointwise_48 -> T_Fin_10 -> AgdaAny
du_tabulate'8315'_286 T_Pointwise_48
v9 T_Fin_10
v10
du_tabulate'8315'_286 ::
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
du_tabulate'8315'_286 :: T_Pointwise_48 -> T_Fin_10 -> AgdaAny
du_tabulate'8315'_286 T_Pointwise_48
v0 T_Fin_10
v1
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v0 of
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v6 T_Pointwise_48
v7
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
               -> (T_Pointwise_48 -> T_Fin_10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48 -> T_Fin_10 -> AgdaAny
du_tabulate'8315'_286 (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v7) (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
             T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.++⁺
d_'43''43''8314'_302 ::
  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] ->
  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'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'43''43''8314'_302 ~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]
v6 [AgdaAny]
v7 ~[AgdaAny]
v8 ~[AgdaAny]
v9 T_Pointwise_48
v10 T_Pointwise_48
v11
  = [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''8314'_302 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v10 T_Pointwise_48
v11
du_'43''43''8314'_302 ::
  [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'_302 :: [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''8314'_302 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2 T_Pointwise_48
v3
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v3
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v8 T_Pointwise_48
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
                      -> (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_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''8314'_302 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v11) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v9) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v3))
                    [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.++-cancelˡ
d_'43''43''45'cancel'737'_314 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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_'43''43''45'cancel'737'_314 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_'43''43''45'cancel'737'_314 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~[AgdaAny]
v4 ~[AgdaAny]
v5 [AgdaAny]
v6 T_Pointwise_48
v7
  = [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'737'_314 [AgdaAny]
v6 T_Pointwise_48
v7
du_'43''43''45'cancel'737'_314 ::
  [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'_314 :: [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'737'_314 [AgdaAny]
v0 T_Pointwise_48
v1
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
      [] -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v1
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v1 of
             MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v8 T_Pointwise_48
v9
               -> ([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
du_'43''43''45'cancel'737'_314 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v9)
             T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.++-cancelʳ
d_'43''43''45'cancel'691'_328 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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_'43''43''45'cancel'691'_328 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_'43''43''45'cancel'691'_328 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~[AgdaAny]
v4 [AgdaAny]
v5 [AgdaAny]
v6 T_Pointwise_48
v7
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'691'_328 [AgdaAny]
v5 [AgdaAny]
v6 T_Pointwise_48
v7
du_'43''43''45'cancel'691'_328 ::
  [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'_328 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'691'_328 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             []
               -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
                    T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
             (:) AgdaAny
v3 [AgdaAny]
v4
               -> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny)
-> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
                    (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                    AgdaAny
forall a. a
erased
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             []
               -> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny)
-> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
                    (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                    AgdaAny
forall a. a
erased
             (:) AgdaAny
v5 [AgdaAny]
v6
               -> case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
                    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v11 T_Pointwise_48
v12
                      -> (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
v11
                           (([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''45'cancel'691'_328 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v12))
                    T_Pointwise_48
_ -> 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
-- Data.List.Relation.Binary.Pointwise.concat⁺
d_concat'8314'_362 ::
  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.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_concat'8314'_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [[AgdaAny]]
-> [[AgdaAny]]
-> T_Pointwise_48
-> T_Pointwise_48
d_concat'8314'_362 ~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]]
v6 [[AgdaAny]]
v7 T_Pointwise_48
v8
  = [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48
du_concat'8314'_362 [[AgdaAny]]
v6 [[AgdaAny]]
v7 T_Pointwise_48
v8
du_concat'8314'_362 ::
  [[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'_362 :: [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48
du_concat'8314'_362 [[AgdaAny]]
v0 [[AgdaAny]]
v1 T_Pointwise_48
v2
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v7 T_Pointwise_48
v8
        -> case [[AgdaAny]] -> [AgdaAny]
forall a b. a -> b
coe [[AgdaAny]]
v0 of
             (:) AgdaAny
v9 [AgdaAny]
v10
               -> case [[AgdaAny]] -> [AgdaAny]
forall a b. a -> b
coe [[AgdaAny]]
v1 of
                    (:) AgdaAny
v11 [AgdaAny]
v12
                      -> ([AgdaAny]
 -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
                           [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'43''43''8314'_302 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)
                           (([[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48
du_concat'8314'_362 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v10) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v8))
                    [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.reverseAcc⁺
d_reverseAcc'8314'_368 ::
  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] ->
  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_reverseAcc'8314'_368 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_reverseAcc'8314'_368 ~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]
v6 ~[AgdaAny]
v7 [AgdaAny]
v8 [AgdaAny]
v9 T_Pointwise_48
v10
                       T_Pointwise_48
v11
  = [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_reverseAcc'8314'_368 [AgdaAny]
v8 [AgdaAny]
v9 T_Pointwise_48
v10 T_Pointwise_48
v11
du_reverseAcc'8314'_368 ::
  [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_reverseAcc'8314'_368 :: [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_reverseAcc'8314'_368 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2 T_Pointwise_48
v3
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v3 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v8 T_Pointwise_48
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
                      -> ([AgdaAny]
 -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
                           [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_reverseAcc'8314'_368 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v11) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13)
                           ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> T_Pointwise_48 -> AgdaAny
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 T_Pointwise_48
v2)
                           (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v9)
                    [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.ʳ++⁺
d_'691''43''43''8314'_378 ::
  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] ->
  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'_378 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'691''43''43''8314'_378 ~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]
v6 [AgdaAny]
v7 ~[AgdaAny]
v8 ~[AgdaAny]
v9 T_Pointwise_48
v10
                          T_Pointwise_48
v11
  = [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'691''43''43''8314'_378 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v10 T_Pointwise_48
v11
du_'691''43''43''8314'_378 ::
  [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'_378 :: [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_'691''43''43''8314'_378 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2 T_Pointwise_48
v3
  = ([AgdaAny]
 -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_reverseAcc'8314'_368 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v3) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v2)
-- Data.List.Relation.Binary.Pointwise.reverse⁺
d_reverse'8314'_384 ::
  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.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_reverse'8314'_384 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_reverse'8314'_384 ~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]
v6 [AgdaAny]
v7
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_reverse'8314'_384 [AgdaAny]
v6 [AgdaAny]
v7
du_reverse'8314'_384 ::
  [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'_384 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_reverse'8314'_384 [AgdaAny]
v0 [AgdaAny]
v1
  = ([AgdaAny]
 -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny]
-> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48
du_reverseAcc'8314'_368 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
      (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)
-- Data.List.Relation.Binary.Pointwise.map⁺
d_map'8314'_394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  [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'_394 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Pointwise_48
-> T_Pointwise_48
d_map'8314'_394 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 [AgdaAny]
v10 [AgdaAny]
v11
                ~AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 T_Pointwise_48
v14
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8314'_394 [AgdaAny]
v10 [AgdaAny]
v11 T_Pointwise_48
v14
du_map'8314'_394 ::
  [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'_394 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8314'_394 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v7 T_Pointwise_48
v8
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
             (:) AgdaAny
v9 [AgdaAny]
v10
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
                    (:) AgdaAny
v11 [AgdaAny]
v12
                      -> (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
v7 (([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8314'_394 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v10) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v8))
                    [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.map⁻
d_map'8315'_416 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  [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'8315'_416 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Pointwise_48
-> T_Pointwise_48
d_map'8315'_416 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 [AgdaAny]
v10 [AgdaAny]
v11
                ~AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 T_Pointwise_48
v14
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8315'_416 [AgdaAny]
v10 [AgdaAny]
v11 T_Pointwise_48
v14
du_map'8315'_416 ::
  [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'8315'_416 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8315'_416 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
      []
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
             ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v2)
                (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))
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v5 [AgdaAny]
v6
               -> case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
                    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v11 T_Pointwise_48
v12
                      -> (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
v11 (([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_map'8315'_416 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v12))
                    T_Pointwise_48
_ -> 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
-- Data.List.Relation.Binary.Pointwise.foldr⁺
d_foldr'8314'_446 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  [AgdaAny] ->
  [AgdaAny] ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  AgdaAny
d_foldr'8314'_446 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [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'_446 ~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]
v6 [AgdaAny]
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12
                  AgdaAny
v13 T_Pointwise_48
v14
  = [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'_446 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 T_Pointwise_48
v14
du_foldr'8314'_446 ::
  [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'_446 :: [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'_446 [AgdaAny]
v0 [AgdaAny]
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 T_Pointwise_48
v8
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v8 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v13 T_Pointwise_48
v14
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
             (:) AgdaAny
v15 [AgdaAny]
v16
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
                    (:) AgdaAny
v17 [AgdaAny]
v18
                      -> (AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                           AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v15 AgdaAny
v17
                           (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)
                              ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v16))
                           (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                              ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v18))
                           AgdaAny
v13
                           (([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
du_foldr'8314'_446 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v16) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v18) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4)
                              (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
v14))
                    [AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise._.filter⁺
d_filter'8314'_492 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (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.Pointwise.Base.T_Pointwise_48
d_filter'8314'_492 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_filter'8314'_492 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> T_Dec_20
v10 AgdaAny -> T_Dec_20
v11
                   ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 [AgdaAny]
v14 [AgdaAny]
v15 T_Pointwise_48
v16
  = (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
du_filter'8314'_492 AgdaAny -> T_Dec_20
v10 AgdaAny -> T_Dec_20
v11 [AgdaAny]
v14 [AgdaAny]
v15 T_Pointwise_48
v16
du_filter'8314'_492 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [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'_492 :: (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
du_filter'8314'_492 AgdaAny -> T_Dec_20
v0 AgdaAny -> T_Dec_20
v1 [AgdaAny]
v2 [AgdaAny]
v3 T_Pointwise_48
v4
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v4 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v4
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v9 T_Pointwise_48
v10
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
             (:) AgdaAny
v11 [AgdaAny]
v12
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
                    (:) AgdaAny
v13 [AgdaAny]
v14
                      -> let v15 :: t
v15 = (AgdaAny -> T_Dec_20) -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v11 in
                         AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
                           (let v16 :: t
v16 = (AgdaAny -> T_Dec_20) -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1 AgdaAny
v13 in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v15 of
                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v17 T_Reflects_16
v18
                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v17
                                        then case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
                                               MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v19 T_Reflects_16
v20
                                                 -> if Bool -> Bool
forall a b. a -> b
coe Bool
v19
                                                      then (AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
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
v9
                                                             (((AgdaAny -> T_Dec_20)
 -> (AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
du_filter'8314'_492 ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0)
                                                                ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14)
                                                                (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v10))
                                                      else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v18)
                                                             ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v20)
                                                                (((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                   (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                                                                   AgdaAny
forall a. a
erased))
                                               T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                        else (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
                                                MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v19 T_Reflects_16
v20
                                                  -> if Bool -> Bool
forall a b. a -> b
coe Bool
v19
                                                       then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                              AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v18)
                                                              ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                 AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v20)
                                                                 (((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                    (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                                                                    AgdaAny
forall a. a
erased))
                                                       else ((AgdaAny -> T_Dec_20)
 -> (AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                              (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
du_filter'8314'_492 ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0) ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1)
                                                              ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v14) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v10)
                                                T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                 T_Dec_20
_ -> AgdaAny
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_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.replicate⁺
d_replicate'8314'_548 ::
  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 ->
  Integer ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_replicate'8314'_548 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> Integer
-> T_Pointwise_48
d_replicate'8314'_548 ~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
v6 ~AgdaAny
v7 AgdaAny
v8 Integer
v9
  = AgdaAny -> Integer -> T_Pointwise_48
du_replicate'8314'_548 AgdaAny
v8 Integer
v9
du_replicate'8314'_548 ::
  AgdaAny ->
  Integer ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_replicate'8314'_548 :: AgdaAny -> Integer -> T_Pointwise_48
du_replicate'8314'_548 AgdaAny
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
             T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
             ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
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
v0 ((AgdaAny -> Integer -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer -> T_Pointwise_48
du_replicate'8314'_548 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)))
-- Data.List.Relation.Binary.Pointwise.lookup⁻
d_lookup'8315'_560 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
   MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_lookup'8315'_560 :: T_Level_18
-> T_Level_18
-> [AgdaAny]
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T__'8801'__12
-> (T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
-> T_Pointwise_48
d_lookup'8315'_560 ~T_Level_18
v0 ~T_Level_18
v1 [AgdaAny]
v2 ~T_Level_18
v3 ~T_Level_18
v4 [AgdaAny]
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~T__'8801'__12
v8 T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny
v9
  = [AgdaAny]
-> [AgdaAny]
-> (T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
-> T_Pointwise_48
du_lookup'8315'_560 [AgdaAny]
v2 [AgdaAny]
v5 T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny
v9
du_lookup'8315'_560 ::
  [AgdaAny] ->
  [AgdaAny] ->
  (MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
   MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_lookup'8315'_560 :: [AgdaAny]
-> [AgdaAny]
-> (T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
-> T_Pointwise_48
du_lookup'8315'_560 [AgdaAny]
v0 [AgdaAny]
v1 T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
      []
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
             (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)
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v5 [AgdaAny]
v6
               -> (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
                    ((T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny
v2 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) AgdaAny
forall a. a
erased)
                    (([AgdaAny]
 -> [AgdaAny]
 -> (T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       [AgdaAny]
-> [AgdaAny]
-> (T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
-> T_Pointwise_48
du_lookup'8315'_560 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6)
                       ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                          (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
                             (T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> AgdaAny
v2 ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16 AgdaAny
v7)
                               ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16 AgdaAny
v8) AgdaAny
forall a. a
erased)))
             [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.lookup⁺
d_lookup'8314'_572 ::
  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.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
d_lookup'8314'_572 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Fin_10
-> AgdaAny
d_lookup'8314'_572 ~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]
v6 [AgdaAny]
v7 T_Pointwise_48
v8 T_Fin_10
v9
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Fin_10 -> AgdaAny
du_lookup'8314'_572 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v8 T_Fin_10
v9
du_lookup'8314'_572 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
du_lookup'8314'_572 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Fin_10 -> AgdaAny
du_lookup'8314'_572 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2 T_Fin_10
v3
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v8 T_Pointwise_48
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_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v3 of
                           T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8
                           MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v15
                             -> ([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Fin_10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Fin_10 -> AgdaAny
du_lookup'8314'_572 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v11) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v9) (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v15)
                           T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
d_Pointwise'45''8801''8658''8801'_580 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_Pointwise'45''8801''8658''8801'_580 :: T_Level_18
-> T_Level_18
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T__'8801'__12
d_Pointwise'45''8801''8658''8801'_580 = T_Level_18
-> T_Level_18
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T__'8801'__12
forall a. a
erased
-- Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
d_'8801''8658'Pointwise'45''8801'_590 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8801''8658'Pointwise'45''8801'_590 :: T_Level_18
-> T_Level_18
-> [AgdaAny]
-> [AgdaAny]
-> T__'8801'__12
-> T_Pointwise_48
d_'8801''8658'Pointwise'45''8801'_590 ~T_Level_18
v0 ~T_Level_18
v1 [AgdaAny]
v2 ~[AgdaAny]
v3 ~T__'8801'__12
v4
  = [AgdaAny] -> T_Pointwise_48
du_'8801''8658'Pointwise'45''8801'_590 [AgdaAny]
v2
du_'8801''8658'Pointwise'45''8801'_590 ::
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8801''8658'Pointwise'45''8801'_590 :: [AgdaAny] -> T_Pointwise_48
du_'8801''8658'Pointwise'45''8801'_590 [AgdaAny]
v0
  = ((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
      AgdaAny
forall a. a
erased ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
-- Data.List.Relation.Binary.Pointwise.Pointwise-≡↔≡
d_Pointwise'45''8801''8596''8801'_592 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_Pointwise'45''8801''8596''8801'_592 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_Pointwise'45''8801''8596''8801'_592 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_1960
du_Pointwise'45''8801''8596''8801'_592
du_Pointwise'45''8801''8596''8801'_592 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Pointwise'45''8801''8596''8801'_592 :: T_Inverse_1960
du_Pointwise'45''8801''8596''8801'_592
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_1960)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> ([AgdaAny] -> T_Pointwise_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Pointwise_48
du_'8801''8658'Pointwise'45''8801'_590 AgdaAny
v0)
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 ->
               ([AgdaAny] -> T_Pointwise_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Pointwise_48
du_'8801''8658'Pointwise'45''8801'_590 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))