{-# 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.Function.Properties.Inverse where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Consequences.Setoid
import qualified MAlonzo.Code.Function.Construct.Composition
import qualified MAlonzo.Code.Function.Construct.Identity
import qualified MAlonzo.Code.Function.Construct.Symmetry
import qualified MAlonzo.Code.Function.Properties.RightInverse
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Properties.Inverse.isEquivalence
d_isEquivalence_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_32 :: T_Level_18 -> T_Level_18 -> T_IsEquivalence_28
d_isEquivalence_32 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsEquivalence_28
du_isEquivalence_32
du_isEquivalence_32 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_isEquivalence_32 :: T_IsEquivalence_28
du_isEquivalence_32
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_28)
-> Any
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_28
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 ->
            T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
MAlonzo.Code.Function.Construct.Identity.du_inverse_636))
      (\ Any
v0 Any
v1 Any
v2 ->
         (T_Inverse_2122 -> T_Inverse_2122) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Symmetry.du_inverse_1096 Any
v2)
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 ->
         (T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122)
-> Any -> Any -> Any
forall a b. a -> b
coe
           T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Composition.du_inverse_2322 Any
v3 Any
v4)
-- Function.Properties.Inverse.↔-refl
d_'8596''45'refl_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8596''45'refl_36 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'8596''45'refl_36 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_2122
du_'8596''45'refl_36
du_'8596''45'refl_36 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8596''45'refl_36 :: T_Inverse_2122
du_'8596''45'refl_36
  = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
MAlonzo.Code.Function.Construct.Identity.du_'8596''45'id_660
-- Function.Properties.Inverse.↔-sym
d_'8596''45'sym_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8596''45'sym_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
d_'8596''45'sym_38 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'sym_38
du_'8596''45'sym_38 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8596''45'sym_38 :: T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'sym_38
  = (T_Inverse_2122 -> T_Inverse_2122)
-> T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe
      T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Symmetry.du_'8596''45'sym_1196
-- Function.Properties.Inverse.↔-trans
d_'8596''45'trans_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8596''45'trans_40 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
-> T_Inverse_2122
d_'8596''45'trans_40 ~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_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'trans_40
du_'8596''45'trans_40 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8596''45'trans_40 :: T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'trans_40
  = (T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122)
-> T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Composition.du_inverse_2322
-- Function.Properties.Inverse.↔-isEquivalence
d_'8596''45'isEquivalence_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_'8596''45'isEquivalence_42 :: T_Level_18 -> T_IsEquivalence_28
d_'8596''45'isEquivalence_42 ~T_Level_18
v0 = T_IsEquivalence_28
du_'8596''45'isEquivalence_42
du_'8596''45'isEquivalence_42 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_'8596''45'isEquivalence_42 :: T_IsEquivalence_28
du_'8596''45'isEquivalence_42
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_28)
-> (Any -> Any) -> Any -> Any -> T_IsEquivalence_28
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
      (\ Any
v0 -> T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
du_'8596''45'refl_36)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_Inverse_2122 -> T_Inverse_2122) -> Any
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'sym_38))
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> (T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122) -> Any
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'trans_40))
-- Function.Properties.Inverse.toFunction
d_toFunction_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d_toFunction_44 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> T_Func_774
d_toFunction_44 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_46
v5 T_Inverse_2122
v6 = T_Inverse_2122 -> T_Func_774
du_toFunction_44 T_Inverse_2122
v6
du_toFunction_44 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
du_toFunction_44 :: T_Inverse_2122 -> T_Func_774
du_toFunction_44 T_Inverse_2122
v0
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_774)
-> Any -> Any -> T_Func_774
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_774
MAlonzo.Code.Function.Bundles.C_constructor_840
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
-- Function.Properties.Inverse.fromFunction
d_fromFunction_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d_fromFunction_134 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> T_Func_774
d_fromFunction_134 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_46
v5 T_Inverse_2122
v6
  = T_Inverse_2122 -> T_Func_774
du_fromFunction_134 T_Inverse_2122
v6
du_fromFunction_134 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
du_fromFunction_134 :: T_Inverse_2122 -> T_Func_774
du_fromFunction_134 T_Inverse_2122
v0
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_774)
-> Any -> Any -> T_Func_774
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_774
MAlonzo.Code.Function.Bundles.C_constructor_840
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_2140 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
-- Function.Properties.Inverse.Inverse⇒Injection
d_Inverse'8658'Injection_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
d_Inverse'8658'Injection_224 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> T_Injection_842
d_Inverse'8658'Injection_224 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Setoid_46
v5 T_Inverse_2122
v6
  = T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Injection_842
