{-# 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.Surjection 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.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.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Properties.Surjection._.Eq₁._≈_
d__'8776'__40 ::
  T_GeneralizeTel_423 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__40 :: T_GeneralizeTel_423 -> T_Func_714 -> AgdaAny -> AgdaAny -> ()
d__'8776'__40 = T_GeneralizeTel_423 -> T_Func_714 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.Surjection._.Eq₂._≈_
d__'8776'__64 ::
  T_GeneralizeTel_423 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__64 :: T_GeneralizeTel_423 -> T_Func_714 -> AgdaAny -> AgdaAny -> ()
d__'8776'__64 = T_GeneralizeTel_423 -> T_Func_714 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.Surjection.mkSurjection
d_mkSurjection_86 ::
  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_Func_714 ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_mkSurjection_86 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_Func_714
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_846
d_mkSurjection_86 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 T_Func_714
v6 AgdaAny -> T_Σ_14
v7
  = T_Func_714 -> (AgdaAny -> T_Σ_14) -> T_Surjection_846
du_mkSurjection_86 T_Func_714
v6 AgdaAny -> T_Σ_14
v7
du_mkSurjection_86 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_mkSurjection_86 :: T_Func_714 -> (AgdaAny -> T_Σ_14) -> T_Surjection_846
du_mkSurjection_86 T_Func_714
v0 AgdaAny -> T_Σ_14
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14)
 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_846
MAlonzo.Code.Function.Bundles.C_Surjection'46'constructor_11197
      ((T_Func_714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v0))
      ((T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_722 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v0)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
v1)
-- Function.Properties.Surjection.↠⇒⟶
d_'8608''8658''10230'_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_'8608''8658''10230'_150 :: () -> () -> () -> () -> T_Surjection_846 -> T_Func_714
d_'8608''8658''10230'_150 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Surjection_846 -> T_Func_714
du_'8608''8658''10230'_150
du_'8608''8658''10230'_150 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_'8608''8658''10230'_150 :: T_Surjection_846 -> T_Func_714
du_'8608''8658''10230'_150
  = (T_Surjection_846 -> T_Func_714) -> T_Surjection_846 -> T_Func_714
forall a b. a -> b
coe T_Surjection_846 -> T_Func_714
MAlonzo.Code.Function.Bundles.du_function_860
-- Function.Properties.Surjection.↠⇒↪
d_'8608''8658''8618'_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_'8608''8658''8618'_152 :: () -> () -> () -> () -> T_Surjection_846 -> T_RightInverse_1880
d_'8608''8658''8618'_152 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Surjection_846
v4
  = T_Surjection_846 -> T_RightInverse_1880
