{-# 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.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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Consequences
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Nullary

-- Relation.Binary.Structures.IsPartialEquivalence
d_IsPartialEquivalence_16 :: p -> p -> p -> p -> ()
d_IsPartialEquivalence_16 p
a0 p
a1 p
a2 p
a3 = ()
data T_IsPartialEquivalence_16
  = C_IsPartialEquivalence'46'constructor_273 (AgdaAny ->
                                               AgdaAny -> AgdaAny -> AgdaAny)
                                              (AgdaAny ->
                                               AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Structures.IsPartialEquivalence.sym
d_sym_22 ::
  T_IsPartialEquivalence_16 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_22 :: T_IsPartialEquivalence_16
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_22 T_IsPartialEquivalence_16
v0
  = case T_IsPartialEquivalence_16 -> T_IsPartialEquivalence_16
forall a b. a -> b
coe T_IsPartialEquivalence_16
v0 of
      C_IsPartialEquivalence'46'constructor_273 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> 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_IsPartialEquivalence_16
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsPartialEquivalence.trans
d_trans_24 ::
  T_IsPartialEquivalence_16 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_24 :: T_IsPartialEquivalence_16
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_24 T_IsPartialEquivalence_16
v0
  = case T_IsPartialEquivalence_16 -> T_IsPartialEquivalence_16
forall a b. a -> b
coe T_IsPartialEquivalence_16
v0 of
      C_IsPartialEquivalence'46'constructor_273 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_IsPartialEquivalence_16
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsEquivalence
d_IsEquivalence_26 :: p -> p -> p -> p -> ()
d_IsEquivalence_26 p
a0 p
a1 p
a2 p
a3 = ()
data T_IsEquivalence_26
  = C_IsEquivalence'46'constructor_743 (AgdaAny -> AgdaAny)
                                       (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                       (AgdaAny ->
                                        AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Structures.IsEquivalence.refl
d_refl_34 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 T_IsEquivalence_26
v0
  = case T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v0 of
      C_IsEquivalence'46'constructor_743 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1
      T_IsEquivalence_26
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsEquivalence.sym
d_sym_36 ::
  T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 T_IsEquivalence_26
v0
  = case T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v0 of
      C_IsEquivalence'46'constructor_743 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> 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_IsEquivalence_26
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsEquivalence.trans
d_trans_38 ::
  T_IsEquivalence_26 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 :: T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 T_IsEquivalence_26
v0
  = case T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v0 of
      C_IsEquivalence'46'constructor_743 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsEquivalence_26
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsEquivalence.reflexive
d_reflexive_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsEquivalence_26 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_40 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_40 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsEquivalence_26
v4 AgdaAny
v5 ~AgdaAny
v6 ~T__'8801'__12
v7
  = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 T_IsEquivalence_26
v4 AgdaAny
v5
du_reflexive_40 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 T_IsEquivalence_26
v0 AgdaAny
v1 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 T_IsEquivalence_26
v0 AgdaAny
v1
-- Relation.Binary.Structures.IsEquivalence.isPartialEquivalence
d_isPartialEquivalence_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsEquivalence_26 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_42 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_26
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_42 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsEquivalence_26
v4
  = T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 T_IsEquivalence_26
v4
du_isPartialEquivalence_42 ::
  T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 :: T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 T_IsEquivalence_26
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialEquivalence_16
C_IsPartialEquivalence'46'constructor_273 ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
      ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
-- Relation.Binary.Structures.IsDecEquivalence
d_IsDecEquivalence_44 :: p -> p -> p -> p -> ()
d_IsDecEquivalence_44 p
a0 p
a1 p
a2 p
a3 = ()
data T_IsDecEquivalence_44
  = C_IsDecEquivalence'46'constructor_3075 T_IsEquivalence_26
                                           (AgdaAny ->
                                            AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32)
-- Relation.Binary.Structures.IsDecEquivalence.isEquivalence
d_isEquivalence_50 :: T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 :: T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 T_IsDecEquivalence_44
v0
  = case T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
forall a b. a -> b
coe T_IsDecEquivalence_44
v0 of
      C_IsDecEquivalence'46'constructor_3075 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 -> T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v1
      T_IsDecEquivalence_44
_ -> T_IsEquivalence_26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecEquivalence._≟_
d__'8799'__52 ::
  T_IsDecEquivalence_44 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__52 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__52 T_IsDecEquivalence_44
v0
  = case T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
forall a b. a -> b
coe T_IsDecEquivalence_44
v0 of
      C_IsDecEquivalence'46'constructor_3075 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2
      T_IsDecEquivalence_44
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecEquivalence._.isPartialEquivalence
d_isPartialEquivalence_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecEquivalence_44 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_56 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_44
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_56 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsDecEquivalence_44
v4
  = T_IsDecEquivalence_44 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_56 T_IsDecEquivalence_44
v4
du_isPartialEquivalence_56 ::
  T_IsDecEquivalence_44 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_56 :: T_IsDecEquivalence_44 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_56 T_IsDecEquivalence_44
v0
  = (T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
-- Relation.Binary.Structures.IsDecEquivalence._.refl
d_refl_58 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny
d_refl_58 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny
d_refl_58 T_IsDecEquivalence_44
v0 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
-- Relation.Binary.Structures.IsDecEquivalence._.reflexive
d_reflexive_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecEquivalence_44 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_60 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_44
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_60 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsDecEquivalence_44
v4 = T_IsDecEquivalence_44
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_60 T_IsDecEquivalence_44
v4
du_reflexive_60 ::
  T_IsDecEquivalence_44 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_60 :: T_IsDecEquivalence_44
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_60 T_IsDecEquivalence_44
v0 AgdaAny
v1 AgdaAny
v2 T__'8801'__12
v3
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0)) AgdaAny
v1
-- Relation.Binary.Structures.IsDecEquivalence._.sym
d_sym_62 ::
  T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_62 :: T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_62 T_IsDecEquivalence_44
v0 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
-- Relation.Binary.Structures.IsDecEquivalence._.trans
d_trans_64 ::
  T_IsDecEquivalence_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_64 :: T_IsDecEquivalence_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_64 T_IsDecEquivalence_44
v0 = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0))
-- Relation.Binary.Structures.IsPreorder
d_IsPreorder_70 :: p -> p -> p -> p -> p -> p -> ()
d_IsPreorder_70 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsPreorder_70
  = C_IsPreorder'46'constructor_3993 T_IsEquivalence_26
                                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                     (AgdaAny ->
                                      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Structures.IsPreorder.isEquivalence
d_isEquivalence_80 :: T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 :: T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 T_IsPreorder_70
v0
  = case T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0 of
      C_IsPreorder'46'constructor_3993 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v1
      T_IsPreorder_70
_ -> T_IsEquivalence_26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsPreorder.reflexive
d_reflexive_82 ::
  T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 T_IsPreorder_70
v0
  = case T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0 of
      C_IsPreorder'46'constructor_3993 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> 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_IsPreorder_70
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsPreorder.trans
d_trans_84 ::
  T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84 T_IsPreorder_70
v0
  = case T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0 of
      C_IsPreorder'46'constructor_3993 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsPreorder_70
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsPreorder.Eq.isPartialEquivalence
d_isPartialEquivalence_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPreorder_70 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_88 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_88 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_88 T_IsPreorder_70
v6
du_isPartialEquivalence_88 ::
  T_IsPreorder_70 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_88 :: T_IsPreorder_70 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_88 T_IsPreorder_70
v0
  = (T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Structures.IsPreorder.Eq.refl
d_refl_90 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny
d_refl_90 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny
d_refl_90 T_IsPreorder_70
v0 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Structures.IsPreorder.Eq.reflexive
d_reflexive_92 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_92 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_92 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 = T_IsPreorder_70 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_92 T_IsPreorder_70
v6
du_reflexive_92 ::
  T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_92 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_92 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 T__'8801'__12
v3
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)) AgdaAny
v1
-- Relation.Binary.Structures.IsPreorder.Eq.sym
d_sym_94 ::
  T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_94 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_94 T_IsPreorder_70
v0 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Structures.IsPreorder.Eq.trans
d_trans_96 ::
  T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_96 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_96 T_IsPreorder_70
v0 = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Structures.IsPreorder.refl
d_refl_98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> AgdaAny -> AgdaAny
d_refl_98 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
d_refl_98 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 = T_IsPreorder_70 -> AgdaAny -> AgdaAny
du_refl_98 T_IsPreorder_70
v6 AgdaAny
v7
du_refl_98 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny
du_refl_98 :: T_IsPreorder_70 -> AgdaAny -> AgdaAny
du_refl_98 T_IsPreorder_70
v0 AgdaAny
v1
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v1
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 (T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0)) AgdaAny
v1)
-- Relation.Binary.Structures.IsPreorder.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_100 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_100 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7
                                    AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_'8764''45'resp'737''45''8776'_100 ::
  T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84 T_IsPreorder_70
