{-# 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.Algebra.Construct.NaturalChoice.Min 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.Bundles
import qualified MAlonzo.Code.Algebra.Bundles.Raw
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Base
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Algebra.Construct.NaturalChoice.Min._.totalPreorder
d_totalPreorder_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240
d_totalPreorder_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_TotalPreorder_240
d_totalPreorder_60 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_TotalPreorder_240
du_totalPreorder_60 T_TotalOrder_986
v3
du_totalPreorder_60 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240
du_totalPreorder_60 :: T_TotalOrder_986 -> T_TotalPreorder_240
du_totalPreorder_60 T_TotalOrder_986
v0
  = (T_TotalOrder_986 -> T_TotalPreorder_240)
-> Any -> T_TotalPreorder_240
forall a b. a -> b
coe
      T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)
-- Algebra.Construct.NaturalChoice.Min._⊓_
d__'8851'__102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d__'8851'__102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any
v5 = T_TotalOrder_986 -> Any -> Any -> Any
du__'8851'__102 T_TotalOrder_986
v3 Any
v4 Any
v5
du__'8851'__102 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__102 :: T_TotalOrder_986 -> Any -> Any -> Any
du__'8851'__102 T_TotalOrder_986
v0 Any
v1 Any
v2
  = let v3 :: Any
v3
          = (T_IsTotalOrder_488 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_488 -> Any -> Any -> Any
forall a b. a -> b
coe
              T_IsTotalOrder_488 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_498
              (T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> T_TotalOrder_986
forall a b. a -> b
coe T_TotalOrder_986
v0))
              Any
v1 Any
v2 in
    Any -> Any
forall a b. a -> b
coe
      (case Any -> T__'8846'__30
forall a b. a -> b
coe Any
v3 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v4 -> Any -> Any
forall a b. a -> b
coe Any
v1
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v4 -> Any -> Any
forall a b. a -> b
coe Any
v2
         T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Algebra.Construct.NaturalChoice.Min.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'y'8776'x_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any
v5 Any
v6
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 T_TotalOrder_986
v3 Any
v4 Any
v5 Any
v6
du_x'8804'y'8658'x'8851'y'8776'x_128 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'y'8776'x_128 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 T_TotalOrder_986
v0 Any
v1 Any
v2 Any
v3
  = let v4 :: Any
v4
          = (T_IsTotalOrder_488 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_488 -> Any -> Any -> Any
forall a b. a -> b
coe
              T_IsTotalOrder_488 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_498
              (T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> T_TotalOrder_986
forall a b. a -> b
coe T_TotalOrder_986
v0))
              Any
v1 Any
v2 in
    Any -> Any
forall a b. a -> b
coe
      (case Any -> T__'8846'__30
forall a b. a -> b
coe Any
v4 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
           -> (T_IsEquivalence_28 -> Any -> Any)
-> T_IsEquivalence_28 -> Any -> Any
forall a b. a -> b
coe
                T_IsEquivalence_28 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                (T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
                   ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> Any -> T_IsPreorder_76
forall a b. a -> b
coe
                      T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                      ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> Any -> Any
forall a b. a -> b
coe
                         T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                         ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> Any -> Any
forall a b. a -> b
coe
                            T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                            (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)))))
                Any
v1
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
           -> (T_IsPartialOrder_248 -> Any -> Any -> Any -> Any -> Any)