du_'8608''8658''8618'_152 T_Surjection_846
v4
du_'8608''8658''8618'_152 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_'8608''8658''8618'_152 :: T_Surjection_846 -> T_RightInverse_1880
du_'8608''8658''8618'_152 T_Surjection_846
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
 -> T_RightInverse_1880)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_RightInverse_1880
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.du_mk'8618'_2320
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
              ((T_IsSurjection_162 -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                 T_IsSurjection_162 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.du_strictlySurjective_230
                 ((T_Setoid_44
 -> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                       T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
                    (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                       T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
                    (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
      ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0)) AgdaAny
forall a. a
erased
-- Function.Properties.Surjection._..extendedlambda0
d_'46'extendedlambda0_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'46'extendedlambda0_228 :: ()
-> ()
-> ()
-> ()
-> T_Surjection_846
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'46'extendedlambda0_228 = ()
-> ()
-> ()
-> ()
-> T_Surjection_846
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Function.Properties.Surjection.↠⇒⇔
d_'8608''8658''8660'_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8608''8658''8660'_230 :: () -> () -> () -> () -> T_Surjection_846 -> T_Equivalence_1714
d_'8608''8658''8660'_230 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Surjection_846
v4
  = T_Surjection_846 -> T_Equivalence_1714
du_'8608''8658''8660'_230 T_Surjection_846
v4
du_'8608''8658''8660'_230 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8608''8658''8660'_230 :: T_Surjection_846 -> T_Equivalence_1714
du_'8608''8658''8660'_230 T_Surjection_846
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
              ((T_Surjection_846 -> AgdaAny -> T_Σ_14)
-> T_Surjection_846 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_858 T_Surjection_846
v0 AgdaAny
v1)))
-- Function.Properties.Surjection.refl
d_refl_306 ::
  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_Surjection_846
d_refl_306 :: () -> () -> T_Setoid_44 -> T_Surjection_846
d_refl_306 ~()
v0 ~()
v1 ~T_Setoid_44
v2 = T_Surjection_846
du_refl_306
du_refl_306 :: MAlonzo.Code.Function.Bundles.T_Surjection_846
du_refl_306 :: T_Surjection_846
du_refl_306
  = T_Surjection_846 -> T_Surjection_846
forall a b. a -> b
coe T_Surjection_846
MAlonzo.Code.Function.Construct.Identity.du_surjection_786
-- Function.Properties.Surjection.trans
d_trans_310 ::
  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_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_trans_310 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
d_trans_310 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 ~T_Setoid_44
v8 = T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du_trans_310
du_trans_310 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_trans_310 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du_trans_310
  = (T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
forall a b. a -> b
coe
      T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
MAlonzo.Code.Function.Construct.Composition.du_surjection_1460
-- Function.Properties.Surjection._.to⁻
d_to'8315'_330 ::
  T_GeneralizeTel_9221 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  AgdaAny -> AgdaAny
d_to'8315'_330 :: T_GeneralizeTel_9221 -> T_Surjection_846 -> AgdaAny -> AgdaAny
d_to'8315'_330 ~T_GeneralizeTel_9221
v0 T_Surjection_846
v1 = T_Surjection_846 -> AgdaAny -> AgdaAny
du_to'8315'_330 T_Surjection_846
v1
du_to'8315'_330 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  AgdaAny -> AgdaAny
du_to'8315'_330 :: T_Surjection_846 -> AgdaAny -> AgdaAny
du_to'8315'_330 T_Surjection_846
v0
  = (T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0)
-- Function.Properties.Surjection._.Eq₁._≈_
d__'8776'__336 ::
  T_GeneralizeTel_9221 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__336 :: T_GeneralizeTel_9221
-> T_Surjection_846 -> AgdaAny -> AgdaAny -> ()
d__'8776'__336 = T_GeneralizeTel_9221
-> T_Surjection_846 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.Surjection._.Eq₂._≈_
d__'8776'__360 ::
  T_GeneralizeTel_9221 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__360 :: T_GeneralizeTel_9221
-> T_Surjection_846 -> AgdaAny -> AgdaAny -> ()
d__'8776'__360 = T_GeneralizeTel_9221
-> T_Surjection_846 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.Surjection.injective⇒to⁻-cong
d_injective'8658'to'8315''45'cong_382 ::
  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_Surjection_846 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective'8658'to'8315''45'cong_382 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_Surjection_846
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_injective'8658'to'8315''45'cong_382 ~()
v0 ~()
v1 T_Setoid_44
v2 ~()
v3 ~()
v4 T_Setoid_44
v5 T_Surjection_846
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
                                      AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = T_Setoid_44
-> T_Setoid_44
-> T_Surjection_846
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective'8658'to'8315''45'cong_382 T_Setoid_44
v2 T_Setoid_44
v5 T_Surjection_846
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_injective'8658'to'8315''45'cong_382 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective'8658'to'8315''45'cong_382 :: T_Setoid_44
-> T_Setoid_44
-> T_Surjection_846
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective'8658'to'8315''45'cong_382 T_Setoid_44
v0 T_Setoid_44
v1 T_Surjection_846
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
      ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
         (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
            (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
         ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
            ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
         ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
            ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                  ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1))))
            ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
               ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
            AgdaAny
v4
            ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
               ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                     ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1))))
               AgdaAny
