{-# 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.Syntax
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
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66 (\ AgdaAny
v4 -> AgdaAny
v2)
(\ AgdaAny
v4 -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
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))
d__'9702'__128 ::
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_436 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8
= T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__128 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8
du__'9702'__128 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__128 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__128 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_sel'45''8801'_130 ::
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_436 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_sel'45''8801'_130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_sel'45''8801'_130 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
= T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_sel'45''8801'_130 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_sel'45''8801'_130 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_sel'45''8801'_130 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_sel'45''8801'_130 T_IsSelectiveMagma_436
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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_152 ::
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_436 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_distrib_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_distrib_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 ~T_Level_18
v6 ~T_Level_18
v7 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
= T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_distrib_152 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 T_IsSelectiveMagma_436
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= let v4 :: t
v4
= (T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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'__186 ::
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_436 ->
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'__186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__186 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8
du__'9702'__186 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__186 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__186 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_sel_188 ::
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_436 ->
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_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_188 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12
du_sel_188 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(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_188 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_188 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__186 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__186 T_IsSelectiveMagma_436
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4) AgdaAny
v4)
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
du_sel'45''8801'_130 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_194 ::
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_436 ->
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_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_idem_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_idem_194 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v10
du_idem_194 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
AgdaAny -> AgdaAny
du_idem_194 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_idem_194 T_IsSelectiveMagma_436
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_20
((T_IsSelectiveMagma_436
-> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_188 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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'__212 ::
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_436 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8
du__'9702'__212 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_cong_214 ::
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_436 ->
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_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_cong_214 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_214 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_cong_214 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_cong_214 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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
(((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 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
(\ AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 ->
(T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36
AgdaAny
v17)
((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
v8)
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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)
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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)
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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)
(let v15 :: AgdaAny -> AgdaAny
v15
= T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v15))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v8)))
AgdaAny
v14)
((T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
(T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> T_IsSelectiveMagma_436
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176)
-> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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
(((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 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
(\ AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 ->
(T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36
AgdaAny
v17)
((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)
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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)
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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)
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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)
(let v15 :: AgdaAny -> AgdaAny
v15
= T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444
(T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v15))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v6)))
AgdaAny
v14)
((T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
(T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> T_IsSelectiveMagma_436
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176)
-> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_306 ::
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_436 ->
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_306 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_306 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_assoc_306 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
du_assoc_306 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_assoc_306 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_assoc_306 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6) AgdaAny
v7)
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7))
(((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 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
(\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
(T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v10)
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6) AgdaAny
v7))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> 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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_370
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1)))))
(T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> 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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_370
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1)))))
(T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
(let v8 :: AgdaAny -> AgdaAny
v8
= T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v8))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v2
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))))
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
((T_IsMagma_176
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__128 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7))
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_176
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__128 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6))
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))))
d_comm_316 ::
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_436 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_comm_316 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_316 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_comm_316 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13
du_comm_316 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_comm_316 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_comm_316 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5)
(((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 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
(\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
(T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> 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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_370
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1)))))
(T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
(((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 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_IsMagma_176 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))
(let v7 :: AgdaAny -> AgdaAny
v7
= T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
((T_IsSelectiveMagma_436 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_444 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v1))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
(((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v7))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 ((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__212 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v5))))
((T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_distrib_152 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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'__356 ::
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_436 ->
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'__356 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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'__356 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__356 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v9
du__'9702'__356 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__356 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__356 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_isMagma_358 ::
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_436 ->
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_176
d_isMagma_358 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_176
d_isMagma_358 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_176
du_isMagma_358 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12
du_isMagma_358 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_isMagma_358 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_176
du_isMagma_358 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
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_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v5)
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_cong_214 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_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_436 ->
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_472
d_isSemigroup_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_472
d_isSemigroup_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_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472
du_isSemigroup_362 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_362 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(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_472
du_isSemigroup_362 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472
du_isSemigroup_362 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
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_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
T_IsMagma_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_176)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_176
du_isMagma_358 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_assoc_306 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_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_436 ->
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_508
d_isBand_368 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_508
d_isBand_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_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_508
du_isBand_368 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_368 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(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_508
du_isBand_368 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_508
du_isBand_368 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
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_472 -> (AgdaAny -> AgdaAny) -> T_IsBand_508)
-> AgdaAny -> AgdaAny -> T_IsBand_508
forall a b. a -> b
coe
T_IsSemigroup_472 -> (AgdaAny -> AgdaAny) -> T_IsBand_508
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472
du_isSemigroup_362 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_idem_194 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_isSelectiveMagma_372 ::
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_436 ->
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_436
d_isSelectiveMagma_372 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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_436
d_isSelectiveMagma_372 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsSelectiveMagma_436
du_isSelectiveMagma_372 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 T_IsEquivalence_26
v12
du_isSelectiveMagma_372 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436
du_isSelectiveMagma_372 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsSelectiveMagma_436
du_isSelectiveMagma_372 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSelectiveMagma_436
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5
= (T_IsMagma_176
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsSelectiveMagma_436)
-> AgdaAny -> AgdaAny -> T_IsSelectiveMagma_436
forall a b. a -> b
coe
T_IsMagma_176
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsSelectiveMagma_436
MAlonzo.Code.Algebra.Structures.C_IsSelectiveMagma'46'constructor_9631
(((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_176)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> T_IsMagma_176
du_isMagma_358 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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_436
-> (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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_sel_188 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
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'__386 ::
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_436 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d__'9702'__386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'9702'__386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> T_Level_18
v9 AgdaAny -> AgdaAny
v10
= T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__386 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v10
du__'9702'__386 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__386 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du__'9702'__386 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 (T_IsSelectiveMagma_436 -> AgdaAny
forall a b. a -> b
coe T_IsSelectiveMagma_436
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_preserves'7506'_400 ::
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_436 ->
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'_400 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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'_400 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_preserves'7506'_400 T_IsSelectiveMagma_436
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'_400 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(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'_400 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
du_preserves'7506'_400 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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'_482 ::
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_436 ->
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'_482 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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'_482 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'691'_482 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
du_preserves'691'_482 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_preserves'691'_482 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'691'_482 T_IsSelectiveMagma_436
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
= let v6 :: t
v6
= (T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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'_520 ::
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_436 ->
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'_520 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_preserves'7495'_520 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'7495'_520 T_IsSelectiveMagma_436
v5 AgdaAny -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
du_preserves'7495'_520 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_preserves'7495'_520 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_preserves'7495'_520 T_IsSelectiveMagma_436
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
= let v6 :: t
v6
= (T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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'_562 ::
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_436 ->
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'_562 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSelectiveMagma_436
-> 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'_562 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSelectiveMagma_436
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_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_forces'7495'_562 T_IsSelectiveMagma_436
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'_562 ::
MAlonzo.Code.Algebra.Structures.T_IsSelectiveMagma_436 ->
(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'_562 :: T_IsSelectiveMagma_436
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
du_forces'7495'_562 T_IsSelectiveMagma_436
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_436 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsSelectiveMagma_436 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Algebra.Structures.d_sel_446 T_IsSelectiveMagma_436
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 -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v9 -> AgdaAny
v4))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v9 -> AgdaAny
v5)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v7))
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 -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v9 -> AgdaAny
v4))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v9 -> AgdaAny
v5)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v7))
AgdaAny
v6 AgdaAny
v8)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)