du_Inverse'8658'Injection_224 T_Setoid_46
v2 T_Setoid_46
v5 T_Inverse_2122
v6
du_Inverse'8658'Injection_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
du_Inverse'8658'Injection_224 :: T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Injection_842
du_Inverse'8658'Injection_224 T_Setoid_46
v0 T_Setoid_46
v1 T_Inverse_2122
v2
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Injection_842)
-> Any -> Any -> Any -> T_Injection_842
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Injection_842
MAlonzo.Code.Function.Bundles.C_constructor_916
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v2))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v2))
      ((T_Setoid_46
 -> T_Setoid_46
 -> (Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any)
-> T_Setoid_46
-> T_Setoid_46
-> (Any -> Any)
-> (Any -> Any)
-> Any
-> Any
forall a b. a -> b
coe
         T_Setoid_46
-> T_Setoid_46
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Function.Consequences.Setoid.du_inverse'691''8658'injective_80
         T_Setoid_46
v0 T_Setoid_46
v1 (T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v2))
         (T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v2))
         ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'691'_2146 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v2)))
-- Function.Properties.Inverse.Inverse⇒Surjection
d_Inverse'8658'Surjection_326 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d_Inverse'8658'Surjection_326 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> T_Surjection_918
d_Inverse'8658'Surjection_326 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_46
v5 T_Inverse_2122
v6
  = T_Inverse_2122 -> T_Surjection_918
du_Inverse'8658'Surjection_326 T_Inverse_2122
v6
du_Inverse'8658'Surjection_326 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du_Inverse'8658'Surjection_326 :: T_Inverse_2122 -> T_Surjection_918
du_Inverse'8658'Surjection_326 T_Inverse_2122
v0
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> T_Σ_14)
 -> T_Surjection_918)
-> Any -> Any -> Any -> T_Surjection_918
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> T_Σ_14)
-> T_Surjection_918
MAlonzo.Code.Function.Bundles.C_constructor_1002
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      (((Any -> Any) -> (Any -> Any -> Any -> Any) -> Any -> T_Σ_14)
-> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any -> Any -> Any) -> Any -> T_Σ_14
MAlonzo.Code.Function.Consequences.Setoid.du_inverse'737''8658'surjective_76
         (T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v0))
         ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'737'_2144 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0)))
-- Function.Properties.Inverse.Inverse⇒Bijection
d_Inverse'8658'Bijection_428 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_Inverse'8658'Bijection_428 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> T_Bijection_1004
d_Inverse'8658'Bijection_428 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Setoid_46
v5 T_Inverse_2122
v6
  = T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Bijection_1004
du_Inverse'8658'Bijection_428 T_Setoid_46
v2 T_Setoid_46
v5 T_Inverse_2122
v6
du_Inverse'8658'Bijection_428 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_Inverse'8658'Bijection_428 :: T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Bijection_1004
du_Inverse'8658'Bijection_428 T_Setoid_46
v0 T_Setoid_46
v1 T_Inverse_2122
v2
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Bijection_1004)
-> Any -> Any -> Any -> T_Bijection_1004
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Bijection_1004
MAlonzo.Code.Function.Bundles.C_constructor_1094
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v2))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v2))
      ((T_Setoid_46
 -> T_Setoid_46 -> (Any -> Any) -> (Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> T_Setoid_46
-> T_Setoid_46
-> (Any -> Any)
-> (Any -> Any)
-> T_Σ_14
-> Any
forall a b. a -> b
coe
         T_Setoid_46
-> T_Setoid_46 -> (Any -> Any) -> (Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Function.Consequences.Setoid.du_inverse'7495''8658'bijective_84
         T_Setoid_46
v0 T_Setoid_46
v1 (T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v2))
         (T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v2))
         (T_Inverse_2122 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_2142 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v2)))
-- Function.Properties.Inverse.Inverse⇒Equivalence
d_Inverse'8658'Equivalence_530 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_Inverse'8658'Equivalence_530 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> T_Equivalence_1858
d_Inverse'8658'Equivalence_530 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_46
v5 T_Inverse_2122
v6
  = T_Inverse_2122 -> T_Equivalence_1858