-> T_IsPartialOrder_248 -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_IsPartialOrder_248 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
                (T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                   ((T_TotalOrder_986 -> T_IsTotalOrder_488)
-> Any -> T_IsTotalOrder_488
forall a b. a -> b
coe
                      T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                Any
v2 Any
v1 Any
v5 Any
v3
         T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Algebra.Construct.NaturalChoice.Min.x≤y⇒y⊓x≈x
d_x'8804'y'8658'y'8851'x'8776'x_158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'y'8851'x'8776'x_158 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'y'8851'x'8776'x_158 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any
v5 Any
v6
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 T_TotalOrder_986
v3 Any
v4 Any
v5 Any
v6
du_x'8804'y'8658'y'8851'x'8776'x_158 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'y'8851'x'8776'x_158 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 T_TotalOrder_986
v0 Any
v1 Any
v2 Any
v3
  = let v4 :: Any
v4
          = (T_IsTotalOrder_488 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_488 -> Any -> Any -> Any
forall a b. a -> b
coe
              T_IsTotalOrder_488 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_498
              (T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> T_TotalOrder_986
forall a b. a -> b
coe T_TotalOrder_986
v0))
              Any
v2 Any
v1 in
    Any -> Any
forall a b. a -> b
coe
      (case Any -> T__'8846'__30
forall a b. a -> b
coe Any
v4 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
           -> (T_IsPartialOrder_248 -> Any -> Any -> Any -> Any -> Any)
-> T_IsPartialOrder_248 -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_IsPartialOrder_248 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
                (T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                   ((T_TotalOrder_986 -> T_IsTotalOrder_488)
-> Any -> T_IsTotalOrder_488
forall a b. a -> b
coe
                      T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)))
                Any
v2 Any
v1 Any
v5 Any
v3
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
           -> (T_IsEquivalence_28 -> Any -> Any)
-> T_IsEquivalence_28 -> Any -> Any
forall a b. a -> b
coe
                T_IsEquivalence_28 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                (T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
                   ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> Any -> T_IsPreorder_76
forall a b. a -> b
coe
                      T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                      ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> Any -> Any
forall a b. a -> b
coe
                         T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                         ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> Any -> Any
forall a b. a -> b
coe
                            T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                            (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)))))
                Any
v1
         T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Algebra.Construct.NaturalChoice.Min.minOperator