v4 AgdaAny
v5
               ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
                  ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_370
                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                     ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1))))
                  (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                     ((T_Setoid_44 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)))
                  AgdaAny
v5
                  ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
                     ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
                  ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
                     ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
                  (let v7 :: AgdaAny -> AgdaAny
v7
                         = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                             ((T_Setoid_44 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                                T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                                (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                        (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                           ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v7))
                        ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v2
                           ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))))
                  ((T_Setoid_44
 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
-> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8728'to'8315'_924 (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_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
               AgdaAny
v6)
            ((T_Setoid_44
 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8728'to'8315'_924 (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_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))))
-- Function.Properties.Surjection..generalizedField-S.a
d_'46'generalizedField'45'S'46'a_411 ::
  T_GeneralizeTel_423 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'a_411 :: T_GeneralizeTel_423 -> ()
d_'46'generalizedField'45'S'46'a_411 T_GeneralizeTel_423
v0
  = case T_GeneralizeTel_423 -> T_GeneralizeTel_423
forall a b. a -> b
coe T_GeneralizeTel_423
v0 of
      C_mkGeneralizeTel_425 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v1
      T_GeneralizeTel_423
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-S.ℓ
d_'46'generalizedField'45'S'46'ℓ_413 ::
  T_GeneralizeTel_423 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'ℓ_413 :: T_GeneralizeTel_423 -> ()
d_'46'generalizedField'45'S'46'ℓ_413 T_GeneralizeTel_423
v0
  = case T_GeneralizeTel_423 -> T_GeneralizeTel_423
forall a b. a -> b
coe T_GeneralizeTel_423
v0 of
      C_mkGeneralizeTel_425 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v2
      T_GeneralizeTel_423
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-S
d_'46'generalizedField'45'S_415 ::
  T_GeneralizeTel_423 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'46'generalizedField'45'S_415 :: T_GeneralizeTel_423 -> T_Setoid_44
d_'46'generalizedField'45'S_415 T_GeneralizeTel_423
v0
  = case T_GeneralizeTel_423 -> T_GeneralizeTel_423
forall a b. a -> b
coe T_GeneralizeTel_423
v0 of
      C_mkGeneralizeTel_425 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v3
      T_GeneralizeTel_423
_ -> T_Setoid_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-T.a
d_'46'generalizedField'45'T'46'a_417 ::
  T_GeneralizeTel_423 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'a_417 :: T_GeneralizeTel_423 -> ()
d_'46'generalizedField'45'T'46'a_417 T_GeneralizeTel_423
v0
  = case T_GeneralizeTel_423 -> T_GeneralizeTel_423
forall a b. a -> b
coe T_GeneralizeTel_423
v0 of
      C_mkGeneralizeTel_425 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v4
      T_GeneralizeTel_423
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-T.ℓ
d_'46'generalizedField'45'T'46'ℓ_419 ::
  T_GeneralizeTel_423 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'ℓ_419 :: T_GeneralizeTel_423 -> ()
d_'46'generalizedField'45'T'46'ℓ_419 T_GeneralizeTel_423
v0
  = case T_GeneralizeTel_423 -> T_GeneralizeTel_423
forall a b. a -> b
coe T_GeneralizeTel_423
v0 of
      C_mkGeneralizeTel_425 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v5
      T_GeneralizeTel_423
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-T
d_'46'generalizedField'45'T_421 ::
  T_GeneralizeTel_423 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'46'generalizedField'45'T_421 :: T_GeneralizeTel_423 -> T_Setoid_44
d_'46'generalizedField'45'T_421 T_GeneralizeTel_423
v0
  = case T_GeneralizeTel_423 -> T_GeneralizeTel_423
forall a b. a -> b
coe T_GeneralizeTel_423
v0 of
      C_mkGeneralizeTel_425 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v6
      T_GeneralizeTel_423
_ -> T_Setoid_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection.GeneralizeTel
d_GeneralizeTel_423 :: ()
d_GeneralizeTel_423 = ()
data T_GeneralizeTel_423
  = C_mkGeneralizeTel_425 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
-- Function.Properties.Surjection..generalizedField-S.a
d_'46'generalizedField'45'S'46'a_9209 ::
  T_GeneralizeTel_9221 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'a_9209 :: T_GeneralizeTel_9221 -> ()
d_'46'generalizedField'45'S'46'a_9209 T_GeneralizeTel_9221
v0
  = case T_GeneralizeTel_9221 -> T_GeneralizeTel_9221
forall a b. a -> b
coe T_GeneralizeTel_9221
v0 of
      C_mkGeneralizeTel_9223 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v1
      T_GeneralizeTel_9221
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-S.ℓ
d_'46'generalizedField'45'S'46'ℓ_9211 ::
  T_GeneralizeTel_9221 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'ℓ_9211 :: T_GeneralizeTel_9221 -> ()
d_'46'generalizedField'45'S'46'ℓ_9211 T_GeneralizeTel_9221
v0
  = case T_GeneralizeTel_9221 -> T_GeneralizeTel_9221
forall a b. a -> b
coe T_GeneralizeTel_9221
v0 of
      C_mkGeneralizeTel_9223 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v2
      T_GeneralizeTel_9221
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-S
d_'46'generalizedField'45'S_9213 ::
  T_GeneralizeTel_9221 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'46'generalizedField'45'S_9213 :: T_GeneralizeTel_9221 -> T_Setoid_44
d_'46'generalizedField'45'S_9213 T_GeneralizeTel_9221
v0
  = case T_GeneralizeTel_9221 -> T_GeneralizeTel_9221
forall a b. a -> b
coe T_GeneralizeTel_9221
v0 of
      C_mkGeneralizeTel_9223 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v3
      T_GeneralizeTel_9221
_ -> T_Setoid_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-T.a
d_'46'generalizedField'45'T'46'a_9215 ::
  T_GeneralizeTel_9221 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'a_9215 :: T_GeneralizeTel_9221 -> ()
d_'46'generalizedField'45'T'46'a_9215 T_GeneralizeTel_9221
v0
  = case T_GeneralizeTel_9221 -> T_GeneralizeTel_9221
forall a b. a -> b
coe T_GeneralizeTel_9221
v0 of
      C_mkGeneralizeTel_9223 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v4
      T_GeneralizeTel_9221
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-T.ℓ
d_'46'generalizedField'45'T'46'ℓ_9217 ::
  T_GeneralizeTel_9221 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'ℓ_9217 :: T_GeneralizeTel_9221 -> ()
d_'46'generalizedField'45'T'46'ℓ_9217 T_GeneralizeTel_9221
v0
  = case T_GeneralizeTel_9221 -> T_GeneralizeTel_9221
forall a b. a -> b
coe T_GeneralizeTel_9221
v0 of
      C_mkGeneralizeTel_9223 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v5
      T_GeneralizeTel_9221
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection..generalizedField-T
d_'46'generalizedField'45'T_9219 ::
  T_GeneralizeTel_9221 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'46'generalizedField'45'T_9219 :: T_GeneralizeTel_9221 -> T_Setoid_44
d_'46'generalizedField'45'T_9219 T_GeneralizeTel_9221
v0
  = case T_GeneralizeTel_9221 -> T_GeneralizeTel_9221
forall a b. a -> b
coe T_GeneralizeTel_9221
v0 of
      C_mkGeneralizeTel_9223 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v6
      T_GeneralizeTel_9221
_ -> T_Setoid_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.Surjection.GeneralizeTel
d_GeneralizeTel_9221 :: ()
d_GeneralizeTel_9221 = ()
data T_GeneralizeTel_9221
  = C_mkGeneralizeTel_9223 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