{-# 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.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.Equality
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Function.LeftInverse
import qualified MAlonzo.Code.Function.Surjection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Bijection.Bijective
d_Bijective_18 :: p -> p -> p -> p -> p -> p -> p -> ()
d_Bijective_18 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_Bijective_18
  = C_Bijective'46'constructor_1705 (AgdaAny ->
                                     AgdaAny -> AgdaAny -> AgdaAny)
                                    MAlonzo.Code.Function.Surjection.T_Surjective_18
-- Function.Bijection.Bijective.injective
d_injective_38 ::
  T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 :: T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 T_Bijective_18
v0
  = case T_Bijective_18 -> T_Bijective_18
forall a b. a -> b
coe T_Bijective_18
v0 of
      C_Bijective'46'constructor_1705 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Surjective_18
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
      T_Bijective_18
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Bijection.Bijective.surjective
d_surjective_40 ::
  T_Bijective_18 -> MAlonzo.Code.Function.Surjection.T_Surjective_18
d_surjective_40 :: T_Bijective_18 -> T_Surjective_18
d_surjective_40 T_Bijective_18
v0
  = case T_Bijective_18 -> T_Bijective_18
forall a b. a -> b
coe T_Bijective_18
v0 of
      C_Bijective'46'constructor_1705 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Surjective_18
v2 -> T_Surjective_18 -> T_Surjective_18
forall a b. a -> b
coe T_Surjective_18
v2
      T_Bijective_18
_ -> T_Surjective_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Bijection.Bijective._.from
d_from_44 ::
  T_Bijective_18 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_44 :: T_Bijective_18 -> T_Π_16
d_from_44 T_Bijective_18
v0
  = (T_Surjective_18 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
      T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
      ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 (T_Bijective_18 -> AgdaAny
forall a b. a -> b
coe T_Bijective_18
v0))
-- Function.Bijection.Bijective._.right-inverse-of
d_right'45'inverse'45'of_46 :: T_Bijective_18 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_46 :: T_Bijective_18 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_46 T_Bijective_18
v0
  = (T_Surjective_18 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Surjective_18 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Surjection.d_right'45'inverse'45'of_40
      ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 (T_Bijective_18 -> AgdaAny
forall a b. a -> b
coe T_Bijective_18
v0))
-- Function.Bijection.Bijective.left-inverse-of
d_left'45'inverse'45'of_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Equality.T_Π_16 ->
  T_Bijective_18 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_48 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Bijective_18
-> AgdaAny
-> AgdaAny
d_left'45'inverse'45'of_48 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Π_16
v6 T_Bijective_18
v7 AgdaAny
v8
  = T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_48 T_Π_16
v6 T_Bijective_18
v7 AgdaAny
v8
du_left'45'inverse'45'of_48 ::
  MAlonzo.Code.Function.Equality.T_Π_16 ->
  T_Bijective_18 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_48 :: T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_48 T_Π_16
v0 T_Bijective_18
v1 AgdaAny
v2
  = (T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 T_Bijective_18
v1
      ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
         (T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
            ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> T_Surjective_18
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 (T_Bijective_18 -> AgdaAny
forall a b. a -> b
coe T_Bijective_18
v1)))
         ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 T_Π_16
v0 AgdaAny
v2))
      AgdaAny
v2
      ((T_Surjective_18 -> AgdaAny -> AgdaAny)
-> T_Surjective_18 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Surjective_18 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Surjection.d_right'45'inverse'45'of_40
         (T_Bijective_18 -> T_Surjective_18
d_surjective_40 (T_Bijective_18 -> T_Bijective_18
forall a b. a -> b
coe T_Bijective_18
v1))
         ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 T_Π_16
v0 AgdaAny
v2))
-- Function.Bijection.Bijection
d_Bijection_64 :: p -> p -> p -> p -> p -> p -> ()
d_Bijection_64 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Bijection_64
  = C_Bijection'46'constructor_4749 MAlonzo.Code.Function.Equality.T_Π_16
                                    T_Bijective_18
-- Function.Bijection.Bijection.to
d_to_82 :: T_Bijection_64 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_82 :: T_Bijection_64 -> T_Π_16
d_to_82 T_Bijection_64
v0
  = case T_Bijection_64 -> T_Bijection_64
