{-# 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_constructor_54 (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_constructor_54 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_66 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRelMonomorphism_66 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_IsRelMonomorphism_66
  = C_constructor_86 T_IsRelHomomorphism_42
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism.isHomomorphism
d_isHomomorphism_78 ::
  T_IsRelMonomorphism_66 -> T_IsRelHomomorphism_42
d_isHomomorphism_78 :: T_IsRelMonomorphism_66 -> T_IsRelHomomorphism_42
d_isHomomorphism_78 T_IsRelMonomorphism_66
v0
  = case T_IsRelMonomorphism_66 -> T_IsRelMonomorphism_66
forall a b. a -> b
coe T_IsRelMonomorphism_66
v0 of
      C_constructor_86 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_66
_ -> T_IsRelHomomorphism_42
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism.injective
d_injective_80 ::
  T_IsRelMonomorphism_66 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_80 :: T_IsRelMonomorphism_66 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_80 T_IsRelMonomorphism_66
v0
  = case T_IsRelMonomorphism_66 -> T_IsRelMonomorphism_66
forall a b. a -> b
coe T_IsRelMonomorphism_66
v0 of
      C_constructor_86 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_66
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelMonomorphism._.cong
d_cong_84 ::
  T_IsRelMonomorphism_66 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_84 :: T_IsRelMonomorphism_66 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_84 T_IsRelMonomorphism_66
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_66 -> T_IsRelHomomorphism_42)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelMonomorphism_66 -> T_IsRelHomomorphism_42
d_isHomomorphism_78 (T_IsRelMonomorphism_66 -> AgdaAny
forall a b. a -> b
coe T_IsRelMonomorphism_66
v0))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism
d_IsRelIsomorphism_98 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_IsRelIsomorphism_98 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_IsRelIsomorphism_98
  = C_constructor_124 T_IsRelMonomorphism_66
                      (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14)
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism.isMonomorphism
d_isMonomorphism_110 ::
  T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66
d_isMonomorphism_110 :: T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66
d_isMonomorphism_110 T_IsRelIsomorphism_98
v0
  = case T_IsRelIsomorphism_98 -> T_IsRelIsomorphism_98
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0 of
      C_constructor_124 T_IsRelMonomorphism_66
v1 AgdaAny -> T_Σ_14
v2 -> T_IsRelMonomorphism_66 -> T_IsRelMonomorphism_66
forall a b. a -> b
coe T_IsRelMonomorphism_66
v1
      T_IsRelIsomorphism_98
_ -> T_IsRelMonomorphism_66
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism.surjective
d_surjective_112 ::
  T_IsRelIsomorphism_98 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_112 :: T_IsRelIsomorphism_98 -> AgdaAny -> T_Σ_14
d_surjective_112 T_IsRelIsomorphism_98
v0
  = case T_IsRelIsomorphism_98 -> T_IsRelIsomorphism_98
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0 of
      C_constructor_124 T_IsRelMonomorphism_66
v1 AgdaAny -> T_Σ_14
v2 -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> T_Σ_14
v2
      T_IsRelIsomorphism_98
_ -> AgdaAny -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism._.cong
d_cong_116 ::
  T_IsRelIsomorphism_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_116 :: T_IsRelIsomorphism_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_116 T_IsRelIsomorphism_98
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_66 -> T_IsRelHomomorphism_42)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelMonomorphism_66 -> T_IsRelHomomorphism_42
d_isHomomorphism_78 ((T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66
d_isMonomorphism_110 (T_IsRelIsomorphism_98 -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0)))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism._.injective
d_injective_118 ::
  T_IsRelIsomorphism_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_118 :: T_IsRelIsomorphism_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_118 T_IsRelIsomorphism_98