du_Inverse'8658'Equivalence_530 T_Inverse_2122
v6
du_Inverse'8658'Equivalence_530 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_Inverse'8658'Equivalence_530 :: T_Inverse_2122 -> T_Equivalence_1858
du_Inverse'8658'Equivalence_530 T_Inverse_2122
v0
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Equivalence_1858)
-> Any -> Any -> Any -> Any -> T_Equivalence_1858
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.C_constructor_1940
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_2140 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v0))
-- Function.Properties.Inverse.↔⇒⟶
d_'8596''8658''10230'_620 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d_'8596''8658''10230'_620 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Func_774
d_'8596''8658''10230'_620 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_Func_774
du_'8596''8658''10230'_620
du_'8596''8658''10230'_620 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
du_'8596''8658''10230'_620 :: T_Inverse_2122 -> T_Func_774
du_'8596''8658''10230'_620 = (T_Inverse_2122 -> T_Func_774) -> T_Inverse_2122 -> T_Func_774
forall a b. a -> b
coe T_Inverse_2122 -> T_Func_774
du_toFunction_44
-- Function.Properties.Inverse.↔⇒⟵
d_'8596''8658''10229'_622 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d_'8596''8658''10229'_622 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Func_774
d_'8596''8658''10229'_622 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_Func_774
du_'8596''8658''10229'_622
du_'8596''8658''10229'_622 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
du_'8596''8658''10229'_622 :: T_Inverse_2122 -> T_Func_774
du_'8596''8658''10229'_622 = (T_Inverse_2122 -> T_Func_774) -> T_Inverse_2122 -> T_Func_774
forall a b. a -> b
coe T_Inverse_2122 -> T_Func_774
du_fromFunction_134
-- Function.Properties.Inverse.↔⇒↣
d_'8596''8658''8611'_624 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
d_'8596''8658''8611'_624 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Injection_842
d_'8596''8658''8611'_624 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_Injection_842
du_'8596''8658''8611'_624
du_'8596''8658''8611'_624 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
du_'8596''8658''8611'_624 :: T_Inverse_2122 -> T_Injection_842
du_'8596''8658''8611'_624
  = (T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Injection_842)
-> Any -> Any -> T_Inverse_2122 -> T_Injection_842
forall a b. a -> b
coe
      T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Injection_842
du_Inverse'8658'Injection_224
      (T_Setoid_46 -> Any
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Setoid_46 -> Any
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
-- Function.Properties.Inverse.↔⇒↠
d_'8596''8658''8608'_626 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d_'8596''8658''8608'_626 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Surjection_918
d_'8596''8658''8608'_626 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_Surjection_918
du_'8596''8658''8608'_626
du_'8596''8658''8608'_626 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du_'8596''8658''8608'_626 :: T_Inverse_2122 -> T_Surjection_918
du_'8596''8658''8608'_626 = (T_Inverse_2122 -> T_Surjection_918)
-> T_Inverse_2122 -> T_Surjection_918
forall a b. a -> b
coe T_Inverse_2122 -> T_Surjection_918
du_Inverse'8658'Surjection_326
-- Function.Properties.Inverse.↔⇒⤖
d_'8596''8658''10518'_628 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_'8596''8658''10518'_628 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Bijection_1004
d_'8596''8658''10518'_628 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_Bijection_1004
du_'8596''8658''10518'_628
du_'8596''8658''10518'_628 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_'8596''8658''10518'_628 :: T_Inverse_2122 -> T_Bijection_1004
du_'8596''8658''10518'_628
  = (T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Bijection_1004)
-> Any -> Any -> T_Inverse_2122 -> T_Bijection_1004
forall a b. a -> b
coe
      T_Setoid_46 -> T_Setoid_46 -> T_Inverse_2122 -> T_Bijection_1004
du_Inverse'8658'Bijection_428
      (T_Setoid_46 -> Any
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Setoid_46 -> Any
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
-- Function.Properties.Inverse.↔⇒⇔
d_'8596''8658''8660'_630 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_'8596''8658''8660'_630 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Equivalence_1858
d_'8596''8658''8660'_630 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_Equivalence_1858
du_'8596''8658''8660'_630
du_'8596''8658''8660'_630 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'8596''8658''8660'_630 :: T_Inverse_2122 -> T_Equivalence_1858
du_'8596''8658''8660'_630 = (T_Inverse_2122 -> T_Equivalence_1858)
-> T_Inverse_2122 -> T_Equivalence_1858
forall a b. a -> b
coe T_Inverse_2122 -> T_Equivalence_1858
du_Inverse'8658'Equivalence_530
-- Function.Properties.Inverse.↔⇒↩
d_'8596''8658''8617'_632 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_'8596''8658''8617'_632 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_LeftInverse_1942
d_'8596''8658''8617'_632 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_LeftInverse_1942
du_'8596''8658''8617'_632
du_'8596''8658''8617'_632 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_'8596''8658''8617'_632 :: T_Inverse_2122 -> T_LeftInverse_1942
du_'8596''8658''8617'_632
  = (T_Inverse_2122 -> T_LeftInverse_1942)
-> T_Inverse_2122 -> T_LeftInverse_1942
forall a b. a -> b
coe T_Inverse_2122 -> T_LeftInverse_1942
MAlonzo.Code.Function.Bundles.du_leftInverse_2148
-- Function.Properties.Inverse.↔⇒↪
d_'8596''8658''8618'_634 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_'8596''8658''8618'_634 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_RightInverse_2036
d_'8596''8658''8618'_634 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122 -> T_RightInverse_2036
du_'8596''8658''8618'_634
du_'8596''8658''8618'_634 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_'8596''8658''8618'_634 :: T_Inverse_2122 -> T_RightInverse_2036
du_'8596''8658''8618'_634
  = (T_Inverse_2122 -> T_RightInverse_2036)
-> T_Inverse_2122 -> T_RightInverse_2036
forall a b. a -> b
coe T_Inverse_2122 -> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.du_rightInverse_2150
-- Function.Properties.Inverse.transportVia
d_transportVia_676 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  (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_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 -> ()) ->
  (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_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
   AgdaAny -> AgdaAny -> AgdaAny) ->
  (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_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
   MAlonzo.Code.Function.Bundles.T_Inverse_2122 -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_2122 -> AgdaAny
d_transportVia_676 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Level_18)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Setoid_46
    -> Any
    -> Any
    -> Any)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Inverse_2122
    -> Any)
