{-# 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.Bijection where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Bundles
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.Inverse
import qualified MAlonzo.Code.Function.Properties.Surjection
import qualified MAlonzo.Code.Function.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Properties.Bijection.refl
d_refl_28 ::
  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_Bijection_926
d_refl_28 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Bijection_926
d_refl_28 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Bijection_926
du_refl_28
du_refl_28 :: MAlonzo.Code.Function.Bundles.T_Bijection_926
du_refl_28 :: T_Bijection_926
du_refl_28
  = T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926
MAlonzo.Code.Function.Construct.Identity.du_bijection_788
-- Function.Properties.Bijection.sym-≡
d_sym'45''8801'_30 ::
  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.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_sym'45''8801'_30 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Bijection_926
d_sym'45''8801'_30 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 = T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926
du_sym'45''8801'_30 T_Setoid_44
v2
du_sym'45''8801'_30 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_sym'45''8801'_30 :: T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926
du_sym'45''8801'_30 T_Setoid_44
v0
  = (T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926)
-> Any -> T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe
      T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926
MAlonzo.Code.Function.Construct.Symmetry.du_bijection'45''8801'_722
      (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v0)
-- Function.Properties.Bijection.trans
d_trans_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_trans_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
d_trans_32 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 ~T_Setoid_44
v8 = T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du_trans_32
du_trans_32 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_trans_32 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du_trans_32
  = (T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926)
-> T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
MAlonzo.Code.Function.Construct.Composition.du_bijection_1606
-- Function.Properties.Bijection.⤖-isEquivalence
d_'10518''45'isEquivalence_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'10518''45'isEquivalence_34 :: T_Level_18 -> T_IsEquivalence_26
d_'10518''45'isEquivalence_34 ~T_Level_18
v0 = T_IsEquivalence_26
du_'10518''45'isEquivalence_34
du_'10518''45'isEquivalence_34 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'10518''45'isEquivalence_34 :: T_IsEquivalence_26
du_'10518''45'isEquivalence_34
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_26)
-> 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_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
du_refl_28))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 Any
v1 ->
            (T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926) -> Any -> Any
forall a b. a -> b
coe
              T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926
du_sym'45''8801'_30
              (T_Setoid_44 -> Any
forall a b. a -> b
coe
                 T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)))
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> (T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926) -> Any
forall a b. a -> b
coe T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du_trans_32))
-- Function.Properties.Bijection.Bijection⇒Inverse
d_Bijection'8658'Inverse_36 ::
  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_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_Bijection'8658'Inverse_36 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Bijection_926
-> T_Inverse_1960
d_Bijection'8658'Inverse_36 ~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_Bijection_926
v6
  = T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960
du_Bijection'8658'Inverse_36 T_Setoid_44
v2 T_Setoid_44
v5 T_Bijection_926
v6
du_Bijection'8658'Inverse_36 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Bijection'8658'Inverse_36 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960
du_Bijection'8658'Inverse_36 T_Setoid_44
v0 T_Setoid_44
v1 T_Bijection_926
v2
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> T_Inverse_1960)
-> Any -> Any -> Any -> Any -> Any -> T_Inverse_1960
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      ((T_Bijection_926 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2))
      ((T_Surjection_846 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_Surjection_846 -> Any -> Any
MAlonzo.Code.Function.Bundles.du_to'8315'_920
         ((T_Bijection_926 -> T_Surjection_846) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2)))
      ((T_Bijection_926 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_936 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2))
      ((T_Setoid_44
 -> T_Setoid_44
 -> T_Surjection_846
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         T_Setoid_44
-> T_Setoid_44
-> T_Surjection_846
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Function.Properties.Surjection.du_injective'8658'to'8315''45'cong_382
         (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_Bijection_926 -> T_Surjection_846) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2))
         ((T_Bijection_926 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_injective_940 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2)))
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
         ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v3 Any
v4 Any
v5 ->
               let v6 :: t
v6
                     = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> Any -> Any -> Any -> t
forall a b. a -> b
coe
                         T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238
MAlonzo.Code.Function.Bundles.du_isBijection_960 (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_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) in
               Any -> Any
