{-# 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.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.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.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Surjection.Surjective
d_Surjective_18 :: p -> p -> p -> p -> p -> p -> p -> ()
d_Surjective_18 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_Surjective_18
  = C_Surjective'46'constructor_1229 MAlonzo.Code.Function.Equality.T_Π_16
                                     (AgdaAny -> AgdaAny)
-- Function.Surjection.Surjective.from
d_from_38 ::
  T_Surjective_18 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_38 :: T_Surjective_18 -> T_Π_16
d_from_38 T_Surjective_18
v0
  = case T_Surjective_18 -> T_Surjective_18
forall a b. a -> b
coe T_Surjective_18
v0 of
      C_Surjective'46'constructor_1229 T_Π_16
v1 AgdaAny -> AgdaAny
v2 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1
      T_Surjective_18
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Surjection.Surjective.right-inverse-of
d_right'45'inverse'45'of_40 ::
  T_Surjective_18 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_40 :: T_Surjective_18 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_40 T_Surjective_18
v0
  = case T_Surjective_18 -> T_Surjective_18
forall a b. a -> b
coe T_Surjective_18
v0 of
      C_Surjective'46'constructor_1229 T_Π_16
v1 AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2
      T_Surjective_18
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Surjection.Surjection
d_Surjection_54 :: p -> p -> p -> p -> p -> p -> ()
d_Surjection_54 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Surjection_54
  = C_Surjection'46'constructor_2369 MAlonzo.Code.Function.Equality.T_Π_16
                                     T_Surjective_18
-- Function.Surjection.Surjection.to
d_to_72 :: T_Surjection_54 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_72 :: T_Surjection_54 -> T_Π_16
d_to_72 T_Surjection_54
v0
  = case T_Surjection_54 -> T_Surjection_54
forall a b. a -> b
coe T_Surjection_54
v0 of
      C_Surjection'46'constructor_2369 T_Π_16
v1 T_Surjective_18
v2 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1
      T_Surjection_54
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Surjection.Surjection.surjective
d_surjective_74 :: T_Surjection_54 -> T_Surjective_18
d_surjective_74 :: T_Surjection_54 -> T_Surjective_18
d_surjective_74 T_Surjection_54
v0
  = case T_Surjection_54 -> T_Surjection_54
forall a b. a -> b
coe T_Surjection_54
v0 of
      C_Surjection'46'constructor_2369 T_Π_16
v1 T_Surjective_18
v2 -> T_Surjective_18 -> T_Surjective_18
forall a b. a -> b
coe T_Surjective_18
v2
      T_Surjection_54
_ -> T_Surjective_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Surjection.Surjection._.from
d_from_78 ::
  T_Surjection_54 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_78 :: T_Surjection_54 -> T_Π_16
d_from_78 T_Surjection_54
v0 = (T_Surjective_18 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Surjective_18 -> T_Π_16
d_from_38 ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0))
-- Function.Surjection.Surjection._.right-inverse-of
d_right'45'inverse'45'of_80 ::
  T_Surjection_54 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_80 :: T_Surjection_54 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_80 T_Surjection_54
v0
  = (T_Surjective_18 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjective_18 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_40 ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0))
-- Function.Surjection.Surjection.right-inverse
d_right'45'inverse_82 ::
  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_Surjection_54 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_right'45'inverse_82 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_LeftInverse_82
d_right'45'inverse_82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Surjection_54
v6
  = T_Surjection_54 -> T_LeftInverse_82
du_right'45'inverse_82 T_Surjection_54
v6
du_right'45'inverse_82 ::
  T_Surjection_54 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_right'45'inverse_82 :: T_Surjection_54 -> T_LeftInverse_82
