{-# 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_26
d_isEquivalence_32 :: T_Level_18 -> T_Level_18 -> T_IsEquivalence_26
d_isEquivalence_32 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsEquivalence_26
du_isEquivalence_32
du_isEquivalence_32 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_32 :: T_IsEquivalence_26
du_isEquivalence_32
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_26)
-> Any
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 ->
            T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
MAlonzo.Code.Function.Construct.Identity.du_inverse_796))
      (\ Any
v0 Any
v1 Any
v2 ->
         (T_Inverse_1960 -> T_Inverse_1960) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Symmetry.du_inverse_1052 Any
v2)
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 ->
         (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> Any -> Any -> Any
forall a b. a -> b
coe
           T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Composition.du_inverse_2210 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_1960
d_'8596''45'refl_36 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'8596''45'refl_36 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_1960
du_'8596''45'refl_36
du_'8596''45'refl_36 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8596''45'refl_36 :: T_Inverse_1960
du_'8596''45'refl_36
  = T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
MAlonzo.Code.Function.Construct.Identity.du_'8596''45'id_820
-- 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_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'8596''45'sym_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Inverse_1960
d_'8596''45'sym_38 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'sym_38
du_'8596''45'sym_38 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8596''45'sym_38 :: T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'sym_38
  = (T_Inverse_1960 -> T_Inverse_1960)
-> T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe
      T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Symmetry.du_'8596''45'sym_1148
-- 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_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
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_1960
-> T_Inverse_1960
-> T_Inverse_1960
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_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'trans_40
du_'8596''45'trans_40 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8596''45'trans_40 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'trans_40
  = (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Composition.du_inverse_2210
-- Function.Properties.Inverse.↔-isEquivalence
d_'8596''45'isEquivalence_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8596''45'isEquivalence_42 :: T_Level_18 -> T_IsEquivalence_26
d_'8596''45'isEquivalence_42 ~T_Level_18
v0 = T_IsEquivalence_26
du_'8596''45'isEquivalence_42
du_'8596''45'isEquivalence_42 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'8596''45'isEquivalence_42 :: T_IsEquivalence_26
du_'8596''45'isEquivalence_42
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_26)
-> (Any -> Any) -> Any -> Any -> T_IsEquivalence_26
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
      (\ Any
v0 -> T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
du_'8596''45'refl_36)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_Inverse_1960 -> T_Inverse_1960) -> Any
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'sym_38))
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960) -> Any
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
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_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_toFunction_44 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Func_714
d_toFunction_44 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 T_Inverse_1960
v6 = T_Inverse_1960 -> T_Func_714
du_toFunction_44 T_Inverse_1960
v6
du_toFunction_44 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_toFunction_44 :: T_Inverse_1960 -> T_Func_714
du_toFunction_44 T_Inverse_1960
v0
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714)
-> Any -> Any -> T_Func_714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Function.Properties.Inverse.fromFunction
d_fromFunction_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_fromFunction_130 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Func_714
d_fromFunction_130 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 T_Inverse_1960
v6
  = T_Inverse_1960 -> T_Func_714
du_fromFunction_130 T_Inverse_1960
v6
du_fromFunction_130 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_fromFunction_130 :: T_Inverse_1960 -> T_Func_714
du_fromFunction_130 T_Inverse_1960
v0
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714)
-> Any -> Any -> T_Func_714
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Function.Properties.Inverse.Inverse⇒Injection
d_Inverse'8658'Injection_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d_Inverse'8658'Injection_216 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Injection_776
d_Inverse'8658'Injection_216 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Setoid_44
v5 T_Inverse_1960
v6
  = T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776
du_Inverse'8658'Injection_216 T_Setoid_44
v2 T_Setoid_44
v5 T_Inverse_1960
v6
du_Inverse'8658'Injection_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du_Inverse'8658'Injection_216 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776
du_Inverse'8658'Injection_216 T_Setoid_44
v0 T_Setoid_44
v1 T_Inverse_1960
v2
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Injection_776)
-> Any -> Any -> Any -> T_Injection_776
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Injection_776
MAlonzo.Code.Function.Bundles.C_Injection'46'constructor_8675
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v2))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v2))
      ((T_Setoid_44
 -> T_Setoid_44
 -> (Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any)
-> T_Setoid_44
-> T_Setoid_44
-> (Any -> Any)
-> (Any -> Any)
-> Any
-> Any
forall a b. a -> b
coe
         T_Setoid_44
-> T_Setoid_44
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Function.Consequences.Setoid.du_inverse'691''8658'injective_76
         T_Setoid_44
v0 T_Setoid_44
v1 (T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v2))
         (T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v2))
         ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'691'_1984 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v2)))