forall a b. a -> b
coe T_Bijection_64
v0 of
      C_Bijection'46'constructor_4749 T_Π_16
v1 T_Bijective_18
v2 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1
      T_Bijection_64
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Bijection.Bijection.bijective
d_bijective_84 :: T_Bijection_64 -> T_Bijective_18
d_bijective_84 :: T_Bijection_64 -> T_Bijective_18
d_bijective_84 T_Bijection_64
v0
  = case T_Bijection_64 -> T_Bijection_64
forall a b. a -> b
coe T_Bijection_64
v0 of
      C_Bijection'46'constructor_4749 T_Π_16
v1 T_Bijective_18
v2 -> T_Bijective_18 -> T_Bijective_18
forall a b. a -> b
coe T_Bijective_18
v2
      T_Bijection_64
_ -> T_Bijective_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Bijection.Bijection._.from
d_from_88 ::
  T_Bijection_64 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_88 :: T_Bijection_64 -> T_Π_16
d_from_88 T_Bijection_64
v0
  = (T_Surjective_18 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
      T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
      ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0)))
-- Function.Bijection.Bijection._.injective
d_injective_90 ::
  T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_90 :: T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_90 T_Bijection_64
v0
  = (T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
-- Function.Bijection.Bijection._.left-inverse-of
d_left'45'inverse'45'of_92 ::
  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 ->
  T_Bijection_64 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_92 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
d_left'45'inverse'45'of_92 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_64
v6
  = T_Bijection_64 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_92 T_Bijection_64
v6
du_left'45'inverse'45'of_92 :: T_Bijection_64 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_92 :: T_Bijection_64 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_92 T_Bijection_64
v0
  = (T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_48 ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
      ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
-- Function.Bijection.Bijection._.right-inverse-of
d_right'45'inverse'45'of_94 :: T_Bijection_64 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_94 :: T_Bijection_64 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_94 T_Bijection_64
v0
  = (T_Surjective_18 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Surjective_18 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Surjection.d_right'45'inverse'45'of_40
      ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0)))
-- Function.Bijection.Bijection._.surjective
d_surjective_96 ::
  T_Bijection_64 -> MAlonzo.Code.Function.Surjection.T_Surjective_18
d_surjective_96 :: T_Bijection_64 -> T_Surjective_18
d_surjective_96 T_Bijection_64
v0
  = (T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> T_Surjective_18
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
-- Function.Bijection.Bijection.injection
d_injection_98 ::
  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 ->
  T_Bijection_64 -> MAlonzo.Code.Function.Injection.T_Injection_88
d_injection_98 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> T_Injection_88
d_injection_98 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_64
v6 = T_Bijection_64 -> T_Injection_88
du_injection_98 T_Bijection_64
v6
du_injection_98 ::
  T_Bijection_64 -> MAlonzo.Code.Function.Injection.T_Injection_88
du_injection_98 :: T_Bijection_64 -> T_Injection_88
du_injection_98 T_Bijection_64
v0
  = (T_Π_16
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
      T_Π_16
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88
MAlonzo.Code.Function.Injection.C_Injection'46'constructor_3057
      ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
      ((T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0)))
-- Function.Bijection.Bijection.surjection
d_surjection_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Bijection_64 -> MAlonzo.Code.Function.Surjection.T_Surjection_54
d_surjection_100 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> T_Surjection_54
d_surjection_100 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_64
v6 = T_Bijection_64 -> T_Surjection_54
du_surjection_100 T_Bijection_64
v6
du_surjection_100 ::
  T_Bijection_64 -> MAlonzo.Code.Function.Surjection.T_Surjection_54
du_surjection_100 :: T_Bijection_64 -> T_Surjection_54
du_surjection_100 T_Bijection_64
v0
  = (T_Π_16 -> T_Surjective_18 -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> T_Surjection_54
forall a b. a -> b
coe
      T_Π_16 -> T_Surjective_18 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.C_Surjection'46'constructor_2369
      ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
      ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0)))
-- Function.Bijection.Bijection._.equivalence
d_equivalence_104 ::
  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 ->
  T_Bijection_64 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_equivalence_104 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> T_Equivalence_16
d_equivalence_104 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_64
v6
  = T_Bijection_64 -> T_Equivalence_16
