{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Algebra.Construct.NaturalChoice.Max where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Base
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MaxOp
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Min
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd

-- Algebra.Construct.NaturalChoice.Max._.totalPreorder
d_totalPreorder_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240
d_totalPreorder_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_TotalPreorder_240
d_totalPreorder_60 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_TotalPreorder_240
du_totalPreorder_60 T_TotalOrder_986
v3
du_totalPreorder_60 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240
du_totalPreorder_60 :: T_TotalOrder_986 -> T_TotalPreorder_240
du_totalPreorder_60 T_TotalOrder_986
v0
  = (T_TotalOrder_986 -> T_TotalPreorder_240)
-> Any -> T_TotalPreorder_240
forall a b. a -> b
coe
      T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)
-- Algebra.Construct.NaturalChoice.Max.Min.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_110 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'y'8776'x_110 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_110 T_TotalOrder_986
v3
du_x'8804'y'8658'x'8851'y'8776'x_110 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'y'8776'x_110 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'y'8776'x_110 T_TotalOrder_986
v0
  = (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'x'8851'y'8776'x_128
      ((T_TotalOrder_986 -> T_TotalOrder_986) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_928
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Max.Min.x≤y⇒y⊓x≈x
d_x'8804'y'8658'y'8851'x'8776'x_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'y'8851'x'8776'x_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'y'8851'x'8776'x_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_114 T_TotalOrder_986
v3
du_x'8804'y'8658'y'8851'x'8776'x_114 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'y'8851'x'8776'x_114 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8804'y'8658'y'8851'x'8776'x_114 T_TotalOrder_986
v0
  = (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'y'8851'x'8776'x_158
      ((T_TotalOrder_986 -> T_TotalOrder_986) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_928
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Max._⊔_
d__'8852'__192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d__'8852'__192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du__'8852'__192 T_TotalOrder_986
v3
du__'8852'__192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8852'__192 :: T_TotalOrder_986 -> Any -> Any -> Any
du__'8852'__192 T_TotalOrder_986
v0
  = (T_TotalOrder_986 -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_TotalOrder_986 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__102
      ((T_TotalOrder_986 -> T_TotalOrder_986) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_928
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Max.maxOperator
d_maxOperator_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138
d_maxOperator_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_MaxOperator_138
d_maxOperator_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 T_TotalOrder_986
v3
du_maxOperator_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138
du_maxOperator_194 :: T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 T_TotalOrder_986
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_MaxOperator_138)
-> Any -> Any -> Any -> T_MaxOperator_138
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_MaxOperator_138
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.C_constructor_168
      ((T_TotalOrder_986 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__102
         ((T_TotalOrder_986 -> T_TotalOrder_986) -> Any -> Any
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_928
            (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 ->
            (T_TotalOrder_986 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'y'8851'x'8776'x_158
              ((T_TotalOrder_986 -> T_TotalOrder_986) -> Any -> Any
forall a b. a -> b
coe
                 T_TotalOrder_986 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_928
                 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
              (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v1)))
      ((T_TotalOrder_986 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_x'8804'y'8658'x'8851'y'8776'x_128
         ((T_TotalOrder_986 -> T_TotalOrder_986) -> Any -> Any
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalOrder_928
            (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0)))
-- Algebra.Construct.NaturalChoice.Max._.mono-≤-distrib-⊔
d_mono'45''8804''45'distrib'45''8852'_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
d_mono'45''8804''45'distrib'45''8852'_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8852'_198 T_TotalOrder_986
v3
du_mono'45''8804''45'distrib'45''8852'_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_198 :: T_TotalOrder_986
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
du_mono'45''8804''45'distrib'45''8852'_198 T_TotalOrder_986
v0
  = (T_TotalPreorder_240
 -> T_MaxOperator_138
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any)
-> Any
-> Any
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
forall a b. a -> b
coe
      T_TotalPreorder_240
-> T_MaxOperator_138
-> (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'_190
      ((T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
         T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
         (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
      ((T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≤x
d_x'8851'y'8804'x_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d_x'8851'y'8804'x_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'x_200 T_TotalOrder_986
v3
du_x'8851'y'8804'x_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_200 :: T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'x_200 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_2924
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⇒x⊓z≤y
d_x'8804'y'8658'x'8851'z'8804'y_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'x'8851'z'8804'y_202 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_202 T_TotalOrder_986
v3
du_x'8804'y'8658'x'8851'z'8804'y_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_202 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'x'8851'z'8804'y_202 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_3276
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⇒z⊓x≤y
d_x'8804'y'8658'z'8851'x'8804'y_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8658'z'8851'x'8804'y_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_204 T_TotalOrder_986
v3
du_x'8804'y'8658'z'8851'x'8804'y_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_204 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8658'z'8851'x'8804'y_204 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_3288
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≤y
d_x'8851'y'8804'y_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d_x'8851'y'8804'y_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'y_206 T_TotalOrder_986
v3
du_x'8851'y'8804'y_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_206 :: T_TotalOrder_986 -> Any -> Any -> Any
du_x'8851'y'8804'y_206 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_2950
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≈x⇒x≤y
d_x'8851'y'8776'x'8658'x'8804'y_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'x'8658'x'8804'y_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_208 T_TotalOrder_986
v3
du_x'8851'y'8776'x'8658'x'8804'y_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_208 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'x'8658'x'8804'y_208 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3184
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x⊓y≈y⇒y≤x
d_x'8851'y'8776'y'8658'y'8804'x_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_x'8851'y'8776'y'8658'y'8804'x_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_210 T_TotalOrder_986
v3
du_x'8851'y'8776'y'8658'y'8804'x_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_210 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_x'8851'y'8776'y'8658'y'8804'x_210 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3216
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⊓z⇒x≤y
d_x'8804'y'8851'z'8658'x'8804'y_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'y_212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_212 T_TotalOrder_986
v3
du_x'8804'y'8851'z'8658'x'8804'y_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_212 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'y_212 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_3300
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.x≤y⊓z⇒x≤z
d_x'8804'y'8851'z'8658'x'8804'z_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_x'8804'y'8851'z'8658'x'8804'z_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_214 T_TotalOrder_986
v3
du_x'8804'y'8851'z'8658'x'8804'z_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_214 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_x'8804'y'8851'z'8658'x'8804'z_214 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_3314
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-assoc
d_'8851''45'assoc_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_'8851''45'assoc_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_216 T_TotalOrder_986
v3
du_'8851''45'assoc_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_216 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'assoc_216 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_3060
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-band
d_'8851''45'band_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_620
d_'8851''45'band_218 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_Band_620
d_'8851''45'band_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_Band_620
du_'8851''45'band_218 T_TotalOrder_986
v3
du_'8851''45'band_218 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_620
du_'8851''45'band_218 :: T_TotalOrder_986 -> T_Band_620
du_'8851''45'band_218 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_Band_620
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_Band_620)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_Band_620
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_3168
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-comm
d_'8851''45'comm_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
d_'8851''45'comm_220 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any
du_'8851''45'comm_220 T_TotalOrder_986
v3
du_'8851''45'comm_220 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_220 :: T_TotalOrder_986 -> Any -> Any -> Any
du_'8851''45'comm_220 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_688
d_'8851''45'commutativeSemigroup_222 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_CommutativeSemigroup_688
d_'8851''45'commutativeSemigroup_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_CommutativeSemigroup_688
du_'8851''45'commutativeSemigroup_222 T_TotalOrder_986
v3
du_'8851''45'commutativeSemigroup_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_688
du_'8851''45'commutativeSemigroup_222 :: T_TotalOrder_986 -> T_CommutativeSemigroup_688
du_'8851''45'commutativeSemigroup_222 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_CommutativeSemigroup_688
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_CommutativeSemigroup_688)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> T_CommutativeSemigroup_688
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_3170
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-cong
d_'8851''45'cong_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_224 T_TotalOrder_986
v3
du_'8851''45'cong_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_224 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong_224 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_3046
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-congʳ
d_'8851''45'cong'691'_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'691'_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_226 T_TotalOrder_986
v3
du_'8851''45'cong'691'_226 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_226 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'691'_226 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_3036
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-congˡ
d_'8851''45'cong'737'_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'cong'737'_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_228 T_TotalOrder_986
v3
du_'8851''45'cong'737'_228 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_228 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'cong'737'_228 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_2998
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-idem
d_'8851''45'idem_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_230 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> Any -> Any
d_'8851''45'idem_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any
du_'8851''45'idem_230 T_TotalOrder_986
v3
du_'8851''45'idem_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_230 :: T_TotalOrder_986 -> Any -> Any
du_'8851''45'idem_230 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_3100
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-identity
d_'8851''45'identity_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'identity_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_232 T_TotalOrder_986
v3
du_'8851''45'identity_232 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_232 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'identity_232 T_TotalOrder_986
v0
  = let v1 :: Any
v1 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_160
                      Any
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_166
                      Any
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'_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'691'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_234 T_TotalOrder_986
v3
du_'8851''45'identity'691'_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_234 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'691'_234 T_TotalOrder_986
v0
  = let v1 :: Any
v1 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_166
              Any
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'_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'identity'737'_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_236 T_TotalOrder_986
v3
du_'8851''45'identity'737'_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_236 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'identity'737'_236 T_TotalOrder_986
v0
  = let v1 :: Any
v1 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_160
              Any
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_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
d_'8851''45'isBand_238 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_IsBand_526
d_'8851''45'isBand_238 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_IsBand_526
du_'8851''45'isBand_238 T_TotalOrder_986
v3
du_'8851''45'isBand_238 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
du_'8851''45'isBand_238 :: T_TotalOrder_986 -> T_IsBand_526
du_'8851''45'isBand_238 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_IsBand_526
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsBand_526)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsBand_526
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_3150
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_568
d_'8851''45'isCommutativeSemigroup_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_IsCommutativeSemigroup_568
d_'8851''45'isCommutativeSemigroup_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsCommutativeSemigroup_568
du_'8851''45'isCommutativeSemigroup_240 T_TotalOrder_986
v3
du_'8851''45'isCommutativeSemigroup_240 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_568
du_'8851''45'isCommutativeSemigroup_240 :: T_TotalOrder_986 -> T_IsCommutativeSemigroup_568
du_'8851''45'isCommutativeSemigroup_240 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_IsCommutativeSemigroup_568
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsCommutativeSemigroup_568)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> T_IsCommutativeSemigroup_568
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_3152
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isMagma
d_'8851''45'isMagma_242 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8851''45'isMagma_242 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_IsMagma_178
d_'8851''45'isMagma_242 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsMagma_178
du_'8851''45'isMagma_242 T_TotalOrder_986
v3
du_'8851''45'isMagma_242 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8851''45'isMagma_242 :: T_TotalOrder_986 -> T_IsMagma_178
du_'8851''45'isMagma_242 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_IsMagma_178
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsMagma_178)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsMagma_178
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_3146
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isMonoid
d_'8851''45'isMonoid_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
d_'8851''45'isMonoid_244 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_IsMonoid_712
d_'8851''45'isMonoid_244 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_IsMonoid_712
du_'8851''45'isMonoid_244 T_TotalOrder_986
v3
du_'8851''45'isMonoid_244 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
du_'8851''45'isMonoid_244 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_IsMonoid_712
du_'8851''45'isMonoid_244 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> (Any -> Any) -> T_IsMonoid_712
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> (Any -> Any) -> T_IsMonoid_712)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> (Any -> Any) -> T_IsMonoid_712
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_3158
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_246 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_450
d_'8851''45'isSelectiveMagma_246 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_IsSelectiveMagma_450
d_'8851''45'isSelectiveMagma_246 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsSelectiveMagma_450
du_'8851''45'isSelectiveMagma_246 T_TotalOrder_986
v3
du_'8851''45'isSelectiveMagma_246 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_450
du_'8851''45'isSelectiveMagma_246 :: T_TotalOrder_986 -> T_IsSelectiveMagma_450
du_'8851''45'isSelectiveMagma_246 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_IsSelectiveMagma_450
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsSelectiveMagma_450)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSelectiveMagma_450
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3154
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-isSemigroup
d_'8851''45'isSemigroup_248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8851''45'isSemigroup_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_IsSemigroup_488
d_'8851''45'isSemigroup_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_IsSemigroup_488
du_'8851''45'isSemigroup_248 T_TotalOrder_986
v3
du_'8851''45'isSemigroup_248 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8851''45'isSemigroup_248 :: T_TotalOrder_986 -> T_IsSemigroup_488
du_'8851''45'isSemigroup_248 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_IsSemigroup_488
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSemigroup_488)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_3148
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-glb
d_'8851''45'glb_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'glb_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_250 T_TotalOrder_986
v3
du_'8851''45'glb_250 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_250 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'glb_250 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_3394
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-magma
d_'8851''45'magma_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
d_'8851''45'magma_252 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_Magma_74
d_'8851''45'magma_252 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_Magma_74
du_'8851''45'magma_252 T_TotalOrder_986
v3
du_'8851''45'magma_252 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
du_'8851''45'magma_252 :: T_TotalOrder_986 -> T_Magma_74
du_'8851''45'magma_252 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_Magma_74
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_Magma_74)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_Magma_74
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_3164
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-mono-≤
d_'8851''45'mono'45''8804'_254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'45''8804'_254 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_254 T_TotalOrder_986
v3
du_'8851''45'mono'45''8804'_254 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_254 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'45''8804'_254 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_3322
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoid
d_'8851''45'monoid_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'8851''45'monoid_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_Monoid_914
d_'8851''45'monoid_256 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Monoid_914
du_'8851''45'monoid_256 T_TotalOrder_986
v3
du_'8851''45'monoid_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'8851''45'monoid_256 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Monoid_914
du_'8851''45'monoid_256 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> (Any -> Any) -> T_Monoid_914
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> (Any -> Any) -> T_Monoid_914)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> (Any -> Any) -> T_Monoid_914
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_3176
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoʳ-≤
d_'8851''45'mono'691''45''8804'_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_258 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'691''45''8804'_258 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_258 T_TotalOrder_986
v3
du_'8851''45'mono'691''45''8804'_258 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_258 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'691''45''8804'_258 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_3382
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-monoˡ-≤
d_'8851''45'mono'737''45''8804'_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
-> Any
d_'8851''45'mono'737''45''8804'_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_260 T_TotalOrder_986
v3
du_'8851''45'mono'737''45''8804'_260 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_260 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any -> Any
du_'8851''45'mono'737''45''8804'_260 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_3372
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-sel
d_'8851''45'sel_262 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> T__'8846'__30
d_'8851''45'sel_262 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_262 T_TotalOrder_986
v3
du_'8851''45'sel_262 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_262 :: T_TotalOrder_986 -> Any -> Any -> T__'8846'__30
du_'8851''45'sel_262 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> T__'8846'__30
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_3104
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-selectiveMagma
d_'8851''45'selectiveMagma_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_130
d_'8851''45'selectiveMagma_264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_SelectiveMagma_130
d_'8851''45'selectiveMagma_264 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_SelectiveMagma_130
du_'8851''45'selectiveMagma_264 T_TotalOrder_986
v3
du_'8851''45'selectiveMagma_264 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_130
du_'8851''45'selectiveMagma_264 :: T_TotalOrder_986 -> T_SelectiveMagma_130
du_'8851''45'selectiveMagma_264 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_SelectiveMagma_130
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_SelectiveMagma_130)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_SelectiveMagma_130
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_3172
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-semigroup
d_'8851''45'semigroup_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_'8851''45'semigroup_266 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_Semigroup_558
d_'8851''45'semigroup_266 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> T_Semigroup_558
du_'8851''45'semigroup_266 T_TotalOrder_986
v3
du_'8851''45'semigroup_266 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_'8851''45'semigroup_266 :: T_TotalOrder_986 -> T_Semigroup_558
du_'8851''45'semigroup_266 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> T_Semigroup_558
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semigroup_558)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semigroup_558
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_3166
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-triangulate
d_'8851''45'triangulate_268 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_268 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> Any
-> Any
-> Any
d_'8851''45'triangulate_268 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_268 T_TotalOrder_986
v3
du_'8851''45'triangulate_268 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_268 :: T_TotalOrder_986 -> Any -> Any -> Any -> Any
du_'8851''45'triangulate_268 T_TotalOrder_986
v0
  = let v1 :: Any
v1
          = (T_TotalOrder_986 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
              T_TotalOrder_986 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_1088
              (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
    Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      (let v2 :: Any
v2 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
v0) in
       Any -> Any
forall a b. a -> b
coe
         ((T_TotalPreorder_240
 -> T_MinOperator_106 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_TotalPreorder_240
-> T_MinOperator_106 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_3408
            ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> Any -> Any
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
               (Any -> Any
forall a b. a -> b
coe Any
v1))
            ((T_MaxOperator_138 -> T_MinOperator_106) -> Any -> Any
forall a b. a -> b
coe
               T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
               (Any -> Any
forall a b. a -> b
coe Any
v2))))
-- Algebra.Construct.NaturalChoice.Max._.⊓-zero
d_'8851''45'zero_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_270 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> T_Σ_14
d_'8851''45'zero_270 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_270 T_TotalOrder_986
v3
du_'8851''45'zero_270 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_270 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> T_Σ_14
du_'8851''45'zero_270 T_TotalOrder_986
v0
  = let v1 :: Any
v1 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_166
                      Any
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_160
                      Any
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'_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_272 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'691'_272 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_272 T_TotalOrder_986
v3
du_'8851''45'zero'691'_272 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_272 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'691'_272 T_TotalOrder_986
v0
  = let v1 :: Any
v1 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_160
              Any
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'_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_274 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> Any
-> (Any -> Any)
-> Any
-> Any
d_'8851''45'zero'737'_274 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_274 T_TotalOrder_986
v3
du_'8851''45'zero'737'_274 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_274 :: T_TotalOrder_986 -> Any -> (Any -> Any) -> Any -> Any
du_'8851''45'zero'737'_274 T_TotalOrder_986
v0
  = let v1 :: Any
v1 = (T_TotalOrder_986 -> T_MaxOperator_138) -> Any -> Any
forall a b. a -> b
coe T_TotalOrder_986 -> T_MaxOperator_138
du_maxOperator_194 (T_TotalOrder_986 -> Any
forall a b. a -> b
coe T_TotalOrder_986
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_138 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_MaxOperator_138 -> Any -> Any -> Any -> Any
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_166
              Any
v1 Any
v2 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))