-> T_Inverse_2122
-> Any
-> T_Inverse_2122
-> Any
d_transportVia_676 T_Level_18
v0 T_Level_18
v1 T_Setoid_46
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_46
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_46
v8 T_Level_18
v9 T_Level_18
v10 T_Setoid_46
v11 ~T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Level_18
v12 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
v13
                   T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
v14 T_Inverse_2122
v15 Any
v16 T_Inverse_2122
v17
  = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Setoid_46
    -> Any
    -> Any
    -> Any)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Inverse_2122
    -> Any)
-> T_Inverse_2122
-> Any
-> T_Inverse_2122
-> Any
du_transportVia_676
      T_Level_18
v0 T_Level_18
v1 T_Setoid_46
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_46
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_46
v8 T_Level_18
v9 T_Level_18
v10 T_Setoid_46
v11 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
v13 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
v14 T_Inverse_2122
v15 Any
v16 T_Inverse_2122
v17
du_transportVia_676 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  (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_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
   AgdaAny -> AgdaAny -> AgdaAny) ->
  (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_46 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
   MAlonzo.Code.Function.Bundles.T_Inverse_2122 -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_2122 -> AgdaAny
du_transportVia_676 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Setoid_46
    -> Any
    -> Any
    -> Any)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_46
    -> T_Setoid_46
    -> T_Inverse_2122
    -> Any)
-> T_Inverse_2122
-> Any
-> T_Inverse_2122
-> Any
du_transportVia_676 T_Level_18
v0 T_Level_18
v1 T_Setoid_46
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_46
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_46
v8 T_Level_18
v9 T_Level_18
v10 T_Setoid_46
v11 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
v12 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
v13
                    T_Inverse_2122
v14 Any
v15 T_Inverse_2122
v16
  = (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_46
 -> T_Setoid_46
 -> T_Setoid_46
 -> Any
 -> Any
 -> Any)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
forall a b. a -> b
coe
      T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
v12 T_Level_18
v0 T_Level_18
v3 T_Level_18
v9 T_Level_18
v1 T_Level_18
v4 T_Level_18
v10 T_Setoid_46
v2 T_Setoid_46
v5 T_Setoid_46
v11 ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_46
 -> T_Setoid_46
 -> T_Inverse_2122
 -> Any)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
v13 T_Level_18
v0 T_Level_18
v3 T_Level_18
v1 T_Level_18
v4 T_Setoid_46
v2 T_Setoid_46
v5 T_Inverse_2122
v14)
      ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_46
 -> T_Setoid_46
 -> T_Setoid_46
 -> Any
 -> Any
 -> Any)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
