{-# 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.Properties.Poset where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Consequences
import qualified MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
import qualified MAlonzo.Code.Relation.Binary.Properties.Preorder
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Binary.Properties.Poset._._≳_
d__'8819'__24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> ()
d__'8819'__24 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8819'__24 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset._._⋦_
d__'8934'__26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> ()
d__'8934'__26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8934'__26 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset._.Eq._≉_
d__'8777'__64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> ()
d__'8777'__64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8777'__64 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset.PreorderProperties.converse-isPreorder
d_converse'45'isPreorder_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_converse'45'isPreorder_134 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_IsPreorder_70
d_converse'45'isPreorder_134 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314 -> T_IsPreorder_70
du_converse'45'isPreorder_134 T_Poset_314
v3
du_converse'45'isPreorder_134 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_converse'45'isPreorder_134 :: T_Poset_314 -> T_IsPreorder_70
du_converse'45'isPreorder_134 T_Poset_314
v0
  = (T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_converse'45'isPreorder_78
      ((T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset.PreorderProperties.converse-preorder
d_converse'45'preorder_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_converse'45'preorder_136 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_Preorder_132
d_converse'45'preorder_136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314 -> T_Preorder_132
du_converse'45'preorder_136 T_Poset_314
v3
du_converse'45'preorder_136 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_converse'45'preorder_136 :: T_Poset_314 -> T_Preorder_132
du_converse'45'preorder_136 T_Poset_314
v0
  = (T_Preorder_132 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_Preorder_132 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_converse'45'preorder_80
      ((T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset.≥-isPartialOrder
d_'8805''45'isPartialOrder_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8805''45'isPartialOrder_142 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_IsPartialOrder_174
d_'8805''45'isPartialOrder_142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314 -> T_IsPartialOrder_174
du_'8805''45'isPartialOrder_142 T_Poset_314
v3
du_'8805''45'isPartialOrder_142 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_'8805''45'isPartialOrder_142 :: T_Poset_314 -> T_IsPartialOrder_174
du_'8805''45'isPartialOrder_142 T_Poset_314
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_converse'45'isPreorder_78
         ((T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
              (T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                 (T_Poset_314 -> T_Poset_314
forall a b. a -> b
coe T_Poset_314
v0))
              AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3))
-- Relation.Binary.Properties.Poset.≥-poset
d_'8805''45'poset_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8805''45'poset_144 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_Poset_314
d_'8805''45'poset_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 = T_Poset_314 -> T_Poset_314
du_'8805''45'poset_144 T_Poset_314
v3
du_'8805''45'poset_144 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_'8805''45'poset_144 :: T_Poset_314 -> T_Poset_314
du_'8805''45'poset_144 T_Poset_314
v0
  = (T_IsPartialOrder_174 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
du_'8805''45'isPartialOrder_142 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset._.antisym
d_antisym_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_148 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
  = T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_148 T_Poset_314
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
du_antisym_148 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_148 :: T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_148 T_Poset_314
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
  = (T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
      (T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
         (T_Poset_314 -> T_Poset_314
forall a b. a -> b
coe T_Poset_314
v0))
      AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3
-- Relation.Binary.Properties.Poset._.refl
d_refl_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny
d_refl_150 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_314 -> AgdaAny -> AgdaAny
d_refl_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_150 T_Poset_314
v3
du_refl_150 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny
du_refl_150 :: T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_150 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Poset_314
du_'8805''45'poset_144 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2
             = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       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
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Properties.Poset._.reflexive
d_reflexive_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_152 T_Poset_314
v3
du_reflexive_152 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_152 :: T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_152 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Poset_314
du_'8805''45'poset_144 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))))
-- Relation.Binary.Properties.Poset._.trans
d_trans_154 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_154 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_154 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_154 T_Poset_314
v3
du_trans_154 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_154 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_154 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Poset_314
du_'8805''45'poset_144 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
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
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))))
-- Relation.Binary.Properties.Poset.≰-respˡ-≈
d_'8816''45'resp'737''45''8776'_156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8816''45'resp'737''45''8776'_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8816''45'resp'737''45''8776'_156 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset.≰-respʳ-≈
d_'8816''45'resp'691''45''8776'_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8816''45'resp'691''45''8776'_162 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8816''45'resp'691''45''8776'_162 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset._<_
d__'60'__168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__168 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset.<-isStrictPartialOrder
d_'60''45'isStrictPartialOrder_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_170 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_170 T_Poset_314
v3
du_'60''45'isStrictPartialOrder_170 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_170 :: T_Poset_314 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_170 T_Poset_314
v0
  = (T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'60''45'isStrictPartialOrder_444
      ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset.<-strictPartialOrder
d_'60''45'strictPartialOrder_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314 -> T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_172 T_Poset_314
v3
du_'60''45'strictPartialOrder_172 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_172 :: T_Poset_314 -> T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_172 T_Poset_314
v0
  = (T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556)
-> AgdaAny -> T_StrictPartialOrder_556
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_11097
      ((T_Poset_314 -> T_IsStrictPartialOrder_290) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_170 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset._._≮_
d__'8814'__176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny -> AgdaAny -> ()
d__'8814'__176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8814'__176 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset._.asym
d_asym_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_asym_178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_asym_178 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset._.irrefl
d_irrefl_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
d_irrefl_180 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset._.<-resp-≈
d_'60''45'resp'45''8776'_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'45''8776'_182 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_Σ_14
d_'60''45'resp'45''8776'_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314 -> T_Σ_14
du_'60''45'resp'45''8776'_182 T_Poset_314
v3
du_'60''45'resp'45''8776'_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'45''8776'_182 :: T_Poset_314 -> T_Σ_14
du_'60''45'resp'45''8776'_182 T_Poset_314
v0
  = (T_IsStrictPartialOrder_290 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
      ((T_Poset_314 -> T_IsStrictPartialOrder_290) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_170 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset._.<-respʳ-≈
d_'60''45'resp'691''45''8776'_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'691''45''8776'_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'691''45''8776'_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'691''45''8776'_184 T_Poset_314
v3
du_'60''45'resp'691''45''8776'_184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'691''45''8776'_184 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'691''45''8776'_184 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_StrictPartialOrder_556) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_172 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsStrictPartialOrder_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'60''45'resp'691''45''8776'_328
         ((T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_578
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Properties.Poset._.<-respˡ-≈
d_'60''45'resp'737''45''8776'_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'737''45''8776'_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'737''45''8776'_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3
  = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'737''45''8776'_186 T_Poset_314
v3
du_'60''45'resp'737''45''8776'_186 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'737''45''8776'_186 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'737''45''8776'_186 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_StrictPartialOrder_556) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_172 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsStrictPartialOrder_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'60''45'resp'737''45''8776'_330
         ((T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_578
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Properties.Poset._.trans
d_trans_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_trans_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_trans_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_trans_188 T_Poset_314
v3
du_trans_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_trans_188 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_trans_188 T_Poset_314
v0
  = (T_IsStrictPartialOrder_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_306
      ((T_Poset_314 -> T_IsStrictPartialOrder_290) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_170 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Properties.Poset.<⇒≉
d_'60''8658''8777'_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''8658''8777'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
d_'60''8658''8777'_194 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset.≤∧≉⇒<
d_'8804''8743''8777''8658''60'_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''8743''8777''8658''60'_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
d_'8804''8743''8777''8658''60'_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Poset_314
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
du_'8804''8743''8777''8658''60'_200
du_'8804''8743''8777''8658''60'_200 ::
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''8743''8777''8658''60'_200 :: AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
du_'8804''8743''8777''8658''60'_200
  = (AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14)
-> AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'8804''8743''8777''8658''60'_44
-- Relation.Binary.Properties.Poset.<⇒≱
d_'60''8658''8817'_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''8658''8817'_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
d_'60''8658''8817'_206 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset.≤⇒≯
d_'8804''8658''8815'_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8804''8658''8815'_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
d_'8804''8658''8815'_212 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset.≤-dec⇒≈-dec
d_'8804''45'dec'8658''8776''45'dec_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8804''45'dec'8658''8776''45'dec_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_'8804''45'dec'8658''8776''45'dec_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny
v5 AgdaAny
v6
  = T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_214 T_Poset_314
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny
v5 AgdaAny
v6
du_'8804''45'dec'8658''8776''45'dec_214 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_214 :: T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_214 T_Poset_314
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = let v4 :: t
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3 in
    AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      (let v5 :: t
v5 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v3 AgdaAny
v2 in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v4 of
            MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
              -> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
                   then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v7 of
                          MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v8
                            -> case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
                                        then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
                                               MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v11
                                                 -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                      Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                      (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
                                                      ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                         ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                            T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
                                                            (T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
                                                               (T_Poset_314 -> T_Poset_314
forall a b. a -> b
coe T_Poset_314
v0))
                                                            AgdaAny
v2 AgdaAny
v3 AgdaAny
v8 AgdaAny
v11))
                                               T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                        else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
                                               ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                  Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                  (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
                                                  (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
                                                     T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                                 T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                          T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                   else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
                          ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
                             (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
            T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
-- Relation.Binary.Properties.Poset.≤-dec⇒isDecPartialOrder
d_'8804''45'dec'8658'isDecPartialOrder_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
d_'8804''45'dec'8658'isDecPartialOrder_258 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_224
d_'8804''45'dec'8658'isDecPartialOrder_258 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4
  = T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecPartialOrder_224
du_'8804''45'dec'8658'isDecPartialOrder_258 T_Poset_314
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4
du_'8804''45'dec'8658'isDecPartialOrder_258 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
du_'8804''45'dec'8658'isDecPartialOrder_258 :: T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecPartialOrder_224
du_'8804''45'dec'8658'isDecPartialOrder_258 T_Poset_314
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1
  = (T_IsPartialOrder_174
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecPartialOrder_224)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_224
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_224
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_11683
      ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
      ((T_Poset_314
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_214 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1))
      ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1)
-- Relation.Binary.Properties.Poset.mono⇒cong
d_mono'8658'cong_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono'8658'cong_264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_mono'8658'cong_264 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 AgdaAny -> AgdaAny
v4
  = T_Poset_314
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_264 T_Poset_314
v3 AgdaAny -> AgdaAny
v4
du_mono'8658'cong_264 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_mono'8658'cong_264 :: T_Poset_314
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_264 T_Poset_314
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Consequences.du_mono'8658'cong_276
      (let v2 :: t
v2
             = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v3 :: t
v3
                = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Preorder_132 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)))))
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
               (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))))
      ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
            (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
-- Relation.Binary.Properties.Poset.antimono⇒cong
d_antimono'8658'cong_268 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antimono'8658'cong_268 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_314
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antimono'8658'cong_268 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_314
v3 AgdaAny -> AgdaAny
v4
  = T_Poset_314
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_268 T_Poset_314
v3 AgdaAny -> AgdaAny
v4
du_antimono'8658'cong_268 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antimono'8658'cong_268 :: T_Poset_314
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_268 T_Poset_314
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Consequences.du_antimono'8658'cong_290
      (let v2 :: t
v2
             = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
                 T_Poset_314 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v3 :: t
v3
                = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Preorder_132 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)))))
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
               (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))))
      ((T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
            (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)