forall a b. a -> b
coe
                 (let v7 :: T_IsInjection_92
v7
                        = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (Any -> T_IsBijection_238
forall a b. a -> b
coe Any
forall {t}. t
v6) in
                  Any -> Any
forall a b. a -> b
coe
                    (let v8 :: T_IsCongruent_22
v8
                           = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v7) in
                     Any -> Any
forall a b. a -> b
coe
                       (let v9 :: t
v9
                              = (T_IsCongruent_22 -> T_Setoid_44) -> Any -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> Any
forall a b. a -> b
coe T_IsCongruent_22
v8) in
                        Any -> Any
forall a b. a -> b
coe
                          ((T_IsEquivalence_26 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                             T_IsEquivalence_26 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                             (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (Any -> T_Setoid_44
forall a b. a -> b
coe Any
forall {t}. t
v9))
                             ((T_Bijection_926 -> Any -> Any) -> T_Bijection_926 -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 T_Bijection_926
v2 Any
v4)
                             ((T_Bijection_926 -> Any -> Any) -> T_Bijection_926 -> Any -> Any
forall a b. a -> b
coe
                                T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 T_Bijection_926
v2
                                ((T_Surjection_846 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                   T_Surjection_846 -> Any -> Any
MAlonzo.Code.Function.Bundles.du_to'8315'_920
                                   ((T_Bijection_926 -> T_Surjection_846) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2))
                                   (Any -> Any
forall a b. a -> b
coe Any
v3)))
                             Any
v3
                             ((T_Bijection_926 -> Any -> Any -> Any -> Any)
-> T_Bijection_926 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_936 T_Bijection_926
v2 Any
v4
                                ((T_Surjection_846 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                   T_Surjection_846 -> Any -> Any
MAlonzo.Code.Function.Bundles.du_to'8315'_920
                                   ((T_Bijection_926 -> T_Surjection_846) -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2))
                                   (Any -> Any
forall a b. a -> b
coe Any
v3))
                                Any
v5)
                             ((T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> Any -> Any
du_to'8728'to'8315'_118 (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_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) (Any -> Any
forall a b. a -> b
coe Any
v3))))))))
         ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v3 Any
v4 Any
v5 ->
               (T_Bijection_926 -> Any -> Any -> Any -> Any)
-> T_Bijection_926 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                 T_Bijection_926 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_injective_940 T_Bijection_926
v2
                 (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                    (let v6 :: t
v6
                           = (T_Bijection_926 -> T_Surjection_846) -> Any -> t
forall a b. a -> b
coe T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) in
                     Any -> T_Σ_14
forall a b. a -> b
coe
                       ((T_IsSurjection_162 -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_IsSurjection_162 -> Any -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_230
                          ((T_Setoid_44
 -> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Setoid_44
-> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162
MAlonzo.Code.Function.Bundles.du_isSurjection_914 (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)
                             (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6))
                          (Any -> Any
forall a b. a -> b
coe Any
v4))))
                 Any
v3
                 (let v6 :: t
v6
                        = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> Any -> Any -> Any -> t
forall a b. a -> b
coe
                            T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238
MAlonzo.Code.Function.Bundles.du_isBijection_960 (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_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) in
                  Any -> Any
forall a b. a -> b
coe
                    (let v7 :: T_IsInjection_92
v7
                           = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (Any -> T_IsBijection_238
forall a b. a -> b
coe Any
forall {t}. t
v6) in
                     Any -> Any
forall a b. a -> b
coe
                       (let v8 :: T_IsCongruent_22
v8
                              = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v7) in
                        Any -> Any
forall a b. a -> b
coe
                          (let v9 :: t
v9
                                 = (T_IsCongruent_22 -> T_Setoid_44) -> Any -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> Any
forall a b. a -> b
coe T_IsCongruent_22
v8) in
                           Any -> Any
forall a b. a -> b
coe
                             ((T_IsEquivalence_26 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                T_IsEquivalence_26 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                                (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (Any -> T_Setoid_44
forall a b. a -> b
coe Any
forall {t}. t
v9))
                                ((T_Bijection_926 -> Any -> Any) -> T_Bijection_926 -> Any -> Any
forall a b. a -> b
coe
                                   T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 T_Bijection_926
v2
                                   (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                                      (let v10 :: t
v10
                                             = (T_Bijection_926 -> T_Surjection_846) -> Any -> t
forall a b. a -> b
coe
                                                 T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946
                                                 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) in
                                       Any -> T_Σ_14
forall a b. a -> b
coe
                                         ((T_IsSurjection_162 -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                            T_IsSurjection_162 -> Any -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_230
                                            ((T_Setoid_44
 -> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Setoid_44
-> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162
MAlonzo.Code.Function.Bundles.du_isSurjection_914
                                               (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) (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v10))
                                            (Any -> Any
forall a b. a -> b
coe Any
v4)))))
                                Any
v4 ((T_Bijection_926 -> Any -> Any) -> T_Bijection_926 -> Any -> Any
forall a b. a -> b
coe T_Bijection_926 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_934 T_Bijection_926
v2 Any
v3)
                                ((T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> Any -> Any
du_to'8728'to'8315'_118 (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_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) (Any -> Any
forall a b. a -> b
coe Any
v4))
                                Any
v5))))))))
-- Function.Properties.Bijection._.to∘to⁻
d_to'8728'to'8315'_118 ::
  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_Bijection_926 -> AgdaAny -> AgdaAny