-- Function.Properties.Inverse.Inverse⇒Surjection
d_Inverse'8658'Surjection_328 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_Inverse'8658'Surjection_328 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Surjection_846
d_Inverse'8658'Surjection_328 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 T_Inverse_1960
v6
  = T_Inverse_1960 -> T_Surjection_846
du_Inverse'8658'Surjection_328 T_Inverse_1960
v6
du_Inverse'8658'Surjection_328 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_Inverse'8658'Surjection_328 :: T_Inverse_1960 -> T_Surjection_846
du_Inverse'8658'Surjection_328 T_Inverse_1960
v0
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> T_Σ_14)
 -> T_Surjection_846)
-> Any -> Any -> Any -> T_Surjection_846
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> T_Σ_14)
-> T_Surjection_846
MAlonzo.Code.Function.Bundles.C_Surjection'46'constructor_11197
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
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_72
         (T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_inverse'737'_1982 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0)))
-- Function.Properties.Inverse.Inverse⇒Bijection
d_Inverse'8658'Bijection_440 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_Inverse'8658'Bijection_440 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Bijection_926
d_Inverse'8658'Bijection_440 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Setoid_44
v5 T_Inverse_1960
v6
  = T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926
du_Inverse'8658'Bijection_440 T_Setoid_44
v2 T_Setoid_44
v5 T_Inverse_1960
v6
du_Inverse'8658'Bijection_440 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_Inverse'8658'Bijection_440 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926
du_Inverse'8658'Bijection_440 T_Setoid_44
v0 T_Setoid_44
v1 T_Inverse_1960
v2
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Bijection_926)
-> Any -> Any -> Any -> T_Bijection_926
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Bijection_926
MAlonzo.Code.Function.Bundles.C_Bijection'46'constructor_15277
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v2))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v2))
      ((T_Setoid_44
 -> T_Setoid_44 -> (Any -> Any) -> (Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> T_Setoid_44
-> T_Setoid_44
-> (Any -> Any)
-> (Any -> Any)
-> T_Σ_14
-> Any
forall a b. a -> b
coe
         T_Setoid_44
-> T_Setoid_44 -> (Any -> Any) -> (Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Function.Consequences.Setoid.du_inverse'7495''8658'bijective_80
         T_Setoid_44
v0 T_Setoid_44
v1 (T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v2))
         (T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v2))
         (T_Inverse_1960 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_1980 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v2)))
-- Function.Properties.Inverse.Inverse⇒Equivalence
d_Inverse'8658'Equivalence_552 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_Inverse'8658'Equivalence_552 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> T_Equivalence_1714
d_Inverse'8658'Equivalence_552 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Setoid_44
v5 T_Inverse_1960
v6
  = T_Inverse_1960 -> T_Equivalence_1714
du_Inverse'8658'Equivalence_552 T_Inverse_1960
v6
du_Inverse'8658'Equivalence_552 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_Inverse'8658'Equivalence_552 :: T_Inverse_1960 -> T_Equivalence_1714
du_Inverse'8658'Equivalence_552 T_Inverse_1960
v0
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Equivalence_1714)
-> Any -> Any -> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.C_Equivalence'46'constructor_25797
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Function.Properties.Inverse.↔⇒⟶
d_'8596''8658''10230'_638 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_'8596''8658''10230'_638 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Func_714
d_'8596''8658''10230'_638 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_Func_714
du_'8596''8658''10230'_638
du_'8596''8658''10230'_638 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_'8596''8658''10230'_638 :: T_Inverse_1960 -> T_Func_714
du_'8596''8658''10230'_638 = (T_Inverse_1960 -> T_Func_714) -> T_Inverse_1960 -> T_Func_714
forall a b. a -> b
coe T_Inverse_1960 -> T_Func_714
du_toFunction_44
-- Function.Properties.Inverse.↔⇒⟵
d_'8596''8658''10229'_640 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_'8596''8658''10229'_640 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Func_714
d_'8596''8658''10229'_640 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_Func_714
du_'8596''8658''10229'_640
du_'8596''8658''10229'_640 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_'8596''8658''10229'_640 :: T_Inverse_1960 -> T_Func_714
du_'8596''8658''10229'_640 = (T_Inverse_1960 -> T_Func_714) -> T_Inverse_1960 -> T_Func_714
forall a b. a -> b
coe T_Inverse_1960 -> T_Func_714
du_fromFunction_130
-- Function.Properties.Inverse.↔⇒↣
d_'8596''8658''8611'_642 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d_'8596''8658''8611'_642 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Injection_776
d_'8596''8658''8611'_642 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_Injection_776
du_'8596''8658''8611'_642
du_'8596''8658''8611'_642 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du_'8596''8658''8611'_642 :: T_Inverse_1960 -> T_Injection_776
du_'8596''8658''8611'_642
  = (T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776)
-> Any -> Any -> T_Inverse_1960 -> T_Injection_776
forall a b. a -> b
coe
      T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776
