{-# 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.Flip.EqAndOrd
d__'8776'__22 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> ()
d__'8776'__22 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> ()
d__'8776'__22 = T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
d__'8818'__24 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> ()
d__'8818'__24 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> ()
d__'8818'__24 = T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
d_x'8804'y'8658'x'8851'z'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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_98 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8658'x'8851'z'8804'y_98 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_98 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8804'y'8658'x'8851'z'8804'y_98 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_98 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'x'8851'z'8804'y_98 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'x'8851'z'8804'y_3160
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8804'y'8658'z'8851'x'8804'y_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_100 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8658'z'8851'x'8804'y_100 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_100 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8804'y'8658'z'8851'x'8804'y_100 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_100 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8658'z'8851'x'8804'y_100 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8658'z'8851'x'8804'y_3172
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8804'y'8851'z'8658'x'8804'y_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_102 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'y_102 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_102 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8804'y'8851'z'8658'x'8804'y_102 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_102 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'y_102 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'y_3184
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8804'y'8851'z'8658'x'8804'z_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_104 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8804'y'8851'z'8658'x'8804'z_104 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_104 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8804'y'8851'z'8658'x'8804'z_104 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_104 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_x'8804'y'8851'z'8658'x'8804'z_104 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8804'y'8851'z'8658'x'8804'z_3198
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8851'y'8776'x'8658'x'8804'y_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_106 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8776'x'8658'x'8804'y_106 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_106 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8851'y'8776'x'8658'x'8804'y_106 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_106 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'x'8658'x'8804'y_106 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'x'8658'x'8804'y_3068
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8851'y'8776'y'8658'y'8804'x_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_108 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8776'y'8658'y'8804'x_108 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_108 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8851'y'8776'y'8658'y'8804'x_108 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_108 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8776'y'8658'y'8804'x_108 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8776'y'8658'y'8804'x_3100
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8851'y'8804'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_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'x_110 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8804'x_110 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_110 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8851'y'8804'x_110 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_110 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'x_110 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'x_2808
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_x'8851'y'8804'y_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny
d_x'8851'y'8804'y_112 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8851'y'8804'y_112 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_112 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_x'8851'y'8804'y_112 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_112 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8851'y'8804'y_112 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_x'8851'y'8804'y_2834
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'assoc_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'assoc_114 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'assoc_114 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_114 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'assoc_114 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_114 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'assoc_114 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'band_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_Band_596
d_'8851''45'band_116 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_Band_596
d_'8851''45'band_116 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Band_596
du_'8851''45'band_116 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'band_116 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_Band_596
du_'8851''45'band_116 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Band_596
du_'8851''45'band_116 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Band_596)
-> AgdaAny -> AgdaAny -> T_Band_596
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_Band_596
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'band_3052
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'comm_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'comm_118 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'comm_118 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_118 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'comm_118 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_118 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'comm_118 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'commutativeSemigroup_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
d_'8851''45'commutativeSemigroup_120 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_CommutativeSemigroup_662
d_'8851''45'commutativeSemigroup_120 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_120 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'commutativeSemigroup_120 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_120 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> T_CommutativeSemigroup_662
du_'8851''45'commutativeSemigroup_120 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> T_CommutativeSemigroup_662)
-> AgdaAny -> AgdaAny -> T_CommutativeSemigroup_662
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> T_CommutativeSemigroup_662
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'commutativeSemigroup_3054
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'cong_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong_122 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'cong_122 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong_122 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'cong_122 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong_122 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong_122 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'cong'691'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'691'_124 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'cong'691'_124 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'691'_124 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'cong'691'_124 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'691'_124 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'691'_124 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'691'_2920
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'cong'737'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'cong'737'_126 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'cong'737'_126 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'737'_126 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'cong'737'_126 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'cong'737'_126 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'cong'737'_126 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong'737'_2882
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'glb_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'glb_128 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'glb_128 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4 = T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'glb_128 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'glb_128 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'glb_128 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'glb_128 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'glb_3278
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'idem_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny
d_'8851''45'idem_130 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
d_'8851''45'idem_130 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny
du_'8851''45'idem_130 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'idem_130 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny
du_'8851''45'idem_130 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny
du_'8851''45'idem_130 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'idem_2984
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'identity_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'identity_132 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8851''45'identity_132 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
= T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'identity_132 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
du_'8851''45'identity_132 ::
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'identity_132 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'identity_132 T_MaxOperator_128
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_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
T_MaxOperator_128
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_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
T_MaxOperator_128
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
d_'8851''45'identity'691'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'691'_134 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'identity'691'_134 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_134 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'identity'691'_134 ::
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_134 :: T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'691'_134 T_MaxOperator_128
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
= (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
T_MaxOperator_128
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
d_'8851''45'identity'737'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'identity'737'_136 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'identity'737'_136 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_136 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'identity'737'_136 ::
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_136 :: T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'identity'737'_136 T_MaxOperator_128
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
= (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
T_MaxOperator_128
v0 AgdaAny
v1 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
d_'8851''45'isBand_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8851''45'isBand_138 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_IsBand_508
d_'8851''45'isBand_138 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsBand_508
du_'8851''45'isBand_138 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'isBand_138 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8851''45'isBand_138 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsBand_508
du_'8851''45'isBand_138 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508)
-> AgdaAny -> AgdaAny -> T_IsBand_508
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_3034
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'isCommutativeSemigroup_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
d_'8851''45'isCommutativeSemigroup_140 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_IsCommutativeSemigroup_548
d_'8851''45'isCommutativeSemigroup_140 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_140 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'isCommutativeSemigroup_140 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_140 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> T_IsCommutativeSemigroup_548
du_'8851''45'isCommutativeSemigroup_140 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> T_IsCommutativeSemigroup_548)
-> AgdaAny -> AgdaAny -> T_IsCommutativeSemigroup_548
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> T_IsCommutativeSemigroup_548
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isCommutativeSemigroup_3036
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'isMagma_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8851''45'isMagma_142 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_IsMagma_176
d_'8851''45'isMagma_142 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsMagma_176
du_'8851''45'isMagma_142 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'isMagma_142 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8851''45'isMagma_142 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsMagma_176
du_'8851''45'isMagma_142 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsMagma_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsMagma_176
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMagma_3030
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'isMonoid_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'8851''45'isMonoid_144 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_686
d_'8851''45'isMonoid_144 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_686
du_'8851''45'isMonoid_144 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'isMonoid_144 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
du_'8851''45'isMonoid_144 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_686
du_'8851''45'isMonoid_144 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_686)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_686
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_IsMonoid_686
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isMonoid_3042
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'isSelectiveMagma_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
d_'8851''45'isSelectiveMagma_146 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_IsSelectiveMagma_436
d_'8851''45'isSelectiveMagma_146 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_146 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'isSelectiveMagma_146 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_146 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSelectiveMagma_436
du_'8851''45'isSelectiveMagma_146 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> T_IsSelectiveMagma_436
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSelectiveMagma_3038
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'isSemigroup_148 ::
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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8851''45'isSemigroup_148 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_IsSemigroup_472
d_'8851''45'isSemigroup_148 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSemigroup_472
du_'8851''45'isSemigroup_148 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'isSemigroup_148 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8851''45'isSemigroup_148 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsSemigroup_472
du_'8851''45'isSemigroup_148 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isSemigroup_3032
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'magma_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_Magma_68
d_'8851''45'magma_150 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_Magma_68
d_'8851''45'magma_150 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Magma_68
du_'8851''45'magma_150 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'magma_150 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_Magma_68
du_'8851''45'magma_150 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Magma_68
du_'8851''45'magma_150 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Magma_68)
-> AgdaAny -> AgdaAny -> T_Magma_68
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_Magma_68
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'magma_3048
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'mono'45''8804'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'45''8804'_152 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'mono'45''8804'_152 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'45''8804'_152 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'mono'45''8804'_152 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'45''8804'_152 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'45''8804'_152 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'45''8804'_3206
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'monoid_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'8851''45'monoid_154 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_882
d_'8851''45'monoid_154 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_882
du_'8851''45'monoid_154 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'monoid_154 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'8851''45'monoid_154 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_882
du_'8851''45'monoid_154 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_882)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_882
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Monoid_882
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'monoid_3060
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'mono'691''45''8804'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'691''45''8804'_156 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'mono'691''45''8804'_156 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'691''45''8804'_156 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'mono'691''45''8804'_156 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'691''45''8804'_156 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'691''45''8804'_156 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'691''45''8804'_3266
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'mono'737''45''8804'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'mono'737''45''8804'_158 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'mono'737''45''8804'_158 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'737''45''8804'_158 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'mono'737''45''8804'_158 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'mono'737''45''8804'_158 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''45'mono'737''45''8804'_158 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'mono'737''45''8804'_3256
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'sel_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''45'sel_162 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8851''45'sel_162 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4 = T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''45'sel_162 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'sel_162 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''45'sel_162 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''45'sel_162 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'sel_2988
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'selectiveMagma_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_122
d_'8851''45'selectiveMagma_164 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_SelectiveMagma_122
d_'8851''45'selectiveMagma_164 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_SelectiveMagma_122
du_'8851''45'selectiveMagma_164 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'selectiveMagma_164 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_SelectiveMagma_122
du_'8851''45'selectiveMagma_164 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_SelectiveMagma_122
du_'8851''45'selectiveMagma_164 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_SelectiveMagma_122)
-> AgdaAny -> AgdaAny -> T_SelectiveMagma_122
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_SelectiveMagma_122
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'selectiveMagma_3056
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'semigroup_166 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'8851''45'semigroup_166 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_Semigroup_536
d_'8851''45'semigroup_166 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semigroup_536
du_'8851''45'semigroup_166 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'semigroup_166 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_'8851''45'semigroup_166 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semigroup_536
du_'8851''45'semigroup_166 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semigroup_536)
-> AgdaAny -> AgdaAny -> T_Semigroup_536
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semigroup_536
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'semigroup_3050
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'triangulate_168 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''45'triangulate_168 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''45'triangulate_168 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
= T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_168 T_TotalPreorder_222
v3 T_MaxOperator_128
v4
du_'8851''45'triangulate_168 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_168 :: T_TotalPreorder_222
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''45'triangulate_168 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
= (T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'triangulate_3292
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
d_'8851''45'zero_170 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''45'zero_170 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8851''45'zero_170 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
= T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'zero_170 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
du_'8851''45'zero_170 ::
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny ->
(AgdaAny -> AgdaAny) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''45'zero_170 :: T_MaxOperator_128 -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Σ_14
du_'8851''45'zero_170 T_MaxOperator_128
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_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
T_MaxOperator_128
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_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
T_MaxOperator_128
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
d_'8851''45'zero'691'_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_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'691'_172 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'zero'691'_172 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_172 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'zero'691'_172 ::
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_172 :: T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'691'_172 T_MaxOperator_128
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
= (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8804'y'8658'x'8852'y'8776'y_150
T_MaxOperator_128
v0 AgdaAny
v3 AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
d_'8851''45'zero'737'_174 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_'8851''45'zero'737'_174 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_'8851''45'zero'737'_174 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_174 T_MaxOperator_128
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''45'zero'737'_174 ::
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_174 :: T_MaxOperator_128
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'8851''45'zero'737'_174 T_MaxOperator_128
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
= (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d_x'8805'y'8658'x'8852'y'8776'x_156
T_MaxOperator_128
v0 AgdaAny
v1 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
d_mono'45''8804''45'distrib'45''8852'_182 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_182 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_mono'45''8804''45'distrib'45''8852'_182 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
= T_TotalPreorder_222
-> T_MaxOperator_128
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_182 T_TotalPreorder_222
v3 T_MaxOperator_128
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
du_mono'45''8804''45'distrib'45''8852'_182 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_182 :: T_TotalPreorder_222
-> T_MaxOperator_128
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'45''8804''45'distrib'45''8852'_182 T_TotalPreorder_222
v0 T_MaxOperator_128
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4
= (T_TotalPreorder_222
-> T_MinOperator_98
-> (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_222
-> T_MinOperator_98
-> (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'_3114
((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
(T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
(T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
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))