du_equivalence_104 T_Bijection_64
v6
du_equivalence_104 ::
  T_Bijection_64 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_equivalence_104 :: T_Bijection_64 -> T_Equivalence_16
du_equivalence_104 T_Bijection_64
v0
  = (T_Surjection_54 -> T_Equivalence_16)
-> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Surjection_54 -> T_Equivalence_16
MAlonzo.Code.Function.Surjection.du_equivalence_92
      ((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
du_surjection_100 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
-- Function.Bijection.Bijection._.to-from
d_to'45'from_106 ::
  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 ->
  T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_106 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_to'45'from_106 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_Setoid_44
v5 T_Bijection_64
v6
  = T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_106 T_Setoid_44
v4 T_Setoid_44
v5 T_Bijection_64
v6
du_to'45'from_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_106 :: T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_106 T_Setoid_44
v0 T_Setoid_44
v1 T_Bijection_64
v2
  = let v3 :: t
v3 = (T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> t
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
du_surjection_100 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v2) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_Setoid_44
 -> T_Setoid_44
 -> T_LeftInverse_82
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Function.LeftInverse.du_to'45'from_192 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
         ((T_Surjection_54 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Surjection_54 -> T_LeftInverse_82
MAlonzo.Code.Function.Surjection.du_right'45'inverse_82 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)))
-- Function.Bijection.Bijection._.right-inverse
d_right'45'inverse_108 ::
  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 ->
  T_Bijection_64 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_right'45'inverse_108 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> T_LeftInverse_82
d_right'45'inverse_108 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_64
v6
  = T_Bijection_64 -> T_LeftInverse_82
du_right'45'inverse_108 T_Bijection_64
v6
du_right'45'inverse_108 ::
  T_Bijection_64 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_right'45'inverse_108 :: T_Bijection_64 -> T_LeftInverse_82
du_right'45'inverse_108 T_Bijection_64
v0
  = (T_Surjection_54 -> T_LeftInverse_82)
-> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
      T_Surjection_54 -> T_LeftInverse_82
MAlonzo.Code.Function.Surjection.du_right'45'inverse_82
      ((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
du_surjection_100 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
-- Function.Bijection.Bijection.left-inverse
d_left'45'inverse_110 ::
  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 ->
  T_Bijection_64 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_left'45'inverse_110 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> T_LeftInverse_82
d_left'45'inverse_110 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_64
v6
  = T_Bijection_64 -> T_LeftInverse_82
du_left'45'inverse_110 T_Bijection_64
v6
du_left'45'inverse_110 ::
  T_Bijection_64 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_left'45'inverse_110 :: T_Bijection_64 -> T_LeftInverse_82
du_left'45'inverse_110 T_Bijection_64
v0
  = (T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.C_LeftInverse'46'constructor_4555
      ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
      ((T_Surjective_18 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
         ((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijective_18 -> T_Surjective_18
d_surjective_40 ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))))
      ((T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny
du_left'45'inverse'45'of_48 ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0))
         ((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v0)))
-- Function.Bijection.Bijection._.to-from
d_to'45'from_114 ::
  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 ->
  T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_114 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_to'45'from_114 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_Setoid_44
v5 T_Bijection_64
v6
  = T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_114 T_Setoid_44
v4 T_Setoid_44
v5 T_Bijection_64
v6
du_to'45'from_114 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_114 :: T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_114 T_Setoid_44
v0 T_Setoid_44
v1 T_Bijection_64
v2
  = (T_Setoid_44
 -> T_Setoid_44
 -> T_LeftInverse_82
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Function.LeftInverse.du_to'45'from_192 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1) ((T_Bijection_64 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_LeftInverse_82
du_left'45'inverse_110 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v2))
-- Function.Bijection._⤖_
d__'10518'__120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d__'10518'__120 :: () -> () -> () -> () -> ()
d__'10518'__120 = () -> () -> () -> () -> ()
forall a. a
erased
-- Function.Bijection.bijection
d_bijection_144 ::
  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) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_Bijection_64
d_bijection_144 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Bijection_64
d_bijection_144 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v6 AgdaAny -> T__'8801'__12
v7
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Bijection_64
du_bijection_144 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v6 AgdaAny -> T__'8801'__12
v7
du_bijection_144 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_Bijection_64
du_bijection_144 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Bijection_64
du_bijection_144 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v2 AgdaAny -> T__'8801'__12
v3
  = (T_Π_16 -> T_Bijective_18 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> T_Bijection_64
forall a b. a -> b
coe
      T_Π_16 -> T_Bijective_18 -> T_Bijection_64
C_Bijection'46'constructor_4749
      ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
         ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
               AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
         AgdaAny -> AgdaAny
v0)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Surjective_18 -> T_Bijective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Surjective_18 -> T_Bijective_18
C_Bijective'46'constructor_1705 ((AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v2)
         ((T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18
MAlonzo.Code.Function.Surjection.C_Surjective'46'constructor_1229
            ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
               ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
                  (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
                     AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
               AgdaAny -> AgdaAny
v1)
            ((AgdaAny -> T__'8801'__12) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8801'__12
v3)))
-- Function.Bijection.id
d_id_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> T_Bijection_64
d_id_160 :: () -> () -> T_Setoid_44 -> T_Bijection_64
d_id_160 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Bijection_64
du_id_160 T_Setoid_44
v2
du_id_160 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> T_Bijection_64
du_id_160 :: T_Setoid_44 -> T_Bijection_64
du_id_160 T_Setoid_44
v0
  = (T_Π_16 -> T_Bijective_18 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> T_Bijection_64
forall a b. a -> b
coe
      T_Π_16 -> T_Bijective_18 -> T_Bijection_64
C_Bijection'46'constructor_4749
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Surjective_18 -> T_Bijective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Surjective_18 -> T_Bijective_18
C_Bijective'46'constructor_1705
         ((T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Injection.d_injective_108
            (T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
MAlonzo.Code.Function.Injection.du_id_152))
         ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74
            ((T_Setoid_44 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du_id_168 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))))
-- Function.Bijection._∘_
d__'8728'__182 ::
  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 ->
  T_Bijection_64 -> T_Bijection_64 -> T_Bijection_64
d__'8728'__182 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_64
-> T_Bijection_64
-> T_Bijection_64
d__'8728'__182 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 T_Setoid_44
v8 T_Bijection_64
v9 T_Bijection_64
v10
  = T_Setoid_44 -> T_Bijection_64 -> T_Bijection_64 -> T_Bijection_64
du__'8728'__182 T_Setoid_44
v8 T_Bijection_64
v9 T_Bijection_64
v10
du__'8728'__182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Bijection_64 -> T_Bijection_64 -> T_Bijection_64
du__'8728'__182 :: T_Setoid_44 -> T_Bijection_64 -> T_Bijection_64 -> T_Bijection_64
du__'8728'__182 T_Setoid_44
v0 T_Bijection_64
v1 T_Bijection_64
v2
  = (T_Π_16 -> T_Bijective_18 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> T_Bijection_64
forall a b. a -> b
coe
      T_Π_16 -> T_Bijective_18 -> T_Bijection_64
C_Bijection'46'constructor_4749
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Π_16 -> T_Π_16
MAlonzo.Code.Function.Equality.du__'8728'__82
         ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v1)) ((T_Bijection_64 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v2)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Surjective_18 -> T_Bijective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Surjective_18 -> T_Bijective_18
C_Bijective'46'constructor_1705
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
               (T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 (T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> T_Bijection_64
forall a b. a -> b
coe T_Bijection_64
v2)) AgdaAny
v3 AgdaAny
v4
                 ((T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_38 (T_Bijection_64 -> T_Bijective_18
d_bijective_84 (T_Bijection_64 -> T_Bijection_64
forall a b. a -> b
coe T_Bijection_64
v1))
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> T_Bijection_64
forall a b. a -> b
coe T_Bijection_64
v2)) AgdaAny
v3)
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_Bijection_64 -> T_Π_16
d_to_82 (T_Bijection_64 -> T_Bijection_64
forall a b. a -> b
coe T_Bijection_64
v2)) AgdaAny
v4)
                    AgdaAny
v5)))
         ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74
            ((T_Setoid_44
 -> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du__'8728'__196 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
               ((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
du_surjection_100 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v1))
               ((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
du_surjection_100 (T_Bijection_64 -> AgdaAny
forall a b. a -> b
coe T_Bijection_64
v2)))))