v0 AgdaAny
v3 AgdaAny
v2 AgdaAny
v1
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 T_IsPreorder_70
v0 AgdaAny
v3 AgdaAny
v2
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 (T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0)) AgdaAny
v2 AgdaAny
v3 AgdaAny
v4))
      AgdaAny
v5
-- Relation.Binary.Structures.IsPreorder.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_106 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_106 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7
                                    AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_'8764''45'resp'691''45''8776'_106 ::
  T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5 ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 T_IsPreorder_70
v0 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)
-- Relation.Binary.Structures.IsPreorder.∼-resp-≈
d_'8764''45'resp'45''8776'_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPreorder_70 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_112 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_Σ_14
d_'8764''45'resp'45''8776'_112 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70 -> T_Σ_14
du_'8764''45'resp'45''8776'_112 T_IsPreorder_70
v6
du_'8764''45'resp'45''8776'_112 ::
  T_IsPreorder_70 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_112 :: T_IsPreorder_70 -> T_Σ_14
du_'8764''45'resp'45''8776'_112 T_IsPreorder_70
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_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Structures.IsTotalPreorder
d_IsTotalPreorder_118 :: p -> p -> p -> p -> p -> p -> ()
d_IsTotalPreorder_118 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsTotalPreorder_118
  = C_IsTotalPreorder'46'constructor_7939 T_IsPreorder_70
                                          (AgdaAny ->
                                           AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30)
