{-# 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_52 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsBijection_52 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Function.Construct.Identity._._.IsCongruent
d_IsCongruent_56 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsCongruent_56 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_64 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsInverse_64 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Function.Construct.Identity._._.IsLeftInverse
d_IsLeftInverse_68 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsLeftInverse_68 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Function.Construct.Identity._._.IsRightInverse
d_IsRightInverse_72 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRightInverse_72 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
-- Function.Construct.Identity._._.IsSurjection
d_IsSurjection_76 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsSurjection_76 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Function.Construct.Identity._._.IsBijection.isInjection
d_isInjection_94 ::
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98
d_isInjection_94 :: T_IsBijection_256 -> T_IsInjection_98
d_isInjection_94 T_IsBijection_256
v0
  = (T_IsBijection_256 -> T_IsInjection_98)
-> AgdaAny -> T_IsInjection_98
forall a b. a -> b
coe T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v0)
-- Function.Construct.Identity._._.IsBijection.surjective
d_surjective_100 ::
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_100 :: T_IsBijection_256 -> AgdaAny -> T_Σ_14
d_surjective_100 T_IsBijection_256
v0
  = (T_IsBijection_256 -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_IsBijection_256 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_266 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v0)
-- Function.Construct.Identity._._.IsCongruent.cong
d_cong_156 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_156 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_156 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'_158 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence'8321'_158 :: T_IsCongruent_22 -> T_IsEquivalence_28
d_isEquivalence'8321'_158 T_IsCongruent_22
v0
  = (T_IsCongruent_22 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      T_IsCongruent_22 -> T_IsEquivalence_28
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'_160 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence'8322'_160 :: T_IsCongruent_22 -> T_IsEquivalence_28
d_isEquivalence'8322'_160 T_IsCongruent_22
v0
  = (T_IsCongruent_22 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      T_IsCongruent_22 -> T_IsEquivalence_28
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_218 ::
  MAlonzo.Code.Function.Structures.T_IsInjection_98 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_218 :: T_IsInjection_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_218 T_IsInjection_98
v0
  = (T_IsInjection_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_injective_108 (T_IsInjection_98 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98
v0)
-- Function.Construct.Identity._._.IsInjection.isCongruent
d_isCongruent_220 ::
  MAlonzo.Code.Function.Structures.T_IsInjection_98 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_220 :: T_IsInjection_98 -> T_IsCongruent_22
d_isCongruent_220 T_IsInjection_98
v0
  = (T_IsInjection_98 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106 (T_IsInjection_98 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98
v0)
-- Function.Construct.Identity._._.IsInverse.inverseʳ
d_inverse'691'_284 ::
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_284 :: T_IsInverse_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_284 T_IsInverse_526
v0
  = (T_IsInverse_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_538 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v0)
-- Function.Construct.Identity._._.IsInverse.isLeftInverse
d_isLeftInverse_294 ::
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
d_isLeftInverse_294 :: T_IsInverse_526 -> T_IsLeftInverse_346
d_isLeftInverse_294 T_IsInverse_526
v0
  = (T_IsInverse_526 -> T_IsLeftInverse_346)
-> AgdaAny -> T_IsLeftInverse_346
forall a b. a -> b
coe T_IsInverse_526 -> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.d_isLeftInverse_536 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v0)
-- Function.Construct.Identity._._.IsLeftInverse.from-cong
d_from'45'cong_360 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_360 :: T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_360 T_IsLeftInverse_346
v0
  = (T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_360 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0)
-- Function.Construct.Identity._._.IsLeftInverse.inverseˡ
d_inverse'737'_362 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_362 :: T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_362 T_IsLeftInverse_346
v0
  = (T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_362 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0)
-- Function.Construct.Identity._._.IsLeftInverse.isCongruent
d_isCongruent_364 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_364 :: T_IsLeftInverse_346 -> T_IsCongruent_22
d_isCongruent_364 T_IsLeftInverse_346
v0
  = (T_IsLeftInverse_346 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsLeftInverse_346 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_358 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0)
-- Function.Construct.Identity._._.IsRightInverse.from-cong
d_from'45'cong_430 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_430 :: T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_from'45'cong_430 T_IsRightInverse_438
v0
  = (T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_452 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0)
-- Function.Construct.Identity._._.IsRightInverse.inverseʳ
d_inverse'691'_432 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_432 :: T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_432 T_IsRightInverse_438
v0
  = (T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_454 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0)
-- Function.Construct.Identity._._.IsRightInverse.isCongruent
d_isCongruent_434 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_434 :: T_IsRightInverse_438 -> T_IsCongruent_22
d_isCongruent_434 T_IsRightInverse_438
v0
  = (T_IsRightInverse_438 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsRightInverse_438 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_450 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0)
-- Function.Construct.Identity._._.IsSurjection.isCongruent
d_isCongruent_500 ::
  MAlonzo.Code.Function.Structures.T_IsSurjection_174 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_500 :: T_IsSurjection_174 -> T_IsCongruent_22
d_isCongruent_500 T_IsSurjection_174
v0
  = (T_IsSurjection_174 -> T_IsCongruent_22)
-> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe T_IsSurjection_174 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_182 (T_IsSurjection_174 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174
v0)
-- Function.Construct.Identity._._.IsSurjection.surjective
d_surjective_508 ::
  MAlonzo.Code.Function.Structures.T_IsSurjection_174 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_508 :: T_IsSurjection_174 -> AgdaAny -> T_Σ_14
d_surjective_508 T_IsSurjection_174
v0
  = (T_IsSurjection_174 -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_IsSurjection_174 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_184 (T_IsSurjection_174 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174
v0)
-- Function.Construct.Identity._.isCongruent
d_isCongruent_574 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_574 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsCongruent_22
d_isCongruent_574 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsCongruent_22
du_isCongruent_574 T_IsEquivalence_28
v4
du_isCongruent_574 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
du_isCongruent_574 :: T_IsEquivalence_28 -> T_IsCongruent_22
du_isCongruent_574 T_IsEquivalence_28
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_constructor_94
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3)) (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0) (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)
-- Function.Construct.Identity._.isInjection
d_isInjection_576 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98
d_isInjection_576 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsInjection_98
d_isInjection_576 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsInjection_98
du_isInjection_576 T_IsEquivalence_28
v4
du_isInjection_576 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98
du_isInjection_576 :: T_IsEquivalence_28 -> T_IsInjection_98
du_isInjection_576 T_IsEquivalence_28
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_98)
-> AgdaAny -> AgdaAny -> T_IsInjection_98
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_98
MAlonzo.Code.Function.Structures.C_constructor_170
      ((T_IsEquivalence_28 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> T_IsCongruent_22
du_isCongruent_574 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
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_578 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174
d_isSurjection_578 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsSurjection_174
d_isSurjection_578 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsSurjection_174
du_isSurjection_578 T_IsEquivalence_28
v4
du_isSurjection_578 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174
du_isSurjection_578 :: T_IsEquivalence_28 -> T_IsSurjection_174
du_isSurjection_578 T_IsEquivalence_28
v0
  = (T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_174)
-> AgdaAny -> AgdaAny -> T_IsSurjection_174
forall a b. a -> b
coe
      T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_174
MAlonzo.Code.Function.Structures.C_constructor_252
      ((T_IsEquivalence_28 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> T_IsCongruent_22
du_isCongruent_574 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
du_surjective_26)
-- Function.Construct.Identity._.isBijection
d_isBijection_580 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
d_isBijection_580 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsBijection_256
d_isBijection_580 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsBijection_256
du_isBijection_580 T_IsEquivalence_28
v4
du_isBijection_580 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
du_isBijection_580 :: T_IsEquivalence_28 -> T_IsBijection_256
du_isBijection_580 T_IsEquivalence_28
v0
  = (T_IsInjection_98 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_256)
-> AgdaAny -> AgdaAny -> T_IsBijection_256
forall a b. a -> b
coe
      T_IsInjection_98 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_256
MAlonzo.Code.Function.Structures.C_constructor_340
      ((T_IsEquivalence_28 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> T_IsInjection_98
du_isInjection_576 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)) ((AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
du_surjective_26)
-- Function.Construct.Identity._.isLeftInverse
d_isLeftInverse_582 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
d_isLeftInverse_582 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsLeftInverse_346
d_isLeftInverse_582 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsLeftInverse_346
du_isLeftInverse_582 T_IsEquivalence_28
v4
du_isLeftInverse_582 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
du_isLeftInverse_582 :: T_IsEquivalence_28 -> T_IsLeftInverse_346
du_isLeftInverse_582 T_IsEquivalence_28
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_346)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLeftInverse_346
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.C_constructor_432
      ((T_IsEquivalence_28 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> T_IsCongruent_22
du_isCongruent_574 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
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_584 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438
d_isRightInverse_584 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsRightInverse_438
d_isRightInverse_584 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsRightInverse_438
du_isRightInverse_584 T_IsEquivalence_28
v4
du_isRightInverse_584 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438
du_isRightInverse_584 :: T_IsEquivalence_28 -> T_IsRightInverse_438
du_isRightInverse_584 T_IsEquivalence_28
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRightInverse_438)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRightInverse_438
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRightInverse_438
MAlonzo.Code.Function.Structures.C_constructor_520
      ((T_IsEquivalence_28 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> T_IsCongruent_22
du_isCongruent_574 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
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_586 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526
d_isInverse_586 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsInverse_526
d_isInverse_586 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsInverse_526
du_isInverse_586 T_IsEquivalence_28
v4
du_isInverse_586 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526
du_isInverse_586 :: T_IsEquivalence_28 -> T_IsInverse_526
du_isInverse_586 T_IsEquivalence_28
v0
  = (T_IsLeftInverse_346
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_526)
-> AgdaAny -> AgdaAny -> T_IsInverse_526
forall a b. a -> b
coe
      T_IsLeftInverse_346
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_526
MAlonzo.Code.Function.Structures.C_constructor_618
      ((T_IsEquivalence_28 -> T_IsLeftInverse_346) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> T_IsLeftInverse_346
du_isLeftInverse_582 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
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_622 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d_function_622 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Func_774
d_function_622 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Func_774
du_function_622
du_function_622 :: MAlonzo.Code.Function.Bundles.T_Func_774
du_function_622 :: T_Func_774
du_function_622
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_774)
-> AgdaAny -> AgdaAny -> T_Func_774
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_774
MAlonzo.Code.Function.Bundles.C_constructor_840 ((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_624 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
d_injection_624 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Injection_842
d_injection_624 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Injection_842
du_injection_624
du_injection_624 :: MAlonzo.Code.Function.Bundles.T_Injection_842
du_injection_624 :: T_Injection_842
du_injection_624
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Injection_842)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Injection_842
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Injection_842
MAlonzo.Code.Function.Bundles.C_constructor_916 ((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_626 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d_surjection_626 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Surjection_918
d_surjection_626 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Surjection_918
du_surjection_626
du_surjection_626 :: MAlonzo.Code.Function.Bundles.T_Surjection_918
du_surjection_626 :: T_Surjection_918
du_surjection_626
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14)
 -> T_Surjection_918)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Surjection_918
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_918
MAlonzo.Code.Function.Bundles.C_constructor_1002 ((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_628 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_bijection_628 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Bijection_1004
d_bijection_628 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Bijection_1004
du_bijection_628
du_bijection_628 :: MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_bijection_628 :: T_Bijection_1004
du_bijection_628
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Bijection_1004)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_1004
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Bijection_1004
MAlonzo.Code.Function.Bundles.C_constructor_1094 ((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_630 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_equivalence_630 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Equivalence_1858
d_equivalence_630 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Equivalence_1858
du_equivalence_630
du_equivalence_630 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_equivalence_630 :: T_Equivalence_1858
du_equivalence_630
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.C_constructor_1940 ((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_632 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_leftInverse_632 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_LeftInverse_1942
d_leftInverse_632 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_LeftInverse_1942
du_leftInverse_632
du_leftInverse_632 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_leftInverse_632 :: T_LeftInverse_1942
du_leftInverse_632
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1942)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1942
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942
MAlonzo.Code.Function.Bundles.C_constructor_2034 ((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_634 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_rightInverse_634 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_RightInverse_2036
d_rightInverse_634 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_RightInverse_2036
du_rightInverse_634
du_rightInverse_634 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_rightInverse_634 :: T_RightInverse_2036
du_rightInverse_634
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_2036)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_2036
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.C_constructor_2120 ((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_636 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_inverse_636 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Inverse_2122
d_inverse_636 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Inverse_2122
du_inverse_636
du_inverse_636 :: MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_inverse_636 :: T_Inverse_2122
du_inverse_636
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_2122)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_2122
MAlonzo.Code.Function.Bundles.C_constructor_2220 ((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_646 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Func_774
d_'10230''45'id_646 :: T_Level_18 -> T_Level_18 -> T_Func_774
d_'10230''45'id_646 ~T_Level_18
v0 ~T_Level_18
v1 = T_Func_774
du_'10230''45'id_646
du_'10230''45'id_646 :: MAlonzo.Code.Function.Bundles.T_Func_774
du_'10230''45'id_646 :: T_Func_774
du_'10230''45'id_646 = T_Func_774 -> T_Func_774
forall a b. a -> b
coe T_Func_774
du_function_622
-- Function.Construct.Identity._.↣-id
d_'8611''45'id_648 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Injection_842
d_'8611''45'id_648 :: T_Level_18 -> T_Level_18 -> T_Injection_842
d_'8611''45'id_648 ~T_Level_18
v0 ~T_Level_18
v1 = T_Injection_842
du_'8611''45'id_648
du_'8611''45'id_648 ::
  MAlonzo.Code.Function.Bundles.T_Injection_842
du_'8611''45'id_648 :: T_Injection_842
du_'8611''45'id_648 = T_Injection_842 -> T_Injection_842
forall a b. a -> b
coe T_Injection_842
du_injection_624
-- Function.Construct.Identity._.↠-id
d_'8608''45'id_650 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Surjection_918
d_'8608''45'id_650 :: T_Level_18 -> T_Level_18 -> T_Surjection_918
d_'8608''45'id_650 ~T_Level_18
v0 ~T_Level_18
v1 = T_Surjection_918
du_'8608''45'id_650
du_'8608''45'id_650 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du_'8608''45'id_650 :: T_Surjection_918
du_'8608''45'id_650 = T_Surjection_918 -> T_Surjection_918
forall a b. a -> b
coe T_Surjection_918
du_surjection_626
-- Function.Construct.Identity._.⤖-id
d_'10518''45'id_652 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_'10518''45'id_652 :: T_Level_18 -> T_Level_18 -> T_Bijection_1004
d_'10518''45'id_652 ~T_Level_18
v0 ~T_Level_18
v1 = T_Bijection_1004
du_'10518''45'id_652
du_'10518''45'id_652 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_'10518''45'id_652 :: T_Bijection_1004
du_'10518''45'id_652 = T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004
du_bijection_628
-- Function.Construct.Identity._.⇔-id
d_'8660''45'id_654 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_'8660''45'id_654 :: T_Level_18 -> T_Level_18 -> T_Equivalence_1858
d_'8660''45'id_654 ~T_Level_18
v0 ~T_Level_18
v1 = T_Equivalence_1858
du_'8660''45'id_654
du_'8660''45'id_654 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'8660''45'id_654 :: T_Equivalence_1858
du_'8660''45'id_654 = T_Equivalence_1858 -> T_Equivalence_1858
forall a b. a -> b
coe T_Equivalence_1858
du_equivalence_630
-- Function.Construct.Identity._.↩-id
d_'8617''45'id_656 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_'8617''45'id_656 :: T_Level_18 -> T_Level_18 -> T_LeftInverse_1942
d_'8617''45'id_656 ~T_Level_18
v0 ~T_Level_18
v1 = T_LeftInverse_1942
du_'8617''45'id_656
du_'8617''45'id_656 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_'8617''45'id_656 :: T_LeftInverse_1942
du_'8617''45'id_656 = T_LeftInverse_1942 -> T_LeftInverse_1942
forall a b. a -> b
coe T_LeftInverse_1942
du_leftInverse_632
-- Function.Construct.Identity._.↪-id
d_'8618''45'id_658 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_'8618''45'id_658 :: T_Level_18 -> T_Level_18 -> T_RightInverse_2036
d_'8618''45'id_658 ~T_Level_18
v0 ~T_Level_18
v1 = T_RightInverse_2036
du_'8618''45'id_658
du_'8618''45'id_658 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_'8618''45'id_658 :: T_RightInverse_2036
du_'8618''45'id_658 = T_RightInverse_2036 -> T_RightInverse_2036
forall a b. a -> b
coe T_RightInverse_2036
du_rightInverse_634
-- Function.Construct.Identity._.↔-id
d_'8596''45'id_660 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8596''45'id_660 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'8596''45'id_660 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_2122
du_'8596''45'id_660
du_'8596''45'id_660 :: MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8596''45'id_660 :: T_Inverse_2122
du_'8596''45'id_660 = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
du_inverse_636
-- Function.Construct.Identity.id-⟶
d_id'45''10230'_662 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Func_774
d_id'45''10230'_662 :: T_Level_18 -> T_Level_18 -> T_Func_774
d_id'45''10230'_662 T_Level_18
v0 T_Level_18
v1 = T_Func_774 -> T_Func_774
forall a b. a -> b
coe T_Func_774
du_'10230''45'id_646
-- Function.Construct.Identity.id-↣
d_id'45''8611'_664 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Injection_842
d_id'45''8611'_664 :: T_Level_18 -> T_Level_18 -> T_Injection_842
d_id'45''8611'_664 T_Level_18
v0 T_Level_18
v1 = T_Injection_842 -> T_Injection_842
forall a b. a -> b
coe T_Injection_842
du_'8611''45'id_648
-- Function.Construct.Identity.id-↠
d_id'45''8608'_666 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Surjection_918
d_id'45''8608'_666 :: T_Level_18 -> T_Level_18 -> T_Surjection_918
d_id'45''8608'_666 T_Level_18
v0 T_Level_18
v1 = T_Surjection_918 -> T_Surjection_918
forall a b. a -> b
coe T_Surjection_918
du_'8608''45'id_650
-- Function.Construct.Identity.id-⤖
d_id'45''10518'_668 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_id'45''10518'_668 :: T_Level_18 -> T_Level_18 -> T_Bijection_1004
d_id'45''10518'_668 T_Level_18
v0 T_Level_18
v1 = T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004
du_'10518''45'id_652
-- Function.Construct.Identity.id-⇔
d_id'45''8660'_670 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_id'45''8660'_670 :: T_Level_18 -> T_Level_18 -> T_Equivalence_1858
d_id'45''8660'_670 T_Level_18
v0 T_Level_18
v1 = T_Equivalence_1858 -> T_Equivalence_1858
forall a b. a -> b
coe T_Equivalence_1858
du_'8660''45'id_654
-- Function.Construct.Identity.id-↩
d_id'45''8617'_672 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_id'45''8617'_672 :: T_Level_18 -> T_Level_18 -> T_LeftInverse_1942
d_id'45''8617'_672 T_Level_18
v0 T_Level_18
v1 = T_LeftInverse_1942 -> T_LeftInverse_1942
forall a b. a -> b
coe T_LeftInverse_1942
du_'8617''45'id_656
-- Function.Construct.Identity.id-↪
d_id'45''8618'_674 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_id'45''8618'_674 :: T_Level_18 -> T_Level_18 -> T_RightInverse_2036
d_id'45''8618'_674 T_Level_18
v0 T_Level_18
v1 = T_RightInverse_2036 -> T_RightInverse_2036
forall a b. a -> b
coe T_RightInverse_2036
du_'8618''45'id_658
-- Function.Construct.Identity.id-↔
d_id'45''8596'_676 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_id'45''8596'_676 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_id'45''8596'_676 T_Level_18
v0 T_Level_18
v1 = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
du_'8596''45'id_660