du_Inverse'8658'Injection_216
      (T_Setoid_44 -> Any
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Setoid_44 -> Any
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
-- Function.Properties.Inverse.↔⇒↠
d_'8596''8658''8608'_644 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_'8596''8658''8608'_644 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Surjection_846
d_'8596''8658''8608'_644 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_Surjection_846
du_'8596''8658''8608'_644
du_'8596''8658''8608'_644 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_'8596''8658''8608'_644 :: T_Inverse_1960 -> T_Surjection_846
du_'8596''8658''8608'_644 = (T_Inverse_1960 -> T_Surjection_846)
-> T_Inverse_1960 -> T_Surjection_846
forall a b. a -> b
coe T_Inverse_1960 -> T_Surjection_846
du_Inverse'8658'Surjection_328
-- Function.Properties.Inverse.↔⇒⤖
d_'8596''8658''10518'_646 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_'8596''8658''10518'_646 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Bijection_926
d_'8596''8658''10518'_646 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_Bijection_926
du_'8596''8658''10518'_646
du_'8596''8658''10518'_646 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_'8596''8658''10518'_646 :: T_Inverse_1960 -> T_Bijection_926
du_'8596''8658''10518'_646
  = (T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926)
-> Any -> Any -> T_Inverse_1960 -> T_Bijection_926
forall a b. a -> b
coe
      T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926
du_Inverse'8658'Bijection_440
      (T_Setoid_44 -> Any
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Setoid_44 -> Any
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
-- Function.Properties.Inverse.↔⇒⇔
d_'8596''8658''8660'_648 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8596''8658''8660'_648 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Equivalence_1714
d_'8596''8658''8660'_648 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_Equivalence_1714
du_'8596''8658''8660'_648
du_'8596''8658''8660'_648 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8596''8658''8660'_648 :: T_Inverse_1960 -> T_Equivalence_1714
du_'8596''8658''8660'_648 = (T_Inverse_1960 -> T_Equivalence_1714)
-> T_Inverse_1960 -> T_Equivalence_1714
forall a b. a -> b
coe T_Inverse_1960 -> T_Equivalence_1714
du_Inverse'8658'Equivalence_552
-- Function.Properties.Inverse.↔⇒↩
d_'8596''8658''8617'_650 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_'8596''8658''8617'_650 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_LeftInverse_1792
d_'8596''8658''8617'_650 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_LeftInverse_1792
du_'8596''8658''8617'_650
du_'8596''8658''8617'_650 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_'8596''8658''8617'_650 :: T_Inverse_1960 -> T_LeftInverse_1792
du_'8596''8658''8617'_650
  = (T_Inverse_1960 -> T_LeftInverse_1792)
-> T_Inverse_1960 -> T_LeftInverse_1792
forall a b. a -> b
coe T_Inverse_1960 -> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.du_leftInverse_1986
-- Function.Properties.Inverse.↔⇒↪
d_'8596''8658''8618'_652 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_'8596''8658''8618'_652 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_RightInverse_1880
d_'8596''8658''8618'_652 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960 -> T_RightInverse_1880
du_'8596''8658''8618'_652
du_'8596''8658''8618'_652 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_'8596''8658''8618'_652 :: T_Inverse_1960 -> T_RightInverse_1880
du_'8596''8658''8618'_652
  = (T_Inverse_1960 -> T_RightInverse_1880)
-> T_Inverse_1960 -> T_RightInverse_1880
forall a b. a -> b
coe T_Inverse_1960 -> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.du_rightInverse_1988
-- Function.Properties.Inverse.transportVia
d_transportVia_694 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> ()) ->
  (MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.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 ->
   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_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
d_transportVia_694 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Level_18)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Setoid_44
    -> Any
    -> Any
    -> Any)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> Any)
-> T_Inverse_1960
-> Any
-> T_Inverse_1960
-> Any
d_transportVia_694 T_Level_18
v0 T_Level_18
v1 T_Setoid_44
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_44
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_44
v8 T_Level_18
v9 T_Level_18
v10 T_Setoid_44
v11 ~T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Level_18
v12 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
-> Any
-> Any
-> Any
v13
                   T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
v14 T_Inverse_1960
v15 Any
v16 T_Inverse_1960
v17
  = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (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
    -> Any
    -> Any
    -> Any)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> Any)
-> T_Inverse_1960
-> Any
-> T_Inverse_1960
-> Any
du_transportVia_694
      T_Level_18
v0 T_Level_18
v1 T_Setoid_44
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_44
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_44
v8 T_Level_18
v9 T_Level_18
v10 T_Setoid_44
v11 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
-> Any
-> Any
-> Any
v13 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
v14 T_Inverse_1960
v15 Any
v16 T_Inverse_1960
v17
du_transportVia_694 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (MAlonzo.Code.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 ->
   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_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
du_transportVia_694 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (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
    -> Any
    -> Any
    -> Any)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> Any)