-- Relation.Binary.Structures.IsTotalPreorder.isPreorder
d_isPreorder_126 :: T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 :: T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 T_IsTotalPreorder_118
v0
  = case T_IsTotalPreorder_118 -> T_IsTotalPreorder_118
forall a b. a -> b
coe T_IsTotalPreorder_118
v0 of
      C_IsTotalPreorder'46'constructor_7939 T_IsPreorder_70
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 -> T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v1
      T_IsTotalPreorder_118
_ -> T_IsPreorder_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsTotalPreorder.total
d_total_128 ::
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_128 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> T__'8846'__30
d_total_128 T_IsTotalPreorder_118
v0
  = case T_IsTotalPreorder_118 -> T_IsTotalPreorder_118
forall a b. a -> b
coe T_IsTotalPreorder_118
v0 of
      C_IsTotalPreorder'46'constructor_7939 T_IsPreorder_70
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2
      T_IsTotalPreorder_118
_ -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsTotalPreorder._.isEquivalence
d_isEquivalence_132 :: T_IsTotalPreorder_118 -> T_IsEquivalence_26
d_isEquivalence_132 :: T_IsTotalPreorder_118 -> T_IsEquivalence_26
d_isEquivalence_132 T_IsTotalPreorder_118
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.refl
d_refl_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny
d_refl_134 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalPreorder_118
-> AgdaAny
-> AgdaAny
d_refl_134 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalPreorder_118
v6 = T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny
du_refl_134 T_IsTotalPreorder_118
v6
du_refl_134 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny
du_refl_134 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny
du_refl_134 T_IsTotalPreorder_118
v0 = (T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> AgdaAny
du_refl_98 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.reflexive
d_reflexive_136 ::
  T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_136 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_136 T_IsTotalPreorder_118
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.trans
d_trans_138 ::
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_138 :: T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_138 T_IsTotalPreorder_118
v0 = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.∼-resp-≈
d_'8764''45'resp'45''8776'_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsTotalPreorder_118 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_140 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalPreorder_118
-> T_Σ_14
d_'8764''45'resp'45''8776'_140 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalPreorder_118
v6
  = T_IsTotalPreorder_118 -> T_Σ_14
du_'8764''45'resp'45''8776'_140 T_IsTotalPreorder_118
v6
du_'8764''45'resp'45''8776'_140 ::
  T_IsTotalPreorder_118 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_140 :: T_IsTotalPreorder_118 -> T_Σ_14
du_'8764''45'resp'45''8776'_140 T_IsTotalPreorder_118
v0
  = (T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Σ_14
du_'8764''45'resp'45''8776'_112 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_142 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalPreorder_118
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_142 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalPreorder_118
v6
  = T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_142 T_IsTotalPreorder_118
v6
du_'8764''45'resp'691''45''8776'_142 ::
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_142 :: T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_142 T_IsTotalPreorder_118
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106
      ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_144 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalPreorder_118
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_144 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalPreorder_118
v6
  = T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_144 T_IsTotalPreorder_118
v6
du_'8764''45'resp'737''45''8776'_144 ::
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_144 :: T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_144 T_IsTotalPreorder_118
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100
      ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0))
-- Relation.Binary.Structures.IsTotalPreorder._.Eq.isPartialEquivalence
d_isPartialEquivalence_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsTotalPreorder_118 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_148 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalPreorder_118
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_148 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalPreorder_118
v6
  = T_IsTotalPreorder_118 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_148 T_IsTotalPreorder_118
v6
du_isPartialEquivalence_148 ::
  T_IsTotalPreorder_118 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_148 :: T_IsTotalPreorder_118 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_148 T_IsTotalPreorder_118
v0
  = let v1 :: T_IsPreorder_70
v1 = T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> T_IsTotalPreorder_118
forall a b. a -> b
coe T_IsTotalPreorder_118
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
-- Relation.Binary.Structures.IsTotalPreorder._.Eq.refl
d_refl_150 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny
d_refl_150 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny
d_refl_150 T_IsTotalPreorder_118
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0)))
-- Relation.Binary.Structures.IsTotalPreorder._.Eq.reflexive
d_reflexive_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsTotalPreorder_118 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_152 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalPreorder_118
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_152 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalPreorder_118
v6 = T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_152 T_IsTotalPreorder_118
v6
du_reflexive_152 ::
  T_IsTotalPreorder_118 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_152 :: T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_152 T_IsTotalPreorder_118
v0
  = let v1 :: T_IsPreorder_70
