{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.List.Extrema.Core where

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

-- Data.List.Extrema.Core._._<_
d__'60'__96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__96 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.List.Extrema.Core._._⊓_
d__'8851'__192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8851'__192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__192 T_TotalOrder_764
v3
du__'8851'__192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__192 :: T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__192 T_TotalOrder_764
v0
  = (T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__94
      (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
-- Data.List.Extrema.Core.<-transʳ
d_'60''45'trans'691'_284 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'691'_284 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'trans'691'_284 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'691'_284 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'691'_284 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'8804''45''60''45'trans_274
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((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_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
               ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
      ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
         ((T_IsTotalOrder_404 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
            ((T_TotalOrder_764 -> T_IsTotalOrder_404) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))))
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
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_'8818''45'resp'737''45''8776'_100
               ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
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'_286 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'737'_286 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_'60''45'trans'737'_286 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'737'_286 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'737'_286 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'60''45''8804''45'trans_256
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v6 :: t
v6
                   = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe
                       T_Preorder_132 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5) 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_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v6))))))
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((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_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
               ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
      ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
         ((T_IsTotalOrder_404 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
            ((T_TotalOrder_764 -> T_IsTotalOrder_404) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))))
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
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_'8818''45'resp'691''45''8776'_106
               ((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)))))
      (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'_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8321'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8321'_302 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_302 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8321'_302 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8321'_302 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_302 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = let v7 :: t
v7
          = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
               T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
         ((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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
            ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
            ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
               (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 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'_314 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8322'_314 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8322'_314 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_314 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8322'_314 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8322'_314 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_314 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = let v7 :: t
v7
          = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
               T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
         ((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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
            ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
            ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
               (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 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'_326 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lemma'8323'_326 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8323'_326 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_326 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8323'_326 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8323'_326 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_326 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
  = (T_TotalOrder_764
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 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'_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_764 ->
  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'_338 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8324'_338 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_338 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8324'_338 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8324'_338 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_338 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
  = (T_TotalOrder_764
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 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'_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_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480'_344 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480'_344 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_344 T_TotalOrder_764
v3
du_'8851''7480'_344 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_344 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_344 T_TotalOrder_764
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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_2988
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
-- Data.List.Extrema.Core.⊔ᴸ
d_'8852''7480'_346 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480'_346 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480'_346 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_346 T_TotalOrder_764
v3
du_'8852''7480'_346 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_346 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_346 T_TotalOrder_764
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_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v2 :: t
v2
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_2988
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)))))
-- Data.List.Extrema.Core.⊓ᴸ-sel
d_'8851''7480''45'sel_350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''7480''45'sel_350 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8851''7480''45'sel_350 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_350 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_'8851''7480''45'sel_350 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''7480''45'sel_350 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_350 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
  = (T_IsSelectiveMagma_436
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_130
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.Core.⊓ᴸ-presᵒ-≤v
d_'8851''7480''45'pres'7506''45''8804'v_362 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_362 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_362 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''8804'v_362 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_362 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_362 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 ->
            (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_302 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
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_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_314 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
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_374 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'pres'7506''45''60'v_374 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
d_'8851''7480''45'pres'7506''45''60'v_374 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_374 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''60'v_374 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_374 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_374 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 ->
            (T_TotalOrder_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_326 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
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_764
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_338 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
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'_386 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_386 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'8804'_386 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_386 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_386 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_436
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
-- Data.List.Extrema.Core.⊓ᴸ-presᵇ-v<
d_'8851''7480''45'pres'7495''45'v'60'_402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  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'_402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8851''7480''45'pres'7495''45'v'60'_402 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_402 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'60'_402 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (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'_402 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_402 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
-- Data.List.Extrema.Core.⊓ᴸ-forcesᵇ-v≤
d_'8851''7480''45'forces'7495''45'v'8804'_418 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_418 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_418 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4
                                              ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_418 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'forces'7495''45'v'8804'_418 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_418 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_418 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_forces'7495'_562
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
         ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
         ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            let v7 :: t
v7
                  = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
                    ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
                       T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
                 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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
                    ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
                    ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
                       (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
                    ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 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 ->
            let v7 :: t
v7
                  = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
                    ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
                       T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
                 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_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
                    ((T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
                    ((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
                       (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
                    ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 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_434 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8852''7480''45'sel_434 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8852''7480''45'sel_434 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_434 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_'8852''7480''45'sel_434 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8852''7480''45'sel_434 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_434 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
  = (T_IsSelectiveMagma_436
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_130
      (let v2 :: t
v2
             = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v3 :: t
v3
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (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'_446 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_446 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_446 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_446 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'8804'_446 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_446 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_446 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      (let v3 :: t
v3
             = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (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 ->
            let v7 :: t
v7
                  = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
                    ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
                       T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
                 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 v8 :: t
v8
                        = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (let v9 :: t
v9
                           = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                               T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                               (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
                          ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                          ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
                          ((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 ->
            let v7 :: t
v7
                  = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
                    ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
                       T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
                 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 v8 :: t
v8
                        = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (let v9 :: t
v9
                           = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                               T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                               (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
                          ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                          ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
                          ((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'_468 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'pres'7506''45'v'60'_468 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
d_'8852''7480''45'pres'7506''45'v'60'_468 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_468 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'60'_468 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_468 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_468 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
      (let v3 :: t
v3
             = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (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_764
 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
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_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
                       ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                          (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_764
 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
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_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                         (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v8 :: t
v8
                        = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
                       ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                          (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_490 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_490 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_490 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_490 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''8804'v_490 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_490 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_490 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_436
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (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_506 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'pres'7495''45''60'v_506 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8852''7480''45'pres'7495''45''60'v_506 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
                                          ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_506 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''60'v_506 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (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_506 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_506 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
      (let v4 :: t
v4
             = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: t
v5
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (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_522 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_522 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4
                                              ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_522 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'forces'7495''45''8804'v_522 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_522 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_522 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_IsSelectiveMagma_436
 -> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_forces'7495'_562
      (let v3 :: t
v3
             = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                    (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
               ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
               ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                  (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 ->
            let v7 :: t
v7
                  = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
                    ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
                       T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
                 ((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 v8 :: t
v8
                        = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (let v9 :: t
v9
                           = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                               T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                               (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
                          ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                          ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
                          ((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 ->
            let v7 :: t
v7
                  = (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              ((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
                    ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
                       T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
                 ((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 v8 :: t
v8
                        = (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
                            T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
                            (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (let v9 :: t
v9
                           = (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
                               T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
                               (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
                          ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                          ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
                          ((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)))