-> T_Inverse_1960
-> Any
-> T_Inverse_1960
-> Any
du_transportVia_694 T_Level_18
v0 T_Level_18
v1 T_Setoid_44
v2 T_Level_18
v3 T_Level_18
v4 T_Setoid_44
v5 T_Level_18
v6 T_Level_18
v7 T_Setoid_44
v8 T_Level_18
v9 T_Level_18
v10 T_Setoid_44
v11 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
-> Any
-> Any
-> Any
v12 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
v13
                    T_Inverse_1960
v14 Any
v15 T_Inverse_1960
v16
  = (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
 -> Any
 -> Any
 -> Any)
-> 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
-> 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_44
-> T_Setoid_44
-> T_Setoid_44
-> 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_44
v2 T_Setoid_44
v5 T_Setoid_44
v11 ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Inverse_1960
 -> Any)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
v13 T_Level_18
v0 T_Level_18
v3 T_Level_18
v1 T_Level_18
v4 T_Setoid_44
v2 T_Setoid_44
v5 T_Inverse_1960
v14)
      ((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
 -> Any
 -> Any
 -> Any)
-> 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
-> 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_44
-> T_Setoid_44
-> T_Setoid_44
-> 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_44
v5 T_Setoid_44
v8 T_Setoid_44
v11 Any
v15
         ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Inverse_1960
 -> Any)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> Any
v13 T_Level_18
v6 T_Level_18
v9 T_Level_18
v7 T_Level_18
v10 T_Setoid_44
v8 T_Setoid_44
v11 T_Inverse_1960
v16))
-- Function.Properties.Inverse._.↔-fun
d_'8596''45'fun_716 ::
  (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_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'8596''45'fun_716 :: (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_1960
-> T_Inverse_1960
-> T_Inverse_1960
d_'8596''45'fun_716 ~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_1960
v9 T_Inverse_1960
v10
  = T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'fun_716 T_Inverse_1960
v9 T_Inverse_1960
v10
du_'8596''45'fun_716 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8596''45'fun_716 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'fun_716 T_Inverse_1960
v0 T_Inverse_1960
v1
  = ((Any -> Any) -> (Any -> Any) -> T_Inverse_1960)
-> Any -> Any -> T_Inverse_1960
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 ->
            (T_Inverse_1960 -> Any -> Any) -> T_Inverse_1960 -> Any -> Any
forall a b. a -> b
coe
              T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v1
              (Any -> Any -> Any
forall a b. a -> b
coe Any
v2 ((T_Inverse_1960 -> Any -> Any) -> T_Inverse_1960 -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v0 Any
v3))))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 Any
v3 ->
            (T_Inverse_1960 -> Any -> Any) -> T_Inverse_1960 -> Any -> Any
forall a b. a -> b
coe
              T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v1
              (Any -> Any -> Any
forall a b. a -> b
coe Any
v2 ((T_Inverse_1960 -> Any -> Any) -> T_Inverse_1960 -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v0 Any
v3))))
-- Function.Properties.Inverse._._.Eq₁._≈_
d__'8776'__784 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__784 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> Any
-> Any
-> T_Level_18
d__'8776'__784 = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Function.Properties.Inverse._._.Eq₂._≈_
d__'8776'__808 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__808 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> Any
-> Any
-> T_Level_18
d__'8776'__808 = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Function.Properties.Inverse._.to-from
d_to'45'from_834 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_834 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Inverse_1960
-> Any
-> Any
-> Any
-> Any
d_to'45'from_834 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Setoid_44
v5 T_Inverse_1960
v6 Any
v7 Any
v8
  = T_Setoid_44
-> T_Setoid_44 -> T_Inverse_1960 -> Any -> Any -> Any -> Any
du_to'45'from_834 T_Setoid_44
v2 T_Setoid_44
v5 T_Inverse_1960
v6 Any
v7 Any
v8
du_to'45'from_834 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_834 :: T_Setoid_44
-> T_Setoid_44 -> T_Inverse_1960 -> Any -> Any -> Any -> Any
du_to'45'from_834 T_Setoid_44
v0 T_Setoid_44
v1 T_Inverse_1960
v2 Any
v3 Any
v4
  = (T_Setoid_44
 -> T_Setoid_44 -> T_RightInverse_1880 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Setoid_44
-> T_Setoid_44 -> T_RightInverse_1880 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Properties.RightInverse.du_to'45'from_486
      (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_1960 -> T_RightInverse_1880) -> Any -> Any
forall a b. a -> b
coe T_Inverse_1960 -> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.du_rightInverse_1988 (T_Inverse_1960 -> Any
forall a b. a -> b
coe T_Inverse_1960
v2))
      (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v4)