v0
  = (T_IsRelMonomorphism_66
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelMonomorphism_66 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_80 ((T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66
d_isMonomorphism_110 (T_IsRelIsomorphism_98 -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism._.isHomomorphism
d_isHomomorphism_120 ::
  T_IsRelIsomorphism_98 -> T_IsRelHomomorphism_42
d_isHomomorphism_120 :: T_IsRelIsomorphism_98 -> T_IsRelHomomorphism_42
d_isHomomorphism_120 T_IsRelIsomorphism_98
v0
  = (T_IsRelMonomorphism_66 -> T_IsRelHomomorphism_42)
-> AgdaAny -> T_IsRelHomomorphism_42
forall a b. a -> b
coe T_IsRelMonomorphism_66 -> T_IsRelHomomorphism_42
d_isHomomorphism_78 ((T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66
d_isMonomorphism_110 (T_IsRelIsomorphism_98 -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0))
-- Relation.Binary.Morphism.Structures.IsRelIsomorphism.bijective
d_bijective_122 ::
  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_98 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_bijective_122 :: 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_98
-> T_Σ_14
d_bijective_122 ~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_98
v9
  = T_IsRelIsomorphism_98 -> T_Σ_14
du_bijective_122 T_IsRelIsomorphism_98
v9
du_bijective_122 ::
  T_IsRelIsomorphism_98 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_bijective_122 :: T_IsRelIsomorphism_98 -> T_Σ_14
du_bijective_122 T_IsRelIsomorphism_98
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_66
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelMonomorphism_66 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_80 ((T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98 -> T_IsRelMonomorphism_66
d_isMonomorphism_110 (T_IsRelIsomorphism_98 -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0)))
      ((T_IsRelIsomorphism_98 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98 -> AgdaAny -> T_Σ_14
d_surjective_112 (T_IsRelIsomorphism_98 -> AgdaAny
forall a b. a -> b
coe T_IsRelIsomorphism_98
v0))
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism
d_IsOrderHomomorphism_144 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> T_Level_18
d_IsOrderHomomorphism_144 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_144
  = C_constructor_170 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.cong
d_cong_160 ::
  T_IsOrderHomomorphism_144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_160 :: T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_160 T_IsOrderHomomorphism_144
v0
  = case T_IsOrderHomomorphism_144 -> T_IsOrderHomomorphism_144
forall a b. a -> b
coe T_IsOrderHomomorphism_144
v0 of
      C_constructor_170 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_144
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.mono
d_mono_162 ::
  T_IsOrderHomomorphism_144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_162 :: T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_162 T_IsOrderHomomorphism_144
v0
  = case T_IsOrderHomomorphism_144 -> T_IsOrderHomomorphism_144
forall a b. a -> b
coe T_IsOrderHomomorphism_144
v0 of
      C_constructor_170 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_144
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.Eq.isRelHomomorphism
d_isRelHomomorphism_166 ::
  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_144 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_166 :: 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_144
-> T_IsRelHomomorphism_42
d_isRelHomomorphism_166 ~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_144
v13
  = T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_166 T_IsOrderHomomorphism_144
v13
du_isRelHomomorphism_166 ::
  T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_166 :: T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_166 T_IsOrderHomomorphism_144
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_constructor_54 ((T_IsOrderHomomorphism_144
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_160 (T_IsOrderHomomorphism_144 -> AgdaAny
forall a b. a -> b
coe T_IsOrderHomomorphism_144
v0))
-- Relation.Binary.Morphism.Structures.IsOrderHomomorphism.isRelHomomorphism
d_isRelHomomorphism_168 ::
  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_144 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_168 :: 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_144
-> T_IsRelHomomorphism_42
d_isRelHomomorphism_168 ~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_144
v13
  = T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_168 T_IsOrderHomomorphism_144
v13
du_isRelHomomorphism_168 ::
  T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_168 :: T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_168 T_IsOrderHomomorphism_144
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_constructor_54 ((T_IsOrderHomomorphism_144
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_162 (T_IsOrderHomomorphism_144 -> AgdaAny
forall a b. a -> b
coe T_IsOrderHomomorphism_144
v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism
d_IsOrderMonomorphism_190 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> T_Level_18
d_IsOrderMonomorphism_190 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_190
  = C_constructor_228 T_IsOrderHomomorphism_144
                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.isOrderHomomorphism
d_isOrderHomomorphism_208 ::
  T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 :: T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 T_IsOrderMonomorphism_190
v0
  = case T_IsOrderMonomorphism_190 -> T_IsOrderMonomorphism_190
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0 of
      C_constructor_228 T_IsOrderHomomorphism_144
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> T_IsOrderHomomorphism_144 -> T_IsOrderHomomorphism_144
forall a b. a -> b
coe T_IsOrderHomomorphism_144
v1
      T_IsOrderMonomorphism_190
_ -> T_IsOrderHomomorphism_144
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.injective
d_injective_210 ::
  T_IsOrderMonomorphism_190 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_210 :: T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_210 T_IsOrderMonomorphism_190
v0
  = case T_IsOrderMonomorphism_190 -> T_IsOrderMonomorphism_190
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0 of
      C_constructor_228 T_IsOrderHomomorphism_144
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_190
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.cancel
d_cancel_212 ::
  T_IsOrderMonomorphism_190 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_212 :: T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_212 T_IsOrderMonomorphism_190
v0
  = case T_IsOrderMonomorphism_190 -> T_IsOrderMonomorphism_190
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0 of
      C_constructor_228 T_IsOrderHomomorphism_144
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_190
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism._.cong
d_cong_216 ::
  T_IsOrderMonomorphism_190 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_216 :: T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_216 T_IsOrderMonomorphism_190
v0
  = (T_IsOrderHomomorphism_144
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_160 ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism._.isRelHomomorphism
d_isRelHomomorphism_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_190 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_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_190
-> T_IsRelHomomorphism_42
d_isRelHomomorphism_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_190
v13
  = T_IsOrderMonomorphism_190 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_218 T_IsOrderMonomorphism_190
v13
du_isRelHomomorphism_218 ::
  T_IsOrderMonomorphism_190 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_218 :: T_IsOrderMonomorphism_190 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_218 T_IsOrderMonomorphism_190
v0
  = (T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42)
-> AgdaAny -> T_IsRelHomomorphism_42
forall a b. a -> b
coe
      T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_168 ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism._.mono
d_mono_220 ::
  T_IsOrderMonomorphism_190 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_220 :: T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_220 T_IsOrderMonomorphism_190
v0
  = (T_IsOrderHomomorphism_144
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_162 ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.Eq.isRelMonomorphism
d_isRelMonomorphism_224 ::
  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_190 -> T_IsRelMonomorphism_66
d_isRelMonomorphism_224 :: 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_190
-> T_IsRelMonomorphism_66
d_isRelMonomorphism_224 ~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_190
v13
  = T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_224 T_IsOrderMonomorphism_190
v13
du_isRelMonomorphism_224 ::
  T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_224 :: T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_224 T_IsOrderMonomorphism_190
v0
  = (T_IsRelHomomorphism_42
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny -> T_IsRelMonomorphism_66
forall a b. a -> b
coe
      T_IsRelHomomorphism_42
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRelMonomorphism_66
C_constructor_86
      ((T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_166 ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0)))
      ((T_IsOrderMonomorphism_190
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_210 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0))
-- Relation.Binary.Morphism.Structures.IsOrderMonomorphism.isRelMonomorphism
d_isRelMonomorphism_226 ::
  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_190 -> T_IsRelMonomorphism_66
d_isRelMonomorphism_226 :: 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_190
-> T_IsRelMonomorphism_66
d_isRelMonomorphism_226 ~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_190
v13
  = T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_226 T_IsOrderMonomorphism_190
v13
du_isRelMonomorphism_226 ::
  T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_226 :: T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_226 T_IsOrderMonomorphism_190
v0
  = (T_IsRelHomomorphism_42
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny -> T_IsRelMonomorphism_66
forall a b. a -> b
coe
      T_IsRelHomomorphism_42
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRelMonomorphism_66
C_constructor_86
      ((T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_168 ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0)))
      ((T_IsOrderMonomorphism_190
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_212 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism
d_IsOrderIsomorphism_248 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> T_Level_18
d_IsOrderIsomorphism_248 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_248
  = C_constructor_288 T_IsOrderMonomorphism_190
                      (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14)
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism.isOrderMonomorphism
d_isOrderMonomorphism_264 ::
  T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 :: T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 T_IsOrderIsomorphism_248
v0
  = case T_IsOrderIsomorphism_248 -> T_IsOrderIsomorphism_248
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0 of
      C_constructor_288 T_IsOrderMonomorphism_190
v1 AgdaAny -> T_Σ_14
v2 -> T_IsOrderMonomorphism_190 -> T_IsOrderMonomorphism_190
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v1
      T_IsOrderIsomorphism_248
_ -> T_IsOrderMonomorphism_190
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism.surjective
d_surjective_266 ::
  T_IsOrderIsomorphism_248 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_266 :: T_IsOrderIsomorphism_248 -> AgdaAny -> T_Σ_14
d_surjective_266 T_IsOrderIsomorphism_248
v0
  = case T_IsOrderIsomorphism_248 -> T_IsOrderIsomorphism_248
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0 of
      C_constructor_288 T_IsOrderMonomorphism_190
v1 AgdaAny -> T_Σ_14
v2 -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> T_Σ_14
v2
      T_IsOrderIsomorphism_248
_ -> AgdaAny -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.cancel
d_cancel_270 ::
  T_IsOrderIsomorphism_248 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_270 :: T_IsOrderIsomorphism_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_270 T_IsOrderIsomorphism_248
v0
  = (T_IsOrderMonomorphism_190
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cancel_212 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.cong
d_cong_272 ::
  T_IsOrderIsomorphism_248 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_272 :: T_IsOrderIsomorphism_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_272 T_IsOrderIsomorphism_248
v0
  = (T_IsOrderHomomorphism_144
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_160
      ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0)))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.injective
d_injective_274 ::
  T_IsOrderIsomorphism_248 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_274 :: T_IsOrderIsomorphism_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_274 T_IsOrderIsomorphism_248
v0
  = (T_IsOrderMonomorphism_190
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_210 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.isOrderHomomorphism
d_isOrderHomomorphism_276 ::
  T_IsOrderIsomorphism_248 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_276 :: T_IsOrderIsomorphism_248 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_276 T_IsOrderIsomorphism_248
v0
  = (T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> T_IsOrderHomomorphism_144
forall a b. a -> b
coe
      T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.isRelHomomorphism
d_isRelHomomorphism_278 ::
  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_248 -> T_IsRelHomomorphism_42
d_isRelHomomorphism_278 :: 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_248
-> T_IsRelHomomorphism_42
d_isRelHomomorphism_278 ~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_248
v13
  = T_IsOrderIsomorphism_248 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_278 T_IsOrderIsomorphism_248
v13
du_isRelHomomorphism_278 ::
  T_IsOrderIsomorphism_248 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_278 :: T_IsOrderIsomorphism_248 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_278 T_IsOrderIsomorphism_248
v0
  = let v1 :: T_IsOrderMonomorphism_190
v1 = T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> T_IsOrderIsomorphism_248
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0) in
    AgdaAny -> T_IsRelHomomorphism_42
forall a b. a -> b
coe
      ((T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsOrderHomomorphism_144 -> T_IsRelHomomorphism_42
du_isRelHomomorphism_168 ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 (T_IsOrderMonomorphism_190 -> AgdaAny
forall a b. a -> b
coe T_IsOrderMonomorphism_190
v1)))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.isRelMonomorphism
d_isRelMonomorphism_280 ::
  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_248 -> T_IsRelMonomorphism_66
d_isRelMonomorphism_280 :: 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_248
-> T_IsRelMonomorphism_66
d_isRelMonomorphism_280 ~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_248
v13
  = T_IsOrderIsomorphism_248 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_280 T_IsOrderIsomorphism_248
v13
du_isRelMonomorphism_280 ::
  T_IsOrderIsomorphism_248 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_280 :: T_IsOrderIsomorphism_248 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_280 T_IsOrderIsomorphism_248
v0
  = (T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66)
-> AgdaAny -> T_IsRelMonomorphism_66
forall a b. a -> b
coe
      T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_226 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism._.mono
d_mono_282 ::
  T_IsOrderIsomorphism_248 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_282 :: T_IsOrderIsomorphism_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_282 T_IsOrderIsomorphism_248
v0
  = (T_IsOrderHomomorphism_144
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsOrderHomomorphism_144
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono_162
      ((T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsOrderMonomorphism_190 -> T_IsOrderHomomorphism_144
d_isOrderHomomorphism_208 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0)))
-- Relation.Binary.Morphism.Structures.IsOrderIsomorphism.Eq.isRelIsomorphism
d_isRelIsomorphism_286 ::
  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_248 -> T_IsRelIsomorphism_98
d_isRelIsomorphism_286 :: 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_248
-> T_IsRelIsomorphism_98
d_isRelIsomorphism_286 ~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_248
v13
  = T_IsOrderIsomorphism_248 -> T_IsRelIsomorphism_98
du_isRelIsomorphism_286 T_IsOrderIsomorphism_248
v13
du_isRelIsomorphism_286 ::
  T_IsOrderIsomorphism_248 -> T_IsRelIsomorphism_98
du_isRelIsomorphism_286 :: T_IsOrderIsomorphism_248 -> T_IsRelIsomorphism_98
du_isRelIsomorphism_286 T_IsOrderIsomorphism_248
v0
  = (T_IsRelMonomorphism_66
 -> (AgdaAny -> T_Σ_14) -> T_IsRelIsomorphism_98)
-> AgdaAny -> AgdaAny -> T_IsRelIsomorphism_98
forall a b. a -> b
coe
      T_IsRelMonomorphism_66
-> (AgdaAny -> T_Σ_14) -> T_IsRelIsomorphism_98
C_constructor_124
      ((T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsOrderMonomorphism_190 -> T_IsRelMonomorphism_66
du_isRelMonomorphism_224 ((T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> T_IsOrderMonomorphism_190
d_isOrderMonomorphism_264 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0)))
      ((T_IsOrderIsomorphism_248 -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248 -> AgdaAny -> T_Σ_14
d_surjective_266 (T_IsOrderIsomorphism_248 -> AgdaAny
forall a b. a -> b
coe T_IsOrderIsomorphism_248
v0))