{-# 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.Propositional 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.Function.Setoid
import qualified MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Function.Bijection
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.Related
import qualified MAlonzo.Code.Function.Surjection
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
d__'8846''45''8660'__28 ::
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.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d__'8846''45''8660'__28 :: 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_Equivalence_16
-> T_Equivalence_16
-> T_Equivalence_16
d__'8846''45''8660'__28 ~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_Equivalence_16
v8 T_Equivalence_16
v9
= T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8846''45''8660'__28 T_Equivalence_16
v8 T_Equivalence_16
v9
du__'8846''45''8660'__28 ::
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du__'8846''45''8660'__28 :: T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8846''45''8660'__28 T_Equivalence_16
v0 T_Equivalence_16
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
MAlonzo.Code.Function.Equivalence.du__'8728'__82
((T_Surjection_54 -> T_Equivalence_16) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_Equivalence_16
MAlonzo.Code.Function.Surjection.du_equivalence_92
((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 -> T_Setoid_44 -> T_Setoid_44) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__484
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550))))
((T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du__'8728'__82
((T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'equivalence__150
(T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v0) (T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v1))
((T_Equivalence_16 -> T_Equivalence_16) -> Any -> Any
forall a b. a -> b
coe
T_Equivalence_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_sym_100
((T_Surjection_54 -> T_Equivalence_16) -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_Equivalence_16
MAlonzo.Code.Function.Surjection.du_equivalence_92
((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 -> T_Setoid_44 -> T_Setoid_44) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__484
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550))))))
d__'8846''45''8611'__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.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88
d__'8846''45''8611'__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_Injection_88
-> T_Injection_88
-> T_Injection_88
d__'8846''45''8611'__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_Injection_88
v8 T_Injection_88
v9
= T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8846''45''8611'__38 T_Injection_88
v8 T_Injection_88
v9
du__'8846''45''8611'__38 ::
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
MAlonzo.Code.Function.Injection.T_Injection_88
du__'8846''45''8611'__38 :: T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8846''45''8611'__38 T_Injection_88
v0 T_Injection_88
v1
= (T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> Any -> Any -> T_Injection_88
forall a b. a -> b
coe
T_Injection_88 -> T_Injection_88 -> T_Injection_88
MAlonzo.Code.Function.Injection.du__'8728'__172
((T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
MAlonzo.Code.Function.LeftInverse.du_injection_184
((T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__484
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
((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
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550)))
((T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Injection_88 -> T_Injection_88 -> T_Injection_88
MAlonzo.Code.Function.Injection.du__'8728'__172
((T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Injection_88 -> T_Injection_88 -> T_Injection_88
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'injection__160
(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))
((T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
MAlonzo.Code.Function.LeftInverse.du_injection_184
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((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 -> T_Inverse_58) -> Any -> Any
forall a b. a -> b
coe
T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550)))))
d__'8846''45''8606'__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.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d__'8846''45''8606'__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_LeftInverse_82
-> T_LeftInverse_82
-> T_LeftInverse_82
d__'8846''45''8606'__48 ~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_LeftInverse_82
v8 T_LeftInverse_82
v9
= T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45''8606'__48 T_LeftInverse_82
v8 T_LeftInverse_82
v9
du__'8846''45''8606'__48 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du__'8846''45''8606'__48 :: T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45''8606'__48 T_LeftInverse_82
v0 T_LeftInverse_82
v1
= (T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> Any -> Any -> Any -> T_LeftInverse_82
forall a b. a -> b
coe
T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.du__'8728'__280
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((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
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550))
((T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.du__'8728'__280
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'left'45'inverse__196
(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_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 -> T_Inverse_58) -> Any -> Any
forall a b. a -> b
coe
T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550))))
d__'8846''45''8608'__58 ::
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.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
d__'8846''45''8608'__58 :: 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_Surjection_54
-> T_Surjection_54
-> T_Surjection_54
d__'8846''45''8608'__58 ~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_Surjection_54
v8 T_Surjection_54
v9
= T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8846''45''8608'__58 T_Surjection_54
v8 T_Surjection_54
v9
du__'8846''45''8608'__58 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
du__'8846''45''8608'__58 :: T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8846''45''8608'__58 T_Surjection_54
v0 T_Surjection_54
v1
= (T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> Any -> Any -> Any -> T_Surjection_54
forall a b. a -> b
coe
T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du__'8728'__196
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((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 -> T_Setoid_44 -> T_Setoid_44) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__484
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550)))
((T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du__'8728'__196
((T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__484
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
((T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'surjection__240
(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_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
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((T_Inverse_58 -> T_Inverse_58) -> Any -> Any
forall a b. a -> b
coe
T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550)))))
d__'8846''45''8596'__68 ::
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.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58
d__'8846''45''8596'__68 :: 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_Inverse_58
-> T_Inverse_58
-> T_Inverse_58
d__'8846''45''8596'__68 ~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_Inverse_58
v8 T_Inverse_58
v9
= T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
du__'8846''45''8596'__68 T_Inverse_58
v8 T_Inverse_58
v9
du__'8846''45''8596'__68 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58
du__'8846''45''8596'__68 :: T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
du__'8846''45''8596'__68 T_Inverse_58
v0 T_Inverse_58
v1
= (T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58)
-> Any -> Any -> Any -> Any -> T_Inverse_58
forall a b. a -> b
coe
T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du__'8728'__208
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550)
((T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du__'8728'__208
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__484
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
((T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'inverse__252
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v0) (T_Inverse_58 -> Any
forall a b. a -> b
coe T_Inverse_58
v1))
((T_Inverse_58 -> T_Inverse_58) -> Any -> Any
forall a b. a -> b
coe
T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226
(T_Inverse_58 -> Any
forall a b. a -> b
coe
T_Inverse_58
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_550)))
d__'8846''45'cong__100 ::
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.Function.Related.T_Kind_52 ->
AgdaAny -> AgdaAny -> AgdaAny
d__'8846''45'cong__100 :: 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_Kind_52
-> Any
-> Any
-> Any
d__'8846''45'cong__100 ~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_Kind_52
v8
= T_Kind_52 -> Any -> Any -> Any
du__'8846''45'cong__100 T_Kind_52
v8
du__'8846''45'cong__100 ::
MAlonzo.Code.Function.Related.T_Kind_52 ->
AgdaAny -> AgdaAny -> AgdaAny
du__'8846''45'cong__100 :: T_Kind_52 -> Any -> Any -> Any
du__'8846''45'cong__100 T_Kind_52
v0
= case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
T_Kind_52
MAlonzo.Code.Function.Related.C_implication_54
-> ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
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_Kind_52
MAlonzo.Code.Function.Related.C_reverse'45'implication_56
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 ->
((Any -> Any) -> T__'8592'__12) -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> T__'8592'__12
MAlonzo.Code.Function.Related.C_lam_26
(((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
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__'8592'__12 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T__'8592'__12 -> Any -> Any
MAlonzo.Code.Function.Related.d_app'45''8592'_24 (Any -> Any
forall a b. a -> b
coe Any
v1))
((T__'8592'__12 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T__'8592'__12 -> Any -> Any
MAlonzo.Code.Function.Related.d_app'45''8592'_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
T_Kind_52
MAlonzo.Code.Function.Related.C_equivalence_58
-> (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8846''45''8660'__28
T_Kind_52
MAlonzo.Code.Function.Related.C_injection_60
-> (T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8846''45''8611'__38
T_Kind_52
MAlonzo.Code.Function.Related.C_reverse'45'injection_62
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 ->
(T_Injection_88 -> T__'8610'__36) -> Any -> Any
forall a b. a -> b
coe
T_Injection_88 -> T__'8610'__36
MAlonzo.Code.Function.Related.C_lam_50
((T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8846''45''8611'__38
((T__'8610'__36 -> T_Injection_88) -> Any -> Any
forall a b. a -> b
coe T__'8610'__36 -> T_Injection_88
MAlonzo.Code.Function.Related.d_app'45''8610'_48 (Any -> Any
forall a b. a -> b
coe Any
v1))
((T__'8610'__36 -> T_Injection_88) -> Any -> Any
forall a b. a -> b
coe T__'8610'__36 -> T_Injection_88
MAlonzo.Code.Function.Related.d_app'45''8610'_48 (Any -> Any
forall a b. a -> b
coe Any
v2))))
T_Kind_52
MAlonzo.Code.Function.Related.C_left'45'inverse_64
-> (T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> Any -> Any -> Any
forall a b. a -> b
coe T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8846''45''8606'__48
T_Kind_52
MAlonzo.Code.Function.Related.C_surjection_66
-> (T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8846''45''8608'__58
T_Kind_52
MAlonzo.Code.Function.Related.C_bijection_68
-> (T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58) -> Any -> Any -> Any
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
du__'8846''45''8596'__68
T_Kind_52
_ -> Any -> Any -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError