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

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Construct.LiftedChoice
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Base
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Max
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Min
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd
import qualified MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.List.Extrema.Core._._<_
d__'60'__104 ::
  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_986 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__104 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__104 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.List.Extrema.Core._._⊓_
d__'8851'__124 ::
  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_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__124 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8851'__124 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__124 T_TotalOrder_986
v3
du__'8851'__124 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__124 :: T_TotalOrder_986 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__124 T_TotalOrder_986
v0
  = (T_TotalOrder_986 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__102
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
-- Data.List.Extrema.Core.<-transʳ
d_'60''45'trans'691'_138 ::
  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_986 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'691'_138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'trans'691'_138 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_138 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'691'_138 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'691'_138 :: T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_138 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'8804''45''60''45'trans_274
      ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
               ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                  (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))))
      ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'737''45''8776'_106
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
               ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                  (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
-- Data.List.Extrema.Core.<-transˡ
d_'60''45'trans'737'_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_986 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'737'_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_'60''45'trans'737'_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_140 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'737'_140 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'737'_140 :: T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_140 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'60''45''8804''45'trans_256
      ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
               ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                  ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                     (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))))
      ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
               ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                  (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))))
      ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'691''45''8776'_112
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
               ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                  (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
-- Data.List.Extrema.Core._.lemma₁
d_lemma'8321'_156 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8321'_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8321'_156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_156 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8321'_156 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8321'_156 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_156 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
      (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v4
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
      AgdaAny
v5
-- Data.List.Extrema.Core._.lemma₂
d_lemma'8322'_168 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8322'_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8322'_168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_168 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8322'_168 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8322'_168 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_168 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
      (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
      AgdaAny
v5
-- Data.List.Extrema.Core._.lemma₃
d_lemma'8323'_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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lemma'8323'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8323'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_180 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8323'_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8323'_180 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_180 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
  = (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_138 T_TotalOrder_986
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v4
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
      T_Σ_14
v5
-- Data.List.Extrema.Core._.lemma₄
d_lemma'8324'_192 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lemma'8324'_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8324'_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_192 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8324'_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8324'_192 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_192 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
  = (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_138 T_TotalOrder_986
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
      T_Σ_14
v5
-- Data.List.Extrema.Core.⊓ᴸ
d_'8851''7480'_198 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480'_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480'_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_198 T_TotalOrder_986
v3
du_'8851''7480'_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_198 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_198 T_TotalOrder_986
v0
  = ((AgdaAny -> AgdaAny -> T__'8846'__30)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_Lift_30
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_3104
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
-- Data.List.Extrema.Core.⊔ᴸ
d_'8852''7480'_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480'_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480'_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_200 T_TotalOrder_986
v3
du_'8852''7480'_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_200 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_200 T_TotalOrder_986
v0
  = ((AgdaAny -> AgdaAny -> T__'8846'__30)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_Lift_30
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_3104
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
-- Data.List.Extrema.Core.⊓ᴸ-sel
d_'8851''7480''45'sel_204 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''7480''45'sel_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8851''7480''45'sel_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_204 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6
du_'8851''7480''45'sel_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''7480''45'sel_204 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_204 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_130
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.Core.⊓ᴸ-presᵒ-≤v
d_'8851''7480''45'pres'7506''45''8804'v_216 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_216 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''8804'v_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_216 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_216 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 ->
            (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_156 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 ->
            (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_168 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
-- Data.List.Extrema.Core.⊓ᴸ-presᵒ-<v
d_'8851''7480''45'pres'7506''45''60'v_228 ::
  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_986 ->
  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_'8851''7480''45'pres'7506''45''60'v_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
d_'8851''7480''45'pres'7506''45''60'v_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_228 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''60'v_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_228 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_228 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 ->
            (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_180 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 ->
            (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_192 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
-- Data.List.Extrema.Core.⊓ᴸ-presᵇ-v≤
d_'8851''7480''45'pres'7495''45'v'8804'_240 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_240 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'8804'_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_240 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_240 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
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.Core.⊓ᴸ-presᵇ-v<
d_'8851''7480''45'pres'7495''45'v'60'_256 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'pres'7495''45'v'60'_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8851''7480''45'pres'7495''45'v'60'_256 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_256 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'60'_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_256 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_256 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
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.Core.⊓ᴸ-forcesᵇ-v≤
d_'8851''7480''45'forces'7495''45'v'8804'_272 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_272 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_272 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4
                                              ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_272 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'forces'7495''45'v'8804'_272 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_272 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_272 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_forces'7495'_562
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
         ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
            (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
              (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                 ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
                    T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                    ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
              AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
                 ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                    (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
                 ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
                    (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
              (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                 ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
                    T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                    ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
              AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v5
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
                 ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                    (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
                 ((T_TotalOrder_986 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_986 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_184
                    (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
-- Data.List.Extrema.Core.⊔ᴸ-sel
d_'8852''7480''45'sel_288 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8852''7480''45'sel_288 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8852''7480''45'sel_288 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_288 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6
du_'8852''7480''45'sel_288 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8852''7480''45'sel_288 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_288 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_130
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.Core.⊔ᴸ-presᵒ-v≤
d_'8852''7480''45'pres'7506''45'v'8804'_300 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_300 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_300 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_300 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'8804'_300 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_300 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_300 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
              (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                 ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
                    T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                    ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
              AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
                 ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
                    ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
                    ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
              (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                 ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
                    T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                    ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
              AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v5
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
                 ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
                    ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
                    ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
-- Data.List.Extrema.Core.⊔ᴸ-presᵒ-v<
d_'8852''7480''45'pres'7506''45'v'60'_322 ::
  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_986 ->
  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_'8852''7480''45'pres'7506''45'v'60'_322 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
d_'8852''7480''45'pres'7506''45'v'60'_322 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_322 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'60'_322 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_322 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_322 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_140 T_TotalOrder_986
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
                 ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
                    ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
                    ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_986
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_140 T_TotalOrder_986
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v5
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
                 ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
                    ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
                    ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
-- Data.List.Extrema.Core.⊔ᴸ-presᵇ-≤v
d_'8852''7480''45'pres'7495''45''8804'v_344 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_344 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_344 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_344 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''8804'v_344 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_344 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_344 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
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.Core.⊔ᴸ-presᵇ-<v
d_'8852''7480''45'pres'7495''45''60'v_360 ::
  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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'pres'7495''45''60'v_360 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8852''7480''45'pres'7495''45''60'v_360 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_360 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''60'v_360 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_360 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_360 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
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.Core.⊔ᴸ-forcesᵇ-≤v
d_'8852''7480''45'forces'7495''45''8804'v_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_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_376 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_376 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4
                                              ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_376 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'forces'7495''45''8804'v_376 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_376 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_376 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_450
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_IsSelectiveMagma_450
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_forces'7495'_562
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
              (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                 ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
                    T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                    ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
              ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v2
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
                 ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
                    ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
                    ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
              AgdaAny
v5))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
              (T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                 ((T_IsTotalOrder_488 -> T_IsPartialOrder_248)
-> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
                    T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                    ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
              ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v2
              ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
                 ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
                    ((T_TotalOrder_986 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
                    ((T_TotalOrder_986 -> T_MaxOperator_138) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_986 -> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_194
                       (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
              AgdaAny
v5))