{-# 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_54 ::
  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.Relation.Binary.Bundles.T_TotalPreorder_222
d_totalPreorder_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_TotalPreorder_222
d_totalPreorder_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> T_TotalPreorder_222
du_totalPreorder_54 T_TotalOrder_764
v3
du_totalPreorder_54 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222
du_totalPreorder_54 :: T_TotalOrder_764 -> T_TotalPreorder_222
du_totalPreorder_54 T_TotalOrder_764
v0
  = (T_TotalOrder_764 -> T_TotalPreorder_222)
-> Any -> T_TotalPreorder_222
forall a b. a -> b
coe
      T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0)
-- Algebra.Construct.NaturalChoice.Min._⊓_
d__'8851'__94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d__'8851'__94 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any
v5 = T_TotalOrder_764 -> Any -> Any -> Any
du__'8851'__94 T_TotalOrder_764
v3 Any
v4 Any
v5
du__'8851'__94 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__94 :: T_TotalOrder_764 -> Any -> Any -> Any
du__'8851'__94 T_TotalOrder_764
v0 Any
v1 Any
v2
  = let v3 :: t
v3
          = (T_IsTotalOrder_404 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_404 -> Any -> Any -> t
forall a b. a -> b
coe
              T_IsTotalOrder_404 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_414
              (T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> T_TotalOrder_764
forall a b. a -> b
coe T_TotalOrder_764
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
forall {t}. t
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 {t}. t
MAlonzo.RTE.mazUnreachableError)
-- Algebra.Construct.NaturalChoice.Min.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_120 ::
  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
d_x'8804'y'8658'x'8851'y'8776'x_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'y'8776'x_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any
v5 Any
v6
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 T_TotalOrder_764
v3 Any
v4 Any
v5 Any
v6
du_x'8804'y'8658'x'8851'y'8776'x_120 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'y'8776'x_120 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 T_TotalOrder_764
v0 Any
v1 Any
v2 Any
v3
  = let v4 :: t
v4
          = (T_IsTotalOrder_404 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_404 -> Any -> Any -> t
forall a b. a -> b
coe
              T_IsTotalOrder_404 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_414
              (T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> T_TotalOrder_764
forall a b. a -> b
coe T_TotalOrder_764
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
forall {t}. t
v4 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
           -> let v6 :: t
v6
                    = (T_TotalOrder_764 -> T_Poset_314) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
              Any -> Any
forall a b. a -> b
coe
                (let v7 :: t
v7
                       = (T_Poset_314 -> T_Preorder_132) -> Any -> t
forall a b. a -> b
coe
                           T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6) in
                 Any -> Any
forall a b. a -> b
coe
                   ((T_IsEquivalence_26 -> Any -> Any)
-> T_IsEquivalence_26 -> Any -> Any
forall a b. a -> b
coe
                      T_IsEquivalence_26 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                      (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
                            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v7)))
                      Any
v1))
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
           -> (T_IsPartialOrder_174 -> Any -> Any -> Any -> Any -> Any)
-> T_IsPartialOrder_174 -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_IsPartialOrder_174 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
                (T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
                   ((T_TotalOrder_764 -> T_IsTotalOrder_404)
-> Any -> T_IsTotalOrder_404
forall a b. a -> b
coe
                      T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0)))
                Any
v2 Any
v1 Any
v5 Any
v3
         T__'8846'__30
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
-- Algebra.Construct.NaturalChoice.Min.x≤y⇒y⊓x≈x
d_x'8804'y'8658'y'8851'x'8776'x_150 ::
  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
d_x'8804'y'8658'y'8851'x'8776'x_150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'y'8851'x'8776'x_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any
v5 Any
v6
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 T_TotalOrder_764
v3 Any
v4 Any
v5 Any
v6
du_x'8804'y'8658'y'8851'x'8776'x_150 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'y'8851'x'8776'x_150 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 T_TotalOrder_764
v0 Any
v1 Any
v2 Any
v3
  = let v4 :: t
v4
          = (T_IsTotalOrder_404 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_404 -> Any -> Any -> t
forall a b. a -> b
coe
              T_IsTotalOrder_404 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_414
              (T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> T_TotalOrder_764
forall a b. a -> b
coe T_TotalOrder_764
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
forall {t}. t
v4 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v5
           -> (T_IsPartialOrder_174 -> Any -> Any -> Any -> Any -> Any)
-> T_IsPartialOrder_174 -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_IsPartialOrder_174 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
                (T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
                   ((T_TotalOrder_764 -> T_IsTotalOrder_404)
-> Any -> T_IsTotalOrder_404
forall a b. a -> b
coe
                      T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0)))
                Any
v2 Any
v1 Any
v5 Any
v3
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
           -> let v6 :: t
v6
                    = (T_TotalOrder_764 -> T_Poset_314) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
              Any -> Any
forall a b. a -> b
coe
                (let v7 :: t
v7
                       = (T_Poset_314 -> T_Preorder_132) -> Any -> t
forall a b. a -> b
coe
                           T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6) in
                 Any -> Any
forall a b. a -> b
coe
                   ((T_IsEquivalence_26 -> Any -> Any)
-> T_IsEquivalence_26 -> Any -> Any
forall a b. a -> b
coe
                      T_IsEquivalence_26 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                      (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
                            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v7)))
                      Any