du_right'45'inverse_82 T_Surjection_54
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_Surjective_18 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjective_18 -> T_Π_16
d_from_38 ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
      ((T_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
d_to_72 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0))
      ((T_Surjective_18 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjective_18 -> AgdaAny -> AgdaAny
d_right'45'inverse'45'of_40 ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
-- Function.Surjection.Surjection._.to-from
d_to'45'from_86 ::
  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_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_86 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_to'45'from_86 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_Setoid_44
v5 T_Surjection_54
v6
  = T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_86 T_Setoid_44
v4 T_Setoid_44
v5 T_Surjection_54
v6
du_to'45'from_86 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_86 :: T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_86 T_Setoid_44
v0 T_Setoid_44
v1 T_Surjection_54
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
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
du_right'45'inverse_82 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v2))
-- Function.Surjection.Surjection.injective
d_injective_88 ::
  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_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_88 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_injective_88 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 T_Setoid_44
v5 T_Surjection_54
v6 AgdaAny
v7 AgdaAny
v8
  = T_Setoid_44
-> T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_88 T_Setoid_44
v5 T_Surjection_54
v6 AgdaAny
v7 AgdaAny
v8
du_injective_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_88 :: T_Setoid_44
-> T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_88 T_Setoid_44
v0 T_Surjection_54
v1 AgdaAny
v2 AgdaAny
v3
  = (T_Setoid_44
 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Setoid_44
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.LeftInverse.du_injective_176 (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
du_right'45'inverse_82 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v1)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
-- Function.Surjection.Surjection.injection
d_injection_90 ::
  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_Surjection_54 -> MAlonzo.Code.Function.Injection.T_Injection_88
d_injection_90 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_Injection_88
d_injection_90 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 T_Setoid_44
v5 T_Surjection_54
v6 = T_Setoid_44 -> T_Surjection_54 -> T_Injection_88
du_injection_90 T_Setoid_44
v5 T_Surjection_54
v6
du_injection_90 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Surjection_54 -> MAlonzo.Code.Function.Injection.T_Injection_88
du_injection_90 :: T_Setoid_44 -> T_Surjection_54 -> T_Injection_88
du_injection_90 T_Setoid_44
v0 T_Surjection_54
v1
  = (T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
      T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
MAlonzo.Code.Function.LeftInverse.du_injection_184 (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
du_right'45'inverse_82 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v1))
-- Function.Surjection.Surjection.equivalence
d_equivalence_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_Surjection_54 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_equivalence_92 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_Equivalence_16
d_equivalence_92 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Surjection_54
v6 = T_Surjection_54 -> T_Equivalence_16
du_equivalence_92 T_Surjection_54
v6
du_equivalence_92 ::
  T_Surjection_54 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_equivalence_92 :: T_Surjection_54 -> T_Equivalence_16
du_equivalence_92 T_Surjection_54
v0
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.C_Equivalence'46'constructor_433
      ((T_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
d_to_72 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0))
      ((T_Surjective_18 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjective_18 -> T_Π_16
d_from_38 ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
-- Function.Surjection.fromRightInverse
d_fromRightInverse_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 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
  T_Surjection_54
d_fromRightInverse_106 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> T_Surjection_54
d_fromRightInverse_106 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_LeftInverse_82
v6
  = T_LeftInverse_82 -> T_Surjection_54
du_fromRightInverse_106 T_LeftInverse_82
v6
du_fromRightInverse_106 ::
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
  T_Surjection_54
du_fromRightInverse_106 :: T_LeftInverse_82 -> T_Surjection_54
du_fromRightInverse_106 T_LeftInverse_82
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
C_Surjection'46'constructor_2369
      ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_from_104 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0))
      ((T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18
C_Surjective'46'constructor_1229
         ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_to_102 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0))
         ((T_LeftInverse_82 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_LeftInverse_82 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106
            (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0)))
-- Function.Surjection._↠_
d__'8608'__134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d__'8608'__134 :: () -> () -> () -> () -> ()
d__'8608'__134 = () -> () -> () -> () -> ()
forall a. a
erased
-- Function.Surjection.surjection
d_surjection_154 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_Surjection_54
d_surjection_154 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T_Surjection_54
d_surjection_154 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> T__'8801'__12
v6
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T_Surjection_54
du_surjection_154 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> T__'8801'__12
v6
du_surjection_154 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_Surjection_54
du_surjection_154 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T_Surjection_54
du_surjection_154 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> T__'8801'__12
v2
  = (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
C_Surjection'46'constructor_2369
      ((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)
      ((T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18
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
v2))
-- Function.Surjection.id
d_id_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> T_Surjection_54
d_id_168 :: () -> () -> T_Setoid_44 -> T_Surjection_54
d_id_168 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Surjection_54
du_id_168 T_Setoid_44
v2
du_id_168 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> T_Surjection_54
du_id_168 :: T_Setoid_44 -> T_Surjection_54
du_id_168 T_Setoid_44
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
C_Surjection'46'constructor_2369
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
      ((T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18
C_Surjective'46'constructor_1229
         ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_to_102
            ((T_Setoid_44 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_LeftInverse_82
du_id'8242'_176 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
         ((T_LeftInverse_82 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_LeftInverse_82 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106
            ((T_Setoid_44 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_LeftInverse_82
du_id'8242'_176 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))))
-- Function.Surjection._.id′
d_id'8242'_176 ::
  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.LeftInverse.T_LeftInverse_82
d_id'8242'_176 :: () -> () -> T_Setoid_44 -> T_LeftInverse_82
d_id'8242'_176 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_LeftInverse_82
du_id'8242'_176 T_Setoid_44
v2
du_id'8242'_176 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_id'8242'_176 :: T_Setoid_44 -> T_LeftInverse_82
du_id'8242'_176 T_Setoid_44
v0
  = (T_Setoid_44 -> T_LeftInverse_82) -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe T_Setoid_44 -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.du_id_256 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
-- Function.Surjection._∘_
d__'8728'__196 ::
  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_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
d__'8728'__196 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_Surjection_54
-> T_Surjection_54
d__'8728'__196 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 T_Setoid_44
v8 T_Surjection_54
v9 T_Surjection_54
v10
  = T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8728'__196 T_Setoid_44
v8 T_Surjection_54
v9 T_Surjection_54
v10
du__'8728'__196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8728'__196 :: T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
du__'8728'__196 T_Setoid_44
v0 T_Surjection_54
v1 T_Surjection_54
v2
  = (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
C_Surjection'46'constructor_2369
      ((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_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
d_to_72 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v1)) ((T_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
d_to_72 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v2)))
      ((T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18
C_Surjective'46'constructor_1229
         ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_to_102
            ((T_Setoid_44
 -> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_g'8728'f_206 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v1) (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v2)))
         ((T_LeftInverse_82 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_LeftInverse_82 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.LeftInverse.d_left'45'inverse'45'of_106
            ((T_Setoid_44
 -> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_g'8728'f_206 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v1) (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v2))))
-- Function.Surjection._.g∘f
d_g'8728'f_206 ::
  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_Surjection_54 ->
  T_Surjection_54 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_g'8728'f_206 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Surjection_54
-> T_Surjection_54
-> T_LeftInverse_82
d_g'8728'f_206 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 T_Setoid_44
v8 T_Surjection_54
v9 T_Surjection_54
v10
  = T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_g'8728'f_206 T_Setoid_44
v8 T_Surjection_54
v9 T_Surjection_54
v10
du_g'8728'f_206 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Surjection_54 ->
  T_Surjection_54 ->
  MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_g'8728'f_206 :: T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82
du_g'8728'f_206 T_Setoid_44
v0 T_Surjection_54
v1 T_Surjection_54
v2
  = (T_Setoid_44
 -> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
      T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.du__'8728'__280 (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
du_right'45'inverse_82 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v2))
      ((T_Surjection_54 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_LeftInverse_82
du_right'45'inverse_82 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v1))