{-# 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_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_refl_28 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Bijection_1004
d_refl_28 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Bijection_1004
du_refl_28
du_refl_28 :: MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_refl_28 :: T_Bijection_1004
du_refl_28
  = T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004
MAlonzo.Code.Function.Construct.Identity.du_bijection_628
-- 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_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_sym'45''8801'_30 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Bijection_1004
d_sym'45''8801'_30 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 ~T_Level_18
v3 ~T_Level_18
v4 = T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004
du_sym'45''8801'_30 T_Setoid_46
v2
du_sym'45''8801'_30 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_sym'45''8801'_30 :: T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004
du_sym'45''8801'_30 T_Setoid_46
v0
  = (T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004)
-> Any -> T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe
      T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004
MAlonzo.Code.Function.Construct.Symmetry.du_bijection'45''8801'_750
      (T_Setoid_46 -> Any
forall a b. a -> b
coe T_Setoid_46
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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_trans_32 :: 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
-> T_Bijection_1004
-> T_Bijection_1004
-> T_Bijection_1004
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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 = T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du_trans_32
du_trans_32 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_trans_32 :: T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du_trans_32
  = (T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004)
-> T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
MAlonzo.Code.Function.Construct.Composition.du_bijection_1686
-- Function.Properties.Bijection.⤖-isEquivalence
d_'10518''45'isEquivalence_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_'10518''45'isEquivalence_34 :: T_Level_18 -> T_IsEquivalence_28
d_'10518''45'isEquivalence_34 ~T_Level_18
v0 = T_IsEquivalence_28
du_'10518''45'isEquivalence_34
du_'10518''45'isEquivalence_34 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_'10518''45'isEquivalence_34 :: T_IsEquivalence_28
du_'10518''45'isEquivalence_34
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_28)
-> 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_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
du_refl_28))
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 Any
v1 ->
            (T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004) -> Any -> Any
forall a b. a -> b
coe
              T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004
du_sym'45''8801'_30
              (T_Setoid_46 -> Any
forall a b. a -> b
coe
                 T_Setoid_46
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_1004 -> T_Bijection_1004 -> T_Bijection_1004) -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
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_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_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Bijection'8658'Inverse_36 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Bijection_1004
-> T_Inverse_2122
d_Bijection'8658'Inverse_36 ~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_Bijection_1004
v6
  = T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> T_Inverse_2122