d_minOperator_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106
d_minOperator_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_MinOperator_106
d_minOperator_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 T_TotalOrder_986
v3
du_minOperator_184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106
du_minOperator_184 :: T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 T_TotalOrder_986
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_MinOperator_106)
-> Any -> Any -> Any -> T_MinOperator_106
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.C_constructor_136
      ((T_TotalOrder_986 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> Any -> Any -> Any
du__'8851'__102 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 ->
            (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Construct.NaturalChoice.Min._.mono-≤-distrib-⊓
d_mono'45''8804''45'distrib'45''8851'_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8851'_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
d_mono'45''8804''45'distrib'45''8851'_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8851'_188 T_TotalOrder_986
v3
du_mono'45''8804''45'distrib'45''8851'_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8851'_188 :: T_TotalOrder_986
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8851'_188 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any)
-> Any
-> Any
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_mono'45''8804''45'distrib'45''8851'_3230
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⇒x⊓z≤y
d_x'8804'y'8658'x'8851'z'8804'y_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'z'8804'y_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_190 T_TotalOrder_986
v3
du_x'8804'y'8658'x'8851'z'8804'y_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_190 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_190 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_3276
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⇒z⊓x≤y
d_x'8804'y'8658'z'8851'x'8804'y_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'z'8851'x'8804'y_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_192 T_TotalOrder_986
v3
du_x'8804'y'8658'z'8851'x'8804'y_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_192 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_192 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_3288
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⊓z⇒x≤y
d_x'8804'y'8851'z'8658'x'8804'y_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'y_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_194 T_TotalOrder_986
v3
du_x'8804'y'8851'z'8658'x'8804'y_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_194 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_194 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_3300
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⊓z⇒x≤z
d_x'8804'y'8851'z'8658'x'8804'z_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'z_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_196 T_TotalOrder_986
v3
du_x'8804'y'8851'z'8658'x'8804'z_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_196 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_196 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_3314
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≈x⇒x≤y
d_x'8851'y'8776'x'8658'x'8804'y_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'x'8658'x'8804'y_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_198 T_TotalOrder_986
v3
du_x'8851'y'8776'x'8658'x'8804'y_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_198 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_198 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≈y⇒y≤x
d_x'8851'y'8776'y'8658'y'8804'x_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'y'8658'y'8804'x_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_200 T_TotalOrder_986
v3
du_x'8851'y'8776'y'8658'y'8804'x_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_200 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_200 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≤x
d_x'8851'y'8804'x_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d_x'8851'y'8804'x_202 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'x_202 T_TotalOrder_986
v3
du_x'8851'y'8804'x_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_202 :: T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'x_202 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_2924
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≤y
d_x'8851'y'8804'y_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d_x'8851'y'8804'y_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'y_204 T_TotalOrder_986
v3
du_x'8851'y'8804'y_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_204 :: T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'y_204 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_2950
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-assoc
d_'8851''45'assoc_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_'8851''45'assoc_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_206 T_TotalOrder_986
v3
du_'8851''45'assoc_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_206 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_206 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_3060
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-band
d_'8851''45'band_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_620
d_'8851''45'band_208 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_Band_620
d_'8851''45'band_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_Band_620
du_'8851''45'band_208 T_TotalOrder_986
v3
du_'8851''45'band_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_620
du_'8851''45'band_208 :: T_TotalOrder_986 -> T_Band_620
du_'8851''45'band_208 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_Band_620)
-> Any -> Any -> T_Band_620
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_Band_620
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_3168
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-comm
d_'8851''45'comm_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d_'8851''45'comm_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du_'8851''45'comm_210 T_TotalOrder_986
v3
du_'8851''45'comm_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_210 :: T_TotalOrder_986 -> Any -> Any -> Any
du_'8851''45'comm_210 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_688
d_'8851''45'commutativeSemigroup_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_CommutativeSemigroup_688
d_'8851''45'commutativeSemigroup_212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_CommutativeSemigroup_688
du_'8851''45'commutativeSemigroup_212 T_TotalOrder_986
v3
du_'8851''45'commutativeSemigroup_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_688
du_'8851''45'commutativeSemigroup_212 :: T_TotalOrder_986 -> T_CommutativeSemigroup_688
du_'8851''45'commutativeSemigroup_212 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> T_CommutativeSemigroup_688)
-> Any -> Any -> T_CommutativeSemigroup_688
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> T_CommutativeSemigroup_688
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_3170
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-cong
d_'8851''45'cong_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_214 T_TotalOrder_986
v3
du_'8851''45'cong_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_214 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_214 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_3046
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-congʳ
d_'8851''45'cong'691'_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'691'_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_216 T_TotalOrder_986
v3
du_'8851''45'cong'691'_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_216 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_216 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_3036
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-congˡ
d_'8851''45'cong'737'_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'737'_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_218 T_TotalOrder_986
v3
du_'8851''45'cong'737'_218 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_218 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_218 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_2998
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-glb
d_'8851''45'glb_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'glb_220 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_220 T_TotalOrder_986
v3
du_'8851''45'glb_220 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_220 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_220 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_3394
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-idem
d_'8851''45'idem_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_222 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> Any -> Any
d_'8851''45'idem_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any
du_'8851''45'idem_222 T_TotalOrder_986
v3
du_'8851''45'idem_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_222 :: T_TotalOrder_986 -> Any -> Any
du_'8851''45'idem_222 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_3100
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-identity
d_'8851''45'identity_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'identity_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_224 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5
du_'8851''45'identity_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_224 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_224 T_TotalOrder_986
v0 Any
v1 Any -> Any
v2
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v3 ->
            (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v1)
              ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v3 ->
            (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v1)
              ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)))
-- Algebra.Construct.NaturalChoice.Min._.⊓-identityʳ
d_'8851''45'identity'691'_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'691'_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_226 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'identity'691'_226 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_226 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_226 T_TotalOrder_986
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v1)
      ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)
-- Algebra.Construct.NaturalChoice.Min._.⊓-identityˡ
d_'8851''45'identity'737'_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'737'_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_228 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'identity'737'_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_228 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_228 T_TotalOrder_986
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v1)
      ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)
