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

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

-- Data.List.Extrema._._<_
d__'60'__94 ::
  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_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__94 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.List.Extrema.argmin
d_argmin_132 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmin_132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmin_132 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_argmin_132 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
  = ((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
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.argmax
d_argmax_136 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmax_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmax_136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_136 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_argmax_136 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_136 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_136 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
  = ((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
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.min
d_min_140 ::
  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_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_min_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_min_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min_140 T_TotalOrder_764
v3
du_min_140 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_min_140 :: T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min_140 T_TotalOrder_764
v0 = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.max
d_max_142 ::
  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_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_max_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_max_142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_max_142 T_TotalOrder_764
v3
du_max_142 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_max_142 :: T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_max_142 T_TotalOrder_764
v0 = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_136 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema._.f[argmin]≤v⁺
d_f'91'argmin'93''8804'v'8314'_160 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_f'91'argmin'93''8804'v'8314'_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_f'91'argmin'93''8804'v'8314'_160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_f'91'argmin'93''8804'v'8314'_160 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4252
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7506''45''8804'v_362
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.f[argmin]<v⁺
d_f'91'argmin'93''60'v'8314'_170 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_f'91'argmin'93''60'v'8314'_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_f'91'argmin'93''60'v'8314'_170 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_170 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_f'91'argmin'93''60'v'8314'_170 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_f'91'argmin'93''60'v'8314'_170 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_170 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4252
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7506''45''60'v_374
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.v≤f[argmin]⁺
d_v'8804'f'91'argmin'93''8314'_180 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_v'8804'f'91'argmin'93''8314'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_v'8804'f'91'argmin'93''8314'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                   [AgdaAny]
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_180 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_v'8804'f'91'argmin'93''8314'_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_v'8804'f'91'argmin'93''8314'_180 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_180 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4212
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7495''45'v'8804'_386
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.v<f[argmin]⁺
d_v'60'f'91'argmin'93''8314'_190 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'f'91'argmin'93''8314'_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'f'91'argmin'93''8314'_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                 [AgdaAny]
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_190 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_v'60'f'91'argmin'93''8314'_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'f'91'argmin'93''8314'_190 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_190 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4212
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7495''45'v'60'_402
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[argmin]≤f[⊤]
d_f'91'argmin'93''8804'f'91''8868''93'_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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_f'91'argmin'93''8804'f'91''8868''93'_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_f'91'argmin'93''8804'f'91''8868''93'_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                           AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_196 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'argmin'93''8804'f'91''8868''93'_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_196 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_196 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v2 [AgdaAny]
v3
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         (let v4 :: AgdaAny
v4
                = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: AgdaAny
v5
                   = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                  ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))
-- Data.List.Extrema._.f[argmin]≤f[xs]
d_f'91'argmin'93''8804'f'91'xs'93'_208 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
                                       [AgdaAny]
v8
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_208 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'argmin'93''8804'f'91'xs'93'_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_208 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_208 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
MAlonzo.Code.Data.List.Properties.du_foldr'45'forces'7495'_4190
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'forces'7495''45'v'8804'_418
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
      (let v4 :: AgdaAny
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: AgdaAny
v5
                = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
               ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))))
-- Data.List.Extrema._.f[argmin]≈f[v]⁺
d_f'91'argmin'93''8776'f'91'v'93''8314'_222 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_f'91'argmin'93''8776'f'91'v'93''8314'_222 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_f'91'argmin'93''8776'f'91'v'93''8314'_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_222
      T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
du_f'91'argmin'93''8776'f'91'v'93''8314'_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_222 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_222 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 T_All_44
v6
                                             AgdaAny
v7
  = (T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
-> 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_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
         ((T_TotalOrder_764 -> T_IsTotalOrder_404)
-> AgdaAny -> T_IsTotalOrder_404
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_132 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v3 [AgdaAny]
v4
         ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
            ((AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_50 AgdaAny
v2 [AgdaAny]
v4 T_Any_34
v5
               (let v8 :: AgdaAny
v8
                      = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v9 :: AgdaAny
v9
                         = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                        ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9))
                        ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))))
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_180 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4 AgdaAny
v7 T_All_44
v6)
-- Data.List.Extrema.argmin[xs]≤argmin[ys]⁺
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
                                                   ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248
      T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                                                    [AgdaAny]
