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

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Construct.Identity._.congruent
d_congruent_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_congruent_22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_congruent_22 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 AgdaAny
v6 = AgdaAny -> AgdaAny
du_congruent_22 AgdaAny
v6
du_congruent_22 :: AgdaAny -> AgdaAny
du_congruent_22 :: AgdaAny -> AgdaAny
du_congruent_22 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Construct.Identity._.injective
d_injective_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_24 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_injective_24 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 AgdaAny
v6 = AgdaAny -> AgdaAny
du_injective_24 AgdaAny
v6
du_injective_24 :: AgdaAny -> AgdaAny
du_injective_24 :: AgdaAny -> AgdaAny
du_injective_24 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Construct.Identity._.surjective
d_surjective_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Σ_14
d_surjective_26 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny
v4 = AgdaAny -> T_Σ_14
du_surjective_26 AgdaAny
v4
du_surjective_26 ::
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_surjective_26 :: AgdaAny -> T_Σ_14
du_surjective_26 AgdaAny
v0
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._.bijective
d_bijective_30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_bijective_30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
d_bijective_30 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 = T_Σ_14
du_bijective_30
du_bijective_30 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_bijective_30 :: T_Σ_14
du_bijective_30
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
du_surjective_26)
-- Function.Construct.Identity._.inverseˡ
d_inverse'737'_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_inverse'737'_32 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 AgdaAny
v6
  = AgdaAny -> AgdaAny
du_inverse'737'_32 AgdaAny
v6
du_inverse'737'_32 :: AgdaAny -> AgdaAny
du_inverse'737'_32 :: AgdaAny -> AgdaAny
du_inverse'737'_32 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Construct.Identity._.inverseʳ
d_inverse'691'_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_34 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_inverse'691'_34 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 AgdaAny
v6
  = AgdaAny -> AgdaAny
du_inverse'691'_34 AgdaAny
v6
du_inverse'691'_34 :: AgdaAny -> AgdaAny
du_inverse'691'_34 :: AgdaAny -> AgdaAny
du_inverse'691'_34 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Construct.Identity._.inverseᵇ
d_inverse'7495'_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_inverse'7495'_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
d_inverse'7495'_36 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 = T_Σ_14
du_inverse'7495'_36
du_inverse'7495'_36 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_inverse'7495'_36 :: T_Σ_14
du_inverse'7495'_36
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._._.IsBijection
d_IsBijection_56 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsBijection_56 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Function.Construct.Identity._._.IsCongruent
d_IsCongruent_58 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCongruent_58 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Function.Construct.Identity._._.IsInjection
d_IsInjection_60 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsInjection_60 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Function.Construct.Identity._._.IsInverse
d_IsInverse_62 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsInverse_62 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Function.Construct.Identity._._.IsLeftInverse
d_IsLeftInverse_64 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsLeftInverse_64 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Function.Construct.Identity._._.IsRightInverse
d_IsRightInverse_66 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRightInverse_66 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Function.Construct.Identity._._.IsSurjection
d_IsSurjection_70 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsSurjection_70 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Function.Construct.Identity._._.IsBijection.isInjection
d_isInjection_214 ::
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92
d_isInjection_214 :: T_IsBijection_238 -> T_IsInjection_92
d_isInjection_214 T_IsBijection_238
v0
  = (T_IsBijection_238 -> T_IsInjection_92)
-> AgdaAny -> T_IsInjection_92
forall a b. a -> b
coe T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v0)
-- Function.Construct.Identity._._.IsBijection.surjective
d_surjective_220 ::
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_220 :: T_IsBijection_238 -> AgdaAny -> T_Σ_14
d_surjective_220 T_IsBijection_238
v0
  = (T_IsBijection_238 -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_IsBijection_238 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_248 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v0)
-- Function.Construct.Identity._._.IsCongruent.cong
d_cong_272 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_272 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_272 T_IsCongruent_22
v0
  = (T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_cong_32 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v0)
