{-# 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.Relation.Binary.Morphism.Structures 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

-- Relation.Binary.Morphism.Structures._.Homomorphic₂
d_Homomorphic'8322'_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> ()
d_Homomorphic'8322'_18 = erased
-- Relation.Binary.Morphism.Structures.IsRelHomomorphism
d_IsRelHomomorphism_42 a0 a1 a2 a3 a4 a5 a6 a7 a8 = ()
newtype T_IsRelHomomorphism_42
  = C_IsRelHomomorphism'46'constructor_371 (AgdaAny ->
                                            AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsRelHomomorphism.cong
d_cong_52 ::
  T_IsRelHomomorphism_42 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_52 v0
  = case coe v0 of
      C_IsRelHomomorphism'46'constructor_371 v1 -> coe v1
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism
d_IsRelMonomorphism_64 a0 a1 a2 a3 a4 a5 a6 a7 a8 = ()
data T_IsRelMonomorphism_64
  = C_IsRelMonomorphism'46'constructor_1081 T_IsRelHomomorphism_42
                                            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism.isHomomorphism
d_isHomomorphism_76 ::
  T_IsRelMonomorphism_64 -> T_IsRelHomomorphism_42
d_isHomomorphism_76 v0
  = case coe v0 of
      C_IsRelMonomorphism'46'constructor_1081 v1 v2 -> coe v1
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism.injective
d_injective_78 ::
  T_IsRelMonomorphism_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_78 v0
  = case coe v0 of
      C_IsRelMonomorphism'46'constructor_1081 v1 v2 -> coe v2
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism._.cong
d_cong_82 ::
  T_IsRelMonomorphism_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_82 v0 = coe d_cong_52 (coe d_isHomomorphism_76 (coe v0))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism
d_IsRelIsomorphism_94 a0 a1 a2 a3 a4 a5 a6 a7 a8 = ()
data T_IsRelIsomorphism_94
  = C_IsRelIsomorphism'46'constructor_2169 T_IsRelMonomorphism_64
                                           (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14)
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism.isMonomorphism
d_isMonomorphism_106 ::
  T_IsRelIsomorphism_94 -> T_IsRelMonomorphism_64
d_isMonomorphism_106 v0
  = case coe v0 of
      C_IsRelIsomorphism'46'constructor_2169 v1 v2 -> coe v1
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism.surjective
d_surjective_108 ::
  T_IsRelIsomorphism_94 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_108 v0
  = case coe v0 of
      C_IsRelIsomorphism'46'constructor_2169 v1 v2 -> coe v2
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism._.cong
d_cong_112 ::
  T_IsRelIsomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_112 v0
  = coe
      d_cong_52
      (coe d_isHomomorphism_76 (coe d_isMonomorphism_106 (coe v0)))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism._.injective
d_injective_114 ::
  T_IsRelIsomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_114 v0
  = coe d_injective_78 (coe d_isMonomorphism_106 (coe v0))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism._.isHomomorphism
d_isHomomorphism_116 ::
  T_IsRelIsomorphism_94 -> T_IsRelHomomorphism_42
d_isHomomorphism_116 v0
  = coe d_isHomomorphism_76 (coe d_isMonomorphism_106 (coe v0))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism.bijective
d_bijective_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsRelIsomorphism_94 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_bijective_118 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
  = du_bijective_118 v9
du_bijective_118 ::
  T_IsRelIsomorphism_94 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_bijective_118 v0
  = coe
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (coe d_injective_78 (coe d_isMonomorphism_106 (coe v0)))
      (coe d_surjective_108 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism
d_IsOrderHomomorphism_138 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
  = ()
data T_IsOrderHomomorphism_138
  = C_IsOrderHomomorphism'46'constructor_4003 (AgdaAny ->
                                               AgdaAny -> AgdaAny -> AgdaAny)
                                              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.cong
d_cong_154 ::
  T_IsOrderHomomorphism_138 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_154 v0
  = case coe v0 of
      C_IsOrderHomomorphism'46'constructor_4003 v1 v2 -> coe v1
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.mono
d_mono_156 ::
  T_IsOrderHomomorphism_138 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_156 v0
  = case coe v0 of
      C_IsOrderHomomorphism'46'constructor_4003 v1 v2 -> coe v2
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.Eq.isRelHomomorphism
d_isRelHomomorphism_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_160 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelHomomorphism_160 v13
du_isRelHomomorphism_160 ::
  T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_160 v0
  = coe
      C_IsRelHomomorphism'46'constructor_371 (coe d_cong_154 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.isRelHomomorphism
d_isRelHomomorphism_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_162 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelHomomorphism_162 v13
du_isRelHomomorphism_162 ::
  T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_162 v0
  = coe
      C_IsRelHomomorphism'46'constructor_371 (coe d_mono_156 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism
d_IsOrderMonomorphism_182 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
  = ()
data T_IsOrderMonomorphism_182
  = C_IsOrderMonomorphism'46'constructor_6709 T_IsOrderHomomorphism_138
                                              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.isOrderHomomorphism
d_isOrderHomomorphism_200 ::
  T_IsOrderMonomorphism_182 -> T_IsOrderHomomorphism_138
d_isOrderHomomorphism_200 v0
  = case coe v0 of
      C_IsOrderMonomorphism'46'constructor_6709 v1 v2 v3 -> coe v1
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.injective
d_injective_202 ::
  T_IsOrderMonomorphism_182 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_202 v0
  = case coe v0 of
      C_IsOrderMonomorphism'46'constructor_6709 v1 v2 v3 -> coe v2
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.cancel
d_cancel_204 ::
  T_IsOrderMonomorphism_182 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_204 v0
  = case coe v0 of
      C_IsOrderMonomorphism'46'constructor_6709 v1 v2 v3 -> coe v3
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism._.cong
d_cong_208 ::
  T_IsOrderMonomorphism_182 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_208 v0
  = coe d_cong_154 (coe d_isOrderHomomorphism_200 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism._.isRelHomomorphism
d_isRelHomomorphism_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderMonomorphism_182 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_210 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelHomomorphism_210 v13
du_isRelHomomorphism_210 ::
  T_IsOrderMonomorphism_182 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_210 v0
  = coe
      du_isRelHomomorphism_162 (coe d_isOrderHomomorphism_200 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism._.mono
d_mono_212 ::
  T_IsOrderMonomorphism_182 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_212 v0
  = coe d_mono_156 (coe d_isOrderHomomorphism_200 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.Eq.isRelMonomorphism
d_isRelMonomorphism_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64
d_isRelMonomorphism_216 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelMonomorphism_216 v13
du_isRelMonomorphism_216 ::
  T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64
du_isRelMonomorphism_216 v0
  = coe
      C_IsRelMonomorphism'46'constructor_1081
      (coe
         du_isRelHomomorphism_160 (coe d_isOrderHomomorphism_200 (coe v0)))
      (coe d_injective_202 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.isRelMonomorphism
d_isRelMonomorphism_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64
d_isRelMonomorphism_218 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelMonomorphism_218 v13
du_isRelMonomorphism_218 ::
  T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64
du_isRelMonomorphism_218 v0
  = coe
      C_IsRelMonomorphism'46'constructor_1081
      (coe
         du_isRelHomomorphism_162 (coe d_isOrderHomomorphism_200 (coe v0)))
      (coe d_cancel_204 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism
d_IsOrderIsomorphism_238 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
  = ()
data T_IsOrderIsomorphism_238
  = C_IsOrderIsomorphism'46'constructor_10541 T_IsOrderMonomorphism_182
                                              (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14)
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism.isOrderMonomorphism
d_isOrderMonomorphism_254 ::
  T_IsOrderIsomorphism_238 -> T_IsOrderMonomorphism_182
d_isOrderMonomorphism_254 v0
  = case coe v0 of
      C_IsOrderIsomorphism'46'constructor_10541 v1 v2 -> coe v1
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism.surjective
d_surjective_256 ::
  T_IsOrderIsomorphism_238 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_256 v0
  = case coe v0 of
      C_IsOrderIsomorphism'46'constructor_10541 v1 v2 -> coe v2
      _ -> MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.cancel
d_cancel_260 ::
  T_IsOrderIsomorphism_238 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_260 v0
  = coe d_cancel_204 (coe d_isOrderMonomorphism_254 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.cong
d_cong_262 ::
  T_IsOrderIsomorphism_238 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_262 v0
  = coe
      d_cong_154
      (coe
         d_isOrderHomomorphism_200 (coe d_isOrderMonomorphism_254 (coe v0)))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.injective
d_injective_264 ::
  T_IsOrderIsomorphism_238 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_264 v0
  = coe d_injective_202 (coe d_isOrderMonomorphism_254 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.isOrderHomomorphism
d_isOrderHomomorphism_266 ::
  T_IsOrderIsomorphism_238 -> T_IsOrderHomomorphism_138
d_isOrderHomomorphism_266 v0
  = coe
      d_isOrderHomomorphism_200 (coe d_isOrderMonomorphism_254 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.isRelHomomorphism
d_isRelHomomorphism_268 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderIsomorphism_238 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_268 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelHomomorphism_268 v13
du_isRelHomomorphism_268 ::
  T_IsOrderIsomorphism_238 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_268 v0
  = let v1 = d_isOrderMonomorphism_254 (coe v0) in
    coe
      du_isRelHomomorphism_162 (coe d_isOrderHomomorphism_200 (coe v1))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.isRelMonomorphism
d_isRelMonomorphism_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderIsomorphism_238 -> T_IsRelMonomorphism_64
d_isRelMonomorphism_270 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                        ~v10 ~v11 ~v12 v13
  = du_isRelMonomorphism_270 v13
du_isRelMonomorphism_270 ::
  T_IsOrderIsomorphism_238 -> T_IsRelMonomorphism_64
du_isRelMonomorphism_270 v0
  = coe
      du_isRelMonomorphism_218 (coe d_isOrderMonomorphism_254 (coe v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.mono
d_mono_272 ::
  T_IsOrderIsomorphism_238 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_272 v0
  = coe
      d_mono_156
      (coe
         d_isOrderHomomorphism_200 (coe d_isOrderMonomorphism_254 (coe v0)))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism.Eq.isRelIsomorphism
d_isRelIsomorphism_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  MAlonzo.Code.Agda.Primitive.T_Level_14 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  T_IsOrderIsomorphism_238 -> T_IsRelIsomorphism_94
d_isRelIsomorphism_276 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 ~v12 v13
  = du_isRelIsomorphism_276 v13
du_isRelIsomorphism_276 ::
  T_IsOrderIsomorphism_238 -> T_IsRelIsomorphism_94
du_isRelIsomorphism_276 v0
  = coe
      C_IsRelIsomorphism'46'constructor_2169
      (coe
         du_isRelMonomorphism_216 (coe d_isOrderMonomorphism_254 (coe v0)))
      (coe d_surjective_256 (coe v0))