-- Algebra.Construct.NaturalChoice.Min._.⊓-isBand
d_'8851''45'isBand_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
d_'8851''45'isBand_230 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_IsBand_526
d_'8851''45'isBand_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_IsBand_526
du_'8851''45'isBand_230 T_TotalOrder_986
v3
du_'8851''45'isBand_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
du_'8851''45'isBand_230 :: T_TotalOrder_986 -> T_IsBand_526
du_'8851''45'isBand_230 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsBand_526)
-> Any -> Any -> T_IsBand_526
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsBand_526
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_3150
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_568
d_'8851''45'isCommutativeSemigroup_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_IsCommutativeSemigroup_568
d_'8851''45'isCommutativeSemigroup_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsCommutativeSemigroup_568
du_'8851''45'isCommutativeSemigroup_232 T_TotalOrder_986
v3
du_'8851''45'isCommutativeSemigroup_232 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_568
du_'8851''45'isCommutativeSemigroup_232 :: T_TotalOrder_986 -> T_IsCommutativeSemigroup_568
du_'8851''45'isCommutativeSemigroup_232 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsCommutativeSemigroup_568)
-> Any -> Any -> T_IsCommutativeSemigroup_568
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> T_IsCommutativeSemigroup_568
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_3152
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isMagma
d_'8851''45'isMagma_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8851''45'isMagma_234 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_IsMagma_178
d_'8851''45'isMagma_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsMagma_178
du_'8851''45'isMagma_234 T_TotalOrder_986
v3
du_'8851''45'isMagma_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8851''45'isMagma_234 :: T_TotalOrder_986 -> T_IsMagma_178
du_'8851''45'isMagma_234 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsMagma_178)
-> Any -> Any -> T_IsMagma_178
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsMagma_178
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_3146
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isMonoid
d_'8851''45'isMonoid_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
d_'8851''45'isMonoid_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_IsMonoid_712
d_'8851''45'isMonoid_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_IsMonoid_712
du_'8851''45'isMonoid_236 T_TotalOrder_986
v3
du_'8851''45'isMonoid_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
du_'8851''45'isMonoid_236 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_IsMonoid_712
du_'8851''45'isMonoid_236 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> (Any -> Any) -> T_IsMonoid_712)
-> Any -> Any -> Any -> (Any -> Any) -> T_IsMonoid_712
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> (Any -> Any) -> T_IsMonoid_712
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_3158
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_450
d_'8851''45'isSelectiveMagma_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_IsSelectiveMagma_450
d_'8851''45'isSelectiveMagma_238 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsSelectiveMagma_450
du_'8851''45'isSelectiveMagma_238 T_TotalOrder_986
v3
du_'8851''45'isSelectiveMagma_238 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_450
du_'8851''45'isSelectiveMagma_238 :: T_TotalOrder_986 -> T_IsSelectiveMagma_450
du_'8851''45'isSelectiveMagma_238 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> Any -> Any -> T_IsSelectiveMagma_450
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSemigroup
d_'8851''45'isSemigroup_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8851''45'isSemigroup_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_IsSemigroup_488
d_'8851''45'isSemigroup_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsSemigroup_488
du_'8851''45'isSemigroup_240 T_TotalOrder_986
v3
du_'8851''45'isSemigroup_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8851''45'isSemigroup_240 :: T_TotalOrder_986 -> T_IsSemigroup_488
du_'8851''45'isSemigroup_240 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSemigroup_488)
-> Any -> Any -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_3148
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-magma
d_'8851''45'magma_242 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
d_'8851''45'magma_242 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_Magma_74
d_'8851''45'magma_242 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_Magma_74
du_'8851''45'magma_242 T_TotalOrder_986
v3
du_'8851''45'magma_242 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
du_'8851''45'magma_242 :: T_TotalOrder_986 -> T_Magma_74
du_'8851''45'magma_242 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_Magma_74)
-> Any -> Any -> T_Magma_74
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_Magma_74
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_3164
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-mono-≤
d_'8851''45'mono'45''8804'_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_244 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'45''8804'_244 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_244 T_TotalOrder_986
v3
du_'8851''45'mono'45''8804'_244 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_244 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_244 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_3322
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoid
d_'8851''45'monoid_246 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'8851''45'monoid_246 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_Monoid_914
d_'8851''45'monoid_246 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Monoid_914
du_'8851''45'monoid_246 T_TotalOrder_986
v3
du_'8851''45'monoid_246 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'8851''45'monoid_246 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Monoid_914
du_'8851''45'monoid_246 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> (Any -> Any) -> T_Monoid_914)
-> Any -> Any -> Any -> (Any -> Any) -> T_Monoid_914
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> (Any -> Any) -> T_Monoid_914
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_3176
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoʳ-≤
d_'8851''45'mono'691''45''8804'_248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'691''45''8804'_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_248 T_TotalOrder_986
v3
du_'8851''45'mono'691''45''8804'_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_248 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_248 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_3382
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoˡ-≤
d_'8851''45'mono'737''45''8804'_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'737''45''8804'_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_250 T_TotalOrder_986
v3
du_'8851''45'mono'737''45''8804'_250 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_250 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_250 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_3372
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-rawMagma
d_'8851''45'rawMagma_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_44
d_'8851''45'rawMagma_252 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_RawMagma_44
d_'8851''45'rawMagma_252 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_RawMagma_44
du_'8851''45'rawMagma_252 T_TotalOrder_986
v3
du_'8851''45'rawMagma_252 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_44
du_'8851''45'rawMagma_252 :: T_TotalOrder_986 -> T_RawMagma_44
du_'8851''45'rawMagma_252 T_TotalOrder_986
v0
  = (T_MinOperator_106 -> T_RawMagma_44) -> Any -> T_RawMagma_44