v1 = T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> T_IsTotalPreorder_118
forall a b. a -> b
coe T_IsTotalPreorder_118
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)) AgdaAny
v2)
-- Relation.Binary.Structures.IsTotalPreorder._.Eq.sym
d_sym_154 ::
  T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_154 :: T_IsTotalPreorder_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_154 T_IsTotalPreorder_118
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0)))
-- Relation.Binary.Structures.IsTotalPreorder._.Eq.trans
d_trans_156 ::
  T_IsTotalPreorder_118 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_156 :: T_IsTotalPreorder_118
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_156 T_IsTotalPreorder_118
v0
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsTotalPreorder_118 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118 -> T_IsPreorder_70
d_isPreorder_126 (T_IsTotalPreorder_118 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_118
v0)))
-- Relation.Binary.Structures.IsPartialOrder
d_IsPartialOrder_162 :: p -> p -> p -> p -> p -> p -> ()
d_IsPartialOrder_162 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsPartialOrder_162
  = C_IsPartialOrder'46'constructor_9297 T_IsPreorder_70
                                         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Structures.IsPartialOrder.isPreorder
d_isPreorder_170 :: T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 :: T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 T_IsPartialOrder_162
v0
  = case T_IsPartialOrder_162 -> T_IsPartialOrder_162
forall a b. a -> b
coe T_IsPartialOrder_162
v0 of
      C_IsPartialOrder'46'constructor_9297 T_IsPreorder_70
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v1
      T_IsPartialOrder_162
_ -> T_IsPreorder_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsPartialOrder.antisym
d_antisym_172 ::
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_172 :: T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_172 T_IsPartialOrder_162
v0
  = case T_IsPartialOrder_162 -> T_IsPartialOrder_162
forall a b. a -> b
coe T_IsPartialOrder_162
v0 of
      C_IsPartialOrder'46'constructor_9297 T_IsPreorder_70
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_IsPartialOrder_162
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsPartialOrder._.isEquivalence
d_isEquivalence_176 :: T_IsPartialOrder_162 -> T_IsEquivalence_26
d_isEquivalence_176 :: T_IsPartialOrder_162 -> T_IsEquivalence_26
d_isEquivalence_176 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.refl
d_refl_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPartialOrder_162 -> AgdaAny -> AgdaAny
d_refl_178 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
d_refl_178 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6 = T_IsPartialOrder_162 -> AgdaAny -> AgdaAny
du_refl_178 T_IsPartialOrder_162
v6
du_refl_178 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny
du_refl_178 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny
du_refl_178 T_IsPartialOrder_162
v0 = (T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> AgdaAny
du_refl_98 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.reflexive
d_reflexive_180 ::
  T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_180 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_180 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.trans
d_trans_182 ::
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_182 :: T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_182 T_IsPartialOrder_162
v0 = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.∼-resp-≈
d_'8764''45'resp'45''8776'_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPartialOrder_162 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_184 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> T_Σ_14
d_'8764''45'resp'45''8776'_184 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6
  = T_IsPartialOrder_162 -> T_Σ_14
du_'8764''45'resp'45''8776'_184 T_IsPartialOrder_162
v6
du_'8764''45'resp'45''8776'_184 ::
  T_IsPartialOrder_162 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_184 :: T_IsPartialOrder_162 -> T_Σ_14
du_'8764''45'resp'45''8776'_184 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Σ_14
du_'8764''45'resp'45''8776'_112 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_186 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_186 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6
  = T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_186 T_IsPartialOrder_162
v6
du_'8764''45'resp'691''45''8776'_186 ::
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_186 :: T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_186 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106
      ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_188 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_188 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6
  = T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_188 T_IsPartialOrder_162
v6
du_'8764''45'resp'737''45''8776'_188 ::
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_188 :: T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_188 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100
      ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0))
-- Relation.Binary.Structures.IsPartialOrder._.Eq.isPartialEquivalence
d_isPartialEquivalence_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPartialOrder_162 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_192 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_192 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6
  = T_IsPartialOrder_162 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_192 T_IsPartialOrder_162
v6
du_isPartialEquivalence_192 ::
  T_IsPartialOrder_162 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_192 :: T_IsPartialOrder_162 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_192 T_IsPartialOrder_162
v0
  = let v1 :: T_IsPreorder_70
v1 = T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> T_IsPartialOrder_162
forall a b. a -> b
coe T_IsPartialOrder_162
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
-- Relation.Binary.Structures.IsPartialOrder._.Eq.refl
d_refl_194 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny
d_refl_194 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny
d_refl_194 T_IsPartialOrder_162
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0)))
-- Relation.Binary.Structures.IsPartialOrder._.Eq.reflexive
d_reflexive_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsPartialOrder_162 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_196 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_196 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6 = T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_196 T_IsPartialOrder_162
v6
du_reflexive_196 ::
  T_IsPartialOrder_162 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_196 :: T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_196 T_IsPartialOrder_162
v0
  = let v1 :: T_IsPreorder_70
v1 = T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> T_IsPartialOrder_162
forall a b. a -> b
coe T_IsPartialOrder_162
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)) AgdaAny
v2)
-- Relation.Binary.Structures.IsPartialOrder._.Eq.sym
d_sym_198 ::
  T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_198 :: T_IsPartialOrder_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_198 T_IsPartialOrder_162
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0)))
-- Relation.Binary.Structures.IsPartialOrder._.Eq.trans
d_trans_200 ::
  T_IsPartialOrder_162 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_200 :: T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_200 T_IsPartialOrder_162