-- Function.Construct.Identity._._.IsCongruent.isEquivalence₁
d_isEquivalence'8321'_274 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence'8321'_274 :: T_IsCongruent_22 -> T_IsEquivalence_26
d_isEquivalence'8321'_274 T_IsCongruent_22
v0
  = (T_IsCongruent_22 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v0)
-- Function.Construct.Identity._._.IsCongruent.isEquivalence₂
d_isEquivalence'8322'_276 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence'8322'_276 :: T_IsCongruent_22 -> T_IsEquivalence_26
d_isEquivalence'8322'_276 T_IsCongruent_22
v0
  = (T_IsCongruent_22 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v0)
-- Function.Construct.Identity._._.IsInjection.injective
d_injective_330 ::
  MAlonzo.Code.Function.Structures.T_IsInjection_92 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_330 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_330 T_IsInjection_92
v0
  = (T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_injective_102 (T_IsInjection_92 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92
v0)
-- Function.Construct.Identity._._.IsInjection.isCongruent
d_isCongruent_332 ::
  MAlonzo.Code.Function.Structures.T_IsInjection_92 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_332 :: T_IsInjection_92 -> T_IsCongruent_22
d_isCongruent_332 T_IsInjection_92
v0
  = (T_IsInjection_92 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92
v0)
-- Function.Construct.Identity._._.IsInverse.inverseʳ
d_inverse'691'_392 ::
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_392 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_392 T_IsInverse_490
v0
  = (T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_502 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v0)
-- Function.Construct.Identity._._.IsInverse.isLeftInverse
d_isLeftInverse_402 ::
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
d_isLeftInverse_402 :: T_IsInverse_490 -> T_IsLeftInverse_322
d_isLeftInverse_402 T_IsInverse_490
v0
  = (T_IsInverse_490 -> T_IsLeftInverse_322)
-> AgdaAny -> T_IsLeftInverse_322
forall a b. a -> b
coe T_IsInverse_490 -> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.d_isLeftInverse_500 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v0)
-- Function.Construct.Identity._._.IsLeftInverse.from-cong
d_from'45'cong_464 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_464 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_464 T_IsLeftInverse_322
v0
  = (T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_336 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v0)
-- Function.Construct.Identity._._.IsLeftInverse.inverseˡ
d_inverse'737'_466 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_466 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_466 T_IsLeftInverse_322
v0
  = (T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_338 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v0)
-- Function.Construct.Identity._._.IsLeftInverse.isCongruent
d_isCongruent_468 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_468 :: T_IsLeftInverse_322 -> T_IsCongruent_22
d_isCongruent_468 T_IsLeftInverse_322
v0
  = (T_IsLeftInverse_322 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsLeftInverse_322 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_334 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v0)
-- Function.Construct.Identity._._.IsRightInverse.from-cong
d_from'45'cong_530 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_530 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_530 T_IsRightInverse_408
v0
  = (T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_422 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v0)
-- Function.Construct.Identity._._.IsRightInverse.inverseʳ
d_inverse'691'_532 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_532 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_532 T_IsRightInverse_408
v0
  = (T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_424 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v0)
-- Function.Construct.Identity._._.IsRightInverse.isCongruent
d_isCongruent_534 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_534 :: T_IsRightInverse_408 -> T_IsCongruent_22
d_isCongruent_534 T_IsRightInverse_408
v0
  = (T_IsRightInverse_408 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v0)
-- Function.Construct.Identity._._.IsSurjection.isCongruent
d_isCongruent_666 ::
  MAlonzo.Code.Function.Structures.T_IsSurjection_162 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_666 :: T_IsSurjection_162 -> T_IsCongruent_22