v5 [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_180 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v2 AgdaAny
v4 [AgdaAny]
v6
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4) AgdaAny
v3 [AgdaAny]
v5 T__'8846'__30
v7)
      (((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
v9 ->
               (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v9) AgdaAny
v3 [AgdaAny]
v5))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmin[xs]<argmin[ys]⁺
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4
                                                 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276
      T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 [AgdaAny]
v5
                                                  [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_190 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v2 AgdaAny
v4 [AgdaAny]
v6
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_170 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4) AgdaAny
v3 [AgdaAny]
v5 T__'8846'__30
v7)
      (((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
v9 ->
               (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_170 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v9) AgdaAny
v3 [AgdaAny]
v5))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmin-sel
d_argmin'45'sel_292 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmin'45'sel_292 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmin'45'sel_292 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmin'45'sel_292 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_argmin'45'sel_292 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_argmin'45'sel_292 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmin'45'sel_292 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Propositional.Properties.du_foldr'45'selective_682
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'sel_350
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Data.List.Extrema.argmin-all
d_argmin'45'all_304 ::
  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_TotalOrder_764 ->
  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.Unary.All.T_All_44 -> AgdaAny
d_argmin'45'all_304 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmin'45'all_304 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 ~AgdaAny -> T_Level_18
v10 AgdaAny
v11
                    T_All_44
v12
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmin'45'all_304 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 AgdaAny
v11 T_All_44
v12
du_argmin'45'all_304 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmin'45'all_304 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmin'45'all_304 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 AgdaAny
v4 T_All_44
v5
  = let v6 :: AgdaAny
v6
          = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Setoid.Properties.du_foldr'45'selective_1712
              (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
              ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_344 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
              ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'sel_350
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v6 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
           -> ([AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_lookup_434 [AgdaAny]
v3 T_All_44
v5 AgdaAny
v7
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.List.Extrema._.v≤f[argmax]⁺
d_v'8804'f'91'argmax'93''8314'_366 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_v'8804'f'91'argmax'93''8314'_366 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_v'8804'f'91'argmax'93''8314'_366 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_v'8804'f'91'argmax'93''8314'_366 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4252
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7506''45'v'8804'_446
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.v<f[argmax]⁺
d_v'60'f'91'argmax'93''8314'_376 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'f'91'argmax'93''8314'_376 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'f'91'argmax'93''8314'_376 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_376 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_v'60'f'91'argmax'93''8314'_376 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'f'91'argmax'93''8314'_376 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_376 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4252
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7506''45'v'60'_468
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.f[argmax]≤v⁺
d_f'91'argmax'93''8804'v'8314'_386 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_f'91'argmax'93''8804'v'8314'_386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_f'91'argmax'93''8804'v'8314'_386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                   [AgdaAny]
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_386 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_f'91'argmax'93''8804'v'8314'_386 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_f'91'argmax'93''8804'v'8314'_386 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_386 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4212
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7495''45''8804'v_490
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[argmax]<v⁺
d_f'91'argmax'93''60'v'8314'_396 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_f'91'argmax'93''60'v'8314'_396 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_f'91'argmax'93''60'v'8314'_396 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                 [AgdaAny]
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_396 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_f'91'argmax'93''60'v'8314'_396 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_f'91'argmax'93''60'v'8314'_396 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_396 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4212
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7495''45''60'v_506
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[⊥]≤f[argmax]
d_f'91''8869''93''8804'f'91'argmax'93'_402 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_f'91''8869''93''8804'f'91'argmax'93'_402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_f'91''8869''93''8804'f'91'argmax'93'_402 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                           AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_402 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91''8869''93''8804'f'91'argmax'93'_402 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_402 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_402 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v2 [AgdaAny]
v3
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         (let v4 :: AgdaAny
v4
                = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: AgdaAny
v5
                   = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                  ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))
-- Data.List.Extrema._.f[xs]≤f[argmax]
d_f'91'xs'93''8804'f'91'argmax'93'_414 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_414 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_414 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
                                       [AgdaAny]
v8
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_414 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'xs'93''8804'f'91'argmax'93'_414 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_414 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_414 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
MAlonzo.Code.Data.List.Properties.du_foldr'45'forces'7495'_4190
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'forces'7495''45''8804'v_522
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_136 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
      (let v4 :: AgdaAny
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: AgdaAny
v5
                = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
               ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v1
                  (((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
                     ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))))))
-- Data.List.Extrema._.f[argmax]≈f[v]⁺
d_f'91'argmax'93''8776'f'91'v'93''8314'_428 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_f'91'argmax'93''8776'f'91'v'93''8314'_428 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_f'91'argmax'93''8776'f'91'v'93''8314'_428 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_428
      T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
du_f'91'argmax'93''8776'f'91'v'93''8314'_428 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_428 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_428 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 T_All_44
v6
                                             AgdaAny
v7
  = (T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
-> 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_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
         ((T_TotalOrder_764 -> T_IsTotalOrder_404)
-> AgdaAny -> T_IsTotalOrder_404
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_136 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_386 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4 AgdaAny
v7 T_All_44
v6)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v3 [AgdaAny]
v4
         ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
            ((AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_50 AgdaAny
v2 [AgdaAny]
v4 T_Any_34
v5
               (let v8 :: AgdaAny
v8
                      = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v9 :: AgdaAny
v9
                         = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                        ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9))
                        ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))))
