{-# 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.Converse
import qualified MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.List.Extrema.Core._._<_
d__'60'__82 ::
  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_652 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__82 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__82 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.List.Extrema.Core._._⊓_
d__'8851'__182 ::
  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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8851'__182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__182 T_TotalOrder_652
v3
du__'8851'__182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__182 :: T_TotalOrder_652 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__182 T_TotalOrder_652
v0
  = (T_TotalOrder_652 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__80
      (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
-- Data.List.Extrema.Core.<-transʳ
d_'60''45'trans'691'_278 ::
  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_652 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'691'_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'trans'691'_278 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_278 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'691'_278 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'691'_278 :: T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_278 T_TotalOrder_652
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_268
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
            ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
               ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                  (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)))))
      ((T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))))
      (let v4 :: T_IsTotalOrder_384
v4
             = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: T_IsPartialOrder_162
v5
                = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'737''45''8776'_100
               ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                  (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v5)))))
      (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'_280 ::
  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_652 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'737'_280 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_'60''45'trans'737'_280 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_280 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'737'_280 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'737'_280 :: T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_280 T_TotalOrder_652
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_250
      (let v4 :: t
v4
             = (T_TotalOrder_652 -> T_Poset_282) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.du_poset_702 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_Poset_282 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                  ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5))))))
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
            ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
               ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                  (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)))))
      ((T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))))
      (let v4 :: T_IsTotalOrder_384
v4
             = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: T_IsPartialOrder_162
v5
                = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'691''45''8776'_106
               ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                  (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v5)))))
      (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'_296 ::
  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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8321'_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8321'_296 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_296 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8321'_296 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8321'_296 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_296 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
      (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_308 ::
  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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8322'_308 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8322'_308 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_308 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8322'_308 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8322'_308 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_308 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
      (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_320 ::
  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_652 ->
  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'_320 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8323'_320 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
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_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_320 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8323'_320 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8323'_320 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_320 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
  = (T_TotalOrder_652
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_278 T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_332 ::
  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_652 ->
  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'_332 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8324'_332 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
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_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_332 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8324'_332 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8324'_332 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_332 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
  = (T_TotalOrder_652
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_278 T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_338 ::
  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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480'_338 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480'_338 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_338 T_TotalOrder_652
v3
du_'8851''7480'_338 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_338 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_338 T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_1806
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)))
-- Data.List.Extrema.Core.⊔ᴸ
d_'8852''7480'_340 ::
  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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480'_340 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480'_340 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_340 T_TotalOrder_652
v3
du_'8852''7480'_340 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_340 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_340 T_TotalOrder_652
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
      (let v1 :: t
v1
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v2 :: t
v2
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_1806
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)))))
-- Data.List.Extrema.Core.⊓ᴸ-sel
d_'8851''7480''45'sel_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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''7480''45'sel_344 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8851''7480''45'sel_344 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_344 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6
du_'8851''7480''45'sel_344 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''7480''45'sel_344 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_344 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = (T_IsSelectiveMagma_158
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_134
      ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_356 ::
  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_652 ->
  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_356 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_356 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_356 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''8804'v_356 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_356 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_356 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (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'_418
      ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_296 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_308 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_368 ::
  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_652 ->
  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_368 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> 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_368 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_368 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''60'v_368 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (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_368 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_368 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (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'_418
      ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_320 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_332 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_380 ::
  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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_380 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_380 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_380 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'8804'_380 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_380 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_380 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_158
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_538
      ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_396 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  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'_396 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> 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'_396 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_396 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'60'_396 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (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'_396 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_396 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_538
      ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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'_412 ::
  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_652 ->
  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'_412 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_412 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4
                                              ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_412 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'forces'7495''45'v'8804'_412 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_412 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_412 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (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'_580
      ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
         ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
         ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                 ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
                    T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
                 ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
                 ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                 ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
                    T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
                 ((T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0))
                 ((T_TotalOrder_652 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_162
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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_428 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8852''7480''45'sel_428 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8852''7480''45'sel_428 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_428 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6
du_'8852''7480''45'sel_428 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8852''7480''45'sel_428 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_428 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = (T_IsSelectiveMagma_158
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_134
      (let v2 :: t
v2
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v3 :: t
v3
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)))))
      ((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'_440 ::
  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_652 ->
  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'_440 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_440 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_440 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'8804'_440 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_440 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_440 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (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'_418
      (let v3 :: t
v3
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
      ((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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                 ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
                    T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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
              (let v7 :: t
v7
                     = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
                       ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                       ((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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                 ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
                    T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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
              (let v7 :: t
v7
                     = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
                       ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                       ((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'_462 ::
  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_652 ->
  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'_462 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> 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'_462 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_462 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'60'_462 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (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'_462 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_462 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (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'_418
      (let v3 :: t
v3
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
      ((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_652
 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_280 T_TotalOrder_652
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
              (let v7 :: t
v7
                     = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
                       ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                       ((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_652
 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_652
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_280 T_TotalOrder_652
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
              (let v7 :: t
v7
                     = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
                       ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                       ((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_484 ::
  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_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_484 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_484 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_484 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''8804'v_484 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_484 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_484 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_158
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_538
      (let v4 :: t
v4
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))
      ((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_500 ::
  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_652 ->
  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_500 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> 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_500 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_500 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''60'v_500 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (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_500 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_500 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_538
      (let v4 :: t
v4
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))
      ((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_516 ::
  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_652 ->
  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_516 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_516 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4
                                              ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_516 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'forces'7495''45''8804'v_516 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_516 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_516 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_158
 -> (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_158
-> (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'_580
      (let v3 :: t
v3
             = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                    (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
               ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
               ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
      ((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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                 ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
                    T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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
              (let v7 :: t
v7
                     = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
                       ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                       ((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_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
                 ((T_IsTotalOrder_384 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
                    T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
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
              (let v7 :: t
v7
                     = (T_TotalOrder_652 -> T_TotalPreorder_204) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
                         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_652 -> T_MaxOperator_114) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_652 -> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_176
                            (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
                       ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                       ((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))