d_isCongruent_666 T_IsSurjection_162
v0
  = (T_IsSurjection_162 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsSurjection_162 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_170 (T_IsSurjection_162 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162
v0)
-- Function.Construct.Identity._._.IsSurjection.surjective
d_surjective_674 ::
  MAlonzo.Code.Function.Structures.T_IsSurjection_162 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_674 :: T_IsSurjection_162 -> AgdaAny -> T_Σ_14
d_surjective_674 T_IsSurjection_162
v0
  = (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.d_surjective_172 (T_IsSurjection_162 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162
v0)
-- Function.Construct.Identity._.isCongruent
d_isCongruent_736 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_736 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsCongruent_22
d_isCongruent_736 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsCongruent_22
du_isCongruent_736 T_IsEquivalence_26
v4
du_isCongruent_736 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
du_isCongruent_736 :: T_IsEquivalence_26 -> T_IsCongruent_22
du_isCongruent_736 T_IsEquivalence_26
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_IsCongruent'46'constructor_985
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3)) (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)
-- Function.Construct.Identity._.isInjection
d_isInjection_738 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92
d_isInjection_738 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsInjection_92
d_isInjection_738 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsInjection_92
du_isInjection_738 T_IsEquivalence_26
v4
du_isInjection_738 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92
du_isInjection_738 :: T_IsEquivalence_26 -> T_IsInjection_92
du_isInjection_738 T_IsEquivalence_26
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_92)
-> AgdaAny -> AgdaAny -> T_IsInjection_92
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_92
MAlonzo.Code.Function.Structures.C_IsInjection'46'constructor_3997
      ((T_IsEquivalence_26 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsCongruent_22
du_isCongruent_736 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
-- Function.Construct.Identity._.isSurjection
d_isSurjection_740 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162
d_isSurjection_740 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsSurjection_162
d_isSurjection_740 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsSurjection_162
du_isSurjection_740 T_IsEquivalence_26
v4
du_isSurjection_740 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162
du_isSurjection_740 :: T_IsEquivalence_26 -> T_IsSurjection_162
du_isSurjection_740 T_IsEquivalence_26
v0
  = (T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_162)
-> AgdaAny -> AgdaAny -> T_IsSurjection_162
forall a b. a -> b
coe
      T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_162
MAlonzo.Code.Function.Structures.C_IsSurjection'46'constructor_6463
      ((T_IsEquivalence_26 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsCongruent_22
du_isCongruent_736 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
du_surjective_26)
-- Function.Construct.Identity._.isBijection
d_isBijection_742 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
d_isBijection_742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsBijection_238
d_isBijection_742 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsBijection_238
du_isBijection_742 T_IsEquivalence_26
v4
du_isBijection_742 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
du_isBijection_742 :: T_IsEquivalence_26 -> T_IsBijection_238
du_isBijection_742 T_IsEquivalence_26
v0
  = (T_IsInjection_92 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe
      T_IsInjection_92 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_238
MAlonzo.Code.Function.Structures.C_IsBijection'46'constructor_10113
      ((T_IsEquivalence_26 -> T_IsInjection_92) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsInjection_92
du_isInjection_738 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
du_surjective_26)
-- Function.Construct.Identity._.isLeftInverse
d_isLeftInverse_744 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
d_isLeftInverse_744 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsLeftInverse_322
d_isLeftInverse_744 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsLeftInverse_322
du_isLeftInverse_744 T_IsEquivalence_26
v4
du_isLeftInverse_744 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
du_isLeftInverse_744 :: T_IsEquivalence_26 -> T_IsLeftInverse_322
du_isLeftInverse_744 T_IsEquivalence_26
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_322)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLeftInverse_322
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.C_IsLeftInverse'46'constructor_14363
      ((T_IsEquivalence_26 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsCongruent_22
du_isCongruent_736 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
-- Function.Construct.Identity._.isRightInverse
d_isRightInverse_746 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408
d_isRightInverse_746 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsRightInverse_408
d_isRightInverse_746 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsRightInverse_408
du_isRightInverse_746 T_IsEquivalence_26
v4
du_isRightInverse_746 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408
du_isRightInverse_746 :: T_IsEquivalence_26 -> T_IsRightInverse_408
du_isRightInverse_746 T_IsEquivalence_26
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRightInverse_408)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRightInverse_408
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRightInverse_408
MAlonzo.Code.Function.Structures.C_IsRightInverse'46'constructor_18837
      ((T_IsEquivalence_26 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsCongruent_22
du_isCongruent_736 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
-- Function.Construct.Identity._.isInverse
d_isInverse_748 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490
d_isInverse_748 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsInverse_490
d_isInverse_748 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_26
v4 = T_IsEquivalence_26 -> T_IsInverse_490
du_isInverse_748 T_IsEquivalence_26
v4
du_isInverse_748 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490
du_isInverse_748 :: T_IsEquivalence_26 -> T_IsInverse_490
du_isInverse_748 T_IsEquivalence_26
v0
  = (T_IsLeftInverse_322
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_490)
-> AgdaAny -> AgdaAny -> T_IsInverse_490
forall a b. a -> b
coe
      T_IsLeftInverse_322
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_490
MAlonzo.Code.Function.Structures.C_IsInverse'46'constructor_22449
      ((T_IsEquivalence_26 -> T_IsLeftInverse_322) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsLeftInverse_322
du_isLeftInverse_744 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
-- Function.Construct.Identity._.function
d_function_782 ::
  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
d_function_782 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714
d_function_782 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Func_714
du_function_782
du_function_782 :: MAlonzo.Code.Function.Bundles.T_Func_714
du_function_782 :: T_Func_714
du_function_782
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_714)
-> AgdaAny -> AgdaAny -> T_Func_714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._.injection
d_injection_784 ::
  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_Injection_776
d_injection_784 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Injection_776
d_injection_784 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Injection_776
du_injection_784
du_injection_784 :: MAlonzo.Code.Function.Bundles.T_Injection_776
du_injection_784 :: T_Injection_776
du_injection_784
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Injection_776
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Injection_776
MAlonzo.Code.Function.Bundles.C_Injection'46'constructor_8675
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._.surjection
d_surjection_786 ::
  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_surjection_786 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Surjection_846
d_surjection_786 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Surjection_846
du_surjection_786
du_surjection_786 :: MAlonzo.Code.Function.Bundles.T_Surjection_846
du_surjection_786 :: T_Surjection_846
du_surjection_786
  = ((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
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
du_surjective_26)
-- Function.Construct.Identity._.bijection
d_bijection_788 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_bijection_788 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Bijection_926
d_bijection_788 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Bijection_926
du_bijection_788
du_bijection_788 :: MAlonzo.Code.Function.Bundles.T_Bijection_926
du_bijection_788 :: T_Bijection_926
du_bijection_788
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_926
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Bijection_926
MAlonzo.Code.Function.Bundles.C_Bijection'46'constructor_15277
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_bijective_30)
-- Function.Construct.Identity._.equivalence
d_equivalence_790 ::
  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_Equivalence_1714
d_equivalence_790 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Equivalence_1714
d_equivalence_790 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Equivalence_1714
du_equivalence_790
du_equivalence_790 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_equivalence_790 :: T_Equivalence_1714
du_equivalence_790
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.C_Equivalence'46'constructor_25797
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._.leftInverse
d_leftInverse_792 ::
  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_LeftInverse_1792
d_leftInverse_792 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_1792
d_leftInverse_792 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_LeftInverse_1792
du_leftInverse_792
du_leftInverse_792 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_leftInverse_792 :: T_LeftInverse_1792
du_leftInverse_792
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1792)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1792
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.C_LeftInverse'46'constructor_29775
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._.rightInverse
d_rightInverse_794 ::
  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_RightInverse_1880
d_rightInverse_794 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880
d_rightInverse_794 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_RightInverse_1880
du_rightInverse_794
du_rightInverse_794 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_rightInverse_794 :: T_RightInverse_1880
du_rightInverse_794
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_1880)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_1880
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.C_RightInverse'46'constructor_34573
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Construct.Identity._.inverse
d_inverse_796 ::
  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_Inverse_1960
d_inverse_796 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Inverse_1960
d_inverse_796 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Inverse_1960
du_inverse_796
du_inverse_796 :: MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_inverse_796 :: T_Inverse_1960
du_inverse_796
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_1960)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_inverse'7495'_36)
-- Function.Construct.Identity._.⟶-id
d_'10230''45'id_806 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Func_714
d_'10230''45'id_806 :: T_Level_18 -> T_Level_18 -> T_Func_714
d_'10230''45'id_806 ~T_Level_18
v0 ~T_Level_18
v1 = T_Func_714
du_'10230''45'id_806
du_'10230''45'id_806 :: MAlonzo.Code.Function.Bundles.T_Func_714
du_'10230''45'id_806 :: T_Func_714
du_'10230''45'id_806 = T_Func_714 -> T_Func_714
forall a b. a -> b
coe T_Func_714
du_function_782
-- Function.Construct.Identity._.↣-id
d_'8611''45'id_808 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Injection_776
d_'8611''45'id_808 :: T_Level_18 -> T_Level_18 -> T_Injection_776
d_'8611''45'id_808 ~T_Level_18
v0 ~T_Level_18
v1 = T_Injection_776
du_'8611''45'id_808
du_'8611''45'id_808 ::
  MAlonzo.Code.Function.Bundles.T_Injection_776
du_'8611''45'id_808 :: T_Injection_776
du_'8611''45'id_808 = T_Injection_776 -> T_Injection_776
forall a b. a -> b
coe T_Injection_776
du_injection_784
-- Function.Construct.Identity._.↠-id
d_'8608''45'id_810 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Surjection_846
d_'8608''45'id_810 :: T_Level_18 -> T_Level_18 -> T_Surjection_846
d_'8608''45'id_810 ~T_Level_18
v0 ~T_Level_18
v1 = T_Surjection_846
du_'8608''45'id_810
du_'8608''45'id_810 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_'8608''45'id_810 :: T_Surjection_846
du_'8608''45'id_810 = T_Surjection_846 -> T_Surjection_846
forall a b. a -> b
coe T_Surjection_846
du_surjection_786
-- Function.Construct.Identity._.⤖-id
d_'10518''45'id_812 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Bijection_926
d_'10518''45'id_812 :: T_Level_18 -> T_Level_18 -> T_Bijection_926
d_'10518''45'id_812 ~T_Level_18
v0 ~T_Level_18
v1 = T_Bijection_926
du_'10518''45'id_812
du_'10518''45'id_812 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_'10518''45'id_812 :: T_Bijection_926
du_'10518''45'id_812 = T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926
du_bijection_788
-- Function.Construct.Identity._.⇔-id
d_'8660''45'id_814 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8660''45'id_814 :: T_Level_18 -> T_Level_18 -> T_Equivalence_1714
d_'8660''45'id_814 ~T_Level_18
v0 ~T_Level_18
v1 = T_Equivalence_1714
du_'8660''45'id_814
du_'8660''45'id_814 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8660''45'id_814 :: T_Equivalence_1714
du_'8660''45'id_814 = T_Equivalence_1714 -> T_Equivalence_1714
forall a b. a -> b
coe T_Equivalence_1714
du_equivalence_790
-- Function.Construct.Identity._.↩-id
d_'8617''45'id_816 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_'8617''45'id_816 :: T_Level_18 -> T_Level_18 -> T_LeftInverse_1792
d_'8617''45'id_816 ~T_Level_18
v0 ~T_Level_18
v1 = T_LeftInverse_1792
du_'8617''45'id_816
du_'8617''45'id_816 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_'8617''45'id_816 :: T_LeftInverse_1792
du_'8617''45'id_816 = T_LeftInverse_1792 -> T_LeftInverse_1792
forall a b. a -> b
coe T_LeftInverse_1792
du_leftInverse_792
-- Function.Construct.Identity._.↪-id
d_'8618''45'id_818 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_'8618''45'id_818 :: T_Level_18 -> T_Level_18 -> T_RightInverse_1880
d_'8618''45'id_818 ~T_Level_18
v0 ~T_Level_18
v1 = T_RightInverse_1880
du_'8618''45'id_818
du_'8618''45'id_818 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_'8618''45'id_818 :: T_RightInverse_1880
du_'8618''45'id_818 = T_RightInverse_1880 -> T_RightInverse_1880
forall a b. a -> b
coe T_RightInverse_1880
du_rightInverse_794
-- Function.Construct.Identity._.↔-id
d_'8596''45'id_820 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'8596''45'id_820 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'8596''45'id_820 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_1960
du_'8596''45'id_820
du_'8596''45'id_820 :: MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8596''45'id_820 :: T_Inverse_1960
du_'8596''45'id_820 = T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
du_inverse_796
-- Function.Construct.Identity.id-⟶
d_id'45''10230'_822 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Func_714
d_id'45''10230'_822 :: T_Level_18 -> T_Level_18 -> T_Func_714
d_id'45''10230'_822 T_Level_18
v0 T_Level_18
v1 = T_Func_714 -> T_Func_714
forall a b. a -> b
coe T_Func_714
du_'10230''45'id_806
-- Function.Construct.Identity.id-↣
d_id'45''8611'_824 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Injection_776
d_id'45''8611'_824 :: T_Level_18 -> T_Level_18 -> T_Injection_776
d_id'45''8611'_824 T_Level_18
v0 T_Level_18
v1 = T_Injection_776 -> T_Injection_776
forall a b. a -> b
coe T_Injection_776
du_'8611''45'id_808
-- Function.Construct.Identity.id-↠
d_id'45''8608'_826 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Surjection_846
d_id'45''8608'_826 :: T_Level_18 -> T_Level_18 -> T_Surjection_846
d_id'45''8608'_826 T_Level_18
v0 T_Level_18
v1 = T_Surjection_846 -> T_Surjection_846
forall a b. a -> b
coe T_Surjection_846
du_'8608''45'id_810
-- Function.Construct.Identity.id-⤖
d_id'45''10518'_828 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Bijection_926
d_id'45''10518'_828 :: T_Level_18 -> T_Level_18 -> T_Bijection_926
d_id'45''10518'_828 T_Level_18
v0 T_Level_18
v1 = T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926
du_'10518''45'id_812
-- Function.Construct.Identity.id-⇔
d_id'45''8660'_830 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_id'45''8660'_830 :: T_Level_18 -> T_Level_18 -> T_Equivalence_1714
d_id'45''8660'_830 T_Level_18
v0 T_Level_18
v1 = T_Equivalence_1714 -> T_Equivalence_1714
forall a b. a -> b
coe T_Equivalence_1714
du_'8660''45'id_814
-- Function.Construct.Identity.id-↩
d_id'45''8617'_832 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_id'45''8617'_832 :: T_Level_18 -> T_Level_18 -> T_LeftInverse_1792
d_id'45''8617'_832 T_Level_18
v0 T_Level_18
v1 = T_LeftInverse_1792 -> T_LeftInverse_1792
forall a b. a -> b
coe T_LeftInverse_1792
du_'8617''45'id_816
-- Function.Construct.Identity.id-↪
d_id'45''8618'_834 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_id'45''8618'_834 :: T_Level_18 -> T_Level_18 -> T_RightInverse_1880
d_id'45''8618'_834 T_Level_18
v0 T_Level_18
v1 = T_RightInverse_1880 -> T_RightInverse_1880
forall a b. a -> b
coe T_RightInverse_1880
du_'8618''45'id_818
-- Function.Construct.Identity.id-↔
d_id'45''8596'_836 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_id'45''8596'_836 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_id'45''8596'_836 T_Level_18
v0 T_Level_18
v1 = T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
du_'8596''45'id_820