v1))
         T__'8846'__30
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
-- Algebra.Construct.NaturalChoice.Min.minOperator
d_minOperator_176 ::
  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.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98
d_minOperator_176 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_MinOperator_98
d_minOperator_176 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 T_TotalOrder_764
v3
du_minOperator_176 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98
du_minOperator_176 :: T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 T_TotalOrder_764
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_MinOperator_98)
-> Any -> Any -> Any -> T_MinOperator_98
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.C_MinOperator'46'constructor_1121
      ((T_TotalOrder_764 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> Any -> Any -> Any
du__'8851'__94 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 ->
            (T_TotalOrder_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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'_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8851'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
d_mono'45''8804''45'distrib'45''8851'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8851'_180 T_TotalOrder_764
v3
du_mono'45''8804''45'distrib'45''8851'_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8851'_180 :: T_TotalOrder_764
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8851'_180 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98
 -> (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_222
-> T_MinOperator_98
-> (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'_3114
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⇒x⊓z≤y
d_x'8804'y'8658'x'8851'z'8804'y_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'z'8804'y_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_182 T_TotalOrder_764
v3
du_x'8804'y'8658'x'8851'z'8804'y_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_182 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_182 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_3160
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⇒z⊓x≤y
d_x'8804'y'8658'z'8851'x'8804'y_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'z'8851'x'8804'y_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_184 T_TotalOrder_764
v3
du_x'8804'y'8658'z'8851'x'8804'y_184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_184 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_184 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_3172
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⊓z⇒x≤y
d_x'8804'y'8851'z'8658'x'8804'y_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'y_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_186 T_TotalOrder_764
v3
du_x'8804'y'8851'z'8658'x'8804'y_186 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_186 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_186 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_3184
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⊓z⇒x≤z
d_x'8804'y'8851'z'8658'x'8804'z_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'z_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_188 T_TotalOrder_764
v3
du_x'8804'y'8851'z'8658'x'8804'z_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_188 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_188 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_3198
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≈x⇒x≤y
d_x'8851'y'8776'x'8658'x'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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'x'8658'x'8804'y_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_190 T_TotalOrder_764
v3
du_x'8851'y'8776'x'8658'x'8804'y_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_190 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_190 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≈y⇒y≤x
d_x'8851'y'8776'y'8658'y'8804'x_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 -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'y'8658'y'8804'x_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_192 T_TotalOrder_764
v3
du_x'8851'y'8776'y'8658'y'8804'x_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_192 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_192 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≤x
d_x'8851'y'8804'x_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d_x'8851'y'8804'x_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any
du_x'8851'y'8804'x_194 T_TotalOrder_764
v3
du_x'8851'y'8804'x_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_194 :: T_TotalOrder_764 -> Any -> Any -> Any
du_x'8851'y'8804'x_194 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_2808
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≤y
d_x'8851'y'8804'y_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d_x'8851'y'8804'y_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any
du_x'8851'y'8804'y_196 T_TotalOrder_764
v3
du_x'8851'y'8804'y_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_196 :: T_TotalOrder_764 -> Any -> Any -> Any
du_x'8851'y'8804'y_196 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_2834
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-assoc
d_'8851''45'assoc_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_'8851''45'assoc_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_198 T_TotalOrder_764
v3
du_'8851''45'assoc_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_198 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_198 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-band
d_'8851''45'band_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_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_596
d_'8851''45'band_200 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_Band_596
d_'8851''45'band_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> T_Band_596
du_'8851''45'band_200 T_TotalOrder_764
v3
du_'8851''45'band_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_596
du_'8851''45'band_200 :: T_TotalOrder_764 -> T_Band_596
du_'8851''45'band_200 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Band_596)
-> Any -> Any -> T_Band_596
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_Band_596
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_3052
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-comm
d_'8851''45'comm_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d_'8851''45'comm_202 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any
du_'8851''45'comm_202 T_TotalOrder_764
v3
du_'8851''45'comm_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_202 :: T_TotalOrder_764 -> Any -> Any -> Any
du_'8851''45'comm_202 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_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_764 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
d_'8851''45'commutativeSemigroup_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_CommutativeSemigroup_662
d_'8851''45'commutativeSemigroup_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_204 T_TotalOrder_764
v3
du_'8851''45'commutativeSemigroup_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_204 :: T_TotalOrder_764 -> T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_204 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> T_CommutativeSemigroup_662)
-> Any -> Any -> T_CommutativeSemigroup_662
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> T_CommutativeSemigroup_662
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_3054
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-cong
d_'8851''45'cong_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_764 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_206 T_TotalOrder_764
v3
du_'8851''45'cong_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_206 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_206 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-congʳ
d_'8851''45'cong'691'_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'691'_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_208 T_TotalOrder_764
v3
du_'8851''45'cong'691'_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_208 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_208 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_2920
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-congˡ
d_'8851''45'cong'737'_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'737'_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_210 T_TotalOrder_764
v3
du_'8851''45'cong'737'_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_210 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_210 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_2882
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-glb
d_'8851''45'glb_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'glb_212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_212 T_TotalOrder_764
v3
du_'8851''45'glb_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_212 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_212 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_3278
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-idem
d_'8851''45'idem_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_764 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_214 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> Any -> Any
d_'8851''45'idem_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any
du_'8851''45'idem_214 T_TotalOrder_764
v3
du_'8851''45'idem_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_214 :: T_TotalOrder_764 -> Any -> Any
du_'8851''45'idem_214 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_2984
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-identity
d_'8851''45'identity_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_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'identity_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_216 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5
du_'8851''45'identity_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_216 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_216 T_TotalOrder_764
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_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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'_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_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'691'_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_218 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'identity'691'_218 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_218 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_218 T_TotalOrder_764
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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'_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_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'737'_220 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_220 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'identity'737'_220 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_220 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_220 T_TotalOrder_764
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8851''45'isBand_222 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_IsBand_508
d_'8851''45'isBand_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> T_IsBand_508
du_'8851''45'isBand_222 T_TotalOrder_764
v3
du_'8851''45'isBand_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8851''45'isBand_222 :: T_TotalOrder_764 -> T_IsBand_508
du_'8851''45'isBand_222 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508)
-> Any -> Any -> T_IsBand_508
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_3034
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_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_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
d_'8851''45'isCommutativeSemigroup_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_IsCommutativeSemigroup_548
d_'8851''45'isCommutativeSemigroup_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_224 T_TotalOrder_764
v3
du_'8851''45'isCommutativeSemigroup_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_224 :: T_TotalOrder_764 -> T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_224 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> T_IsCommutativeSemigroup_548)
-> Any -> Any -> T_IsCommutativeSemigroup_548
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> T_IsCommutativeSemigroup_548
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_3036
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isMagma
d_'8851''45'isMagma_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_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8851''45'isMagma_226 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_IsMagma_176
d_'8851''45'isMagma_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_IsMagma_176
du_'8851''45'isMagma_226 T_TotalOrder_764
v3
du_'8851''45'isMagma_226 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8851''45'isMagma_226 :: T_TotalOrder_764 -> T_IsMagma_176
du_'8851''45'isMagma_226 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsMagma_176)
-> Any -> Any -> T_IsMagma_176
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsMagma_176
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_3030
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isMonoid
d_'8851''45'isMonoid_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_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'8851''45'isMonoid_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_IsMonoid_686
d_'8851''45'isMonoid_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> T_IsMonoid_686
du_'8851''45'isMonoid_228 T_TotalOrder_764
v3
du_'8851''45'isMonoid_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
du_'8851''45'isMonoid_228 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_IsMonoid_686
du_'8851''45'isMonoid_228 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> (Any -> Any) -> T_IsMonoid_686)
-> Any -> Any -> Any -> (Any -> Any) -> T_IsMonoid_686
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> (Any -> Any) -> T_IsMonoid_686
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_3042
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_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_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
d_'8851''45'isSelectiveMagma_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_IsSelectiveMagma_436
d_'8851''45'isSelectiveMagma_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_230 T_TotalOrder_764
v3
du_'8851''45'isSelectiveMagma_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_230 :: T_TotalOrder_764 -> T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_230 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> Any -> Any -> T_IsSelectiveMagma_436
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) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSemigroup
d_'8851''45'isSemigroup_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_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8851''45'isSemigroup_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_IsSemigroup_472
d_'8851''45'isSemigroup_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_IsSemigroup_472
du_'8851''45'isSemigroup_232 T_TotalOrder_764
v3
du_'8851''45'isSemigroup_232 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8851''45'isSemigroup_232 :: T_TotalOrder_764 -> T_IsSemigroup_472
du_'8851''45'isSemigroup_232 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSemigroup_472)
-> Any -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_3032
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-magma
d_'8851''45'magma_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_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
d_'8851''45'magma_234 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_Magma_68
d_'8851''45'magma_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> T_Magma_68
du_'8851''45'magma_234 T_TotalOrder_764
v3
du_'8851''45'magma_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
du_'8851''45'magma_234 :: T_TotalOrder_764 -> T_Magma_68
du_'8851''45'magma_234 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Magma_68)
-> Any -> Any -> T_Magma_68
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_Magma_68
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_3048
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-mono-≤
d_'8851''45'mono'45''8804'_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_764 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'45''8804'_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_236 T_TotalOrder_764
v3
du_'8851''45'mono'45''8804'_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_236 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_236 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_3206
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoid
d_'8851''45'monoid_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_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'8851''45'monoid_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_Monoid_882
d_'8851''45'monoid_238 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Monoid_882
du_'8851''45'monoid_238 T_TotalOrder_764
v3
du_'8851''45'monoid_238 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'8851''45'monoid_238 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Monoid_882
du_'8851''45'monoid_238 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> (Any -> Any) -> T_Monoid_882)
-> Any -> Any -> Any -> (Any -> Any) -> T_Monoid_882
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> (Any -> Any) -> T_Monoid_882
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_3060
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoʳ-≤
d_'8851''45'mono'691''45''8804'_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'691''45''8804'_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_240 T_TotalOrder_764
v3
du_'8851''45'mono'691''45''8804'_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_240 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_240 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_3266
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoˡ-≤
d_'8851''45'mono'737''45''8804'_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'737''45''8804'_242 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_242 T_TotalOrder_764
v3
du_'8851''45'mono'737''45''8804'_242 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_242 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_242 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_3256
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-rawMagma
d_'8851''45'rawMagma_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_764 ->
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_36
d_'8851''45'rawMagma_244 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_RawMagma_36
d_'8851''45'rawMagma_244 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_RawMagma_36
du_'8851''45'rawMagma_244 T_TotalOrder_764
v3
du_'8851''45'rawMagma_244 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_36
du_'8851''45'rawMagma_244 :: T_TotalOrder_764 -> T_RawMagma_36
du_'8851''45'rawMagma_244 T_TotalOrder_764
v0
  = (T_MinOperator_98 -> T_RawMagma_36) -> Any -> T_RawMagma_36