v0
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0)))
-- Relation.Binary.Structures.IsDecPartialOrder
d_IsDecPartialOrder_206 :: p -> p -> p -> p -> p -> p -> ()
d_IsDecPartialOrder_206 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsDecPartialOrder_206
  = C_IsDecPartialOrder'46'constructor_10957 T_IsPartialOrder_162
                                             (AgdaAny ->
                                              AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32)
                                             (AgdaAny ->
                                              AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32)
-- Relation.Binary.Structures.IsDecPartialOrder.isPartialOrder
d_isPartialOrder_216 ::
  T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 :: T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 T_IsDecPartialOrder_206
v0
  = case T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0 of
      C_IsDecPartialOrder'46'constructor_10957 T_IsPartialOrder_162
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3 -> T_IsPartialOrder_162 -> T_IsPartialOrder_162
forall a b. a -> b
coe T_IsPartialOrder_162
v1
      T_IsDecPartialOrder_206
_ -> T_IsPartialOrder_162
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecPartialOrder._≟_
d__'8799'__218 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__218 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__218 T_IsDecPartialOrder_206
v0
  = case T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0 of
      C_IsDecPartialOrder'46'constructor_10957 T_IsPartialOrder_162
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2
      T_IsDecPartialOrder_206
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecPartialOrder._≤?_
d__'8804''63'__220 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8804''63'__220 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8804''63'__220 T_IsDecPartialOrder_206
v0
  = case T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0 of
      C_IsDecPartialOrder'46'constructor_10957 T_IsPartialOrder_162
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v3
      T_IsDecPartialOrder_206
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecPartialOrder._.antisym
d_antisym_224 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_224 :: T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_224 T_IsDecPartialOrder_206
v0
  = (T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_172 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))
-- Relation.Binary.Structures.IsDecPartialOrder._.isEquivalence
d_isEquivalence_226 ::
  T_IsDecPartialOrder_206 -> T_IsEquivalence_26
d_isEquivalence_226 :: T_IsDecPartialOrder_206 -> T_IsEquivalence_26
d_isEquivalence_226 T_IsDecPartialOrder_206
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80
      ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
-- Relation.Binary.Structures.IsDecPartialOrder._.isPreorder
d_isPreorder_228 :: T_IsDecPartialOrder_206 -> T_IsPreorder_70
d_isPreorder_228 :: T_IsDecPartialOrder_206 -> T_IsPreorder_70
d_isPreorder_228 T_IsDecPartialOrder_206
v0
  = (T_IsPartialOrder_162 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))
-- Relation.Binary.Structures.IsDecPartialOrder._.refl
d_refl_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
d_refl_230 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
d_refl_230 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6 = T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
du_refl_230 T_IsDecPartialOrder_206
v6
du_refl_230 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
du_refl_230 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
du_refl_230 T_IsDecPartialOrder_206
v0
  = let v1 :: T_IsPartialOrder_162
v1 = T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_IsPreorder_70 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> AgdaAny
du_refl_98 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
-- Relation.Binary.Structures.IsDecPartialOrder._.reflexive
d_reflexive_232 ::
  T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_232 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_232 T_IsDecPartialOrder_206
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_82
      ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
-- Relation.Binary.Structures.IsDecPartialOrder._.trans
d_trans_234 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_234 :: T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_234 T_IsDecPartialOrder_206
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_84
      ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
-- Relation.Binary.Structures.IsDecPartialOrder._.∼-resp-≈
d_'8764''45'resp'45''8776'_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_236 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> T_Σ_14
d_'8764''45'resp'45''8776'_236 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206 -> T_Σ_14
du_'8764''45'resp'45''8776'_236 T_IsDecPartialOrder_206
v6
du_'8764''45'resp'45''8776'_236 ::
  T_IsDecPartialOrder_206 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_236 :: T_IsDecPartialOrder_206 -> T_Σ_14
du_'8764''45'resp'45''8776'_236 T_IsDecPartialOrder_206
v0
  = let v1 :: T_IsPartialOrder_162
v1 = T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_Σ_14
du_'8764''45'resp'45''8776'_112 ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
-- Relation.Binary.Structures.IsDecPartialOrder._.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_238 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_238 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_238 T_IsDecPartialOrder_206
v6
du_'8764''45'resp'691''45''8776'_238 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_238 :: T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_238 T_IsDecPartialOrder_206
v0
  = let v1 :: T_IsPartialOrder_162
v1 = T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_106
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
-- Relation.Binary.Structures.IsDecPartialOrder._.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_240 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_240 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_240 T_IsDecPartialOrder_206
v6
du_'8764''45'resp'737''45''8776'_240 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_240 :: T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_240 T_IsDecPartialOrder_206
v0
  = let v1 :: T_IsPartialOrder_162
v1 = T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_100
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
-- Relation.Binary.Structures.IsDecPartialOrder.Eq.isDecEquivalence
d_isDecEquivalence_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44
d_isDecEquivalence_244 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> T_IsDecEquivalence_44
d_isDecEquivalence_244 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44
du_isDecEquivalence_244 T_IsDecPartialOrder_206
v6
du_isDecEquivalence_244 ::
  T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44
