{-# 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.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_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204
d_totalPreorder_46 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_TotalPreorder_204
d_totalPreorder_46 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_TotalPreorder_204
du_totalPreorder_46 T_TotalOrder_652
v3
du_totalPreorder_46 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204
du_totalPreorder_46 :: T_TotalOrder_652 -> T_TotalPreorder_204
du_totalPreorder_46 T_TotalOrder_652
v0
  = (T_TotalOrder_652 -> T_TotalPreorder_204)
-> Any -> T_TotalPreorder_204
forall a b. a -> b
coe
      T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0)
-- Algebra.Construct.NaturalChoice.Min._⊓_
d__'8851'__80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d__'8851'__80 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any
v5 = T_TotalOrder_652 -> Any -> Any -> Any
du__'8851'__80 T_TotalOrder_652
v3 Any
v4 Any
v5
du__'8851'__80 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__80 :: T_TotalOrder_652 -> Any -> Any -> Any
du__'8851'__80 T_TotalOrder_652
v0 Any
v1 Any
v2
  = let v3 :: t
v3
          = (T_IsTotalOrder_384 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_384 -> Any -> Any -> t
forall a b. a -> b
coe
              T_IsTotalOrder_384 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_394
              (T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0))
              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_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'y'8776'x_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any
v5 Any
v6
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 T_TotalOrder_652
v3 Any
v4 Any
v5 Any
v6
du_x'8804'y'8658'x'8851'y'8776'x_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'y'8776'x_106 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 T_TotalOrder_652
v0 Any
v1 Any
v2 Any
v3
  = let v4 :: t
v4
          = (T_IsTotalOrder_384 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_384 -> Any -> Any -> t
forall a b. a -> b
coe
              T_IsTotalOrder_384 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_394
              (T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0))
              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_652 -> T_Poset_282) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.du_poset_702 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
              Any -> Any
