{-# 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.Product.Function.NonDependent.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.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Function.Base
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__'215''45''10230'__38 ::
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__'215''45''10230'__38 :: 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__'215''45''10230'__38 ~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__'215''45''10230'__38 T_Π_16
v12 T_Π_16
v13
du__'215''45''10230'__38 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
du__'215''45''10230'__38 :: T_Π_16 -> T_Π_16 -> T_Π_16
du__'215''45''10230'__38 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_Σ_14 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14
du_fg_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))
((T_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_fg'45'cong_62 (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'__50 ::
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.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> ()
d__'8776'__50 :: 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_Σ_14
-> T_Σ_14
-> T_Level_18
d__'8776'__50 = 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_Σ_14
-> T_Σ_14
-> T_Level_18
forall a. a
erased
d__'8776'__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.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> ()
d__'8776'__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_Σ_14
-> T_Σ_14
-> T_Level_18
d__'8776'__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_Σ_14
-> T_Σ_14
-> T_Level_18
forall a. a
erased
d_fg_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.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_fg_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_Σ_14
-> T_Σ_14
d_fg_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_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14
du_fg_56 T_Π_16
v12 T_Π_16
v13
du_fg_56 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_fg_56 :: T_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14
du_fg_56 T_Π_16
v0 T_Π_16
v1
= ((Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((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))
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1)))
d_fg'45'cong_62 ::
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.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_fg'45'cong_62 :: 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_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_fg'45'cong_62 ~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_Σ_14
v14 T_Σ_14
v15 T_Σ_14
v16
= T_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_fg'45'cong_62 T_Π_16
v12 T_Π_16
v13 T_Σ_14
v14 T_Σ_14
v15 T_Σ_14
v16
du_fg'45'cong_62 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_fg'45'cong_62 :: T_Π_16 -> T_Π_16 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_fg'45'cong_62 T_Π_16
v0 T_Π_16
v1 T_Σ_14
v2 T_Σ_14
v3 T_Σ_14
v4
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v5 Any
v6
-> (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((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 -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14 -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302
(\ Any
v7 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v7))
(\ Any
v7 Any
v8 -> Any
v7) T_Σ_14
v2 T_Σ_14
v3)
(((Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any -> Any) -> (Any -> Any) -> T_Σ_14 -> T_Σ_14 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
(\ Any
v7 Any
v8 -> Any
v8)
(\ Any
v7 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v7)) T_Σ_14
v2 T_Σ_14
v3)
Any
v5)
((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 -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14 -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302
(\ Any
v7 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v7))
(\ Any
v7 Any
v8 -> Any
v7) T_Σ_14
v2 T_Σ_14
v3)
(((Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any -> Any) -> (Any -> Any) -> T_Σ_14 -> T_Σ_14 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
(\ Any
v7 Any
v8 -> Any
v8)
(\ Any
v7 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v7)) T_Σ_14
v2 T_Σ_14
v3)
Any
v6)
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60'_'44'_'62''8347'_90 ::
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.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
d_'60'_'44'_'62''8347'_90 :: 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_Π_16
-> T_Π_16
-> T_Π_16
d_'60'_'44'_'62''8347'_90 ~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_Setoid_44
v6 ~T_Setoid_44
v7 ~T_Setoid_44
v8 T_Π_16
v9
T_Π_16
v10
= T_Π_16 -> T_Π_16 -> T_Π_16
du_'60'_'44'_'62''8347'_90 T_Π_16
v9 T_Π_16
v10
du_'60'_'44'_'62''8347'_90 ::
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16 ->
MAlonzo.Code.Function.Equality.T_Π_16
du_'60'_'44'_'62''8347'_90 :: T_Π_16 -> T_Π_16 -> T_Π_16
du_'60'_'44'_'62''8347'_90 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) -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132
((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)))
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 Any
v3 ->
((Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132
((T_Π_16 -> Any -> Any -> Any -> Any) -> T_Π_16 -> 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
v2 Any
v3)
((T_Π_16 -> Any -> Any -> Any -> Any) -> T_Π_16 -> 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
v2 Any
v3)))
d_proj'8321''8347'_116 ::
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_proj'8321''8347'_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
d_proj'8321''8347'_116 ~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_proj'8321''8347'_116
du_proj'8321''8347'_116 :: MAlonzo.Code.Function.Equality.T_Π_16
du_proj'8321''8347'_116 :: T_Π_16
du_proj'8321''8347'_116
= ((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
forall a b. a -> b
coe (\ Any
v0 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v0)))
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v0 Any
v1 Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2)))
d_proj'8322''8347'_118 ::
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_proj'8322''8347'_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
d_proj'8322''8347'_118 ~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_proj'8322''8347'_118
du_proj'8322''8347'_118 :: MAlonzo.Code.Function.Equality.T_Π_16
du_proj'8322''8347'_118 :: T_Π_16
du_proj'8322''8347'_118
= ((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
forall a b. a -> b
coe (\ Any
v0 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v0)))
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v0 Any
v1 Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2)))
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_'60'_'44'_'62''8347'_90 (T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
du_proj'8322''8347'_118)
(T_Π_16 -> Any
forall a b. a -> b
coe T_Π_16
du_proj'8321''8347'_116)
d__'215''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__'215''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__'215''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__'215''45'equivalence__150 T_Equivalence_16
v12 T_Equivalence_16
v13
du__'215''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__'215''45'equivalence__150 :: T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'215''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__'215''45''10230'__38
((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__'215''45''10230'__38
((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__'215''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__'215''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__'215''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__'215''45'injection__160 T_Injection_88
v12 T_Injection_88
v13
du__'215''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__'215''45'injection__160 :: T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'215''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__'215''45''10230'__38
((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 ->
((Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Injection_88 -> Any -> Any -> Any -> Any)
-> T_Injection_88 -> 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
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2))
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v3)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 ->
(T_Injection_88 -> Any -> Any -> Any -> Any)
-> T_Injection_88 -> 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
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2))
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v3))))))
d__'215''45'left'45'inverse__170 ::
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__'215''45'left'45'inverse__170 :: 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__'215''45'left'45'inverse__170 ~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__'215''45'left'45'inverse__170 T_LeftInverse_82
v12 T_LeftInverse_82
v13
du__'215''45'left'45'inverse__170 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du__'215''45'left'45'inverse__170 :: T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'215''45'left'45'inverse__170 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_180 (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_180 (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_LeftInverse_82 -> T_LeftInverse_82 -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_82 -> T_LeftInverse_82 -> T_Σ_14 -> T_Σ_14
du_left_182 (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))
d_eq_180 ::
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_180 :: 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_180 ~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_180 T_LeftInverse_82
v12 T_LeftInverse_82
v13
du_eq_180 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_eq_180 :: T_LeftInverse_82 -> T_LeftInverse_82 -> T_Equivalence_16
du_eq_180 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__'215''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_left_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.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_left_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_LeftInverse_82
-> T_LeftInverse_82
-> T_Σ_14
-> T_Σ_14
d_left_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_LeftInverse_82
v12
T_LeftInverse_82
v13 T_Σ_14
v14
= T_LeftInverse_82 -> T_LeftInverse_82 -> T_Σ_14 -> T_Σ_14
du_left_182 T_LeftInverse_82
v12 T_LeftInverse_82
v13 T_Σ_14
v14
du_left_182 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_left_182 :: T_LeftInverse_82 -> T_LeftInverse_82 -> T_Σ_14 -> T_Σ_14
du_left_182 T_LeftInverse_82
v0 T_LeftInverse_82
v1 T_Σ_14
v2
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
-> (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((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
v3)
((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
v4)
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'215''45'surjection__216 ::
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__'215''45'surjection__216 :: 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__'215''45'surjection__216 ~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__'215''45'surjection__216 T_Surjection_54
v12 T_Surjection_54
v13
du__'215''45'surjection__216 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
du__'215''45'surjection__216 :: T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'215''45'surjection__216 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_226 (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_226 (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_226 (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_226 ::
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_226 :: 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_226 ~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_226 T_Surjection_54
v12 T_Surjection_54
v13
du_inv_226 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_inv_226 :: T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_inv_226 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__'215''45'left'45'inverse__170
((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__'215''45'inverse__228 ::
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__'215''45'inverse__228 :: 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__'215''45'inverse__228 ~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__'215''45'inverse__228 T_Setoid_44
v8 T_Setoid_44
v10 T_Inverse_58
v12 T_Inverse_58
v13
du__'215''45'inverse__228 ::
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__'215''45'inverse__228 :: T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
du__'215''45'inverse__228 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_238 (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_238 (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_240 (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_238 (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_238 ::
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_238 :: 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_238 ~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_238 T_Setoid_44
v8 T_Setoid_44
v10 T_Inverse_58
v12 T_Inverse_58
v13
du_surj_238 ::
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_238 :: T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Surjection_54
du_surj_238 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__'215''45'surjection__216
((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_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.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_inv_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_Inverse_58
-> T_Inverse_58
-> T_LeftInverse_82
d_inv_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_Inverse_58
v12 T_Inverse_58
v13
= T_Inverse_58 -> T_Inverse_58 -> T_LeftInverse_82
du_inv_240 T_Inverse_58
v12 T_Inverse_58
v13
du_inv_240 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_inv_240 :: T_Inverse_58 -> T_Inverse_58 -> T_LeftInverse_82
du_inv_240 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__'215''45'left'45'inverse__170
((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))