{-# 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.MaxOp where

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

-- Algebra.Construct.NaturalChoice.MaxOp._._≈_
d__'8776'__20 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__20 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> ()
d__'8776'__20 = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Construct.NaturalChoice.MaxOp._._≲_
d__'8818'__22 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> ()
d__'8818'__22 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> ()
d__'8818'__22 = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x≤y⇒x⊓z≤y
d_x'8804'y'8658'x'8851'z'8804'y_84 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_84 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_84 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_84 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8804'y'8658'x'8851'z'8804'y_84 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_84 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_84 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_1982
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x≤y⇒z⊓x≤y
d_x'8804'y'8658'z'8851'x'8804'y_86 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_86 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_86 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_86 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8804'y'8658'z'8851'x'8804'y_86 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_86 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_86 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_1994
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x≤y⊓z⇒x≤y
d_x'8804'y'8851'z'8658'x'8804'y_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_88 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_88 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_88 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8804'y'8851'z'8658'x'8804'y_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_88 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_88 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_2006
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x≤y⊓z⇒x≤z
d_x'8804'y'8851'z'8658'x'8804'z_90 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_90 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_90 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_90 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8804'y'8851'z'8658'x'8804'z_90 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_90 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_90 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_2020
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x⊓y≈x⇒x≤y
d_x'8851'y'8776'x'8658'x'8804'y_92 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_92 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_92 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_92 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8851'y'8776'x'8658'x'8804'y_92 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_92 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_92 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_1890
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x⊓y≈y⇒y≤x
d_x'8851'y'8776'y'8658'y'8804'x_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_94 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_94 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_94 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8851'y'8776'y'8658'y'8804'x_94 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_94 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_94 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_1922
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x⊓y≤x
d_x'8851'y'8804'x_96 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_96 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8804'x_96 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_96 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8851'y'8804'x_96 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_96 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_96 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_1626
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.x⊓y≤y
d_x'8851'y'8804'y_98 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_98 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8804'y_98 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_98 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_x'8851'y'8804'y_98 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_98 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_98 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_1652
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-assoc
d_'8851''45'assoc_100 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_100 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'assoc_100 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_100 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'assoc_100 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_100 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_100 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_1762
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-band
d_'8851''45'band_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_266
d_'8851''45'band_102 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_Band_266
d_'8851''45'band_102 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Band_266
du_'8851''45'band_102 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'band_102 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Band_266
du_'8851''45'band_102 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Band_266
du_'8851''45'band_102 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Band_266)
-> AgdaAny -> AgdaAny -> T_Band_266
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Band_266
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_1872
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-comm
d_'8851''45'comm_104 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_104 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'comm_104 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_104 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'comm_104 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_104 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_104 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_1674
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-commutativeSemigroup
d_'8851''45'commutativeSemigroup_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_332
d_'8851''45'commutativeSemigroup_106 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_CommutativeSemigroup_332
d_'8851''45'commutativeSemigroup_106 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_106 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'commutativeSemigroup_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_106 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> T_CommutativeSemigroup_332
du_'8851''45'commutativeSemigroup_106 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> T_CommutativeSemigroup_332)
-> AgdaAny -> AgdaAny -> T_CommutativeSemigroup_332
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> T_CommutativeSemigroup_332
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_1874
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-cong
d_'8851''45'cong_108 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_108 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'cong_108 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong_108 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'cong_108 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_108 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong_108 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_1748
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-congʳ
d_'8851''45'cong'691'_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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_110 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'cong'691'_110 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'691'_110 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'cong'691'_110 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_110 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'691'_110 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_1738
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-congˡ
d_'8851''45'cong'737'_112 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_112 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'cong'737'_112 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'737'_112 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'cong'737'_112 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_112 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'737'_112 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_1700
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-glb
d_'8851''45'glb_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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_114 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'glb_114 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4 = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'glb_114 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'glb_114 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_114 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'glb_114 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_2100
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-idem
d_'8851''45'idem_116 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny
d_'8851''45'idem_116 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
d_'8851''45'idem_116 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> AgdaAny -> AgdaAny
du_'8851''45'idem_116 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'idem_116 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny
du_'8851''45'idem_116 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> AgdaAny -> AgdaAny
du_'8851''45'idem_116 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_1802
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-identity
d_'8851''45'identity_118 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_118 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8851''45'identity_118 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
  = T_MaxOperator_114 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'identity_118 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