-- Data.List.Extrema.argmax[xs]≤argmax[ys]⁺
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
                                                   ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454
      T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                                                    [AgdaAny]
v5 [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_386 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v5
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4 [AgdaAny]
v6 T__'8846'__30
v7)
      (((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
v9 ->
               (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v9) AgdaAny
v4 [AgdaAny]
v6))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmax[xs]<argmax[ys]⁺
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4
                                                 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482
      T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 [AgdaAny]
v5
                                                  [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_396 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v5
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_376 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4 [AgdaAny]
v6 T__'8846'__30
v7)
      (((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
v9 ->
               (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_376 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v9) AgdaAny
v4 [AgdaAny]
v6))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmax-sel
d_argmax'45'sel_498 ::
  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_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmax'45'sel_498 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmax'45'sel_498 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmax'45'sel_498 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_argmax'45'sel_498 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_argmax'45'sel_498 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmax'45'sel_498 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Propositional.Properties.du_foldr'45'selective_682
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'sel_434
         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Data.List.Extrema.argmax-all
d_argmax'45'all_510 ::
  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_TotalOrder_764 ->
  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.Unary.All.T_All_44 -> AgdaAny
d_argmax'45'all_510 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmax'45'all_510 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny
v7 ~AgdaAny -> T_Level_18
v8 AgdaAny
v9 [AgdaAny]
v10 AgdaAny
v11
                    T_All_44
v12
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmax'45'all_510 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v7 AgdaAny
v9 [AgdaAny]
v10 AgdaAny
v11 T_All_44
v12
du_argmax'45'all_510 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmax'45'all_510 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmax'45'all_510 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 AgdaAny
v4 T_All_44
v5
  = let v6 :: AgdaAny
v6
          = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Setoid.Properties.du_foldr'45'selective_1712
              (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
              ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_346 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1)
              ((T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'sel_434
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v6 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
           -> ([AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_lookup_434 [AgdaAny]
v3 T_All_44
v5 AgdaAny
v7
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.List.Extrema.min≤v⁺
d_min'8804'v'8314'_564 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_min'8804'v'8314'_564 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_min'8804'v'8314'_564 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4
  = T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_564 T_TotalOrder_764
v3 AgdaAny
v4
du_min'8804'v'8314'_564 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_564 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_564 T_TotalOrder_764
v0 AgdaAny
v1
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_160 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.min<v⁺
d_min'60'v'8314'_574 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'60'v'8314'_574 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_min'60'v'8314'_574 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4
  = T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_min'60'v'8314'_574 T_TotalOrder_764
v3 AgdaAny
v4
du_min'60'v'8314'_574 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_min'60'v'8314'_574 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_min'60'v'8314'_574 T_TotalOrder_764
v0 AgdaAny
v1
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_170 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.v≤min⁺
d_v'8804'min'8314'_584 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_v'8804'min'8314'_584 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_v'8804'min'8314'_584 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_v'8804'min'8314'_584 T_TotalOrder_764
v3 AgdaAny
v5 [AgdaAny]
v6
du_v'8804'min'8314'_584 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_v'8804'min'8314'_584 :: T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_v'8804'min'8314'_584 T_TotalOrder_764
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_180 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.v<min⁺
d_v'60'min'8314'_594 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'min'8314'_594 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'min'8314'_594 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_v'60'min'8314'_594 T_TotalOrder_764
v3 AgdaAny
v5 [AgdaAny]
v6
du_v'60'min'8314'_594 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'min'8314'_594 :: T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_v'60'min'8314'_594 T_TotalOrder_764
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_190 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.min≤⊤
d_min'8804''8868'_600 ::
  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_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_min'8804''8868'_600 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_min'8804''8868'_600 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_600 T_TotalOrder_764
v3
du_min'8804''8868'_600 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_600 :: T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_600 T_TotalOrder_764
v0
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_196 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min≤xs
d_min'8804'xs_608 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_min'8804'xs_608 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_min'8804'xs_608 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> T_All_44
du_min'8804'xs_608 T_TotalOrder_764
v3
du_min'8804'xs_608 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_min'8804'xs_608 :: T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> T_All_44
du_min'8804'xs_608 T_TotalOrder_764
v0
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_208 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min≈v⁺
d_min'8776'v'8314'_618 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_min'8776'v'8314'_618 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_min'8776'v'8314'_618 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_min'8776'v'8314'_618 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
du_min'8776'v'8314'_618 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_min'8776'v'8314'_618 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_min'8776'v'8314'_618 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T_Any_34
 -> T_All_44
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_222 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v4)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema.min[xs]≤min[ys]⁺
d_min'91'xs'93''8804'min'91'ys'93''8314'_634 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_min'91'xs'93''8804'min'91'ys'93''8314'_634 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_min'91'xs'93''8804'min'91'ys'93''8314'_634 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_634 T_TotalOrder_764
v3
du_min'91'xs'93''8804'min'91'ys'93''8314'_634 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_634 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_634 T_TotalOrder_764
v0
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_248 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min[xs]<min[ys]⁺
d_min'91'xs'93''60'min'91'ys'93''8314'_650 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_650 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_650 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_650 T_TotalOrder_764
v3
du_min'91'xs'93''60'min'91'ys'93''8314'_650 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_650 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_650 T_TotalOrder_764
v0
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_276 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min-mono-⊆
d_min'45'mono'45''8838'_660 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
d_min'45'mono'45''8838'_660 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
d_min'45'mono'45''8838'_660 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_min'45'mono'45''8838'_660 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
du_min'45'mono'45''8838'_660 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
du_min'45'mono'45''8838'_660 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_min'45'mono'45''8838'_660 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny -> T_Any_34 -> T_Any_34
v6
  = (T_TotalOrder_764
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_634 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (([AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44)
-> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tabulate_264 [AgdaAny]
v4
         (\ AgdaAny
v7 AgdaAny
v8 ->
            (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
                 (\ AgdaAny
v9 AgdaAny
v10 -> (T_TotalOrder_764 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_666 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ((AgdaAny -> T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34 -> T_Any_34
v6 AgdaAny
v7 AgdaAny
v8))))
-- Data.List.Extrema..extendedlambda0
d_'46'extendedlambda0_666 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_666 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_666 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~[AgdaAny]
v6 ~[AgdaAny]
v7 ~AgdaAny
v8 ~AgdaAny -> T_Any_34 -> T_Any_34
v9
                          AgdaAny
v10 ~T_Any_34
v11 ~AgdaAny
v12 ~T__'8801'__12
v13
  = T_TotalOrder_764 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_666 T_TotalOrder_764
v3 AgdaAny
v10
du_'46'extendedlambda0_666 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny
du_'46'extendedlambda0_666 :: T_TotalOrder_764 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_666 T_TotalOrder_764
v0 AgdaAny
v1
  = let v2 :: AgdaAny
v2
          = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v3 :: AgdaAny
v3
             = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
            ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
-- Data.List.Extrema.max≤v⁺
d_max'8804'v'8314'_676 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_max'8804'v'8314'_676 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_max'8804'v'8314'_676 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_max'8804'v'8314'_676 T_TotalOrder_764
v3 AgdaAny
v5 [AgdaAny]
v6
du_max'8804'v'8314'_676 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_max'8804'v'8314'_676 :: T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_max'8804'v'8314'_676 T_TotalOrder_764
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_386 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.max<v⁺
d_max'60'v'8314'_686 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_max'60'v'8314'_686 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_max'60'v'8314'_686 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_max'60'v'8314'_686 T_TotalOrder_764
v3 AgdaAny
v5 [AgdaAny]
v6
du_max'60'v'8314'_686 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_max'60'v'8314'_686 :: T_TotalOrder_764
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_max'60'v'8314'_686 T_TotalOrder_764
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_396 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.v≤max⁺
d_v'8804'max'8314'_696 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_v'8804'max'8314'_696 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_v'8804'max'8314'_696 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4
  = T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_696 T_TotalOrder_764
v3 AgdaAny
v4
du_v'8804'max'8314'_696 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_696 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_696 T_TotalOrder_764
v0 AgdaAny
v1
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_366 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.v<max⁺
d_v'60'max'8314'_706 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'max'8314'_706 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'max'8314'_706 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4
  = T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_v'60'max'8314'_706 T_TotalOrder_764
v3 AgdaAny
v4
du_v'60'max'8314'_706 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'max'8314'_706 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_v'60'max'8314'_706 T_TotalOrder_764
v0 AgdaAny
v1
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_376 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.⊥≤max
d_'8869''8804'max_712 ::
  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_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_'8869''8804'max_712 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_'8869''8804'max_712 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_712 T_TotalOrder_764
v3
du_'8869''8804'max_712 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_712 :: T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_712 T_TotalOrder_764
v0
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_402 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.xs≤max
d_xs'8804'max_720 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_xs'8804'max_720 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_xs'8804'max_720 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> T_All_44
du_xs'8804'max_720 T_TotalOrder_764
v3
du_xs'8804'max_720 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_xs'8804'max_720 :: T_TotalOrder_764 -> AgdaAny -> [AgdaAny] -> T_All_44
du_xs'8804'max_720 T_TotalOrder_764
v0
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_414 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.max≈v⁺
d_max'8776'v'8314'_730 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_max'8776'v'8314'_730 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_max'8776'v'8314'_730 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_max'8776'v'8314'_730 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
du_max'8776'v'8314'_730 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_max'8776'v'8314'_730 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_max'8776'v'8314'_730 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T_Any_34
 -> T_All_44
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_428 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v4)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema.max[xs]≤max[ys]⁺
d_max'91'xs'93''8804'max'91'ys'93''8314'_746 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_max'91'xs'93''8804'max'91'ys'93''8314'_746 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_max'91'xs'93''8804'max'91'ys'93''8314'_746 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_746 T_TotalOrder_764
v3 AgdaAny
v4
du_max'91'xs'93''8804'max'91'ys'93''8314'_746 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_746 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_746 T_TotalOrder_764
v0 AgdaAny
v1
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_454 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max[xs]<max[ys]⁺
d_max'91'xs'93''60'max'91'ys'93''8314'_762 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_762 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_762 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_762 T_TotalOrder_764
v3 AgdaAny
v4
du_max'91'xs'93''60'max'91'ys'93''8314'_762 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_762 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_762 T_TotalOrder_764
v0 AgdaAny
v1
  = (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_482 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max-mono-⊆
d_max'45'mono'45''8838'_772 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
d_max'45'mono'45''8838'_772 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
d_max'45'mono'45''8838'_772 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
  = T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_max'45'mono'45''8838'_772 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
du_max'45'mono'45''8838'_772 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
du_max'45'mono'45''8838'_772 :: T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_max'45'mono'45''8838'_772 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny -> T_Any_34 -> T_Any_34
v6
  = (T_TotalOrder_764
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_746 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (([AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44)
-> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tabulate_264 [AgdaAny]
v3
         (\ AgdaAny
v7 AgdaAny
v8 ->
            (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
                 (\ AgdaAny
v9 AgdaAny
v10 -> (T_TotalOrder_764 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_778 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ((AgdaAny -> T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34 -> T_Any_34
v6 AgdaAny
v7 AgdaAny
v8))))
-- Data.List.Extrema..extendedlambda1
d_'46'extendedlambda1_778 ::
  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_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_778 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_778 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~[AgdaAny]
v6 ~[AgdaAny]
v7 ~AgdaAny
v8 ~AgdaAny -> T_Any_34 -> T_Any_34
v9
                          AgdaAny
v10 ~T_Any_34
v11 ~AgdaAny
v12 ~T__'8801'__12
v13
  = T_TotalOrder_764 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_778 T_TotalOrder_764
v3 AgdaAny
v10
du_'46'extendedlambda1_778 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny
du_'46'extendedlambda1_778 :: T_TotalOrder_764 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_778 T_TotalOrder_764
v0 AgdaAny
v1
  = let v2 :: AgdaAny
v2
          = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v3 :: AgdaAny
v3
             = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
            ((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))