du_isDecEquivalence_244 :: T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44
du_isDecEquivalence_244 T_IsDecPartialOrder_206
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
C_IsDecEquivalence'46'constructor_3075
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))))
      ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__218 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._._≟_
d__'8799'__248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__248 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d__'8799'__248 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6 = T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
du__'8799'__248 T_IsDecPartialOrder_206
v6
du__'8799'__248 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8799'__248 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
du__'8799'__248 T_IsDecPartialOrder_206
v0 = (T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__218 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._.isEquivalence
d_isEquivalence_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> T_IsEquivalence_26
d_isEquivalence_250 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> T_IsEquivalence_26
d_isEquivalence_250 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206 -> T_IsEquivalence_26
du_isEquivalence_250 T_IsDecPartialOrder_206
v6
du_isEquivalence_250 ::
  T_IsDecPartialOrder_206 -> T_IsEquivalence_26
du_isEquivalence_250 :: T_IsDecPartialOrder_206 -> T_IsEquivalence_26
du_isEquivalence_250 T_IsDecPartialOrder_206
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80
      ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._.isPartialEquivalence
d_isPartialEquivalence_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_252 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_252 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_252 T_IsDecPartialOrder_206
v6
du_isPartialEquivalence_252 ::
  T_IsDecPartialOrder_206 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_252 :: T_IsDecPartialOrder_206 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_252 T_IsDecPartialOrder_206
v0
  = let v1 :: t
v1 = (T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44
du_isDecEquivalence_244 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._.refl
d_refl_254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
d_refl_254 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
d_refl_254 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6 = T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
du_refl_254 T_IsDecPartialOrder_206
v6
du_refl_254 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
du_refl_254 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny
du_refl_254 T_IsDecPartialOrder_206
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))))
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._.reflexive
d_reflexive_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_256 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_256 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6 = T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_256 T_IsDecPartialOrder_206
v6
du_reflexive_256 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_256 :: T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_256 T_IsDecPartialOrder_206
v0
  = let v1 :: t
v1 = (T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsDecEquivalence_44
du_isDecEquivalence_244 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)) AgdaAny
v2)
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._.sym
d_sym_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_258 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sym_258 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6 = T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_258 T_IsDecPartialOrder_206
v6
du_sym_258 ::
  T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_258 :: T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_258 T_IsDecPartialOrder_206
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))))
-- Relation.Binary.Structures.IsDecPartialOrder.Eq._.trans
d_trans_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_260 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_260 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6 = T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_260 T_IsDecPartialOrder_206
v6
du_trans_260 ::
  T_IsDecPartialOrder_206 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_260 :: T_IsDecPartialOrder_206
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_260 T_IsDecPartialOrder_206
v0
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
d_isEquivalence_80
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162 -> T_IsPreorder_70
d_isPreorder_170 ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
d_isPartialOrder_216 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0))))
-- Relation.Binary.Structures.IsStrictPartialOrder
d_IsStrictPartialOrder_266 :: p -> p -> p -> p -> p -> p -> ()
d_IsStrictPartialOrder_266 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsStrictPartialOrder_266
  = C_IsStrictPartialOrder'46'constructor_13145 T_IsEquivalence_26
                                                (AgdaAny ->
                                                 AgdaAny ->
                                                 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                                MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-- Relation.Binary.Structures.IsStrictPartialOrder.isEquivalence
d_isEquivalence_278 ::
  T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 :: T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 T_IsStrictPartialOrder_266
v0
  = case T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0 of
      C_IsStrictPartialOrder'46'constructor_13145 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Σ_14
v4 -> T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v1
      T_IsStrictPartialOrder_266
_ -> T_IsEquivalence_26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsStrictPartialOrder.irrefl
d_irrefl_280 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl_280 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
d_irrefl_280 = T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Structures.IsStrictPartialOrder.trans
d_trans_282 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_282 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_282 T_IsStrictPartialOrder_266
v0
  = case T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0 of
      C_IsStrictPartialOrder'46'constructor_13145 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Σ_14
v4 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_IsStrictPartialOrder_266
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsStrictPartialOrder.<-resp-≈
d_'60''45'resp'45''8776'_284 ::
  T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'45''8776'_284 :: T_IsStrictPartialOrder_266 -> T_Σ_14
d_'60''45'resp'45''8776'_284 T_IsStrictPartialOrder_266
v0
  = case T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0 of
      C_IsStrictPartialOrder'46'constructor_13145 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Σ_14
v4 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4
      T_IsStrictPartialOrder_266
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsStrictPartialOrder.Eq.isPartialEquivalence
d_isPartialEquivalence_288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictPartialOrder_266 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_288 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_288 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictPartialOrder_266
v6
  = T_IsStrictPartialOrder_266 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_288 T_IsStrictPartialOrder_266
v6
du_isPartialEquivalence_288 ::
  T_IsStrictPartialOrder_266 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_288 :: T_IsStrictPartialOrder_266 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_288 T_IsStrictPartialOrder_266
v0
  = (T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
-- Relation.Binary.Structures.IsStrictPartialOrder.Eq.refl
d_refl_290 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny
d_refl_290 :: T_IsStrictPartialOrder_266 -> AgdaAny -> AgdaAny
d_refl_290 T_IsStrictPartialOrder_266
v0 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
-- Relation.Binary.Structures.IsStrictPartialOrder.Eq.reflexive
d_reflexive_292 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictPartialOrder_266 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_292 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_292 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictPartialOrder_266
v6 = T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_292 T_IsStrictPartialOrder_266
v6
du_reflexive_292 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_292 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_292 T_IsStrictPartialOrder_266
v0 AgdaAny
v1 AgdaAny
v2 T__'8801'__12
v3
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)) AgdaAny
v1
-- Relation.Binary.Structures.IsStrictPartialOrder.Eq.sym
d_sym_294 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_294 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_294 T_IsStrictPartialOrder_266
v0 = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
-- Relation.Binary.Structures.IsStrictPartialOrder.Eq.trans
d_trans_296 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_296 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_296 T_IsStrictPartialOrder_266
v0 = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
-- Relation.Binary.Structures.IsStrictPartialOrder.asym
d_asym_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictPartialOrder_266 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asym_298 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asym_298 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Structures.IsStrictPartialOrder.<-respʳ-≈
d_'60''45'resp'691''45''8776'_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'60''45'resp'691''45''8776'_304 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'60''45'resp'691''45''8776'_304 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictPartialOrder_266
v6 AgdaAny
v7 AgdaAny
v8
                                  AgdaAny