d_to'8728'to'8315'_118 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Bijection_926
-> Any
-> Any
d_to'8728'to'8315'_118 ~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_Bijection_926
v6 Any
v7
  = T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> Any -> Any
du_to'8728'to'8315'_118 T_Setoid_44
v2 T_Setoid_44
v5 T_Bijection_926
v6 Any
v7
du_to'8728'to'8315'_118 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny -> AgdaAny
du_to'8728'to'8315'_118 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> Any -> Any
du_to'8728'to'8315'_118 T_Setoid_44
v0 T_Setoid_44
v1 T_Bijection_926
v2 Any
v3
  = (T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
      T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
      (let v4 :: t
v4
             = (T_Bijection_926 -> T_Surjection_846) -> Any -> t
forall a b. a -> b
coe T_Bijection_926 -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_surjection_946 (T_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2) in
       Any -> Any
forall a b. a -> b
coe
         ((T_IsSurjection_162 -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
            T_IsSurjection_162 -> Any -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_230
            ((T_Setoid_44
 -> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               T_Setoid_44
-> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162
MAlonzo.Code.Function.Bundles.du_isSurjection_914 (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)
               (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v4))
            (Any -> Any
forall a b. a -> b
coe Any
v3)))
-- Function.Properties.Bijection.Bijection⇒Equivalence
d_Bijection'8658'Equivalence_124 ::
  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_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_Bijection'8658'Equivalence_124 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Bijection_926
-> T_Equivalence_1714
d_Bijection'8658'Equivalence_124 ~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_Bijection_926
v6
  = T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Equivalence_1714
du_Bijection'8658'Equivalence_124 T_Setoid_44
v2 T_Setoid_44
v5 T_Bijection_926
v6
du_Bijection'8658'Equivalence_124 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_Bijection'8658'Equivalence_124 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Equivalence_1714
du_Bijection'8658'Equivalence_124 T_Setoid_44
v0 T_Setoid_44
v1 T_Bijection_926
v2
  = (T_Inverse_1960 -> T_Equivalence_1714) -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
      T_Inverse_1960 -> T_Equivalence_1714
MAlonzo.Code.Function.Properties.Inverse.du_Inverse'8658'Equivalence_552
      ((T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960
du_Bijection'8658'Inverse_36 (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_Bijection_926 -> Any
forall a b. a -> b
coe T_Bijection_926
v2))
-- Function.Properties.Bijection.⤖⇒↔
d_'10518''8658''8596'_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'10518''8658''8596'_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Inverse_1960
d_'10518''8658''8596'_126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Bijection_926 -> T_Inverse_1960
du_'10518''8658''8596'_126
du_'10518''8658''8596'_126 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'10518''8658''8596'_126 :: T_Bijection_926 -> T_Inverse_1960
du_'10518''8658''8596'_126
  = (T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960)
-> Any -> Any -> T_Bijection_926 -> T_Inverse_1960
forall a b. a -> b
coe
      T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960
du_Bijection'8658'Inverse_36
      (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.Bijection.⤖⇒⇔
d_'10518''8658''8660'_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'10518''8658''8660'_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Equivalence_1714
d_'10518''8658''8660'_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Bijection_926 -> T_Equivalence_1714
du_'10518''8658''8660'_128
du_'10518''8658''8660'_128 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'10518''8658''8660'_128 :: T_Bijection_926 -> T_Equivalence_1714
du_'10518''8658''8660'_128
  = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_Equivalence_1714)
-> Any -> Any -> T_Bijection_926 -> T_Equivalence_1714
forall a b. a -> b
coe
      T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Equivalence_1714
du_Bijection'8658'Equivalence_124
      (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)