forall a b. a -> b
coe
      T_MinOperator_106 -> T_RawMagma_44
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'rawMagma_3162
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-sel
d_'8851''45'sel_254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> T__'8846'__30
d_'8851''45'sel_254 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_254 T_TotalOrder_986
v3
du_'8851''45'sel_254 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_254 :: T_TotalOrder_986 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_254 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> T__'8846'__30)
-> Any -> Any -> Any -> Any -> T__'8846'__30
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_3104
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-selectiveMagma
d_'8851''45'selectiveMagma_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_130
d_'8851''45'selectiveMagma_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_SelectiveMagma_130
d_'8851''45'selectiveMagma_256 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_SelectiveMagma_130
du_'8851''45'selectiveMagma_256 T_TotalOrder_986
v3
du_'8851''45'selectiveMagma_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_130
du_'8851''45'selectiveMagma_256 :: T_TotalOrder_986 -> T_SelectiveMagma_130
du_'8851''45'selectiveMagma_256 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_SelectiveMagma_130)
-> Any -> Any -> T_SelectiveMagma_130
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_SelectiveMagma_130
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_3172
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-semigroup
d_'8851''45'semigroup_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_'8851''45'semigroup_258 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_Semigroup_558
d_'8851''45'semigroup_258 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_Semigroup_558
du_'8851''45'semigroup_258 T_TotalOrder_986
v3
du_'8851''45'semigroup_258 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_'8851''45'semigroup_258 :: T_TotalOrder_986 -> T_Semigroup_558
du_'8851''45'semigroup_258 T_TotalOrder_986
v0
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semigroup_558)
-> Any -> Any -> T_Semigroup_558
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semigroup_558
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_3166
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-triangulate
d_'8851''45'triangulate_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_'8851''45'triangulate_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_260 T_TotalOrder_986
v3
du_'8851''45'triangulate_260 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_260 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_260 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_3408
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MinOperator_106
du_minOperator_184 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-zero
d_'8851''45'zero_262 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'zero_262 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_262 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5
du_'8851''45'zero_262 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_262 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_262 T_TotalOrder_986
v0 Any
v1 Any -> Any
v2
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v3 ->
            (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v3)
              ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v3 ->
            (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v3)
              ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)))
-- Algebra.Construct.NaturalChoice.Min._.⊓-zeroʳ
d_'8851''45'zero'691'_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'691'_264 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_264 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'zero'691'_264 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_264 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_264 T_TotalOrder_986
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_158 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v3)
      ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)
-- Algebra.Construct.NaturalChoice.Min._.⊓-zeroˡ
d_'8851''45'zero'737'_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'737'_266 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_266 T_TotalOrder_986
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'zero'737'_266 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_266 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_266 T_TotalOrder_986
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_128 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v3)
      ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v2 Any
v3)