v9
  = T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_304 T_IsStrictPartialOrder_266
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_'60''45'resp'691''45''8776'_304 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_304 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_304 T_IsStrictPartialOrder_266
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_Σ_14 -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
      (T_IsStrictPartialOrder_266 -> T_Σ_14
d_'60''45'resp'45''8776'_284 (T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)) AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
-- Relation.Binary.Structures.IsStrictPartialOrder.<-respˡ-≈
d_'60''45'resp'737''45''8776'_306 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'60''45'resp'737''45''8776'_306 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'60''45'resp'737''45''8776'_306 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictPartialOrder_266
v6 AgdaAny
v7 AgdaAny
v8
                                  AgdaAny
v9
  = T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_306 T_IsStrictPartialOrder_266
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_'60''45'resp'737''45''8776'_306 ::
  T_IsStrictPartialOrder_266 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_306 :: T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_306 T_IsStrictPartialOrder_266
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_Σ_14 -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
      (T_IsStrictPartialOrder_266 -> T_Σ_14
d_'60''45'resp'45''8776'_284 (T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)) AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
-- Relation.Binary.Structures.IsStrictPartialOrder.asymmetric
d_asymmetric_308 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictPartialOrder_266 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asymmetric_308 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asymmetric_308 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Structures.IsDecStrictPartialOrder
d_IsDecStrictPartialOrder_314 :: p -> p -> p -> p -> p -> p -> ()
d_IsDecStrictPartialOrder_314 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsDecStrictPartialOrder_314
  = C_IsDecStrictPartialOrder'46'constructor_17873 T_IsStrictPartialOrder_266
                                                   (AgdaAny ->
                                                    AgdaAny ->
                                                    MAlonzo.Code.Relation.Nullary.T_Dec_32)
                                                   (AgdaAny ->
                                                    AgdaAny ->
                                                    MAlonzo.Code.Relation.Nullary.T_Dec_32)
-- Relation.Binary.Structures.IsDecStrictPartialOrder.isStrictPartialOrder
d_isStrictPartialOrder_324 ::
  T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 :: T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 T_IsDecStrictPartialOrder_314
v0
  = case T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0 of
      C_IsDecStrictPartialOrder'46'constructor_17873 T_IsStrictPartialOrder_266
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3 -> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1
      T_IsDecStrictPartialOrder_314
_ -> T_IsStrictPartialOrder_266
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecStrictPartialOrder._≟_
d__'8799'__326 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__326 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__326 T_IsDecStrictPartialOrder_314
v0
  = case T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0 of
      C_IsDecStrictPartialOrder'46'constructor_17873 T_IsStrictPartialOrder_266
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2
      T_IsDecStrictPartialOrder_314
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecStrictPartialOrder._<?_
d__'60''63'__328 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'60''63'__328 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'60''63'__328 T_IsDecStrictPartialOrder_314
v0
  = case T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0 of
      C_IsDecStrictPartialOrder'46'constructor_17873 T_IsStrictPartialOrder_266
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v3
      T_IsDecStrictPartialOrder_314
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.<-resp-≈
d_'60''45'resp'45''8776'_332 ::
  T_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'45''8776'_332 :: T_IsDecStrictPartialOrder_314 -> T_Σ_14
d_'60''45'resp'45''8776'_332 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266 -> T_Σ_14
d_'60''45'resp'45''8776'_284
      ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.<-respʳ-≈
d_'60''45'resp'691''45''8776'_334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'60''45'resp'691''45''8776'_334 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'60''45'resp'691''45''8776'_334 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_334 T_IsDecStrictPartialOrder_314
v6
du_'60''45'resp'691''45''8776'_334 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_334 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_334 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'691''45''8776'_304
      ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.<-respˡ-≈