forall a b. a -> b
coe
         T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> Any
-> Any
-> Any
v12 T_Level_18
v3 T_Level_18
v6 T_Level_18
v9 T_Level_18
v4 T_Level_18
v7 T_Level_18
v10 T_Setoid_46
v5 T_Setoid_46
v8 T_Setoid_46
v11 Any
v15
         ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_46
 -> T_Setoid_46
 -> T_Inverse_2122
 -> Any)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> Any
v13 T_Level_18
v6 T_Level_18
v9 T_Level_18
v7 T_Level_18
v10 T_Setoid_46
v8 T_Setoid_46
v11 T_Inverse_2122
v16))
-- Function.Properties.Inverse._.↔-fun
d_'8596''45'fun_698 ::
  (MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   () ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  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.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8596''45'fun_698 :: (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> (Any -> T_Level_18)
 -> (Any -> Any)
 -> (Any -> Any)
 -> (Any -> T__'8801'__12)
 -> T__'8801'__12)
-> 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_2122
-> T_Inverse_2122
-> T_Inverse_2122
d_'8596''45'fun_698 ~T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
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_Level_18
v8 T_Inverse_2122
v9 T_Inverse_2122
v10
  = T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'fun_698 T_Inverse_2122
v9 T_Inverse_2122
v10
du_'8596''45'fun_698 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8596''45'fun_698 :: T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'fun_698 T_Inverse_2122
v0 T_Inverse_2122
v1
  = ((Any -> Any) -> (Any -> Any) -> T_Inverse_2122)
-> Any -> Any -> T_Inverse_2122
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 ->
            (T_Inverse_2122 -> Any -> Any) -> T_Inverse_2122 -> Any -> Any
forall a b. a -> b
coe
              T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 T_Inverse_2122
v1
              (Any -> Any -> Any
forall a b. a -> b
coe Any
v2 ((T_Inverse_2122 -> Any -> Any) -> T_Inverse_2122 -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 T_Inverse_2122
v0 Any
v3))))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 ->
            (T_Inverse_2122 -> Any -> Any) -> T_Inverse_2122 -> Any -> Any
forall a b. a -> b
coe
              T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_2136 T_Inverse_2122
v1
              (Any -> Any -> Any
forall a b. a -> b
coe Any
v2 ((T_Inverse_2122 -> Any -> Any) -> T_Inverse_2122 -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_2134 T_Inverse_2122
v0 Any
v3))))
-- Function.Properties.Inverse._._.Eq₁._≈_
d__'8776'__766 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__766 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> Any
-> Any
-> T_Level_18
d__'8776'__766 = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Function.Properties.Inverse._._.Eq₂._≈_
d__'8776'__792 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__792 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> Any
-> Any
-> T_Level_18
d__'8776'__792 = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Function.Properties.Inverse._.to-from
d_to'45'from_820 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_820 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Inverse_2122
-> Any
-> Any
-> Any
-> Any
d_to'45'from_820 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Setoid_46
v5 T_Inverse_2122
v6 Any
v7 Any
v8
  = T_Setoid_46
-> T_Setoid_46 -> T_Inverse_2122 -> Any -> Any -> Any -> Any
du_to'45'from_820 T_Setoid_46
v2 T_Setoid_46
v5 T_Inverse_2122
v6 Any
v7 Any
v8
du_to'45'from_820 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_820 :: T_Setoid_46
-> T_Setoid_46 -> T_Inverse_2122 -> Any -> Any -> Any -> Any
du_to'45'from_820 T_Setoid_46
v0 T_Setoid_46
v1 T_Inverse_2122
v2 Any
v3 Any
v4
  = (T_Setoid_46
 -> T_Setoid_46 -> T_RightInverse_2036 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Setoid_46
-> T_Setoid_46 -> T_RightInverse_2036 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Properties.RightInverse.du_to'45'from_510
      (T_Setoid_46 -> Any
forall a b. a -> b
coe T_Setoid_46
v0) (T_Setoid_46 -> Any
forall a b. a -> b
coe T_Setoid_46
v1)
      ((T_Inverse_2122 -> T_RightInverse_2036) -> Any -> Any
forall a b. a -> b
coe T_Inverse_2122 -> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.du_rightInverse_2150 (T_Inverse_2122 -> Any
forall a b. a -> b
coe T_Inverse_2122
v2))
      (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v4)