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