{-# 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.Data.List.Extrema.Core 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.Construct.LiftedChoice
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Base
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Max
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.Min
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd
import qualified MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
import qualified MAlonzo.Code.Relation.Binary.Structures
d__'60'__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_TotalOrder_764 ->
AgdaAny -> AgdaAny -> ()
d__'60'__96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__96 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
d__'8851'__192 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8851'__192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 = T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__192 T_TotalOrder_764
v3
du__'8851'__192 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__192 :: T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__192 T_TotalOrder_764
v0
= (T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du__'8851'__94
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)
d_'60''45'trans'691'_284 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'691'_284 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'trans'691'_284 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'691'_284 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'691'_284 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'8804''45''60''45'trans_274
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
((T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
((T_IsTotalOrder_404 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
((T_TotalOrder_764 -> T_IsTotalOrder_404) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))))
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v5 :: t
v5
= (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'737''45''8776'_100
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
d_'60''45'trans'737'_286 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'trans'737'_286 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_'60''45'trans'737'_286 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_'60''45'trans'737'_286 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'trans'737'_286 :: T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'60''45''8804''45'trans_256
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v5 :: t
v5
= (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v6 :: t
v6
= (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe
T_Preorder_132 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v6))))))
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
((T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
((T_IsTotalOrder_404 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
((T_TotalOrder_764 -> T_IsTotalOrder_404) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_786 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))))
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v5 :: t
v5
= (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'691''45''8776'_106
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
d_lemma'8321'_302 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8321'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8321'_302 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_302 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8321'_302 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8321'_302 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_302 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v4
((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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
AgdaAny
v5)
d_lemma'8322'_314 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_lemma'8322'_314 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_lemma'8322'_314 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_314 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_lemma'8322'_314 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_lemma'8322'_314 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_314 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4
((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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
AgdaAny
v5)
d_lemma'8323'_326 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lemma'8323'_326 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8323'_326 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_326 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8323'_326 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8323'_326 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_326 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
= (T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v4
((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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
T_Σ_14
v5
d_lemma'8324'_338 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lemma'8324'_338 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_lemma'8324'_338 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_338 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 AgdaAny
v11
du_lemma'8324'_338 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lemma'8324'_338 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_338 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T_Σ_14
v5 AgdaAny
v6
= (T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'trans'691'_284 T_TotalOrder_764
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4
((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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
T_Σ_14
v5
d_'8851''7480'_344 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480'_344 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480'_344 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_344 T_TotalOrder_764
v3
du_'8851''7480'_344 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_344 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480'_344 T_TotalOrder_764
v0
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_Lift_30
((T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
d_'8852''7480'_346 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480'_346 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480'_346 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 = T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_346 T_TotalOrder_764
v3
du_'8852''7480'_346 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_346 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480'_346 T_TotalOrder_764
v0
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_Lift_30
(let v1 :: t
v1
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v2 :: t
v2
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)))))
d_'8851''7480''45'sel_350 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8851''7480''45'sel_350 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8851''7480''45'sel_350 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_350 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_'8851''7480''45'sel_350 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8851''7480''45'sel_350 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8851''7480''45'sel_350 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_130
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_'8851''7480''45'pres'7506''45''8804'v_362 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8851''7480''45'pres'7506''45''8804'v_362 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_362 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''8804'v_362 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_362 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8851''7480''45'pres'7506''45''8804'v_362 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 ->
(T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8321'_302 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 ->
(T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_lemma'8322'_314 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
d_'8851''7480''45'pres'7506''45''60'v_374 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'pres'7506''45''60'v_374 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
d_'8851''7480''45'pres'7506''45''60'v_374 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
AgdaAny
v7
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_374 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'pres'7506''45''60'v_374 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_374 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8851''7480''45'pres'7506''45''60'v_374 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 ->
(T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8323'_326 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 ->
(T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_lemma'8324'_338 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
d_'8851''7480''45'pres'7495''45'v'8804'_386 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8851''7480''45'pres'7495''45'v'8804'_386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_386 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'8804'_386 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_386 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8851''7480''45'pres'7495''45'v'8804'_386 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
d_'8851''7480''45'pres'7495''45'v'60'_402 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'pres'7495''45'v'60'_402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8851''7480''45'pres'7495''45'v'60'_402 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_402 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8851''7480''45'pres'7495''45'v'60'_402 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_402 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8851''7480''45'pres'7495''45'v'60'_402 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
d_'8851''7480''45'forces'7495''45'v'8804'_418 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_418 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8851''7480''45'forces'7495''45'v'8804'_418 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4
~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_418 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8851''7480''45'forces'7495''45'v'8804'_418 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_418 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8851''7480''45'forces'7495''45'v'8804'_418 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_forces'7495'_562
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5
((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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))))
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v5
((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_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((T_TotalOrder_764 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Min.du_minOperator_176
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))))
d_'8852''7480''45'sel_434 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8852''7480''45'sel_434 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_'8852''7480''45'sel_434 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_434 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6
du_'8852''7480''45'sel_434 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8852''7480''45'sel_434 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_'8852''7480''45'sel_434 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_sel'45''8801'_130
(let v2 :: t
v2
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v3 :: t
v3
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_'8852''7480''45'pres'7506''45'v'8804'_446 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_446 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_'8852''7480''45'pres'7506''45'v'8804'_446 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_446 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'8804'_446 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_446 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_'8852''7480''45'pres'7506''45'v'8804'_446 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
(let v3 :: t
v3
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5
(let v8 :: t
v8
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v9 :: t
v9
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))))))
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v5
(let v8 :: t
v8
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v9 :: t
v9
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))))))
d_'8852''7480''45'pres'7506''45'v'60'_468 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'pres'7506''45'v'60'_468 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
d_'8852''7480''45'pres'7506''45'v'60'_468 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
AgdaAny
v7
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_468 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'pres'7506''45'v'60'_468 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_468 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
du_'8852''7480''45'pres'7506''45'v'60'_468 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7506'_400
(let v3 :: t
v3
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
(T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5
(let v7 :: t
v7
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v8 :: t
v8
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))))
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
(T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14)
-> T_TotalOrder_764
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_TotalOrder_764
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny -> T_Σ_14
du_'60''45'trans'737'_286 T_TotalOrder_764
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v5
(let v7 :: t
v7
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v8 :: t
v8
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))))
d_'8852''7480''45'pres'7495''45''8804'v_490 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_490 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8852''7480''45'pres'7495''45''8804'v_490 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5
AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_490 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''8804'v_490 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_490 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8852''7480''45'pres'7495''45''8804'v_490 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v5 :: t
v5
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
d_'8852''7480''45'pres'7495''45''60'v_506 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'pres'7495''45''60'v_506 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8852''7480''45'pres'7495''45''60'v_506 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
~AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_506 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 AgdaAny
v9
du_'8852''7480''45'pres'7495''45''60'v_506 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_506 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'8852''7480''45'pres'7495''45''60'v_506 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_preserves'7495'_520
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v5 :: t
v5
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
d_'8852''7480''45'forces'7495''45''8804'v_522 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_764
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8852''7480''45'forces'7495''45''8804'v_522 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_764
v3 ~T_Level_18
v4
~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
= T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_522 T_TotalOrder_764
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_'8852''7480''45'forces'7495''45''8804'v_522 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764 ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_522 :: T_TotalOrder_764
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_'8852''7480''45'forces'7495''45''8804'v_522 T_TotalOrder_764
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= (T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Algebra.Construct.LiftedChoice.du_forces'7495'_562
(let v3 :: t
v3
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v4 :: t
v4
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> AgdaAny
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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v2
(let v8 :: t
v8
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v9 :: t
v9
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
AgdaAny
v5)))
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
let v7 :: t
v7
= (T_TotalOrder_764 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalOrder_764 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.du_poset_796 (T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v2
(let v8 :: t
v8
= (T_TotalOrder_764 -> T_TotalPreorder_222) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Bundles.du_totalPreorder_858
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v9 :: t
v9
= (T_TotalOrder_764 -> T_MaxOperator_128) -> AgdaAny -> t
forall a b. a -> b
coe
T_TotalOrder_764 -> T_MaxOperator_128
MAlonzo.Code.Algebra.Construct.NaturalChoice.Max.du_maxOperator_186
(T_TotalOrder_764 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_764
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
AgdaAny
v5)))