du_Bijection'8658'Inverse_36 T_Setoid_46
v2 T_Setoid_46
v5 T_Bijection_1004
v6
du_Bijection'8658'Inverse_36 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Bijection'8658'Inverse_36 :: T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> T_Inverse_2122
du_Bijection'8658'Inverse_36 T_Setoid_46
v0 T_Setoid_46
v1 T_Bijection_1004
v2
  = ((Any -> Any)
 -> (Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> T_Inverse_2122)
-> Any -> Any -> Any -> Any -> Any -> T_Inverse_2122
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Inverse_2122
MAlonzo.Code.Function.Bundles.C_constructor_2220
      ((T_Bijection_1004 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1012 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2))
      ((T_Surjection_918 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
         T_Surjection_918 -> Any -> Any
MAlonzo.Code.Function.Bundles.du_to'8315'_996
         ((T_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2)))
      ((T_Bijection_1004 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_1014 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2))
      ((T_Setoid_46
 -> T_Setoid_46
 -> T_Surjection_918
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         T_Setoid_46
-> T_Setoid_46
-> T_Surjection_918
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Function.Properties.Surjection.du_injective'8658'to'8315''45'cong_402
         (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_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2))
         ((T_Bijection_1004 -> Any -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_injective_1018 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
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 ->
               (T_IsEquivalence_28 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_28 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                 T_IsEquivalence_28 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                 (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v1))
                 ((T_Bijection_1004 -> Any -> Any) -> T_Bijection_1004 -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1012 T_Bijection_1004
v2 Any
v4)
                 ((T_Bijection_1004 -> Any -> Any) -> T_Bijection_1004 -> Any -> Any
forall a b. a -> b
coe
                    T_Bijection_1004 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1012 T_Bijection_1004
v2
                    ((T_Surjection_918 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Surjection_918 -> Any -> Any
MAlonzo.Code.Function.Bundles.du_to'8315'_996
                       ((T_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2))
                       (Any -> Any
forall a b. a -> b
coe Any
v3)))
                 Any
v3
                 ((T_Bijection_1004 -> Any -> Any -> Any -> Any)
-> T_Bijection_1004 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Bijection_1004 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_1014 T_Bijection_1004
v2 Any
v4
                    ((T_Surjection_918 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Surjection_918 -> Any -> Any
MAlonzo.Code.Function.Bundles.du_to'8315'_996
                       ((T_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2))
                       (Any -> Any
forall a b. a -> b
coe Any
v3))
                    Any
v5)
                 ((T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> Any -> Any
du_to'8728'to'8315'_122 (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_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
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_1004 -> Any -> Any -> Any -> Any)
-> T_Bijection_1004 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                 T_Bijection_1004 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.du_injective_1018 T_Bijection_1004
v2
                 (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                    ((T_IsSurjection_174 -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
                       T_IsSurjection_174 -> Any -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_246
                       ((T_Setoid_46
 -> T_Setoid_46 -> T_Surjection_918 -> T_IsSurjection_174)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Setoid_46
-> T_Setoid_46 -> T_Surjection_918 -> T_IsSurjection_174
MAlonzo.Code.Function.Bundles.du_isSurjection_990 (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_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2)))
                       (Any -> Any
forall a b. a -> b
coe Any
v4)))
                 Any
v3
                 ((T_IsEquivalence_28 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_28 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_IsEquivalence_28 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                    (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v1))
                    ((T_Bijection_1004 -> Any -> Any) -> T_Bijection_1004 -> Any -> Any
forall a b. a -> b
coe
                       T_Bijection_1004 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1012 T_Bijection_1004
v2
                       (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                          ((T_IsSurjection_174 -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
                             T_IsSurjection_174 -> Any -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_246
                             ((T_Setoid_46
 -> T_Setoid_46 -> T_Surjection_918 -> T_IsSurjection_174)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                T_Setoid_46
-> T_Setoid_46 -> T_Surjection_918 -> T_IsSurjection_174
MAlonzo.Code.Function.Bundles.du_isSurjection_990 (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_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2)))
                             (Any -> Any
forall a b. a -> b
coe Any
v4))))
                    Any
v4 ((T_Bijection_1004 -> Any -> Any) -> T_Bijection_1004 -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1012 T_Bijection_1004
v2 Any
v3)
                    ((T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> Any -> Any
du_to'8728'to'8315'_122 (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_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2) (Any -> Any
forall a b. a -> b
coe Any
v4))
                    Any
v5))))
-- Function.Properties.Bijection._.to∘to⁻
d_to'8728'to'8315'_122 ::
  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_Bijection_1004 ->
  AgdaAny -> AgdaAny
d_to'8728'to'8315'_122 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Bijection_1004
-> Any
-> Any
d_to'8728'to'8315'_122 ~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_Bijection_1004
v6 Any
v7
  = T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> Any -> Any
du_to'8728'to'8315'_122 T_Setoid_46
v2 T_Setoid_46
v5 T_Bijection_1004
v6 Any
v7
du_to'8728'to'8315'_122 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  AgdaAny -> AgdaAny
du_to'8728'to'8315'_122 :: T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> Any -> Any
du_to'8728'to'8315'_122 T_Setoid_46
v0 T_Setoid_46
v1 T_Bijection_1004
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
      ((T_IsSurjection_174 -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         T_IsSurjection_174 -> Any -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_246
         ((T_Setoid_46
 -> T_Setoid_46 -> T_Surjection_918 -> T_IsSurjection_174)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            T_Setoid_46
-> T_Setoid_46 -> T_Surjection_918 -> T_IsSurjection_174
MAlonzo.Code.Function.Bundles.du_isSurjection_990 (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_Bijection_1004 -> T_Surjection_918) -> Any -> Any
forall a b. a -> b
coe T_Bijection_1004 -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_surjection_1024 (T_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2)))
         (Any -> Any
forall a b. a -> b
coe Any
v3))
-- Function.Properties.Bijection.Bijection⇒Equivalence
d_Bijection'8658'Equivalence_128 ::
  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_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_Bijection'8658'Equivalence_128 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Bijection_1004
-> T_Equivalence_1858
d_Bijection'8658'Equivalence_128 ~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_Bijection_1004
v6
  = T_Setoid_46
-> T_Setoid_46 -> T_Bijection_1004 -> T_Equivalence_1858
du_Bijection'8658'Equivalence_128 T_Setoid_46
v2 T_Setoid_46
v5 T_Bijection_1004
v6
du_Bijection'8658'Equivalence_128 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_Bijection'8658'Equivalence_128 :: T_Setoid_46
-> T_Setoid_46 -> T_Bijection_1004 -> T_Equivalence_1858
du_Bijection'8658'Equivalence_128 T_Setoid_46
v0 T_Setoid_46
v1 T_Bijection_1004
v2
  = (T_Inverse_2122 -> T_Equivalence_1858) -> Any -> T_Equivalence_1858
forall a b. a -> b
coe
      T_Inverse_2122 -> T_Equivalence_1858
MAlonzo.Code.Function.Properties.Inverse.du_Inverse'8658'Equivalence_530
      ((T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> T_Inverse_2122)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> T_Inverse_2122
du_Bijection'8658'Inverse_36 (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_Bijection_1004 -> Any
forall a b. a -> b
coe T_Bijection_1004
v2))
-- Function.Properties.Bijection.⤖⇒↔
d_'10518''8658''8596'_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'10518''8658''8596'_130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Inverse_2122
d_'10518''8658''8596'_130 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Bijection_1004 -> T_Inverse_2122
du_'10518''8658''8596'_130
du_'10518''8658''8596'_130 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'10518''8658''8596'_130 :: T_Bijection_1004 -> T_Inverse_2122
du_'10518''8658''8596'_130
  = (T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> T_Inverse_2122)
-> Any -> Any -> T_Bijection_1004 -> T_Inverse_2122
forall a b. a -> b
coe
      T_Setoid_46 -> T_Setoid_46 -> T_Bijection_1004 -> T_Inverse_2122
du_Bijection'8658'Inverse_36
      (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.Bijection.⤖⇒⇔
d_'10518''8658''8660'_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_'10518''8658''8660'_132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Equivalence_1858
d_'10518''8658''8660'_132 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Bijection_1004 -> T_Equivalence_1858
du_'10518''8658''8660'_132
du_'10518''8658''8660'_132 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'10518''8658''8660'_132 :: T_Bijection_1004 -> T_Equivalence_1858
du_'10518''8658''8660'_132
  = (T_Setoid_46
 -> T_Setoid_46 -> T_Bijection_1004 -> T_Equivalence_1858)
-> Any -> Any -> T_Bijection_1004 -> T_Equivalence_1858
forall a b. a -> b
coe
      T_Setoid_46
-> T_Setoid_46 -> T_Bijection_1004 -> T_Equivalence_1858
du_Bijection'8658'Equivalence_128
      (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)