forall a b. a -> b
coe
                (let v7 :: t
v7
                       = (T_Poset_282 -> T_Preorder_132) -> Any -> t
forall a b. a -> b
coe
                           T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (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_162 -> Any -> Any -> Any -> Any -> Any)
-> T_IsPartialOrder_162 -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_IsPartialOrder_162 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
                (T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                   ((T_TotalOrder_652 -> T_IsTotalOrder_384)
-> Any -> T_IsTotalOrder_384
forall a b. a -> b
coe
                      T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'y'8851'x'8776'x_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'y'8851'x'8776'x_136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any
v5 Any
v6
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 T_TotalOrder_652
v3 Any
v4 Any
v5 Any
v6
du_x'8804'y'8658'y'8851'x'8776'x_136 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'y'8851'x'8776'x_136 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 T_TotalOrder_652
v0 Any
v1 Any
v2 Any
v3
  = let v4 :: t
v4
          = (T_IsTotalOrder_384 -> Any -> Any -> T__'8846'__30)
-> T_IsTotalOrder_384 -> Any -> Any -> t
forall a b. a -> b
coe
              T_IsTotalOrder_384 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_394
              (T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0))
              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_162 -> Any -> Any -> Any -> Any -> Any)
-> T_IsPartialOrder_162 -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_IsPartialOrder_162 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
                (T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                   ((T_TotalOrder_652 -> T_IsTotalOrder_384)
-> Any -> T_IsTotalOrder_384
forall a b. a -> b
coe
                      T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_652 -> T_Poset_282) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.du_poset_702 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
              Any -> Any
forall a b. a -> b
coe
                (let v7 :: t
v7
                       = (T_Poset_282 -> T_Preorder_132) -> Any -> t
forall a b. a -> b
coe
                           T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (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_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_84
d_minOperator_162 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_MinOperator_84
d_minOperator_162 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 T_TotalOrder_652
v3
du_minOperator_162 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_84
du_minOperator_162 :: T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 T_TotalOrder_652
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_MinOperator_84)
-> Any -> Any -> Any -> T_MinOperator_84
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.C_MinOperator'46'constructor_983
      ((T_TotalOrder_652 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> Any -> Any -> Any
du__'8851'__80 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 ->
            (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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'_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8851'_166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
d_mono'45''8804''45'distrib'45''8851'_166 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8851'_166 T_TotalOrder_652
v3
du_mono'45''8804''45'distrib'45''8851'_166 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8851'_166 :: T_TotalOrder_652
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8851'_166 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> (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_204
-> T_MinOperator_84
-> (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'_1936
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⇒x⊓z≤y
d_x'8804'y'8658'x'8851'z'8804'y_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'z'8804'y_168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_168 T_TotalOrder_652
v3
du_x'8804'y'8658'x'8851'z'8804'y_168 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_168 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_168 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_1982
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⇒z⊓x≤y
d_x'8804'y'8658'z'8851'x'8804'y_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'z'8851'x'8804'y_170 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_170 T_TotalOrder_652
v3
du_x'8804'y'8658'z'8851'x'8804'y_170 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_170 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_170 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_1994
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⊓z⇒x≤y
d_x'8804'y'8851'z'8658'x'8804'y_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'y_172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_172 T_TotalOrder_652
v3
du_x'8804'y'8851'z'8658'x'8804'y_172 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_172 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_172 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_2006
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x≤y⊓z⇒x≤z
d_x'8804'y'8851'z'8658'x'8804'z_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'z_174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_174 T_TotalOrder_652
v3
du_x'8804'y'8851'z'8658'x'8804'z_174 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_174 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_174 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_2020
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≈x⇒x≤y
d_x'8851'y'8776'x'8658'x'8804'y_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'x'8658'x'8804'y_176 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_176 T_TotalOrder_652
v3
du_x'8851'y'8776'x'8658'x'8804'y_176 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_176 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_176 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≈y⇒y≤x
d_x'8851'y'8776'y'8658'y'8804'x_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'y'8658'y'8804'x_178 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_178 T_TotalOrder_652
v3
du_x'8851'y'8776'y'8658'y'8804'x_178 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_178 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_178 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≤x
d_x'8851'y'8804'x_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d_x'8851'y'8804'x_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'x_180 T_TotalOrder_652
v3
du_x'8851'y'8804'x_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_180 :: T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'x_180 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_1626
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.x⊓y≤y
d_x'8851'y'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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d_x'8851'y'8804'y_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'y_182 T_TotalOrder_652
v3
du_x'8851'y'8804'y_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_182 :: T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'y_182 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_1652
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-assoc
d_'8851''45'assoc_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_'8851''45'assoc_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_184 T_TotalOrder_652
v3
du_'8851''45'assoc_184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_184 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_184 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_1762
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-band
d_'8851''45'band_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_266
d_'8851''45'band_186 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_Band_266
d_'8851''45'band_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_Band_266
du_'8851''45'band_186 T_TotalOrder_652
v3
du_'8851''45'band_186 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_266
du_'8851''45'band_186 :: T_TotalOrder_652 -> T_Band_266
du_'8851''45'band_186 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Band_266)
-> Any -> Any -> T_Band_266
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Band_266
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_1872
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-comm
d_'8851''45'comm_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d_'8851''45'comm_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du_'8851''45'comm_188 T_TotalOrder_652
v3
du_'8851''45'comm_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_188 :: T_TotalOrder_652 -> Any -> Any -> Any
du_'8851''45'comm_188 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_1674
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_332
d_'8851''45'commutativeSemigroup_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_CommutativeSemigroup_332
d_'8851''45'commutativeSemigroup_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_190 T_TotalOrder_652
v3
du_'8851''45'commutativeSemigroup_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_190 :: T_TotalOrder_652 -> T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_190 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> T_CommutativeSemigroup_332)
-> Any -> Any -> T_CommutativeSemigroup_332
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> T_CommutativeSemigroup_332
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_1874
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-cong
d_'8851''45'cong_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_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_192 T_TotalOrder_652
v3
du_'8851''45'cong_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_192 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_192 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_1748
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-congʳ
d_'8851''45'cong'691'_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'691'_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_194 T_TotalOrder_652
v3
du_'8851''45'cong'691'_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_194 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_194 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_1738
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-congˡ
d_'8851''45'cong'737'_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'737'_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_196 T_TotalOrder_652
v3
du_'8851''45'cong'737'_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_196 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_196 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_1700
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-glb
d_'8851''45'glb_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'glb_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_198 T_TotalOrder_652
v3
du_'8851''45'glb_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_198 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_198 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_2100
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-idem
d_'8851''45'idem_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_652 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_200 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> Any -> Any
d_'8851''45'idem_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any
du_'8851''45'idem_200 T_TotalOrder_652
v3
du_'8851''45'idem_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_200 :: T_TotalOrder_652 -> Any -> Any
du_'8851''45'idem_200 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_1802
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-identity
d_'8851''45'identity_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_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'identity_202 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_202 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5
du_'8851''45'identity_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_202 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_202 T_TotalOrder_652
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_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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'_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_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'691'_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_204 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'identity'691'_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_204 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_204 T_TotalOrder_652
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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'_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_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'737'_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_206 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'identity'737'_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_206 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_206 T_TotalOrder_652
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_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_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8851''45'isBand_208 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_IsBand_230
d_'8851''45'isBand_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_IsBand_230
du_'8851''45'isBand_208 T_TotalOrder_652
v3
du_'8851''45'isBand_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8851''45'isBand_208 :: T_TotalOrder_652 -> T_IsBand_230
du_'8851''45'isBand_208 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsBand_230)
-> Any -> Any -> T_IsBand_230
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsBand_230
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_1852
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_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_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_270
d_'8851''45'isCommutativeSemigroup_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsCommutativeSemigroup_270
d_'8851''45'isCommutativeSemigroup_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_210 T_TotalOrder_652
v3
du_'8851''45'isCommutativeSemigroup_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_210 :: T_TotalOrder_652 -> T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_210 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> T_IsCommutativeSemigroup_270)
-> Any -> Any -> T_IsCommutativeSemigroup_270
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> T_IsCommutativeSemigroup_270
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_1854
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isMagma
d_'8851''45'isMagma_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_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8851''45'isMagma_212 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_IsMagma_86
d_'8851''45'isMagma_212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsMagma_86
du_'8851''45'isMagma_212 T_TotalOrder_652
v3
du_'8851''45'isMagma_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8851''45'isMagma_212 :: T_TotalOrder_652 -> T_IsMagma_86
du_'8851''45'isMagma_212 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsMagma_86)
-> Any -> Any -> T_IsMagma_86
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsMagma_86
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_1848
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isMonoid
d_'8851''45'isMonoid_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_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'8851''45'isMonoid_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_IsMonoid_358
d_'8851''45'isMonoid_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_IsMonoid_358
du_'8851''45'isMonoid_214 T_TotalOrder_652
v3
du_'8851''45'isMonoid_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'8851''45'isMonoid_214 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_IsMonoid_358
du_'8851''45'isMonoid_214 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> (Any -> Any) -> T_IsMonoid_358)
-> Any -> Any -> Any -> (Any -> Any) -> T_IsMonoid_358
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> (Any -> Any) -> T_IsMonoid_358
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_1862
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_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_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
d_'8851''45'isSelectiveMagma_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsSelectiveMagma_158
d_'8851''45'isSelectiveMagma_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_216 T_TotalOrder_652
v3
du_'8851''45'isSelectiveMagma_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_216 :: T_TotalOrder_652 -> T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_216 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> Any -> Any -> T_IsSelectiveMagma_158
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSemigroup
d_'8851''45'isSemigroup_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_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8851''45'isSemigroup_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsSemigroup_194
d_'8851''45'isSemigroup_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsSemigroup_194
du_'8851''45'isSemigroup_218 T_TotalOrder_652
v3
du_'8851''45'isSemigroup_218 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8851''45'isSemigroup_218 :: T_TotalOrder_652 -> T_IsSemigroup_194
du_'8851''45'isSemigroup_218 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemigroup_194)
-> Any -> Any -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_1850
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-isSemilattice
d_'8851''45'isSemilattice_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_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8851''45'isSemilattice_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsSemilattice_312
d_'8851''45'isSemilattice_220 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsSemilattice_312
du_'8851''45'isSemilattice_220 T_TotalOrder_652
v3
du_'8851''45'isSemilattice_220 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8851''45'isSemilattice_220 :: T_TotalOrder_652 -> T_IsSemilattice_312
du_'8851''45'isSemilattice_220 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemilattice_312)
-> Any -> Any -> T_IsSemilattice_312
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_1856
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-magma
d_'8851''45'magma_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
d_'8851''45'magma_222 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_Magma_36
d_'8851''45'magma_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_Magma_36
du_'8851''45'magma_222 T_TotalOrder_652
v3
du_'8851''45'magma_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
du_'8851''45'magma_222 :: T_TotalOrder_652 -> T_Magma_36
du_'8851''45'magma_222 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Magma_36)
-> Any -> Any -> T_Magma_36
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Magma_36
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_1868
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-mono-≤
d_'8851''45'mono'45''8804'_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_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'45''8804'_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_224 T_TotalOrder_652
v3
du_'8851''45'mono'45''8804'_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_224 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_224 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_2028
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoid
d_'8851''45'monoid_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_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'8851''45'monoid_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_Monoid_506
d_'8851''45'monoid_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Monoid_506
du_'8851''45'monoid_226 T_TotalOrder_652
v3
du_'8851''45'monoid_226 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'8851''45'monoid_226 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Monoid_506
du_'8851''45'monoid_226 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> (Any -> Any) -> T_Monoid_506)
-> Any -> Any -> Any -> (Any -> Any) -> T_Monoid_506
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> (Any -> Any) -> T_Monoid_506
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_1882
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoʳ-≤
d_'8851''45'mono'691''45''8804'_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'691''45''8804'_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_228 T_TotalOrder_652
v3
du_'8851''45'mono'691''45''8804'_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_228 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_228 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_2088
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-monoˡ-≤
d_'8851''45'mono'737''45''8804'_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'737''45''8804'_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_230 T_TotalOrder_652
v3
du_'8851''45'mono'737''45''8804'_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_230 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_230 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_2078
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-rawMagma
d_'8851''45'rawMagma_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_RawMagma_8
d_'8851''45'rawMagma_232 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_RawMagma_8
d_'8851''45'rawMagma_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_RawMagma_8
du_'8851''45'rawMagma_232 T_TotalOrder_652
v3
du_'8851''45'rawMagma_232 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_RawMagma_8
du_'8851''45'rawMagma_232 :: T_TotalOrder_652 -> T_RawMagma_8
du_'8851''45'rawMagma_232 T_TotalOrder_652
v0
  = (T_MinOperator_84 -> T_RawMagma_8) -> Any -> T_RawMagma_8
