{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Inverse
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
d_Pointwise_34 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d_Pointwise_34 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 p
a10 p
a11 p
a12 p
a13 = ()
data T_Pointwise_34
= C_inj'8321'_64 AgdaAny | C_inj'8322'_70 AgdaAny
d_drop'45'inj'8321'_96 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> T_Pointwise_34 -> AgdaAny
d_drop'45'inj'8321'_96 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
-> AgdaAny
d_drop'45'inj'8321'_96 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~AgdaAny
v8 ~AgdaAny
v9 T_Pointwise_34
v10
= T_Pointwise_34 -> AgdaAny
du_drop'45'inj'8321'_96 T_Pointwise_34
v10
du_drop'45'inj'8321'_96 :: T_Pointwise_34 -> AgdaAny
du_drop'45'inj'8321'_96 :: T_Pointwise_34 -> AgdaAny
du_drop'45'inj'8321'_96 T_Pointwise_34
v0
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v0 of
C_inj'8321'_64 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
T_Pointwise_34
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_drop'45'inj'8322'_104 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> T_Pointwise_34 -> AgdaAny
d_drop'45'inj'8322'_104 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
-> AgdaAny
d_drop'45'inj'8322'_104 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~AgdaAny
v8 ~AgdaAny
v9 T_Pointwise_34
v10
= T_Pointwise_34 -> AgdaAny
du_drop'45'inj'8322'_104 T_Pointwise_34
v10
du_drop'45'inj'8322'_104 :: T_Pointwise_34 -> AgdaAny
du_drop'45'inj'8322'_104 :: T_Pointwise_34 -> AgdaAny
du_drop'45'inj'8322'_104 T_Pointwise_34
v0
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v0 of
C_inj'8322'_70 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
T_Pointwise_34
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'refl_108 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_34
d_'8846''45'refl_108 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T_Pointwise_34
d_'8846''45'refl_108 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 T__'8846'__30
v10
= (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34
du_'8846''45'refl_108 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 T__'8846'__30
v10
du_'8846''45'refl_108 ::
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_34
du_'8846''45'refl_108 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34
du_'8846''45'refl_108 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T__'8846'__30
v2
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v3
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v3
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'symmetric_122 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
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) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34
d_'8846''45'symmetric_122 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
d_'8846''45'symmetric_122 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T__'8846'__30
v10
T__'8846'__30
v11 T_Pointwise_34
v12
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'symmetric_122 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T__'8846'__30
v10 T__'8846'__30
v11 T_Pointwise_34
v12
du_'8846''45'symmetric_122 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34
du_'8846''45'symmetric_122 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'symmetric_122 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_34
v4
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v4 of
C_inj'8321'_64 AgdaAny
v7
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v7
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'transitive_136 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
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.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
d_'8846''45'transitive_136 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
d_'8846''45'transitive_136 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
T__'8846'__30
v10 T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_34
v13 T_Pointwise_34
v14
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'transitive_136 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T__'8846'__30
v10 T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_34
v13 T_Pointwise_34
v14
du_'8846''45'transitive_136 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
du_'8846''45'transitive_136 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'transitive_136 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_34
v5 T_Pointwise_34
v6
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v5 of
C_inj'8321'_64 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v6 of
C_inj'8321'_64 AgdaAny
v14
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v15
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v11 AgdaAny
v15 AgdaAny
v9 AgdaAny
v14)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v10
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v6 of
C_inj'8322'_70 AgdaAny
v14
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v15
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v10 AgdaAny
v11 AgdaAny
v15 AgdaAny
v9 AgdaAny
v14)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'asymmetric_154 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 ->
T_Pointwise_34 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8846''45'asymmetric_154 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_'8869'_4
d_'8846''45'asymmetric_154 = ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda0_162 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> T_Pointwise_34 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda0_162 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
-> T_'8869'_4
d_'46'extendedlambda0_162 = ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda1_172 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> T_Pointwise_34 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda1_172 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
-> T_'8869'_4
d_'46'extendedlambda1_172 = ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
-> T_'8869'_4
forall a. a
erased
d_'8846''45'substitutive_178 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
((AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
((AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> AgdaAny -> AgdaAny
d_'8846''45'substitutive_178 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ((AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ((AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8846'__30 -> ())
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> AgdaAny
-> AgdaAny
d_'8846''45'substitutive_178 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
(AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T__'8846'__30 -> ()
v11 T__'8846'__30
v12 T__'8846'__30
v13 T_Pointwise_34
v14
= ((AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ((AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8846'__30 -> ())
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> AgdaAny
-> AgdaAny
du_'8846''45'substitutive_178 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T__'8846'__30 -> ()
v11 T__'8846'__30
v12 T__'8846'__30
v13 T_Pointwise_34
v14
du_'8846''45'substitutive_178 ::
((AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
((AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> AgdaAny -> AgdaAny
du_'8846''45'substitutive_178 :: ((AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ((AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8846'__30 -> ())
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> AgdaAny
-> AgdaAny
du_'8846''45'substitutive_178 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30 -> ()
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_34
v5
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v5 of
C_inj'8321'_64 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10
-> ((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
v0
(\ AgdaAny
v11 ->
(T__'8846'__30 -> ()) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> ()
v2 ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)))
AgdaAny
v9 AgdaAny
v10 AgdaAny
v8
T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v10
-> ((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
v1
(\ AgdaAny
v11 ->
(T__'8846'__30 -> ()) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> ()
v2 ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)))
AgdaAny
v9 AgdaAny
v10 AgdaAny
v8
T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'decidable_196 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8846''45'decidable_196 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
d_'8846''45'decidable_196 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> T_Dec_32
v8 AgdaAny -> AgdaAny -> T_Dec_32
v9 T__'8846'__30
v10
T__'8846'__30
v11
= (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
du_'8846''45'decidable_196 AgdaAny -> AgdaAny -> T_Dec_32
v8 AgdaAny -> AgdaAny -> T_Dec_32
v9 T__'8846'__30
v10 T__'8846'__30
v11
du_'8846''45'decidable_196 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8846''45'decidable_196 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
du_'8846''45'decidable_196 AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny -> AgdaAny -> T_Dec_32
v1 T__'8846'__30
v2 T__'8846'__30
v3
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v4
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v5
-> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
((AgdaAny -> T_Pointwise_34) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v4 AgdaAny
v5)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8846'__30
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v4
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5
-> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
((AgdaAny -> T_Pointwise_34) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v1 AgdaAny
v4 AgdaAny
v5)
T__'8846'__30
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'reflexive_258 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
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) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34
d_'8846''45'reflexive_258 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
d_'8846''45'reflexive_258 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8 ~()
v9
~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'reflexive_258 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16
du_'8846''45'reflexive_258 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34
du_'8846''45'reflexive_258 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'reflexive_258 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_34
v4
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v4 of
C_inj'8321'_64 AgdaAny
v7
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v7
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'irreflexive_272 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 ->
T_Pointwise_34 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8846''45'irreflexive_272 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_'8869'_4
d_'8846''45'irreflexive_272 = ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_'8869'_4
forall a. a
erased
d_'8846''45'antisymmetric_290 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
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) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
d_'8846''45'antisymmetric_290 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
d_'8846''45'antisymmetric_290 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
~()
v9 ~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16 T_Pointwise_34
v17
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'antisymmetric_290 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16 T_Pointwise_34
v17
du_'8846''45'antisymmetric_290 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
du_'8846''45'antisymmetric_290 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'antisymmetric_290 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_34
v4 T_Pointwise_34
v5
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v4 of
C_inj'8321'_64 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v5 of
C_inj'8321'_64 AgdaAny
v13 -> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v9 AgdaAny
v10 AgdaAny
v8 AgdaAny
v13)
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v8
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v10
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v5 of
C_inj'8322'_70 AgdaAny
v13 -> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v9 AgdaAny
v10 AgdaAny
v8 AgdaAny
v13)
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'respects'737'_308 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
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.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
d_'8846''45'respects'737'_308 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
d_'8846''45'respects'737'_308 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
~()
v9 ~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T__'8846'__30
v16 T_Pointwise_34
v17 T_Pointwise_34
v18
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'respects'737'_308 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T__'8846'__30
v16 T_Pointwise_34
v17 T_Pointwise_34
v18
du_'8846''45'respects'737'_308 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
du_'8846''45'respects'737'_308 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'respects'737'_308 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_34
v5 T_Pointwise_34
v6
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v5 of
C_inj'8321'_64 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v6 of
C_inj'8321'_64 AgdaAny
v14
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v15
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v10
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v6 of
C_inj'8322'_70 AgdaAny
v14
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v15
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'respects'691'_326 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
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.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
d_'8846''45'respects'691'_326 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
d_'8846''45'respects'691'_326 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
~()
v9 ~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T__'8846'__30
v16 T_Pointwise_34
v17 T_Pointwise_34
v18
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'respects'691'_326 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T__'8846'__30
v14 T__'8846'__30
v15 T__'8846'__30
v16 T_Pointwise_34
v17 T_Pointwise_34
v18
du_'8846''45'respects'691'_326 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> T_Pointwise_34 -> T_Pointwise_34
du_'8846''45'respects'691'_326 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'respects'691'_326 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T__'8846'__30
v2 T__'8846'__30
v3 T__'8846'__30
v4 T_Pointwise_34
v5 T_Pointwise_34
v6
= case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v5 of
C_inj'8321'_64 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v6 of
C_inj'8321'_64 AgdaAny
v14
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v15
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_inj'8322'_70 AgdaAny
v9
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v10
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v4 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v6 of
C_inj'8322'_70 AgdaAny
v14
-> case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v15
-> (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v15 AgdaAny
v10 AgdaAny
v11 AgdaAny
v9 AgdaAny
v14)
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'respects'8322'_344 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8846''45'respects'8322'_344 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8846''45'respects'8322'_344 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
~()
v9 ~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_Σ_14
v12 T_Σ_14
v13
= T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_344 T_Σ_14
v12 T_Σ_14
v13
du_'8846''45'respects'8322'_344 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8846''45'respects'8322'_344 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_344 T_Σ_14
v0 T_Σ_14
v1
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
-> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'respects'691'_326 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'respects'737'_308 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8846''45'isEquivalence_374 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8846''45'isEquivalence_374 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_26
-> T_IsEquivalence_26
-> T_IsEquivalence_26
d_'8846''45'isEquivalence_374 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsEquivalence_26
v8 T_IsEquivalence_26
v9
= T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_374 T_IsEquivalence_26
v8 T_IsEquivalence_26
v9
du_'8846''45'isEquivalence_374 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'8846''45'isEquivalence_374 :: T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_374 T_IsEquivalence_26
v0 T_IsEquivalence_26
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34
du_'8846''45'refl_108
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'symmetric_122
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'transitive_136
((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_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
((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_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
d_'8846''45'isDecEquivalence_384 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8846''45'isDecEquivalence_384 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
d_'8846''45'isDecEquivalence_384 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsDecEquivalence_44
v8
T_IsDecEquivalence_44
v9
= T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_384 T_IsDecEquivalence_44
v8 T_IsDecEquivalence_44
v9
du_'8846''45'isDecEquivalence_384 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_384 :: T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_384 T_IsDecEquivalence_44
v0 T_IsDecEquivalence_44
v1
= (T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3075
((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_374
((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
(T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
(T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v1)))
(((AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
du_'8846''45'decidable_196
((T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
((T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v1)))
d_'8846''45'isPreorder_422 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8846''45'isPreorder_422 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_IsPreorder_70
-> T_IsPreorder_70
d_'8846''45'isPreorder_422 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8 ~()
v9
~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsPreorder_70
v12 T_IsPreorder_70
v13
= T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_422 T_IsPreorder_70
v12 T_IsPreorder_70
v13
du_'8846''45'isPreorder_422 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_'8846''45'isPreorder_422 :: T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_422 T_IsPreorder_70
v0 T_IsPreorder_70
v1
= (T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_374
((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
(T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
(T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'reflexive_258
((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'transitive_136
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
((T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
d_'8846''45'isPartialOrder_432 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8846''45'isPartialOrder_432 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> T_IsPartialOrder_162
-> T_IsPartialOrder_162
d_'8846''45'isPartialOrder_432 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~()
v8
~()
v9 ~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsPartialOrder_162
v12 T_IsPartialOrder_162
v13
= T_IsPartialOrder_162
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8846''45'isPartialOrder_432 T_IsPartialOrder_162
v12 T_IsPartialOrder_162
v13
du_'8846''45'isPartialOrder_432 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_'8846''45'isPartialOrder_432 :: T_IsPartialOrder_162
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8846''45'isPartialOrder_432 T_IsPartialOrder_162
v0 T_IsPartialOrder_162
v1
= (T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
((T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_422
((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'antisymmetric_290
((T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
((T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
d_'8846''45'isStrictPartialOrder_442 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'8846''45'isStrictPartialOrder_442 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266
d_'8846''45'isStrictPartialOrder_442 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
~AgdaAny -> AgdaAny -> ()
v7 ~()
v8 ~()
v9 ~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 T_IsStrictPartialOrder_266
v12 T_IsStrictPartialOrder_266
v13
= T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'8846''45'isStrictPartialOrder_442 T_IsStrictPartialOrder_266
v12 T_IsStrictPartialOrder_266
v13
du_'8846''45'isStrictPartialOrder_442 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
du_'8846''45'isStrictPartialOrder_442 :: T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'8846''45'isStrictPartialOrder_442 T_IsStrictPartialOrder_266
v0 T_IsStrictPartialOrder_266
v1
= (T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_13145
((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_374
((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
(T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
(T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1)))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
-> T_Pointwise_34
du_'8846''45'transitive_136
((T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
((T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1)))
((T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8846''45'respects'8322'_344
((T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
(T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
((T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
(T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1)))
d_'8846''45'setoid_464 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8846''45'setoid_464 :: () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
d_'8846''45'setoid_464 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_Setoid_44
v5
= T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du_'8846''45'setoid_464 T_Setoid_44
v4 T_Setoid_44
v5
du_'8846''45'setoid_464 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_'8846''45'setoid_464 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du_'8846''45'setoid_464 T_Setoid_44
v0 T_Setoid_44
v1
= (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
((T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8846''45'isEquivalence_374
((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)))
d_'8846''45'decSetoid_474 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8846''45'decSetoid_474 :: ()
-> ()
-> ()
-> ()
-> T_DecSetoid_84
-> T_DecSetoid_84
-> T_DecSetoid_84
d_'8846''45'decSetoid_474 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_DecSetoid_84
v4 T_DecSetoid_84
v5
= T_DecSetoid_84 -> T_DecSetoid_84 -> T_DecSetoid_84
du_'8846''45'decSetoid_474 T_DecSetoid_84
v4 T_DecSetoid_84
v5
du_'8846''45'decSetoid_474 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
du_'8846''45'decSetoid_474 :: T_DecSetoid_84 -> T_DecSetoid_84 -> T_DecSetoid_84
du_'8846''45'decSetoid_474 T_DecSetoid_84
v0 T_DecSetoid_84
v1
= (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1385
((T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecEquivalence_44
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8846''45'isDecEquivalence_384
((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
(T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0))
((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
(T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v1)))
d__'8846''8347'__484 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d__'8846''8347'__484 :: () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
d__'8846''8347'__484 ~()
v0 ~()
v1 ~()
v2 ~()
v3 = T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du__'8846''8347'__484
du__'8846''8347'__484 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du__'8846''8347'__484 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du__'8846''8347'__484 = (T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44)
-> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du_'8846''45'setoid_464
d_'8846''45'preorder_502 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8846''45'preorder_502 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Preorder_132
-> T_Preorder_132
-> T_Preorder_132
d_'8846''45'preorder_502 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 T_Preorder_132
v6 T_Preorder_132
v7
= T_Preorder_132 -> T_Preorder_132 -> T_Preorder_132
du_'8846''45'preorder_502 T_Preorder_132
v6 T_Preorder_132
v7
du_'8846''45'preorder_502 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_'8846''45'preorder_502 :: T_Preorder_132 -> T_Preorder_132 -> T_Preorder_132
du_'8846''45'preorder_502 T_Preorder_132
v0 T_Preorder_132
v1
= (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
((T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70
du_'8846''45'isPreorder_422
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v1)))
d_'8846''45'poset_512 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_'8846''45'poset_512 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Poset_282
-> T_Poset_282
-> T_Poset_282
d_'8846''45'poset_512 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 T_Poset_282
v6 T_Poset_282
v7
= T_Poset_282 -> T_Poset_282 -> T_Poset_282
du_'8846''45'poset_512 T_Poset_282
v6 T_Poset_282
v7
du_'8846''45'poset_512 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_'8846''45'poset_512 :: T_Poset_282 -> T_Poset_282 -> T_Poset_282
du_'8846''45'poset_512 T_Poset_282
v0 T_Poset_282
v1
= (T_IsPartialOrder_162 -> T_Poset_282) -> AgdaAny -> T_Poset_282
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
((T_IsPartialOrder_162
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8846''45'isPartialOrder_432
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v1)))
d_Pointwise'45''8801''8658''8801'_534 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
T_Pointwise_34 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_Pointwise'45''8801''8658''8801'_534 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T__'8801'__12
d_Pointwise'45''8801''8658''8801'_534 = ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T__'8801'__12
forall a. a
erased
d_'8801''8658'Pointwise'45''8801'_540 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T_Pointwise_34
d_'8801''8658'Pointwise'45''8801'_540 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> T__'8846'__30
-> T__'8801'__12
-> T_Pointwise_34
d_'8801''8658'Pointwise'45''8801'_540 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T__'8846'__30
v4 ~T__'8846'__30
v5 ~T__'8801'__12
v6
= T__'8846'__30 -> T_Pointwise_34
du_'8801''8658'Pointwise'45''8801'_540 T__'8846'__30
v4
du_'8801''8658'Pointwise'45''8801'_540 ::
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Pointwise_34
du_'8801''8658'Pointwise'45''8801'_540 :: T__'8846'__30 -> T_Pointwise_34
du_'8801''8658'Pointwise'45''8801'_540 T__'8846'__30
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34
du_'8846''45'refl_108 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v0)
d_Pointwise'45''8801''8596''8801'_550 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_Pointwise'45''8801''8596''8801'_550 :: () -> () -> () -> () -> T_Inverse_58
d_Pointwise'45''8801''8596''8801'_550 ~()
v0 ~()
v1 ~()
v2 ~()
v3
= T_Inverse_58
du_Pointwise'45''8801''8596''8801'_550
du_Pointwise'45''8801''8596''8801'_550 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58
du_Pointwise'45''8801''8596''8801'_550 :: T_Inverse_58
du_Pointwise'45''8801''8596''8801'_550
= (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.C_Inverse'46'constructor_3557
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) AgdaAny
forall a. a
erased)
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0))
(\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> (T__'8846'__30 -> T_Pointwise_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T_Pointwise_34
du_'8801''8658'Pointwise'45''8801'_540 AgdaAny
v0))
(((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__InverseOf__20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__InverseOf__20
MAlonzo.Code.Function.Inverse.C__InverseOf_'46'constructor_2103
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_34
du_'8846''45'refl_108 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)))
AgdaAny
forall a. a
erased)
d_'8321''8764''8321'_588 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_34
d_'8321''8764''8321'_588 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
d_'8321''8764''8321'_588 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9
~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 ~AgdaAny
v12 ~AgdaAny
v13
= AgdaAny -> T_Pointwise_34
du_'8321''8764''8321'_588
du_'8321''8764''8321'_588 :: AgdaAny -> T_Pointwise_34
du_'8321''8764''8321'_588 :: AgdaAny -> T_Pointwise_34
du_'8321''8764''8321'_588 = (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8321'_64
d_'8322''8764''8322'_594 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_34
d_'8322''8764''8322'_594 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Pointwise_34
d_'8322''8764''8322'_594 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9
~AgdaAny -> AgdaAny -> ()
v10 ~AgdaAny -> AgdaAny -> ()
v11 ~AgdaAny
v12 ~AgdaAny
v13
= AgdaAny -> T_Pointwise_34
du_'8322''8764''8322'_594
du_'8322''8764''8322'_594 :: AgdaAny -> T_Pointwise_34
du_'8322''8764''8322'_594 :: AgdaAny -> T_Pointwise_34
du_'8322''8764''8322'_594 = (AgdaAny -> T_Pointwise_34) -> AgdaAny -> T_Pointwise_34
forall a b. a -> b
coe AgdaAny -> T_Pointwise_34
C_inj'8322'_70
d__'8846''45''8799'__604 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8846''45''8799'__604 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
d__'8846''45''8799'__604 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny -> T_Dec_32
v4 AgdaAny -> AgdaAny -> T_Dec_32
v5 T__'8846'__30
v6 T__'8846'__30
v7
= (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
du__'8846''45''8799'__604 AgdaAny -> AgdaAny -> T_Dec_32
v4 AgdaAny -> AgdaAny -> T_Dec_32
v5 T__'8846'__30
v6 T__'8846'__30
v7
du__'8846''45''8799'__604 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8846''45''8799'__604 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
du__'8846''45''8799'__604 AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny -> AgdaAny -> T_Dec_32
v1 T__'8846'__30
v2 T__'8846'__30
v3
= ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
AgdaAny
forall a. a
erased
(((AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T__'8846'__30
-> T_Dec_32
du_'8846''45'decidable_196 ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v1) (T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v2) (T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v3))