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

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.List.Relation.Binary.Pointwise.Properties.reflexive
d_reflexive_28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_reflexive_28 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_reflexive_28 ~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 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_reflexive_28
du_reflexive_28 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_reflexive_28 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_reflexive_28
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.du_map_120
-- Data.List.Relation.Binary.Pointwise.Properties.refl
d_refl_30 ::
  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
d_refl_30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> [AgdaAny]
-> T_Pointwise_48
d_refl_30 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny
v4 [AgdaAny]
v5 = (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48
du_refl_30 AgdaAny -> AgdaAny
v4 [AgdaAny]
v5
du_refl_30 ::
  (AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_refl_30 :: (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48
du_refl_30 AgdaAny -> AgdaAny
v0 [AgdaAny]
v1
  = 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
v2 [AgdaAny]
v3
        -> (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 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2) (((AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48
du_refl_30 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
      [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.symmetric
d_symmetric_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_symmetric_40 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
d_symmetric_40 ~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 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v9 [AgdaAny]
v10 T_Pointwise_48
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_symmetric_40 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v9 [AgdaAny]
v10 T_Pointwise_48
v11
du_symmetric_40 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_symmetric_40 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48
du_symmetric_40 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
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
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]
v1 of
             (:) AgdaAny
v10 [AgdaAny]
v11
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v12 AgdaAny
v8)
                           (((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
du_symmetric_40 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
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))
                    [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.Properties.transitive
d_transitive_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_transitive_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_transitive_50 ~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 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 [AgdaAny]
v13 [AgdaAny]
v14 [AgdaAny]
v15 T_Pointwise_48
v16 T_Pointwise_48
v17
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_transitive_50 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 [AgdaAny]
v13 [AgdaAny]
v14 [AgdaAny]
v15 T_Pointwise_48
v16 T_Pointwise_48
v17
du_transitive_50 ::
  (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 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_transitive_50 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_transitive_50 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 [AgdaAny]
v3 T_Pointwise_48
v4 T_Pointwise_48
v5
  = 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
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v5) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v4)
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v10 T_Pointwise_48
v11
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v12 [AgdaAny]
v13
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
                    (:) AgdaAny
v14 [AgdaAny]
v15
                      -> case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v5 of
                           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v20 T_Pointwise_48
v21
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
                                  (:) AgdaAny
v22 [AgdaAny]
v23
                                    -> (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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v12 AgdaAny
v14 AgdaAny
v22 AgdaAny
v10 AgdaAny
v20)
                                         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> 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
du_transitive_50 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v15) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v23)
                                            (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v11) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v21))
                                  [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
                           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
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.antisymmetric
d_antisymmetric_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (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 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_antisymmetric_64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_antisymmetric_64 ~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 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 [AgdaAny]
v11
                   [AgdaAny]
v12 T_Pointwise_48
v13 T_Pointwise_48
v14
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_antisymmetric_64 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 [AgdaAny]
v11 [AgdaAny]
v12 T_Pointwise_48
v13 T_Pointwise_48
v14
du_antisymmetric_64 ::
  (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 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_antisymmetric_64 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_antisymmetric_64 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 T_Pointwise_48
v3 T_Pointwise_48
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_Pointwise_48
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
v4) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v3)
      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_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v4 of
                           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v19 T_Pointwise_48
v20
                             -> (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 -> 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
v19)
                                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_antisymmetric_64 ((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_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v20))
                           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
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.respʳ
d_resp'691'_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  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_resp'691'_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_resp'691'_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v9 [AgdaAny]
v10 [AgdaAny]
v11 T_Pointwise_48
v12
               T_Pointwise_48
v13
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_resp'691'_78 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v9 [AgdaAny]
v10 [AgdaAny]
v11 T_Pointwise_48
v12 T_Pointwise_48
v13
du_resp'691'_78 ::
  (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 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_resp'691'_78 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_resp'691'_78 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 [AgdaAny]
v3 T_Pointwise_48
v4 T_Pointwise_48
v5
  = 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
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v5) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v4)
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v10 T_Pointwise_48
v11
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
             (:) AgdaAny
v12 [AgdaAny]
v13
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
                    (:) AgdaAny
v14 [AgdaAny]
v15
                      -> case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v5 of
                           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v20 T_Pointwise_48
v21
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
                                  (:) AgdaAny
v22 [AgdaAny]
v23
                                    -> (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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v22 AgdaAny
v12 AgdaAny
v14 AgdaAny
v10 AgdaAny
v20)
                                         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> 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
du_resp'691'_78 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v23) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v15)
                                            (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v11) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v21))
                                  [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
                           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
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.respˡ
d_resp'737'_92 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  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_resp'737'_92 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_resp'737'_92 ~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 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v9 [AgdaAny]
v10 [AgdaAny]
v11 T_Pointwise_48
v12
               T_Pointwise_48
v13
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_resp'737'_92 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 [AgdaAny]
v9 [AgdaAny]
v10 [AgdaAny]
v11 T_Pointwise_48
v12 T_Pointwise_48
v13
du_resp'737'_92 ::
  (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 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_resp'737'_92 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
du_resp'737'_92 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2 [AgdaAny]
v3 T_Pointwise_48
v4 T_Pointwise_48
v5
  = 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
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Pointwise_48
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v5) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v4)
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v10 T_Pointwise_48
v11
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
             (:) AgdaAny
v12 [AgdaAny]
v13
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
                    (:) AgdaAny
v14 [AgdaAny]
v15
                      -> case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v5 of
                           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v20 T_Pointwise_48
v21
                             -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
                                  (:) AgdaAny
v22 [AgdaAny]
v23
                                    -> (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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v22 AgdaAny
v12 AgdaAny
v14 AgdaAny
v10 AgdaAny
v20)
                                         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> 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
du_resp'737'_92 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v23) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v13) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v15)
                                            (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v11) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v21))
                                  [AgdaAny]
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
                           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
      T_Pointwise_48
_ -> T_Pointwise_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.respects₂
d_respects'8322'_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_respects'8322'_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_respects'8322'_106 ~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
  = T_Σ_14 -> T_Σ_14
du_respects'8322'_106 T_Σ_14
v6
du_respects'8322'_106 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_respects'8322'_106 :: T_Σ_14 -> T_Σ_14
du_respects'8322'_106 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
             (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> 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
du_resp'691'_78 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)) (((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
du_resp'737'_92 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.decidable
d_decidable_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decidable_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
d_decidable_112 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Dec_20
v6 [AgdaAny]
v7 [AgdaAny]
v8
  = (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_decidable_112 AgdaAny -> AgdaAny -> T_Dec_20
v6 [AgdaAny]
v7 [AgdaAny]
v8
du_decidable_112 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_decidable_112 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_decidable_112 AgdaAny -> AgdaAny -> T_Dec_20
v0 [AgdaAny]
v1 [AgdaAny]
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                       (T_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
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             (:) AgdaAny
v5 [AgdaAny]
v6
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244
                       ((AgdaAny -> T_Pointwise_48 -> 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))
                    ((T_Pointwise_48 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe
                       T_Pointwise_48 -> T_Σ_14
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.du_uncons_76)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v3 AgdaAny
v5) (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_decidable_112 ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6)))
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Pointwise.Properties.irrelevant
d_irrelevant_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  [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.Agda.Builtin.Equality.T__'8801'__12
d_irrelevant_132 :: 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__'8801'__12)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T__'8801'__12
d_irrelevant_132 = 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__'8801'__12)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Pointwise_48
-> T__'8801'__12
forall a. a
erased