forall a b. a -> b
coe
      T_MinOperator_98 -> T_RawMagma_36
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'rawMagma_3046
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-sel
d_'8851''45'sel_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_764 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_246 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> T__'8846'__30
d_'8851''45'sel_246 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_246 T_TotalOrder_764
v3
du_'8851''45'sel_246 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_246 :: T_TotalOrder_764 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_246 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> T__'8846'__30)
-> Any -> Any -> Any -> Any -> T__'8846'__30
forall a b. a -> b
coe
      T_TotalPreorder_222
-> T_MinOperator_98 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_2988
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-selectiveMagma
d_'8851''45'selectiveMagma_248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_122
d_'8851''45'selectiveMagma_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_SelectiveMagma_122
d_'8851''45'selectiveMagma_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_SelectiveMagma_122
du_'8851''45'selectiveMagma_248 T_TotalOrder_764
v3
du_'8851''45'selectiveMagma_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_122
du_'8851''45'selectiveMagma_248 :: T_TotalOrder_764 -> T_SelectiveMagma_122
du_'8851''45'selectiveMagma_248 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_SelectiveMagma_122)
-> Any -> Any -> T_SelectiveMagma_122
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_SelectiveMagma_122
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_3056
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-semigroup
d_'8851''45'semigroup_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_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'8851''45'semigroup_250 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_Semigroup_536
d_'8851''45'semigroup_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> T_Semigroup_536
du_'8851''45'semigroup_250 T_TotalOrder_764
v3
du_'8851''45'semigroup_250 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_'8851''45'semigroup_250 :: T_TotalOrder_764 -> T_Semigroup_536
du_'8851''45'semigroup_250 T_TotalOrder_764
v0
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semigroup_536)
-> Any -> Any -> T_Semigroup_536
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semigroup_536
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_3050
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-triangulate
d_'8851''45'triangulate_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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_252 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_'8851''45'triangulate_252 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_252 T_TotalOrder_764
v3
du_'8851''45'triangulate_252 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_252 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_252 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_3292
      ((T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
      ((T_TotalOrder_764 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MinOperator_98
du_minOperator_176 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-zero
d_'8851''45'zero_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_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'zero_254 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_254 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5
du_'8851''45'zero_254 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_254 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_254 T_TotalOrder_764
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_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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'_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_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'691'_256 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_256 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'zero'691'_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_256 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_256 T_TotalOrder_764
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_150 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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'_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_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_258 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'737'_258 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_258 T_TotalOrder_764
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'zero'737'_258 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_258 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_258 T_TotalOrder_764
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_764 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_120 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
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)