{-# 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.Converse

-- Algebra.Construct.NaturalChoice.Max._.totalPreorder
d_totalPreorder_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204
d_totalPreorder_46 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_TotalPreorder_204
d_totalPreorder_46 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_TotalPreorder_204
du_totalPreorder_46 T_TotalOrder_652
v3
du_totalPreorder_46 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204
du_totalPreorder_46 :: T_TotalOrder_652 -> T_TotalPreorder_204
du_totalPreorder_46 T_TotalOrder_652
v0
  = (T_TotalOrder_652 -> T_TotalPreorder_204)
-> Any -> T_TotalPreorder_204
forall a b. a -> b
coe
      T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0)
-- Algebra.Construct.NaturalChoice.Max.Min.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'y'8776'x_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_88 T_TotalOrder_652
v3
du_x'8804'y'8658'x'8851'y'8776'x_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'y'8776'x_88 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_88 T_TotalOrder_652
v0
  = (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'x'8851'y'8776'x_106
      ((T_TotalOrder_652 -> T_TotalOrder_652) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalOrder_842
         (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Max.Min.x≤y⇒y⊓x≈x
d_x'8804'y'8658'y'8851'x'8776'x_92 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'y'8851'x'8776'x_92 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'y'8851'x'8776'x_92 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_92 T_TotalOrder_652
v3
du_x'8804'y'8658'y'8851'x'8776'x_92 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'y'8851'x'8776'x_92 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_92 T_TotalOrder_652
v0
  = (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'y'8851'x'8776'x_136
      ((T_TotalOrder_652 -> T_TotalOrder_652) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalOrder_842
         (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Max._⊔_
d__'8852'__174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d__'8852'__174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du__'8852'__174 T_TotalOrder_652
v3
du__'8852'__174 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8852'__174 :: T_TotalOrder_652 -> Any -> Any -> Any
du__'8852'__174 T_TotalOrder_652
v0
  = (T_TotalOrder_652 -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_652 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__80
      ((T_TotalOrder_652 -> T_TotalOrder_652) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalOrder_842
         (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Max.maxOperator
d_maxOperator_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114
d_maxOperator_176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_MaxOperator_114
d_maxOperator_176 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 T_TotalOrder_652
v3
du_maxOperator_176 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114
du_maxOperator_176 :: T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 T_TotalOrder_652
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_MaxOperator_114)
-> Any -> Any -> Any -> T_MaxOperator_114
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_MaxOperator_114
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.C_MaxOperator'46'constructor_1521
      ((T_TotalOrder_652 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__80
         ((T_TotalOrder_652 -> T_TotalOrder_652) -> Any -> Any
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalOrder_842
            (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0)))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 ->
            (T_TotalOrder_652 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_652 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'y'8851'x'8776'x_136
              ((T_TotalOrder_652 -> T_TotalOrder_652) -> Any -> Any
forall a b. a -> b
coe
                 T_TotalOrder_652 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalOrder_842
                 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
              (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v1)))
      ((T_TotalOrder_652 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'x'8851'y'8776'x_106
         ((T_TotalOrder_652 -> T_TotalOrder_652) -> Any -> Any
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalOrder_842
            (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0)))
-- Algebra.Construct.NaturalChoice.Max._.mono-≤-distrib-⊔
d_mono'45''8804''45'distrib'45''8852'_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
d_mono'45''8804''45'distrib'45''8852'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8852'_180 T_TotalOrder_652
v3
du_mono'45''8804''45'distrib'45''8852'_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_180 :: T_TotalOrder_652
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8852'_180 T_TotalOrder_652
v0
  = (T_TotalPreorder_204
 -> T_MaxOperator_114
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any)
-> Any
-> Any
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MaxOperator_114
-> (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'_172
      ((T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
      ((T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≤x
d_x'8851'y'8804'x_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d_x'8851'y'8804'x_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'x_182 T_TotalOrder_652
v3
du_x'8851'y'8804'x_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_182 :: T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'x_182 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_1626
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'z'8804'y_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_184 T_TotalOrder_652
v3
du_x'8804'y'8658'x'8851'z'8804'y_184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_184 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_184 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_1982
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'z'8851'x'8804'y_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_186 T_TotalOrder_652
v3
du_x'8804'y'8658'z'8851'x'8804'y_186 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_186 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_186 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_1994
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d_x'8851'y'8804'y_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'y_188 T_TotalOrder_652
v3
du_x'8851'y'8804'y_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_188 :: T_TotalOrder_652 -> Any -> Any -> Any
du_x'8851'y'8804'y_188 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_1652
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'x'8658'x'8804'y_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_190 T_TotalOrder_652
v3
du_x'8851'y'8776'x'8658'x'8804'y_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_190 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_190 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'y'8658'y'8804'x_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_192 T_TotalOrder_652
v3
du_x'8851'y'8776'y'8658'y'8804'x_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_192 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_192 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'y_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_194 T_TotalOrder_652
v3
du_x'8804'y'8851'z'8658'x'8804'y_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_194 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_194 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_2006
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'z_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_196 T_TotalOrder_652
v3
du_x'8804'y'8851'z'8658'x'8804'z_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_196 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_196 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_2020
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-assoc
d_'8851''45'assoc_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_'8851''45'assoc_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_198 T_TotalOrder_652
v3
du_'8851''45'assoc_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_198 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_198 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_1762
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-band
d_'8851''45'band_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_266
d_'8851''45'band_200 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_Band_266
d_'8851''45'band_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_Band_266
du_'8851''45'band_200 T_TotalOrder_652
v3
du_'8851''45'band_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_266
du_'8851''45'band_200 :: T_TotalOrder_652 -> T_Band_266
du_'8851''45'band_200 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_Band_266
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_Band_266)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_Band_266
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_1872
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-comm
d_'8851''45'comm_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
d_'8851''45'comm_202 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any
du_'8851''45'comm_202 T_TotalOrder_652
v3
du_'8851''45'comm_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_202 :: T_TotalOrder_652 -> Any -> Any -> Any
du_'8851''45'comm_202 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_1674
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_332
d_'8851''45'commutativeSemigroup_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_CommutativeSemigroup_332
d_'8851''45'commutativeSemigroup_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_204 T_TotalOrder_652
v3
du_'8851''45'commutativeSemigroup_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_204 :: T_TotalOrder_652 -> T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_204 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_CommutativeSemigroup_332
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> T_CommutativeSemigroup_332)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> T_CommutativeSemigroup_332
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_1874
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-cong
d_'8851''45'cong_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_206 T_TotalOrder_652
v3
du_'8851''45'cong_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_206 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_206 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_1748
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-congʳ
d_'8851''45'cong'691'_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'691'_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_208 T_TotalOrder_652
v3
du_'8851''45'cong'691'_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_208 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_208 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_1738
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-congˡ
d_'8851''45'cong'737'_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'737'_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_210 T_TotalOrder_652
v3
du_'8851''45'cong'737'_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_210 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_210 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_1700
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-idem
d_'8851''45'idem_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_212 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> Any -> Any
d_'8851''45'idem_212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any
du_'8851''45'idem_212 T_TotalOrder_652
v3
du_'8851''45'idem_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_212 :: T_TotalOrder_652 -> Any -> Any
du_'8851''45'idem_212 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_1802
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-identity
d_'8851''45'identity_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'identity_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_214 T_TotalOrder_652
v3
du_'8851''45'identity_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_214 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_214 T_TotalOrder_652
v0
  = let v1 :: t
v1 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
                      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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
                      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'_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'691'_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_216 T_TotalOrder_652
v3
du_'8851''45'identity'691'_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_216 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_216 T_TotalOrder_652
v0
  = let v1 :: t
v1 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
              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'_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'737'_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_218 T_TotalOrder_652
v3
du_'8851''45'identity'737'_218 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_218 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_218 T_TotalOrder_652
v0
  = let v1 :: t
v1 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
              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_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8851''45'isBand_220 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_IsBand_230
d_'8851''45'isBand_220 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_IsBand_230
du_'8851''45'isBand_220 T_TotalOrder_652
v3
du_'8851''45'isBand_220 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8851''45'isBand_220 :: T_TotalOrder_652 -> T_IsBand_230
du_'8851''45'isBand_220 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_IsBand_230
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsBand_230)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsBand_230
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_1852
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_270
d_'8851''45'isCommutativeSemigroup_222 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsCommutativeSemigroup_270
d_'8851''45'isCommutativeSemigroup_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_222 T_TotalOrder_652
v3
du_'8851''45'isCommutativeSemigroup_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_222 :: T_TotalOrder_652 -> T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_222 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_IsCommutativeSemigroup_270
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> T_IsCommutativeSemigroup_270)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> T_IsCommutativeSemigroup_270
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_1854
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isMagma
d_'8851''45'isMagma_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8851''45'isMagma_224 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_IsMagma_86
d_'8851''45'isMagma_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsMagma_86
du_'8851''45'isMagma_224 T_TotalOrder_652
v3
du_'8851''45'isMagma_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8851''45'isMagma_224 :: T_TotalOrder_652 -> T_IsMagma_86
du_'8851''45'isMagma_224 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_IsMagma_86
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsMagma_86)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsMagma_86
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_1848
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isMonoid
d_'8851''45'isMonoid_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'8851''45'isMonoid_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_IsMonoid_358
d_'8851''45'isMonoid_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_IsMonoid_358
du_'8851''45'isMonoid_226 T_TotalOrder_652
v3
du_'8851''45'isMonoid_226 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'8851''45'isMonoid_226 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_IsMonoid_358
du_'8851''45'isMonoid_226 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> (Any -> Any) -> T_IsMonoid_358
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> (Any -> Any) -> T_IsMonoid_358)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> (Any -> Any) -> T_IsMonoid_358
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_1862
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
d_'8851''45'isSelectiveMagma_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsSelectiveMagma_158
d_'8851''45'isSelectiveMagma_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_228 T_TotalOrder_652
v3
du_'8851''45'isSelectiveMagma_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_228 :: T_TotalOrder_652 -> T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_228 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_IsSelectiveMagma_158
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSemigroup
d_'8851''45'isSemigroup_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8851''45'isSemigroup_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsSemigroup_194
d_'8851''45'isSemigroup_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsSemigroup_194
du_'8851''45'isSemigroup_230 T_TotalOrder_652
v3
du_'8851''45'isSemigroup_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8851''45'isSemigroup_230 :: T_TotalOrder_652 -> T_IsSemigroup_194
du_'8851''45'isSemigroup_230 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_IsSemigroup_194
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemigroup_194)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_1850
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSemilattice
d_'8851''45'isSemilattice_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8851''45'isSemilattice_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_IsSemilattice_312
d_'8851''45'isSemilattice_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_IsSemilattice_312
du_'8851''45'isSemilattice_232 T_TotalOrder_652
v3
du_'8851''45'isSemilattice_232 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8851''45'isSemilattice_232 :: T_TotalOrder_652 -> T_IsSemilattice_312
du_'8851''45'isSemilattice_232 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_IsSemilattice_312
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemilattice_312)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_1856
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-glb
d_'8851''45'glb_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'glb_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_234 T_TotalOrder_652
v3
du_'8851''45'glb_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_234 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_234 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_2100
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-magma
d_'8851''45'magma_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
d_'8851''45'magma_236 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_Magma_36
d_'8851''45'magma_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> T_Magma_36
du_'8851''45'magma_236 T_TotalOrder_652
v3
du_'8851''45'magma_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
du_'8851''45'magma_236 :: T_TotalOrder_652 -> T_Magma_36
du_'8851''45'magma_236 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_Magma_36
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_Magma_36)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_Magma_36
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_1868
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-mono-≤
d_'8851''45'mono'45''8804'_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'45''8804'_238 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_238 T_TotalOrder_652
v3
du_'8851''45'mono'45''8804'_238 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_238 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_238 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_2028
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoid
d_'8851''45'monoid_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'8851''45'monoid_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_Monoid_506
d_'8851''45'monoid_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Monoid_506
du_'8851''45'monoid_240 T_TotalOrder_652
v3
du_'8851''45'monoid_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'8851''45'monoid_240 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Monoid_506
du_'8851''45'monoid_240 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> (Any -> Any) -> T_Monoid_506
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> (Any -> Any) -> T_Monoid_506)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> (Any -> Any) -> T_Monoid_506
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_1882
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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'_242 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'691''45''8804'_242 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_242 T_TotalOrder_652
v3
du_'8851''45'mono'691''45''8804'_242 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_242 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_242 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_2088
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (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'_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_244 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'737''45''8804'_244 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_244 T_TotalOrder_652
v3
du_'8851''45'mono'737''45''8804'_244 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_244 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_244 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_2078
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-sel
d_'8851''45'sel_246 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_246 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> T__'8846'__30
d_'8851''45'sel_246 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_246 T_TotalOrder_652
v3
du_'8851''45'sel_246 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_246 :: T_TotalOrder_652 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_246 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> T__'8846'__30
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204
-> T_MinOperator_84 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_1806
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-selectiveMagma
d_'8851''45'selectiveMagma_248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_90
d_'8851''45'selectiveMagma_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_SelectiveMagma_90
d_'8851''45'selectiveMagma_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_SelectiveMagma_90
du_'8851''45'selectiveMagma_248 T_TotalOrder_652
v3
du_'8851''45'selectiveMagma_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_90
du_'8851''45'selectiveMagma_248 :: T_TotalOrder_652 -> T_SelectiveMagma_90
du_'8851''45'selectiveMagma_248 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_SelectiveMagma_90
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_SelectiveMagma_90)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_SelectiveMagma_90
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_1878
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-semigroup
d_'8851''45'semigroup_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'8851''45'semigroup_250 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_652 -> T_Semigroup_206
d_'8851''45'semigroup_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_Semigroup_206
du_'8851''45'semigroup_250 T_TotalOrder_652
v3
du_'8851''45'semigroup_250 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'8851''45'semigroup_250 :: T_TotalOrder_652 -> T_Semigroup_206
du_'8851''45'semigroup_250 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_Semigroup_206
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semigroup_206)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semigroup_206
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_1870
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-semilattice
d_'8851''45'semilattice_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_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8851''45'semilattice_252 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Semilattice_402
d_'8851''45'semilattice_252 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> T_Semilattice_402
du_'8851''45'semilattice_252 T_TotalOrder_652
v3
du_'8851''45'semilattice_252 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8851''45'semilattice_252 :: T_TotalOrder_652 -> T_Semilattice_402
du_'8851''45'semilattice_252 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> T_Semilattice_402
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semilattice_402)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semilattice_402
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_1876
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-triangulate
d_'8851''45'triangulate_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_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> Any
-> Any
-> Any
d_'8851''45'triangulate_254 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_254 T_TotalOrder_652
v3
du_'8851''45'triangulate_254 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_254 :: T_TotalOrder_652 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_254 T_TotalOrder_652
v0
  = let v1 :: t
v1
          = (T_TotalOrder_652 -> T_TotalPreorder_204) -> Any -> t
forall a b. a -> b
coe
              T_TotalOrder_652 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_732
              (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_204
 -> T_MinOperator_84 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_204 -> T_MinOperator_84 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_2114
            ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1))
            ((T_MaxOperator_114 -> T_MinOperator_84) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-zero
d_'8851''45'zero_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_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'zero_256 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_256 T_TotalOrder_652
v3
du_'8851''45'zero_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_256 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_256 T_TotalOrder_652
v0
  = let v1 :: t
v1 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
                      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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
                      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'_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_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_258 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'691'_258 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_258 T_TotalOrder_652
v3
du_'8851''45'zero'691'_258 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_258 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_258 T_TotalOrder_652
v0
  = let v1 :: t
v1 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
              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'_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_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'737'_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_260 T_TotalOrder_652
v3
du_'8851''45'zero'737'_260 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_260 :: T_TotalOrder_652 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_260 T_TotalOrder_652
v0
  = let v1 :: t
v1 = (T_TotalOrder_652 -> T_MaxOperator_114) -> Any -> t
forall a b. a -> b
coe T_TotalOrder_652 -> T_MaxOperator_114
du_maxOperator_176 (T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
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_114 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_114 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
              Any
forall {t}. t
v1 Any
v2 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))