{-# 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.Function.Setoid 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.Primitive
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Function.Bijection
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Function.Inverse
import qualified MAlonzo.Code.Function.LeftInverse
import qualified MAlonzo.Code.Function.Surjection
import qualified MAlonzo.Code.Relation.Binary.Bundles
d__'8846''45''10230'__36 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
d__'8846''45''10230'__36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Π_16
d__'8846''45''10230'__36 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9
~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Π_16
v12 T_Π_16
v13
= T_Π_16 -> T_Π_16 -> T_Π_16
du__'8846''45''10230'__36 T_Π_16
v12 T_Π_16
v13
du__'8846''45''10230'__36 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
du__'8846''45''10230'__36 :: T_Π_16 -> T_Π_16 -> T_Π_16
du__'8846''45''10230'__36 T_Π_16
v0 T_Π_16
v1
= ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16)
-> Any -> Any -> T_Π_16
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171
((T_Π_16 -> T_Π_16 -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> T_Π_16 -> T__'8846'__30 -> T__'8846'__30
du_fg_54 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v0) (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v1))
((T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_fg'45'cong_56 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v0) (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v1))
d__'8776'__48 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()
d__'8776'__48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
d__'8776'__48 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
forall a. a
erased
d__'8776'__52 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()
d__'8776'__52 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
d__'8776'__52 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
forall a. a
erased
d_fg_54 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_fg_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
d_fg_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Π_16
v12 T_Π_16
v13
= T_Π_16 -> T_Π_16 -> T__'8846'__30 -> T__'8846'__30
du_fg_54 T_Π_16
v12 T_Π_16
v13
du_fg_54 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_fg_54 :: T_Π_16 -> T_Π_16 -> T__'8846'__30 -> T__'8846'__30
du_fg_54 T_Π_16
v0 T_Π_16
v1
= ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84
((T_Π_16 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v0))
((T_Π_16 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v1))
d_fg'45'cong_56 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34
d_fg'45'cong_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
d_fg'45'cong_56 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11
T_Π_16
v12 T_Π_16
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16
= T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_fg'45'cong_56 T_Π_16
v12 T_Π_16
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16
du_fg'45'cong_56 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34
du_fg'45'cong_56 :: T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_fg'45'cong_56 T_Π_16
v0 T_Π_16
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
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64 Any
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 Any
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 Any
v9
-> (Any -> T_Pointwise_34) -> Any -> T_Pointwise_34
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64
((T_Π_16 -> Any -> Any -> Any -> Any)
-> T_Π_16 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Equality.d_cong_40 T_Π_16
v0 Any
v8 Any
v9 Any
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
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70 Any
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 Any
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 Any
v9
-> (Any -> T_Pointwise_34) -> Any -> T_Pointwise_34
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70
((T_Π_16 -> Any -> Any -> Any -> Any)
-> T_Π_16 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Equality.d_cong_40 T_Π_16
v1 Any
v8 Any
v9 Any
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_inj'8321''8347'_78 ::
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.Function.Equality.T_Π_16
d_inj'8321''8347'_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
d_inj'8321''8347'_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5
= T_Π_16
du_inj'8321''8347'_78
du_inj'8321''8347'_78 :: MAlonzo.Code.Function.Equality.T_Π_16
du_inj'8321''8347'_78 :: T_Π_16
du_inj'8321''8347'_78
= ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16)
-> Any -> (Any -> Any -> Any -> Any) -> T_Π_16
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171
((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
(\ Any
v0 Any
v1 Any
v2 ->
(Any -> T_Pointwise_34) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64 Any
v2)
d_inj'8322''8347'_80 ::
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.Function.Equality.T_Π_16
d_inj'8322''8347'_80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
d_inj'8322''8347'_80 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5
= T_Π_16
du_inj'8322''8347'_80
du_inj'8322''8347'_80 :: MAlonzo.Code.Function.Equality.T_Π_16
du_inj'8322''8347'_80 :: T_Π_16
du_inj'8322''8347'_80
= ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16)
-> Any -> (Any -> Any -> Any -> Any) -> T_Π_16
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171
((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
(\ Any
v0 Any
v1 Any
v2 ->
(Any -> T_Pointwise_34) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70 Any
v2)
d_'91'_'44'_'93''8347'_88 ::
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.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
d_'91'_'44'_'93''8347'_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Π_16
d_'91'_'44'_'93''8347'_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 T_Π_16
v9
T_Π_16
v10
= T_Π_16 -> T_Π_16 -> T_Π_16
du_'91'_'44'_'93''8347'_88 T_Π_16
v9 T_Π_16
v10
du_'91'_'44'_'93''8347'_88 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
du_'91'_'44'_'93''8347'_88 :: T_Π_16 -> T_Π_16 -> T_Π_16
du_'91'_'44'_'93''8347'_88 T_Π_16
v0 T_Π_16
v1
= ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16)
-> Any -> Any -> T_Π_16
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171
(((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
((T_Π_16 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v0))
((T_Π_16 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v1)))
((T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> Any
du_'46'extendedlambda0_98 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v0) (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
v1))
d_'46'extendedlambda0_98 ::
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.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34 ->
AgdaAny
d_'46'extendedlambda0_98 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> Any
d_'46'extendedlambda0_98 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 T_Π_16
v9 T_Π_16
v10
T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_34
v13
= T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> Any
du_'46'extendedlambda0_98 T_Π_16
v9 T_Π_16
v10 T__'8846'__30
v11 T__'8846'__30
v12 T_Pointwise_34
v13
du_'46'extendedlambda0_98 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34 ->
AgdaAny
du_'46'extendedlambda0_98 :: T_Π_16
-> T_Π_16
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> Any
du_'46'extendedlambda0_98 T_Π_16
v0 T_Π_16
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
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64 Any
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 Any
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 Any
v9
-> (T_Π_16 -> Any -> Any -> Any -> Any)
-> T_Π_16 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Equality.d_cong_40 T_Π_16
v0 Any
v8 Any
v9 Any
v7
T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70 Any
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 Any
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 Any
v9
-> (T_Π_16 -> Any -> Any -> Any -> Any)
-> T_Π_16 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Equality.d_cong_40 T_Π_16
v1 Any
v8 Any
v9 Any
v7
T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Pointwise_34
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_swap'8347'_120 ::
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.Function.Equality.T_Π_16
d_swap'8347'_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
d_swap'8347'_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 = T_Π_16
du_swap'8347'_120
du_swap'8347'_120 :: MAlonzo.Code.Function.Equality.T_Π_16
du_swap'8347'_120 :: T_Π_16
du_swap'8347'_120
= (T_Π_16 -> T_Π_16 -> T_Π_16) -> Any -> Any -> T_Π_16
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> T_Π_16
du_'91'_'44'_'93''8347'_88 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
du_inj'8322''8347'_80)
(T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
du_inj'8321''8347'_78)
d__'8846''45'equivalence__150 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d__'8846''45'equivalence__150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Equivalence_16
-> T_Equivalence_16
-> T_Equivalence_16
d__'8846''45'equivalence__150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8
~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Equivalence_16
v12 T_Equivalence_16
v13
= T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8846''45'equivalence__150 T_Equivalence_16
v12 T_Equivalence_16
v13
du__'8846''45'equivalence__150 ::
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du__'8846''45'equivalence__150 :: T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8846''45'equivalence__150 T_Equivalence_16
v0 T_Equivalence_16
v1
= (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> Any -> Any -> T_Equivalence_16
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.C_Equivalence'46'constructor_433
((T_Π_16 -> T_Π_16 -> T_Π_16) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> T_Π_16
du__'8846''45''10230'__36
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v0))
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v1)))
((T_Π_16 -> T_Π_16 -> T_Π_16) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> T_Π_16
du__'8846''45''10230'__36
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36 (T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v0))
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36 (T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v1)))
d__'8846''45'injection__160 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88
d__'8846''45'injection__160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T_Injection_88
d__'8846''45'injection__160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9
~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Injection_88
v12 T_Injection_88
v13
= T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8846''45'injection__160 T_Injection_88
v12 T_Injection_88
v13
du__'8846''45'injection__160 ::
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88
du__'8846''45'injection__160 :: T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8846''45'injection__160 T_Injection_88
v0 T_Injection_88
v1
= (T_Π_16 -> (Any -> Any -> Any -> Any) -> T_Injection_88)
-> Any -> Any -> T_Injection_88
forall a b. a -> b
coe
T_Π_16 -> (Any -> Any -> Any -> Any) -> T_Injection_88
MAlonzo.Code.Function.Injection.C_Injection'46'constructor_3057
((T_Π_16 -> T_Π_16 -> T_Π_16) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> T_Π_16
du__'8846''45''10230'__36
((T_Injection_88 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106 (T_Injection_88 -> Any
forall a b. a -> b
coe T_Injection_88
v0))
((T_Injection_88 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106 (T_Injection_88 -> Any
forall a b. a -> b
coe T_Injection_88
v1)))
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 Any
v3 -> (T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_inj_182 (T_Injection_88 -> Any
forall a b. a -> b
coe T_Injection_88
v0) (T_Injection_88 -> Any
forall a b. a -> b
coe T_Injection_88
v1) (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v3)))
d__'8776'__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 ->
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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()
d__'8776'__172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
d__'8776'__172 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
forall a. a
erased
d__'8776'__176 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()
d__'8776'__176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
d__'8776'__176 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Level_18
forall a. a
erased
d_inj_182 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34
d_inj_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
d_inj_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Injection_88
v12 T_Injection_88
v13
T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16
= T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_inj_182 T_Injection_88
v12 T_Injection_88
v13 T__'8846'__30
v14 T__'8846'__30
v15 T_Pointwise_34
v16
du_inj_182 ::
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34 ->
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.T_Pointwise_34
du_inj_182 :: T_Injection_88
-> T_Injection_88
-> T__'8846'__30
-> T__'8846'__30
-> T_Pointwise_34
-> T_Pointwise_34
du_inj_182 T_Injection_88
v0 T_Injection_88
v1 T__'8846'__30
v2 T__'8846'__30
v3 T_Pointwise_34
v4
= 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 Any
v5
-> 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 Any
v6
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v4 of
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64 Any
v9
-> (Any -> T_Pointwise_34) -> Any -> T_Pointwise_34
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64
((T_Injection_88 -> Any -> Any -> Any -> Any)
-> T_Injection_88 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_88 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Injection.d_injective_108 T_Injection_88
v0 Any
v5 Any
v6 Any
v9)
T_Pointwise_34
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8846'__30
_ -> T_Pointwise_34
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v5
-> 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 Any
v6
-> case T_Pointwise_34 -> T_Pointwise_34
forall a b. a -> b
coe T_Pointwise_34
v4 of
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70 Any
v9
-> (Any -> T_Pointwise_34) -> Any -> T_Pointwise_34
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70
((T_Injection_88 -> Any -> Any -> Any -> Any)
-> T_Injection_88 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_88 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Injection.d_injective_108 T_Injection_88
v1 Any
v5 Any
v6 Any
v9)
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
d__'8846''45'left'45'inverse__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 ->
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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d__'8846''45'left'45'inverse__196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> T_LeftInverse_82
-> T_LeftInverse_82
d__'8846''45'left'45'inverse__196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7
~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_LeftInverse_82
v12 T_LeftInverse_82
v13
= T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45'left'45'inverse__196 T_LeftInverse_82
v12 T_LeftInverse_82
v13
du__'8846''45'left'45'inverse__196 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du__'8846''45'left'45'inverse__196 :: T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45'left'45'inverse__196 T_LeftInverse_82
v0 T_LeftInverse_82
v1
= (T_Π_16 -> T_Π_16 -> (Any -> Any) -> T_LeftInverse_82)
-> Any -> Any -> Any -> T_LeftInverse_82
forall a b. a -> b
coe
T_Π_16 -> T_Π_16 -> (Any -> Any) -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.C_LeftInverse'46'constructor_4555
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe
T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34
((T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16)
-> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16
du_eq_206 (T_LeftInverse_82 -> Any
forall a b. a -> b
coe T_LeftInverse_82
v0) (T_LeftInverse_82 -> Any
forall a b. a -> b
coe T_LeftInverse_82
v1)))
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe
T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
((T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16)
-> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16
du_eq_206 (T_LeftInverse_82 -> Any
forall a b. a -> b
coe T_LeftInverse_82
v0) (T_LeftInverse_82 -> Any
forall a b. a -> b
coe T_LeftInverse_82
v1)))
(((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(Any -> T_Pointwise_34) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8321'_64
((T_LeftInverse_82 -> Any -> Any) -> T_LeftInverse_82 -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> Any -> Any
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106 T_LeftInverse_82
v0
Any
v2)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(Any -> T_Pointwise_34) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Pointwise_34
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.C_inj'8322'_70
((T_LeftInverse_82 -> Any -> Any) -> T_LeftInverse_82 -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> Any -> Any
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106 T_LeftInverse_82
v1
Any
v2))))
d_eq_206 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_eq_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> T_LeftInverse_82
-> T_Equivalence_16
d_eq_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_LeftInverse_82
v12 T_LeftInverse_82
v13
= T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16
du_eq_206 T_LeftInverse_82
v12 T_LeftInverse_82
v13
du_eq_206 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_eq_206 :: T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16
du_eq_206 T_LeftInverse_82
v0 T_LeftInverse_82
v1
= (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> Any -> Any -> T_Equivalence_16
forall a b. a -> b
coe
T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8846''45'equivalence__150
((T_LeftInverse_82 -> T_Equivalence_16) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_82 -> T_Equivalence_16
MAlonzo.Code.Function.LeftInverse.du_equivalence_186 (T_LeftInverse_82 -> Any
forall a b. a -> b
coe T_LeftInverse_82
v0))
((T_LeftInverse_82 -> T_Equivalence_16) -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_82 -> T_Equivalence_16
MAlonzo.Code.Function.LeftInverse.du_equivalence_186 (T_LeftInverse_82 -> Any
forall a b. a -> b
coe T_LeftInverse_82
v1))
d__'8846''45'surjection__240 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
d__'8846''45'surjection__240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_Surjection_54
-> T_Surjection_54
d__'8846''45'surjection__240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8
~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Surjection_54
v12 T_Surjection_54
v13
= T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8846''45'surjection__240 T_Surjection_54
v12 T_Surjection_54
v13
du__'8846''45'surjection__240 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
du__'8846''45'surjection__240 :: T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8846''45'surjection__240 T_Surjection_54
v0 T_Surjection_54
v1
= (T_Π_16 -> T_Surjective_18 -> T_Surjection_54)
-> Any -> Any -> T_Surjection_54
forall a b. a -> b
coe
T_Π_16 -> T_Surjective_18 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.C_Surjection'46'constructor_2369
((T_LeftInverse_82 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_from_104
((T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_inv_250 (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v0) (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v1)))
((T_Π_16 -> (Any -> Any) -> T_Surjective_18) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> (Any -> Any) -> T_Surjective_18
MAlonzo.Code.Function.Surjection.C_Surjective'46'constructor_1229
((T_LeftInverse_82 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_to_102
((T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_inv_250 (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v0) (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v1)))
((T_LeftInverse_82 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> Any -> Any
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106
((T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_inv_250 (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v0) (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v1))))
d_inv_250 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_inv_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_Surjection_54
-> T_LeftInverse_82
d_inv_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Surjection_54
v12 T_Surjection_54
v13
= T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_inv_250 T_Surjection_54
v12 T_Surjection_54
v13
du_inv_250 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_inv_250 :: T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_inv_250 T_Surjection_54
v0 T_Surjection_54
v1
= (T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> Any -> Any -> T_LeftInverse_82
forall a b. a -> b
coe
T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45'left'45'inverse__196
((T_Surjection_54 -> T_LeftInverse_82) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_LeftInverse_82
MAlonzo.Code.Function.Surjection.du_right'45'inverse_82 (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v0))
((T_Surjection_54 -> T_LeftInverse_82) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_LeftInverse_82
MAlonzo.Code.Function.Surjection.du_right'45'inverse_82 (T_Surjection_54 -> Any
forall a b. a -> b
coe T_Surjection_54
v1))
d__'8846''45'inverse__252 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58
d__'8846''45'inverse__252 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_58
-> T_Inverse_58
-> T_Inverse_58
d__'8846''45'inverse__252 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 T_Setoid_44
v8 ~T_Setoid_44
v9
T_Setoid_44
v10 ~T_Setoid_44
v11 T_Inverse_58
v12 T_Inverse_58
v13
= T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
du__'8846''45'inverse__252 T_Setoid_44
v8 T_Setoid_44
v10 T_Inverse_58
v12 T_Inverse_58
v13
du__'8846''45'inverse__252 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58
du__'8846''45'inverse__252 :: T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
du__'8846''45'inverse__252 T_Setoid_44
v0 T_Setoid_44
v1 T_Inverse_58
v2 T_Inverse_58
v3
= (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T_Inverse_58)
-> Any -> Any -> Any -> 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
((T_Surjection_54 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_to_72
((T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54
du_surj_262 (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v0) (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v1) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v2) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v3)))
((T_Surjective_18 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe
T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74
((T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54
du_surj_262 (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v0) (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v1) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v2) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v3))))
(((Any -> Any) -> (Any -> Any) -> T__InverseOf__20)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T__InverseOf__20
MAlonzo.Code.Function.Inverse.C__InverseOf_'46'constructor_2103
((T_LeftInverse_82 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> Any -> Any
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106
((T_Inverse_58 -> T_Inverse_58 -> T_LeftInverse_82)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_LeftInverse_82
du_inv_264 (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v2) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v3)))
((T_Surjective_18 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Surjective_18 -> Any -> Any
MAlonzo.Code.Function.Surjection.d_right'45'inverse'45'of_40
((T_Surjection_54 -> T_Surjective_18) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74
((T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54
du_surj_262 (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v0) (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v1) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v2) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v3)))))
d_surj_262 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
d_surj_262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_58
-> T_Inverse_58
-> T_Surjection_54
d_surj_262 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 T_Setoid_44
v8 ~T_Setoid_44
v9 T_Setoid_44
v10 ~T_Setoid_44
v11 T_Inverse_58
v12 T_Inverse_58
v13
= T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54
du_surj_262 T_Setoid_44
v8 T_Setoid_44
v10 T_Inverse_58
v12 T_Inverse_58
v13
du_surj_262 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
du_surj_262 :: T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54
du_surj_262 T_Setoid_44
v0 T_Setoid_44
v1 T_Inverse_58
v2 T_Inverse_58
v3
= (T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> Any -> Any -> T_Surjection_54
forall a b. a -> b
coe
T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8846''45'surjection__240
((T_Bijection_64 -> T_Surjection_54) -> Any -> Any
forall a b. a -> b
coe
T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100
((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98 (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v0) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v2)))
((T_Bijection_64 -> T_Surjection_54) -> Any -> Any
forall a b. a -> b
coe
T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100
((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98 (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v1) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v3)))
d_inv_264 ::
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.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 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_inv_264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_58
-> T_Inverse_58
-> T_LeftInverse_82
d_inv_264 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Setoid_44
v8 ~T_Setoid_44
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Inverse_58
v12 T_Inverse_58
v13
= T_Inverse_58 -> T_Inverse_58 -> T_LeftInverse_82
du_inv_264 T_Inverse_58
v12 T_Inverse_58
v13
du_inv_264 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_inv_264 :: T_Inverse_58 -> T_Inverse_58 -> T_LeftInverse_82
du_inv_264 T_Inverse_58
v0 T_Inverse_58
v1
= (T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> Any -> Any -> T_LeftInverse_82
forall a b. a -> b
coe
T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45'left'45'inverse__196
((T_Inverse_58 -> T_LeftInverse_82) -> Any -> Any
forall a b. a -> b
coe T_Inverse_58 -> T_LeftInverse_82
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90 (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v0))
((T_Inverse_58 -> T_LeftInverse_82) -> Any -> Any
forall a b. a -> b
coe T_Inverse_58 -> T_LeftInverse_82
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90 (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v1))