{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Algebra.Construct.LiftedChoice 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Consequences.Base
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Setoid
import qualified MAlonzo.Code.Relation.Binary.Structures
d_Lift_30 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_Lift_30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_Lift_30 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny -> T__'8846'__30
v7 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
= (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_Lift_30 AgdaAny -> AgdaAny -> T__'8846'__30
v7 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_Lift_30 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_Lift_30 :: (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_Lift_30 AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= let v4 :: t
v4 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
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) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
d__'9702'__132 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__132 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__132 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8
du__'9702'__132 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__132 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__132 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (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
du_Lift_30 ((T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_sel'45''8801'_134 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_sel'45''8801'_134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_sel'45''8801'_134 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_sel'45''8801'_134 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_sel'45''8801'_134 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_sel'45''8801'_134 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_sel'45''8801'_134 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
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)
d_distrib_156 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_distrib_156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_distrib_156 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= let v4 :: t
v4
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
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) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
d__'9702'__190 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__190 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8
du__'9702'__190 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__190 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__190 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (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
du_Lift_30 ((T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_sel_192 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_sel_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_sel_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_192 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12
du_sel_192 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_sel_192 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_192 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
((AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__190 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4) AgdaAny
v3)
((AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__190 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4) AgdaAny
v4)
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_sel'45''8801'_134 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
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))
d_idem_198 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
AgdaAny -> AgdaAny
d_idem_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_idem_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_idem_198 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10
du_idem_198 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
AgdaAny -> AgdaAny
du_idem_198 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_idem_198 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v2
= ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Consequences.Base.du_sel'8658'idem_16
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_192 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v2))
d__'9702'__216 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8
du__'9702'__216 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (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
du_Lift_30 ((T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_cong_218 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_cong_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
AgdaAny
v15 AgdaAny
v16 AgdaAny
v17
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_cong_218 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17
du_cong_218 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_cong_218 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_cong_218 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
= let v11 :: t
v11
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5)
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v12 :: t
v12
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v11 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v13
-> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v12 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v5 AgdaAny
v8
(T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166
(T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8))
AgdaAny
v14)
((T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
(T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> T_IsSelectiveMagma_158
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v9) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v7 AgdaAny
v8 AgdaAny
v10)))
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> 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_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) AgdaAny
v13)))
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v13
-> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v12 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v7 AgdaAny
v6
(T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166
(T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6))
AgdaAny
v14)
((T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
(T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> T_IsSelectiveMagma_158
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v9) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v7 AgdaAny
v8 AgdaAny
v10)))
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> 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_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7) AgdaAny
v13)))
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
d_assoc_310 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_310 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_assoc_310 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13
AgdaAny
v14
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_assoc_310 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
du_assoc_310 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_assoc_310 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_assoc_310 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6) AgdaAny
v7)
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7))
(T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776''728'_66
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6) AgdaAny
v7))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776''728'_66
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7))))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((T_IsMagma_86
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_112
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__132 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))))
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7)))
((T_IsMagma_86
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_116
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v7) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__132 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))))
d_comm_320 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_320 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_comm_320 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_comm_320 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13
du_comm_320 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_comm_320 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_comm_320 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5)
(T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776''728'_66
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
((T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
((T_IsSelectiveMagma_158 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_166 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__216 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5)))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v5) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_156 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
d__'9702'__360 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__360 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__360 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~T_IsEquivalence_26
v12
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__360 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v9
du__'9702'__360 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__360 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__360 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (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
du_Lift_30 ((T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_isMagma_362 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_isMagma_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86
d_isMagma_362 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86
du_isMagma_362 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12
du_isMagma_362 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_isMagma_362 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86
du_isMagma_362 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5
= (T_IsEquivalence_26
-> (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5)
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_cong_218 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4))
d_isSemigroup_368 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_isSemigroup_368 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
d_isSemigroup_368 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
du_isSemigroup_368 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
du_isSemigroup_368 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_isSemigroup_368 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
du_isSemigroup_368 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
= (T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86
du_isMagma_362 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4)
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5))
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_assoc_310 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6))
d_isBand_376 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_isBand_376 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230
d_isBand_376 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230
du_isBand_376 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
du_isBand_376 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_isBand_376 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230
du_isBand_376 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
= (T_IsSemigroup_194 -> (AgdaAny -> AgdaAny) -> T_IsBand_230)
-> AgdaAny -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe
T_IsSemigroup_194 -> (AgdaAny -> AgdaAny) -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_4787
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
du_isSemigroup_368 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4)
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_idem_198 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
(\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
(T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5)
AgdaAny
v7))
d_isSemilattice_380 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_isSemilattice_380 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
d_isSemilattice_380 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
T_IsEquivalence_26
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny
v14
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
du_isSemilattice_380 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny
v14
du_isSemilattice_380 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_isSemilattice_380 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
du_isSemilattice_380 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny
v7
= (T_IsBand_230
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_312)
-> AgdaAny -> AgdaAny -> T_IsSemilattice_312
forall a b. a -> b
coe
T_IsBand_230
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Structures.C_IsSemilattice'46'constructor_6687
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230
du_isBand_376 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4) (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6))
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_comm_320 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v7))
d_isSelectiveMagma_390 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
d_isSelectiveMagma_390 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsSelectiveMagma_158
d_isSelectiveMagma_390 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
T_IsEquivalence_26
v12
= (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsSelectiveMagma_158
du_isSelectiveMagma_390 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12
du_isSelectiveMagma_390 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158
du_isSelectiveMagma_390 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsSelectiveMagma_158
du_isSelectiveMagma_390 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_158
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5
= (T_IsMagma_86
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsSelectiveMagma_158)
-> AgdaAny -> AgdaAny -> T_IsSelectiveMagma_158
forall a b. a -> b
coe
T_IsMagma_86
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsSelectiveMagma_158
MAlonzo.Code.Algebra.Structures.C_IsSelectiveMagma'46'constructor_3217
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_86
du_isMagma_362 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4)
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5))
((T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_192 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
(\ AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
(T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5)
AgdaAny
v6))
d__'9702'__404 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__404 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__404 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny
v10
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__404 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v10
du__'9702'__404 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__404 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__404 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> (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
du_Lift_30 ((T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 (T_IsSelectiveMagma_158 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_158
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_preserves'7506'_418 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_preserves'7506'_418 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
d_preserves'7506'_418 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny
v10
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny
v13 AgdaAny
v14 T__'8846'__30
v15
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_preserves'7506'_418 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny
v13 AgdaAny
v14 T__'8846'__30
v15
du_preserves'7506'_418 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_preserves'7506'_418 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_preserves'7506'_418 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T__'8846'__30
v6
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v6 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7
-> let v8 :: t
v8
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
v0 ((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
v5) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v8 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7 AgdaAny
v9
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
-> let v8 :: t
v8
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
v0 ((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
v5) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v8 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7 AgdaAny
v9
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_preserves'691'_500 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_preserves'691'_500 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_preserves'691'_500 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'691'_500 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
du_preserves'691'_500 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_preserves'691'_500 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'691'_500 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
= let v6 :: t
v6
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
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) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v6 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
d_preserves'7495'_538 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_preserves'7495'_538 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_preserves'7495'_538 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny
v10
AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'7495'_538 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
du_preserves'7495'_538 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_preserves'7495'_538 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'7495'_538 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
= let v6 :: t
v6
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
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) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v6 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
d_forces'7495'_580 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_forces'7495'_580 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_158
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_forces'7495'_580 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_158
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny
v13 AgdaAny
v14 AgdaAny
v15
= T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_forces'7495'_580 T_IsSelectiveMagma_158
v5 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny
v13 AgdaAny
v14 AgdaAny
v15
du_forces'7495'_580 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_158 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_forces'7495'_580 :: T_IsSelectiveMagma_158
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_forces'7495'_580 T_IsSelectiveMagma_158
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= let v7 :: t
v7
= (T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_158 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_168 T_IsSelectiveMagma_158
v0 ((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
v5) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v8
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v8
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)