{-# 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__'8777'__22 ::
  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_492 ->
  AgdaAny -> AgdaAny -> ()
d__'8777'__22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8777'__22 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset._._∼ᵒ_
d__'8764''7506'__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_492 ->
  AgdaAny -> AgdaAny -> ()
d__'8764''7506'__26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8764''7506'__26 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset._._≁_
d__'8769'__28 ::
  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_492 ->
  AgdaAny -> AgdaAny -> ()
d__'8769'__28 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8769'__28 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset.PreorderProperties.converse-isPreorder
d_converse'45'isPreorder_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_492 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_converse'45'isPreorder_142 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_492 -> T_IsPreorder_76
d_converse'45'isPreorder_142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492 -> T_IsPreorder_76
du_converse'45'isPreorder_142 T_Poset_492
v3
du_converse'45'isPreorder_142 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_converse'45'isPreorder_142 :: T_Poset_492 -> T_IsPreorder_76
du_converse'45'isPreorder_142 T_Poset_492
v0
  = (T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_converse'45'isPreorder_86
      ((T_Poset_492 -> T_Preorder_142) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_522 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset.PreorderProperties.converse-preorder
d_converse'45'preorder_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_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_converse'45'preorder_144 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_492 -> T_Preorder_142
d_converse'45'preorder_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492 -> T_Preorder_142
du_converse'45'preorder_144 T_Poset_492
v3
du_converse'45'preorder_144 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_converse'45'preorder_144 :: T_Poset_492 -> T_Preorder_142
du_converse'45'preorder_144 T_Poset_492
v0
  = (T_Preorder_142 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_Preorder_142 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_converse'45'preorder_88
      ((T_Poset_492 -> T_Preorder_142) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_522 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset.≥-isPartialOrder
d_'8805''45'isPartialOrder_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_492 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_'8805''45'isPartialOrder_150 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_492 -> T_IsPartialOrder_248
d_'8805''45'isPartialOrder_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492 -> T_IsPartialOrder_248
du_'8805''45'isPartialOrder_150 T_Poset_492
v3
du_'8805''45'isPartialOrder_150 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_'8805''45'isPartialOrder_150 :: T_Poset_492 -> T_IsPartialOrder_248
du_'8805''45'isPartialOrder_150 T_Poset_492
v0
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_converse'45'isPreorder_86
         ((T_Poset_492 -> T_Preorder_142) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_522 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
              (T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
                 (T_Poset_492 -> T_Poset_492
forall a b. a -> b
coe T_Poset_492
v0))
              AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3))
-- Relation.Binary.Properties.Poset.≥-poset
d_'8805''45'poset_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_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_'8805''45'poset_152 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_492 -> T_Poset_492
d_'8805''45'poset_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 = T_Poset_492 -> T_Poset_492
du_'8805''45'poset_152 T_Poset_492
v3
du_'8805''45'poset_152 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_'8805''45'poset_152 :: T_Poset_492 -> T_Poset_492
du_'8805''45'poset_152 T_Poset_492
v0
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_IsPartialOrder_248
du_'8805''45'isPartialOrder_150 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset._.antisym
d_antisym_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_492 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
  = T_Poset_492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_156 T_Poset_492
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
du_antisym_156 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_156 :: T_Poset_492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_156 T_Poset_492
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
  = (T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
      (T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
         (T_Poset_492 -> T_Poset_492
forall a b. a -> b
coe T_Poset_492
v0))
      AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3
-- Relation.Binary.Properties.Poset._.refl
d_refl_158 ::
  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_492 ->
  AgdaAny -> AgdaAny
d_refl_158 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_492 -> AgdaAny -> AgdaAny
d_refl_158 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 = T_Poset_492 -> AgdaAny -> AgdaAny
du_refl_158 T_Poset_492
v3
du_refl_158 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  AgdaAny -> AgdaAny
du_refl_158 :: T_Poset_492 -> AgdaAny -> AgdaAny
du_refl_158 T_Poset_492
v0
  = let v1 :: AgdaAny
v1 = (T_Poset_492 -> T_Poset_492) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_Poset_492
du_'8805''45'poset_152 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: AgdaAny
v2
             = (T_Poset_492 -> T_Preorder_142) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Poset_492 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_522 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
            ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Relation.Binary.Properties.Poset._.reflexive
d_reflexive_160 ::
  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_492 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 = T_Poset_492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_160 T_Poset_492
v3
du_reflexive_160 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_160 :: T_Poset_492 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_160 T_Poset_492
v0
  = let v1 :: AgdaAny
v1 = (T_Poset_492 -> T_Poset_492) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_Poset_492
du_'8805''45'poset_152 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
-- Relation.Binary.Properties.Poset._.trans
d_trans_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_492 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_162 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_162 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 = T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_162 T_Poset_492
v3
du_trans_162 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_162 :: T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_162 T_Poset_492
v0
  = let v1 :: AgdaAny
v1 = (T_Poset_492 -> T_Poset_492) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_Poset_492
du_'8805''45'poset_152 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
-- Relation.Binary.Properties.Poset.≰-respˡ-≈
d_'8816''45'resp'737''45''8776'_164 ::
  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_492 ->
  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'_164 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8816''45'resp'737''45''8776'_164 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> 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'_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_492 ->
  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'_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8816''45'resp'691''45''8776'_170 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset._<_
d__'60'__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_492 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__176 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset.<-isStrictPartialOrder
d_'60''45'isStrictPartialOrder_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_492 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_178 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_178 T_Poset_492
v3
du_'60''45'isStrictPartialOrder_178 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_178 :: T_Poset_492 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_178 T_Poset_492
v0
  = (T_IsPartialOrder_248 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'60''45'isStrictPartialOrder_444
      ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset.<-strictPartialOrder
d_'60''45'strictPartialOrder_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_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_'60''45'strictPartialOrder_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> T_StrictPartialOrder_760
d_'60''45'strictPartialOrder_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492 -> T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_180 T_Poset_492
v3
du_'60''45'strictPartialOrder_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_180 :: T_Poset_492 -> T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_180 T_Poset_492
v0
  = (T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760)
-> AgdaAny -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_842
      ((T_Poset_492 -> T_IsStrictPartialOrder_370) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_178 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset._._≁_
d__'8769'__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_492 ->
  AgdaAny -> AgdaAny -> ()
d__'8769'__184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8769'__184 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Poset._.asym
d_asym_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_492 ->
  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_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_asym_186 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset._.irrefl
d_irrefl_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_492 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
d_irrefl_188 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset._.<-resp-≈
d_'60''45'resp'45''8776'_190 ::
  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_492 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'45''8776'_190 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Poset_492 -> T_Σ_14
d_'60''45'resp'45''8776'_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492 -> T_Σ_14
du_'60''45'resp'45''8776'_190 T_Poset_492
v3
du_'60''45'resp'45''8776'_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'45''8776'_190 :: T_Poset_492 -> T_Σ_14
du_'60''45'resp'45''8776'_190 T_Poset_492
v0
  = (T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
      ((T_Poset_492 -> T_IsStrictPartialOrder_370) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_178 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset._.<-respʳ-≈
d_'60''45'resp'691''45''8776'_192 ::
  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_492 ->
  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'_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'691''45''8776'_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'691''45''8776'_192 T_Poset_492
v3
du_'60''45'resp'691''45''8776'_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  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'_192 :: T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'691''45''8776'_192 T_Poset_492
v0
  = let v1 :: AgdaAny
v1 = (T_Poset_492 -> T_StrictPartialOrder_760) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_180 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'60''45'resp'691''45''8776'_408
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
-- Relation.Binary.Properties.Poset._.<-respˡ-≈
d_'60''45'resp'737''45''8776'_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_492 ->
  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'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'737''45''8776'_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3
  = T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'737''45''8776'_194 T_Poset_492
v3
du_'60''45'resp'737''45''8776'_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  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'_194 :: T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'737''45''8776'_194 T_Poset_492
v0
  = let v1 :: AgdaAny
v1 = (T_Poset_492 -> T_StrictPartialOrder_760) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_180 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'60''45'resp'737''45''8776'_410
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
-- Relation.Binary.Properties.Poset._.trans
d_trans_196 ::
  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_492 ->
  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_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_trans_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 = T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_trans_196 T_Poset_492
v3
du_trans_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  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_196 :: T_Poset_492
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_trans_196 T_Poset_492
v0
  = (T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386
      ((T_Poset_492 -> T_IsStrictPartialOrder_370) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_178 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
-- Relation.Binary.Properties.Poset.<⇒≉
d_'60''8658''8777'_202 ::
  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_492 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''8658''8777'_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
d_'60''8658''8777'_202 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset.≤∧≉⇒<
d_'8804''8743''8777''8658''60'_208 ::
  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_492 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''8743''8777''8658''60'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
d_'8804''8743''8777''8658''60'_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Poset_492
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
du_'8804''8743''8777''8658''60'_208
du_'8804''8743''8777''8658''60'_208 ::
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''8743''8777''8658''60'_208 :: AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
du_'8804''8743''8777''8658''60'_208
  = (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'_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_492 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''8658''8817'_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
d_'60''8658''8817'_214 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Poset.≤⇒≯
d_'8804''8658''8815'_220 ::
  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_492 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8804''8658''8815'_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
d_'8804''8658''8815'_220 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> 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_222 ::
  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_492 ->
  (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_222 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_'8804''45'dec'8658''8776''45'dec_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny
v5 AgdaAny
v6
  = T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_222 T_Poset_492
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny
v5 AgdaAny
v6
du_'8804''45'dec'8658''8776''45'dec_222 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  (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_222 :: T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_222 T_Poset_492
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = let v4 :: AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
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 :: AgdaAny
v5 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
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
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
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_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                            T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
                                                            (T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
                                                               (T_Poset_492 -> T_Poset_492
forall a b. a -> b
coe T_Poset_492
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_266 ::
  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_492 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
d_'8804''45'dec'8658'isDecPartialOrder_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
d_'8804''45'dec'8658'isDecPartialOrder_266 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4
  = T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecPartialOrder_300
du_'8804''45'dec'8658'isDecPartialOrder_266 T_Poset_492
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4
du_'8804''45'dec'8658'isDecPartialOrder_266 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
du_'8804''45'dec'8658'isDecPartialOrder_266 :: T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecPartialOrder_300
du_'8804''45'dec'8658'isDecPartialOrder_266 T_Poset_492
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecPartialOrder_300)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_300
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
MAlonzo.Code.Relation.Binary.Structures.C_constructor_364
      ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
      ((T_Poset_492
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_492
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'8804''45'dec'8658''8776''45'dec_222 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
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_272 ::
  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_492 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono'8658'cong_272 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_mono'8658'cong_272 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 AgdaAny -> AgdaAny
v4
  = T_Poset_492
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_272 T_Poset_492
v3 AgdaAny -> AgdaAny
v4
du_mono'8658'cong_272 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_mono'8658'cong_272 :: T_Poset_492
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_272 T_Poset_492
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_278
      ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
               ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
                  (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0)))))
      ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
               (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))))
      ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
            (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
-- Relation.Binary.Properties.Poset.antimono⇒cong
d_antimono'8658'cong_276 ::
  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_492 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antimono'8658'cong_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antimono'8658'cong_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 AgdaAny -> AgdaAny
v4
  = T_Poset_492
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_276 T_Poset_492
v3 AgdaAny -> AgdaAny
v4
du_antimono'8658'cong_276 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antimono'8658'cong_276 :: T_Poset_492
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_276 T_Poset_492
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_292
      ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
               ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
                  (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0)))))
      ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
               (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))))
      ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
            (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)