d_'60''45'resp'737''45''8776'_336 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'60''45'resp'737''45''8776'_336 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'60''45'resp'737''45''8776'_336 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_336 T_IsDecStrictPartialOrder_314
v6
du_'60''45'resp'737''45''8776'_336 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_336 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_336 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'60''45'resp'737''45''8776'_306
      ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.asym
d_asym_338 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asym_338 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asym_338 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.asymmetric
d_asymmetric_340 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asymmetric_340 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asymmetric_340 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.irrefl
d_irrefl_342 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl_342 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
d_irrefl_342 = T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.isEquivalence
d_isEquivalence_344 ::
  T_IsDecStrictPartialOrder_314 -> T_IsEquivalence_26
d_isEquivalence_344 :: T_IsDecStrictPartialOrder_314 -> T_IsEquivalence_26
d_isEquivalence_344 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.trans
d_trans_346 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_346 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_346 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_282 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.Eq.isPartialEquivalence
d_isPartialEquivalence_350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_350 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_350 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_350 T_IsDecStrictPartialOrder_314
v6
du_isPartialEquivalence_350 ::
  T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_350 :: T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_350 T_IsDecStrictPartialOrder_314
v0
  = let v1 :: T_IsStrictPartialOrder_266
v1 = T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1)))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.Eq.refl
d_refl_352 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny
d_refl_352 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny
d_refl_352 T_IsDecStrictPartialOrder_314
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34
      ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.Eq.reflexive
d_reflexive_354 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_354 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_354 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6 = T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_354 T_IsDecStrictPartialOrder_314
v6
du_reflexive_354 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_354 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_354 T_IsDecStrictPartialOrder_314
v0
  = let v1 :: T_IsStrictPartialOrder_266
v1 = T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1)) AgdaAny
v2)
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.Eq.sym
d_sym_356 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_356 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_356 T_IsDecStrictPartialOrder_314
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_36
      ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.SPO.Eq.trans
d_trans_358 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_358 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_358 T_IsDecStrictPartialOrder_314
v0
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_38
      ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq.isDecEquivalence
d_isDecEquivalence_362 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44
d_isDecEquivalence_362 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> T_IsDecEquivalence_44
d_isDecEquivalence_362 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44
du_isDecEquivalence_362 T_IsDecStrictPartialOrder_314
v6
du_isDecEquivalence_362 ::
  T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44
du_isDecEquivalence_362 :: T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44
du_isDecEquivalence_362 T_IsDecStrictPartialOrder_314
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
C_IsDecEquivalence'46'constructor_3075
      ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
      ((T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__326 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq._._≟_
d__'8799'__366 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__366 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d__'8799'__366 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6 = T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
du__'8799'__366 T_IsDecStrictPartialOrder_314
v6
du__'8799'__366 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8799'__366 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
du__'8799'__366 T_IsDecStrictPartialOrder_314
v0 = (T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__326 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq._.isEquivalence
d_isEquivalence_368 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 -> T_IsEquivalence_26
d_isEquivalence_368 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> T_IsEquivalence_26
d_isEquivalence_368 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314 -> T_IsEquivalence_26
du_isEquivalence_368 T_IsDecStrictPartialOrder_314
v6
du_isEquivalence_368 ::
  T_IsDecStrictPartialOrder_314 -> T_IsEquivalence_26
du_isEquivalence_368 :: T_IsDecStrictPartialOrder_314 -> T_IsEquivalence_26
du_isEquivalence_368 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq._.isPartialEquivalence
d_isPartialEquivalence_370 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_370 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> T_IsPartialEquivalence_16
d_isPartialEquivalence_370 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_370 T_IsDecStrictPartialOrder_314
v6
du_isPartialEquivalence_370 ::
  T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_370 :: T_IsDecStrictPartialOrder_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_370 T_IsDecStrictPartialOrder_314
v0
  = let v1 :: t
v1 = (T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44)
-> AgdaAny -> t
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44
du_isDecEquivalence_362 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_42 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq._.refl
d_refl_372 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny
d_refl_372 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
d_refl_372 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6 = T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny
du_refl_372 T_IsDecStrictPartialOrder_314
v6
du_refl_372 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny
du_refl_372 :: T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny
du_refl_372 T_IsDecStrictPartialOrder_314
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_34
      ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
d_isEquivalence_278 ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_324 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq._.reflexive
d_reflexive_374 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_374 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_374 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecStrictPartialOrder_314
v6 = T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_374 T_IsDecStrictPartialOrder_314
v6
du_reflexive_374 ::
  T_IsDecStrictPartialOrder_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_374 :: T_IsDecStrictPartialOrder_314
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_374 T_IsDecStrictPartialOrder_314
v0
  = let v1 :: t
v1 = (T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44)
-> AgdaAny -> t
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314 -> T_IsDecEquivalence_44
du_isDecEquivalence_362 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
du_reflexive_40 ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44 -> T_IsEquivalence_26
d_isEquivalence_50 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)) AgdaAny
v2)
-- Relation.Binary.Structures.IsDecStrictPartialOrder.Eq._.sym
d_sym_376 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsDecStrictPartialOrder_314 ->