{-# 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.Max 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.MaxOp
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Min
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.Construct.Flip.EqAndOrd

-- Algebra.Construct.NaturalChoice.Max._.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.Max.Min.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_102 :: 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_102 ~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'8804'y'8658'x'8851'y'8776'x_102 T_TotalOrder_764
v3
du_x'8804'y'8658'x'8851'y'8776'x_102 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'y'8776'x_102 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_102 T_TotalOrder_764
v0
  = (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
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'x'8851'y'8776'x_120
      ((T_TotalOrder_764 -> T_TotalOrder_764) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_898
         (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Max.Min.x≤y⇒y⊓x≈x
d_x'8804'y'8658'y'8851'x'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_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'y'8851'x'8776'x_106 :: 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_106 ~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'8804'y'8658'y'8851'x'8776'x_106 T_TotalOrder_764
v3
du_x'8804'y'8658'y'8851'x'8776'x_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'y'8851'x'8776'x_106 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_106 T_TotalOrder_764
v0
  = (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
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'y'8851'x'8776'x_150
      ((T_TotalOrder_764 -> T_TotalOrder_764) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_898
         (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Max._⊔_
d__'8852'__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
d__'8852'__184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d__'8852'__184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> Any -> Any
du__'8852'__184 T_TotalOrder_764
v3
du__'8852'__184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8852'__184 :: T_TotalOrder_764 -> Any -> Any -> Any
du__'8852'__184 T_TotalOrder_764
v0
  = (T_TotalOrder_764 -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_764 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__94
      ((T_TotalOrder_764 -> T_TotalOrder_764) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_898
         (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Max.maxOperator
d_maxOperator_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 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128
d_maxOperator_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_MaxOperator_128
d_maxOperator_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 T_TotalOrder_764
v3
du_maxOperator_186 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128
du_maxOperator_186 :: T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 T_TotalOrder_764
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_MaxOperator_128)
-> Any -> Any -> Any -> T_MaxOperator_128
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.C_MaxOperator'46'constructor_1665
      ((T_TotalOrder_764 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__94
         ((T_TotalOrder_764 -> T_TotalOrder_764) -> Any -> Any
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_898
            (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
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'y'8851'x'8776'x_150
              ((T_TotalOrder_764 -> T_TotalOrder_764) -> Any -> Any
forall a b. a -> b
coe
                 T_TotalOrder_764 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_898
                 (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)))
      ((T_TotalOrder_764 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_764 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'x'8851'y'8776'x_120
         ((T_TotalOrder_764 -> T_TotalOrder_764) -> Any -> Any
forall a b. a -> b
coe
            T_TotalOrder_764 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_898
            (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0)))
-- Algebra.Construct.NaturalChoice.Max._.mono-≤-distrib-⊔
d_mono'45''8804''45'distrib'45''8852'_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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_190 :: 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''8852'_190 ~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''8852'_190 T_TotalOrder_764
v3
du_mono'45''8804''45'distrib'45''8852'_190 ::
  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''8852'_190 :: T_TotalOrder_764
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8852'_190 T_TotalOrder_764
v0
  = (T_TotalPreorder_222
 -> T_MaxOperator_128
 -> (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_MaxOperator_128
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MaxOp.du_mono'45''8804''45'distrib'45''8852'_182
      ((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_MaxOperator_128) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≤x
d_x'8851'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
d_x'8851'y'8804'x_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d_x'8851'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
du_x'8851'y'8804'x_192 T_TotalOrder_764
v3
du_x'8851'y'8804'x_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_192 :: T_TotalOrder_764 -> Any -> Any -> Any
du_x'8851'y'8804'x_192 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_2808
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⇒x⊓z≤y
d_x'8804'y'8658'x'8851'z'8804'y_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_194 :: 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_194 ~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_194 T_TotalOrder_764
v3
du_x'8804'y'8658'x'8851'z'8804'y_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_194 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_194 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_3160
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⇒z⊓x≤y
d_x'8804'y'8658'z'8851'x'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 -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_196 :: 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_196 ~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_196 T_TotalOrder_764
v3
du_x'8804'y'8658'z'8851'x'8804'y_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_196 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_196 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_3172
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≤y
d_x'8851'y'8804'y_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d_x'8851'y'8804'y_198 ~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_198 T_TotalOrder_764
v3
du_x'8851'y'8804'y_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_198 :: T_TotalOrder_764 -> Any -> Any -> Any
du_x'8851'y'8804'y_198 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_2834
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≈x⇒x≤y
d_x'8851'y'8776'x'8658'x'8804'y_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 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_200 :: 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_200 ~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_200 T_TotalOrder_764
v3
du_x'8851'y'8776'x'8658'x'8804'y_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_200 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_200 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> 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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≈y⇒y≤x
d_x'8851'y'8776'y'8658'y'8804'x_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_202 :: 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_202 ~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_202 T_TotalOrder_764
v3
du_x'8851'y'8776'y'8658'y'8804'x_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_202 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_202 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> 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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⊓z⇒x≤y
d_x'8804'y'8851'z'8658'x'8804'y_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_204 :: 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_204 ~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_204 T_TotalOrder_764
v3
du_x'8804'y'8851'z'8658'x'8804'y_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_204 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_204 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_3184
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⊓z⇒x≤z
d_x'8804'y'8851'z'8658'x'8804'z_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
d_x'8804'y'8851'z'8658'x'8804'z_206 :: 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_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
du_x'8804'y'8851'z'8658'x'8804'z_206 T_TotalOrder_764
v3
du_x'8804'y'8851'z'8658'x'8804'z_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_206 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_206 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_3198
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-assoc
d_'8851''45'assoc_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
d_'8851''45'assoc_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_'8851''45'assoc_208 ~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_208 T_TotalOrder_764
v3
du_'8851''45'assoc_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_208 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_208 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> 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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-band
d_'8851''45'band_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 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_596
d_'8851''45'band_210 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_Band_596
d_'8851''45'band_210 ~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_210 T_TotalOrder_764
v3
du_'8851''45'band_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_596
du_'8851''45'band_210 :: T_TotalOrder_764 -> T_Band_596
du_'8851''45'band_210 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_Band_596
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_Band_596)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-comm
d_'8851''45'comm_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
d_'8851''45'comm_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
d_'8851''45'comm_212 ~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_212 T_TotalOrder_764
v3
du_'8851''45'comm_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_212 :: T_TotalOrder_764 -> Any -> Any -> Any
du_'8851''45'comm_212 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_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 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
d_'8851''45'commutativeSemigroup_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_CommutativeSemigroup_662
d_'8851''45'commutativeSemigroup_214 ~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_214 T_TotalOrder_764
v3
du_'8851''45'commutativeSemigroup_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_214 :: T_TotalOrder_764 -> T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_214 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_CommutativeSemigroup_662
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_CommutativeSemigroup_662)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-cong
d_'8851''45'cong_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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong_216 ~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_216 T_TotalOrder_764
v3
du_'8851''45'cong_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_216 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_216 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-congʳ
d_'8851''45'cong'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'cong'691'_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'691'_218 ~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'_218 T_TotalOrder_764
v3
du_'8851''45'cong'691'_218 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_218 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_218 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_2920
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-congˡ
d_'8851''45'cong'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'cong'737'_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'737'_220 ~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'_220 T_TotalOrder_764
v3
du_'8851''45'cong'737'_220 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_220 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_220 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_2882
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-idem
d_'8851''45'idem_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_222 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> Any -> Any
d_'8851''45'idem_222 ~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_222 T_TotalOrder_764
v3
du_'8851''45'idem_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_222 :: T_TotalOrder_764 -> Any -> Any
du_'8851''45'idem_222 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> 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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-identity
d_'8851''45'identity_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'identity_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_224 T_TotalOrder_764
v3
du_'8851''45'identity_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_224 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_224 T_TotalOrder_764
v0
  = let v1 :: t
v1 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    Any -> Any -> (Any -> Any) -> T_Σ_14
forall a b. a -> b
coe
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 ->
            (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
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
v4 ->
                    (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
                      Any
forall {t}. t
v1 Any
v2 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v4 ->
                    (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
                      Any
forall {t}. t
v1 Any
v4 Any
v2 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-identityʳ
d_'8851''45'identity'691'_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'691'_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_226 T_TotalOrder_764
v3
du_'8851''45'identity'691'_226 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_226 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_226 T_TotalOrder_764
v0
  = let v1 :: t
v1 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    Any -> Any -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 Any
v4 ->
            (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
              Any
forall {t}. t
v1 Any
v4 Any
v2 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))
-- Algebra.Construct.NaturalChoice.Max._.⊓-identityˡ
d_'8851''45'identity'737'_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'737'_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_228 T_TotalOrder_764
v3
du_'8851''45'identity'737'_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_228 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_228 T_TotalOrder_764
v0
  = let v1 :: t
v1 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    Any -> Any -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 Any
v4 ->
            (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
              Any
forall {t}. t
v1 Any
v2 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isBand
d_'8851''45'isBand_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8851''45'isBand_230 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_IsBand_508
d_'8851''45'isBand_230 ~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_230 T_TotalOrder_764
v3
du_'8851''45'isBand_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8851''45'isBand_230 :: T_TotalOrder_764 -> T_IsBand_508
du_'8851''45'isBand_230 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_IsBand_508
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
d_'8851''45'isCommutativeSemigroup_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_IsCommutativeSemigroup_548
d_'8851''45'isCommutativeSemigroup_232 ~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_232 T_TotalOrder_764
v3
du_'8851''45'isCommutativeSemigroup_232 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_232 :: T_TotalOrder_764 -> T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_232 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_IsCommutativeSemigroup_548
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_IsCommutativeSemigroup_548)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isMagma
d_'8851''45'isMagma_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8851''45'isMagma_234 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_IsMagma_176
d_'8851''45'isMagma_234 ~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_234 T_TotalOrder_764
v3
du_'8851''45'isMagma_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8851''45'isMagma_234 :: T_TotalOrder_764 -> T_IsMagma_176
du_'8851''45'isMagma_234 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_IsMagma_176
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsMagma_176)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isMonoid
d_'8851''45'isMonoid_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'8851''45'isMonoid_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_IsMonoid_686
d_'8851''45'isMonoid_236 ~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_236 T_TotalOrder_764
v3
du_'8851''45'isMonoid_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
du_'8851''45'isMonoid_236 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_IsMonoid_686
du_'8851''45'isMonoid_236 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> (Any -> Any) -> T_IsMonoid_686
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> (Any -> Any) -> T_IsMonoid_686)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
d_'8851''45'isSelectiveMagma_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_IsSelectiveMagma_436
d_'8851''45'isSelectiveMagma_238 ~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_238 T_TotalOrder_764
v3
du_'8851''45'isSelectiveMagma_238 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_238 :: T_TotalOrder_764 -> T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_238 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_IsSelectiveMagma_436
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSemigroup
d_'8851''45'isSemigroup_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8851''45'isSemigroup_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_IsSemigroup_472
d_'8851''45'isSemigroup_240 ~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_240 T_TotalOrder_764
v3
du_'8851''45'isSemigroup_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8851''45'isSemigroup_240 :: T_TotalOrder_764 -> T_IsSemigroup_472
du_'8851''45'isSemigroup_240 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_IsSemigroup_472
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSemigroup_472)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-glb
d_'8851''45'glb_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 -> AgdaAny
d_'8851''45'glb_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'glb_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 -> Any
du_'8851''45'glb_242 T_TotalOrder_764
v3
du_'8851''45'glb_242 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_242 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_242 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> 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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-magma
d_'8851''45'magma_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.T_Magma_68
d_'8851''45'magma_244 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_Magma_68
d_'8851''45'magma_244 ~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_244 T_TotalOrder_764
v3
du_'8851''45'magma_244 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
du_'8851''45'magma_244 :: T_TotalOrder_764 -> T_Magma_68
du_'8851''45'magma_244 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_Magma_68
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_Magma_68)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-mono-≤
d_'8851''45'mono'45''8804'_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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_246 :: 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'_246 ~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'_246 T_TotalOrder_764
v3
du_'8851''45'mono'45''8804'_246 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_246 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_246 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_3206
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoid
d_'8851''45'monoid_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 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'8851''45'monoid_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_Monoid_882
d_'8851''45'monoid_248 ~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_248 T_TotalOrder_764
v3
du_'8851''45'monoid_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'8851''45'monoid_248 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Monoid_882
du_'8851''45'monoid_248 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> (Any -> Any) -> T_Monoid_882
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> (Any -> Any) -> T_Monoid_882)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoʳ-≤
d_'8851''45'mono'691''45''8804'_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'691''45''8804'_250 ~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'_250 T_TotalOrder_764
v3
du_'8851''45'mono'691''45''8804'_250 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_250 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_250 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_3266
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoˡ-≤
d_'8851''45'mono'737''45''8804'_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 -> AgdaAny
d_'8851''45'mono'737''45''8804'_252 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'737''45''8804'_252 ~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'_252 T_TotalOrder_764
v3
du_'8851''45'mono'737''45''8804'_252 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_252 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_252 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((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 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_3256
            ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-sel
d_'8851''45'sel_254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> T__'8846'__30
d_'8851''45'sel_254 ~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_254 T_TotalOrder_764
v3
du_'8851''45'sel_254 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_254 :: T_TotalOrder_764 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_254 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> T__'8846'__30
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> Any -> Any -> T__'8846'__30)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-selectiveMagma
d_'8851''45'selectiveMagma_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_122
d_'8851''45'selectiveMagma_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_SelectiveMagma_122
d_'8851''45'selectiveMagma_256 ~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_256 T_TotalOrder_764
v3
du_'8851''45'selectiveMagma_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_122
du_'8851''45'selectiveMagma_256 :: T_TotalOrder_764 -> T_SelectiveMagma_122
du_'8851''45'selectiveMagma_256 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_SelectiveMagma_122
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_SelectiveMagma_122)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-semigroup
d_'8851''45'semigroup_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'8851''45'semigroup_258 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_Semigroup_536
d_'8851''45'semigroup_258 ~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_258 T_TotalOrder_764
v3
du_'8851''45'semigroup_258 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_'8851''45'semigroup_258 :: T_TotalOrder_764 -> T_Semigroup_536
du_'8851''45'semigroup_258 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> T_Semigroup_536
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semigroup_536)
-> Any -> Any -> Any
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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-triangulate
d_'8851''45'triangulate_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> Any
-> Any
-> Any
d_'8851''45'triangulate_260 ~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_260 T_TotalOrder_764
v3
du_'8851''45'triangulate_260 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_260 :: T_TotalOrder_764 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_260 T_TotalOrder_764
v0
  = let v1 :: t
v1
          = (T_TotalOrder_764 -> T_TotalPreorder_222) -> Any -> t
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) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_222
 -> T_MinOperator_98 -> 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_TotalPreorder_222 -> T_TotalPreorder_222) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_128 -> T_MinOperator_98) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-zero
d_'8851''45'zero_262 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'zero_262 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_262 T_TotalOrder_764
v3
du_'8851''45'zero_262 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_262 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_262 T_TotalOrder_764
v0
  = let v1 :: t
v1 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    Any -> Any -> (Any -> Any) -> T_Σ_14
forall a b. a -> b
coe
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 ->
            (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
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
v4 ->
                    (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
                      Any
forall {t}. t
v1 Any
v2 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v4 ->
                    (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
                      Any
forall {t}. t
v1 Any
v4 Any
v2 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-zeroʳ
d_'8851''45'zero'691'_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'691'_264 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_264 T_TotalOrder_764
v3
du_'8851''45'zero'691'_264 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_264 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_264 T_TotalOrder_764
v0
  = let v1 :: t
v1 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    Any -> Any -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 Any
v4 ->
            (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
              Any
forall {t}. t
v1 Any
v4 Any
v2 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))
-- Algebra.Construct.NaturalChoice.Max._.⊓-zeroˡ
d_'8851''45'zero'737'_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'737'_266 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3
  = T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_266 T_TotalOrder_764
v3
du_'8851''45'zero'737'_266 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_266 :: T_TotalOrder_764 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_266 T_TotalOrder_764
v0
  = let v1 :: t
v1 = (T_TotalOrder_764 -> T_MaxOperator_128) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_MaxOperator_128
du_maxOperator_186 (T_TotalOrder_764 -> Any
forall a b. a -> b
coe T_TotalOrder_764
v0) in
    Any -> Any -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 Any
v4 ->
            (T_MaxOperator_128 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_128 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
              Any
forall {t}. t
v1 Any
v2 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))