forall a b. a -> b
coe
      T_MinOperator_84 -> T_RawMagma_8
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'rawMagma_1866
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-sel
d_'8851''45'sel_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_652 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> T__'8846'__30
d_'8851''45'sel_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_234 T_TotalOrder_652
v3
du_'8851''45'sel_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_234 :: T_TotalOrder_652 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_234 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> T__'8846'__30)
-> Any -> Any -> Any -> Any -> T__'8846'__30
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_1806
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-selectiveMagma
d_'8851''45'selectiveMagma_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_90
d_'8851''45'selectiveMagma_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_SelectiveMagma_90
d_'8851''45'selectiveMagma_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_SelectiveMagma_90
du_'8851''45'selectiveMagma_236 T_TotalOrder_652
v3
du_'8851''45'selectiveMagma_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_90
du_'8851''45'selectiveMagma_236 :: T_TotalOrder_652 -> T_SelectiveMagma_90
du_'8851''45'selectiveMagma_236 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_SelectiveMagma_90)
-> Any -> Any -> T_SelectiveMagma_90
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_SelectiveMagma_90
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_1878
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-semigroup
d_'8851''45'semigroup_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'8851''45'semigroup_238 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_Semigroup_206
d_'8851''45'semigroup_238 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_Semigroup_206
du_'8851''45'semigroup_238 T_TotalOrder_652
v3
du_'8851''45'semigroup_238 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'8851''45'semigroup_238 :: T_TotalOrder_652 -> T_Semigroup_206
du_'8851''45'semigroup_238 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semigroup_206)
-> Any -> Any -> T_Semigroup_206
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semigroup_206
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_1870
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-semilattice
d_'8851''45'semilattice_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8851''45'semilattice_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Semilattice_402
d_'8851''45'semilattice_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_Semilattice_402
du_'8851''45'semilattice_240 T_TotalOrder_652
v3
du_'8851''45'semilattice_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8851''45'semilattice_240 :: T_TotalOrder_652 -> T_Semilattice_402
du_'8851''45'semilattice_240 T_TotalOrder_652
v0
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semilattice_402)
-> Any -> Any -> T_Semilattice_402
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semilattice_402
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_1876
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-triangulate
d_'8851''45'triangulate_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_'8851''45'triangulate_242 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_242 T_TotalOrder_652
v3
du_'8851''45'triangulate_242 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_242 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_242 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_2114
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MinOperator_84
du_minOperator_162 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Min._.⊓-zero
d_'8851''45'zero_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_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_244 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'zero_244 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_244 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5
du_'8851''45'zero_244 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_244 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_244 T_TotalOrder_652
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_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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'_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_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_246 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'691'_246 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_246 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'zero'691'_246 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_246 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_246 T_TotalOrder_652
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_136 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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'_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_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'737'_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_248 T_TotalOrder_652
v3 Any
v4 Any -> Any
v5 Any
v6
du_'8851''45'zero'737'_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_248 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_248 T_TotalOrder_652
v0 Any
v1 Any -> Any
v2 Any
v3
  = (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_106 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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)