du_'8851''45'identity_118 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_118 :: T_MaxOperator_114 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'identity_118 T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
              T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
              T_MaxOperator_114
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-identityʳ
d_'8851''45'identity'691'_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_120 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'identity'691'_120 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_120 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'identity'691'_120 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_120 :: T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_120 T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
  = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
      T_MaxOperator_114
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-identityˡ
d_'8851''45'identity'737'_122 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_122 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'identity'737'_122 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_122 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'identity'737'_122 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_122 :: T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_122 T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
  = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
      T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isBand
d_'8851''45'isBand_124 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8851''45'isBand_124 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_IsBand_230
d_'8851''45'isBand_124 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsBand_230
du_'8851''45'isBand_124 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isBand_124 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8851''45'isBand_124 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsBand_230
du_'8851''45'isBand_124 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsBand_230)
-> AgdaAny -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsBand_230
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_1852
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isCommutativeSemigroup
d_'8851''45'isCommutativeSemigroup_126 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_270
d_'8851''45'isCommutativeSemigroup_126 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_IsCommutativeSemigroup_270
d_'8851''45'isCommutativeSemigroup_126 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_126 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isCommutativeSemigroup_126 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_126 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> T_IsCommutativeSemigroup_270
du_'8851''45'isCommutativeSemigroup_126 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> T_IsCommutativeSemigroup_270)
-> AgdaAny -> AgdaAny -> T_IsCommutativeSemigroup_270
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> T_IsCommutativeSemigroup_270
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_1854
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isMagma
d_'8851''45'isMagma_128 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8851''45'isMagma_128 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_IsMagma_86
d_'8851''45'isMagma_128 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsMagma_86
du_'8851''45'isMagma_128 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isMagma_128 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8851''45'isMagma_128 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsMagma_86
du_'8851''45'isMagma_128 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsMagma_86
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_1848
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isMonoid
d_'8851''45'isMonoid_130 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'8851''45'isMonoid_130 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_358
d_'8851''45'isMonoid_130 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_358
du_'8851''45'isMonoid_130 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isMonoid_130 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'8851''45'isMonoid_130 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_358
du_'8851''45'isMonoid_130 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> T_IsMonoid_358)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_358
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_358
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_1862
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isSelectiveMagma
d_'8851''45'isSelectiveMagma_132 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
d_'8851''45'isSelectiveMagma_132 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_IsSelectiveMagma_158
d_'8851''45'isSelectiveMagma_132 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_132 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isSelectiveMagma_132 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_132 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsSelectiveMagma_158
du_'8851''45'isSelectiveMagma_132 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> T_IsSelectiveMagma_158
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_1858
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isSemigroup
d_'8851''45'isSemigroup_134 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8851''45'isSemigroup_134 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_IsSemigroup_194
d_'8851''45'isSemigroup_134 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsSemigroup_194
du_'8851''45'isSemigroup_134 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isSemigroup_134 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8851''45'isSemigroup_134 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsSemigroup_194
du_'8851''45'isSemigroup_134 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_1850
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-isSemilattice
d_'8851''45'isSemilattice_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8851''45'isSemilattice_136 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_IsSemilattice_312
d_'8851''45'isSemilattice_136 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsSemilattice_312
du_'8851''45'isSemilattice_136 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'isSemilattice_136 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8851''45'isSemilattice_136 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_IsSemilattice_312
du_'8851''45'isSemilattice_136 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemilattice_312)
-> AgdaAny -> AgdaAny -> T_IsSemilattice_312
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_1856
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-magma
d_'8851''45'magma_138 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
d_'8851''45'magma_138 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_Magma_36
d_'8851''45'magma_138 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Magma_36
du_'8851''45'magma_138 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'magma_138 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
du_'8851''45'magma_138 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Magma_36
du_'8851''45'magma_138 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Magma_36)
-> AgdaAny -> AgdaAny -> T_Magma_36
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Magma_36
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_1868
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-mono-≤
d_'8851''45'mono'45''8804'_140 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_140 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'mono'45''8804'_140 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'45''8804'_140 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'mono'45''8804'_140 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_140 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'45''8804'_140 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_2028
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-monoid
d_'8851''45'monoid_142 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'8851''45'monoid_142 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_506
d_'8851''45'monoid_142 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_506
du_'8851''45'monoid_142 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'monoid_142 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'8851''45'monoid_142 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_506
du_'8851''45'monoid_142 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> (AgdaAny -> AgdaAny)
 -> T_Monoid_506)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_506
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_506
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_1882
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-monoʳ-≤
d_'8851''45'mono'691''45''8804'_144 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_144 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'mono'691''45''8804'_144 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'691''45''8804'_144 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'mono'691''45''8804'_144 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_144 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'691''45''8804'_144 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_2088
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-monoˡ-≤
d_'8851''45'mono'737''45''8804'_146 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_146 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'mono'737''45''8804'_146 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'737''45''8804'_146 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'mono'737''45''8804'_146 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_146 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'737''45''8804'_146 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_2078
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-sel
d_'8851''45'sel_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_150 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8851''45'sel_150 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4 = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''45'sel_150 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'sel_150 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_150 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''45'sel_150 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_1806
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-selectiveMagma
d_'8851''45'selectiveMagma_152 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_90
d_'8851''45'selectiveMagma_152 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_SelectiveMagma_90
d_'8851''45'selectiveMagma_152 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_SelectiveMagma_90
du_'8851''45'selectiveMagma_152 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'selectiveMagma_152 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_90
du_'8851''45'selectiveMagma_152 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_SelectiveMagma_90
du_'8851''45'selectiveMagma_152 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_SelectiveMagma_90)
-> AgdaAny -> AgdaAny -> T_SelectiveMagma_90
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_SelectiveMagma_90
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_1878
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-semigroup
d_'8851''45'semigroup_154 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'8851''45'semigroup_154 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_Semigroup_206
d_'8851''45'semigroup_154 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Semigroup_206
du_'8851''45'semigroup_154 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'semigroup_154 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'8851''45'semigroup_154 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Semigroup_206
du_'8851''45'semigroup_154 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semigroup_206)
-> AgdaAny -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semigroup_206
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_1870
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-semilattice
d_'8851''45'semilattice_156 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8851''45'semilattice_156 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_Semilattice_402
d_'8851''45'semilattice_156 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Semilattice_402
du_'8851''45'semilattice_156 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'semilattice_156 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8851''45'semilattice_156 :: T_TotalPreorder_204 -> T_MaxOperator_114 -> T_Semilattice_402
du_'8851''45'semilattice_156 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semilattice_402)
-> AgdaAny -> AgdaAny -> T_Semilattice_402
forall a b. a -> b
coe
      T_TotalPreorder_204 -> T_MinOperator_84 -> T_Semilattice_402
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_1876
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-triangulate
d_'8851''45'triangulate_158 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_158 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'triangulate_158 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_158 T_TotalPreorder_204
v3 T_MaxOperator_114
v4
du_'8851''45'triangulate_158 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_158 :: T_TotalPreorder_204
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_158 T_TotalPreorder_204
v0 T_MaxOperator_114
v1
  = (T_TotalPreorder_204
 -> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_2114
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-zero
d_'8851''45'zero_160 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_160 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8851''45'zero_160 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
  = T_MaxOperator_114 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'zero_160 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
du_'8851''45'zero_160 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_160 :: T_MaxOperator_114 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'zero_160 T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
              T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
              T_MaxOperator_114
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-zeroʳ
d_'8851''45'zero'691'_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_162 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'zero'691'_162 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_162 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'zero'691'_162 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_162 :: T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_162 T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
  = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_136
      T_MaxOperator_114
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
-- Algebra.Construct.NaturalChoice.MaxOp.Min.⊓-zeroˡ
d_'8851''45'zero'737'_164 ::
  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_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_164 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'zero'737'_164 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_164 T_MaxOperator_114
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'zero'737'_164 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_164 :: T_MaxOperator_114
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_164 T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
  = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_142
      T_MaxOperator_114
v0 AgdaAny
v1 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
-- Algebra.Construct.NaturalChoice.MaxOp.mono-≤-distrib-⊔
d_mono'45''8804''45'distrib'45''8852'_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_172 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_172 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
                                          AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
  = T_TotalPreorder_204
-> T_MaxOperator_114
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_172 T_TotalPreorder_204
v3 T_MaxOperator_114
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
du_mono'45''8804''45'distrib'45''8852'_172 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_114 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_172 :: T_TotalPreorder_204
-> T_MaxOperator_114
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_172 T_TotalPreorder_204
v0 T_MaxOperator_114
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4
  = (T_TotalPreorder_204
 -> T_MinOperator_84
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalPreorder_204
-> T_MinOperator_84
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_mono'45''8804''45'distrib'45''8851'_1936
      ((T_TotalPreorder_204 -> T_TotalPreorder_204) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_204 -> T_TotalPreorder_204
MAlonzo.Code.Relation.Binary.Construct.Converse.du_totalPreorder_718
         (T_TotalPreorder_204 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_204
v0))
      ((T_MaxOperator_114 -> T_MinOperator_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_114 -> T_MinOperator_84
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_160
         (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v1))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v6 AgdaAny
v5))