{-# 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.Construct.Add.Supremum.NonStrict 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Maybe.Properties
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.Construct.Add.Supremum.NonStrict._≤⁺_
d__'8804''8314'__20 :: p -> p -> p -> p -> p -> p -> ()
d__'8804''8314'__20 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T__'8804''8314'__20
  = C_'91'_'93'_26 AgdaAny | C__'8804''8868''8314'_30
-- Relation.Binary.Construct.Add.Supremum.NonStrict.[≤]-injective
d_'91''8804''93''45'injective_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T__'8804''8314'__20 -> AgdaAny
d_'91''8804''93''45'injective_36 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8804''8314'__20
-> AgdaAny
d_'91''8804''93''45'injective_36 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__'8804''8314'__20
v6
  = T__'8804''8314'__20 -> AgdaAny
du_'91''8804''93''45'injective_36 T__'8804''8314'__20
v6
du_'91''8804''93''45'injective_36 :: T__'8804''8314'__20 -> AgdaAny
du_'91''8804''93''45'injective_36 :: T__'8804''8314'__20 -> AgdaAny
du_'91''8804''93''45'injective_36 T__'8804''8314'__20
v0
  = case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v0 of
      C_'91'_'93'_26 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
      T__'8804''8314'__20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-trans
d_'8804''8314''45'trans_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8804''8314'__20
d_'8804''8314''45'trans_40 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8804''8314'__20
d_'8804''8314''45'trans_40 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 Maybe AgdaAny
v7 T__'8804''8314'__20
v8 T__'8804''8314'__20
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8804''8314'__20
du_'8804''8314''45'trans_40 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 Maybe AgdaAny
v7 T__'8804''8314'__20
v8 T__'8804''8314'__20
v9
du_'8804''8314''45'trans_40 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8804''8314'__20
du_'8804''8314''45'trans_40 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8804''8314'__20
du_'8804''8314''45'trans_40 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'8804''8314'__20
v4 T__'8804''8314'__20
v5
  = case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v4 of
      C_'91'_'93'_26 AgdaAny
v8
        -> let v9 :: b
v9 = AgdaAny -> b -> b
forall a b. a -> b -> b
seq (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
v5) (T__'8804''8314'__20 -> b
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30) in
           AgdaAny -> T__'8804''8314'__20
forall a b. a -> b
coe
             (case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
                MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                  -> let v11 :: b
v11 = AgdaAny -> b -> b
forall a b. a -> b -> b
seq (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
v5) (T__'8804''8314'__20 -> b
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                          MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v12
                            -> case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v5 of
                                 C_'91'_'93'_26 AgdaAny
v15
                                   -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                                        MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v16
                                          -> (AgdaAny -> T__'8804''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8804''8314'__20
C_'91'_'93'_26 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v12 AgdaAny
v16 AgdaAny
v8 AgdaAny
v15)
                                        Maybe AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                                 T__'8804''8314'__20
C__'8804''8868''8314'_30 -> T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30
                                 T__'8804''8314'__20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                          Maybe AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
                Maybe AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
      T__'8804''8314'__20
C__'8804''8868''8314'_30
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8804''8314'__20
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
v5) (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30)
      T__'8804''8314'__20
_ -> T__'8804''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-maximum
d_'8804''8314''45'maximum_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) -> Maybe AgdaAny -> T__'8804''8314'__20
d_'8804''8314''45'maximum_54 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> Maybe AgdaAny
-> T__'8804''8314'__20
d_'8804''8314''45'maximum_54 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'maximum_54
du_'8804''8314''45'maximum_54 ::
  Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'maximum_54 :: Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'maximum_54 Maybe AgdaAny
v0 = T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-dec
d_'8804''8314''45'dec_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8804''8314''45'dec_56 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Dec_32
d_'8804''8314''45'dec_56 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8804''8314''45'dec_56 AgdaAny -> AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
du_'8804''8314''45'dec_56 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8804''8314''45'dec_56 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8804''8314''45'dec_56 AgdaAny -> AgdaAny -> T_Dec_32
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
               -> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    ((AgdaAny -> T__'8804''8314'__20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8804''8314'__20
C_'91'_'93'_26) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v4 AgdaAny
v3)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
             Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30))
      Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-total
d_'8804''8314''45'total_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8804''8314''45'total_72 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8846'__30
d_'8804''8314''45'total_72 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> T__'8846'__30
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30
du_'8804''8314''45'total_72 AgdaAny -> AgdaAny -> T__'8846'__30
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
du_'8804''8314''45'total_72 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8804''8314''45'total_72 :: (AgdaAny -> AgdaAny -> T__'8846'__30)
-> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30
du_'8804''8314''45'total_72 AgdaAny -> AgdaAny -> T__'8846'__30
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84 ((AgdaAny -> T__'8804''8314'__20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8804''8314'__20
C_'91'_'93'_26)
                    ((AgdaAny -> T__'8804''8314'__20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8804''8314'__20
C_'91'_'93'_26) ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v4 AgdaAny
v3)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                    (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30)
             Maybe AgdaAny
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
             AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
             (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30)
      Maybe AgdaAny
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-irrelevant
d_'8804''8314''45'irrelevant_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8804''8314'__20 ->
  T__'8804''8314'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8804''8314''45'irrelevant_88 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8801'__12
d_'8804''8314''45'irrelevant_88 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-reflexive-≡
d_'8804''8314''45'reflexive'45''8801'_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'8804''8314'__20
d_'8804''8314''45'reflexive'45''8801'_100 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8804''8314'__20
d_'8804''8314''45'reflexive'45''8801'_100 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v4 Maybe AgdaAny
v5 ~Maybe AgdaAny
v6
                                          ~T__'8801'__12
v7
  = (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'reflexive'45''8801'_100 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v4 Maybe AgdaAny
v5
du_'8804''8314''45'reflexive'45''8801'_100 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'reflexive'45''8801'_100 :: (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'reflexive'45''8801'_100 AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v0 Maybe AgdaAny
v1
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
        -> (AgdaAny -> T__'8804''8314'__20) -> AgdaAny -> T__'8804''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'8804''8314'__20
C_'91'_'93'_26 ((AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v2 AgdaAny
forall a. a
erased)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30
      Maybe AgdaAny
_ -> T__'8804''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-antisym-≡
d_'8804''8314''45'antisym'45''8801'_108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8804''8314'__20 ->
  T__'8804''8314'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8804''8314''45'antisym'45''8801'_108 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8801'__12
d_'8804''8314''45'antisym'45''8801'_108 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.NonStrict._._._≈∙_
d__'8776''8729'__128 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__128 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-reflexive
d_'8804''8314''45'reflexive_158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'8804''8314'__20
d_'8804''8314''45'reflexive_158 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8804''8314'__20
d_'8804''8314''45'reflexive_158 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 T__'8776''8729'__20
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8804''8314'__20
du_'8804''8314''45'reflexive_158 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 T__'8776''8729'__20
v9
du_'8804''8314''45'reflexive_158 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'8804''8314'__20
du_'8804''8314''45'reflexive_158 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8804''8314'__20
du_'8804''8314''45'reflexive_158 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 T__'8776''8729'__20
v3
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v3 of
      T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'8729''8776''8729'_22
        -> T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
C__'8804''8868''8314'_30
      MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'91'_'93'_28 AgdaAny
v6
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v7
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
                      -> (AgdaAny -> T__'8804''8314'__20) -> AgdaAny -> T__'8804''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'8804''8314'__20
C_'91'_'93'_26 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v7 AgdaAny
v8 AgdaAny
v6)
                    Maybe AgdaAny
_ -> T__'8804''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'8804''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8776''8729'__20
_ -> T__'8804''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-antisym
d_'8804''8314''45'antisym_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8804''8314'__20 ->
  T__'8804''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_'8804''8314''45'antisym_166 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8776''8729'__20
d_'8804''8314''45'antisym_166 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 T__'8804''8314'__20
v9
                              T__'8804''8314'__20
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8776''8729'__20
du_'8804''8314''45'antisym_166 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 T__'8804''8314'__20
v9 T__'8804''8314'__20
v10
du_'8804''8314''45'antisym_166 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8804''8314'__20 ->
  T__'8804''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_'8804''8314''45'antisym_166 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8776''8729'__20
du_'8804''8314''45'antisym_166 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 T__'8804''8314'__20
v3 T__'8804''8314'__20
v4
  = case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v3 of
      C_'91'_'93'_26 AgdaAny
v7
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v9
                      -> case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v4 of
                           C_'91'_'93'_26 AgdaAny
v12
                             -> (AgdaAny -> T__'8776''8729'__20) -> AgdaAny -> T__'8776''8729'__20
forall a b. a -> b
coe
                                  AgdaAny -> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'91'_'93'_28
                                  ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v8 AgdaAny
v9 AgdaAny
v7 AgdaAny
v12)
                           T__'8804''8314'__20
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8804''8314'__20
C__'8804''8868''8314'_30
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8776''8729'__20
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T__'8804''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'8804''8314'__20
v4)
             (T__'8776''8729'__20 -> AgdaAny
forall a b. a -> b
coe
                T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'8729''8776''8729'_22)
      T__'8804''8314'__20
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-isPreorder-≡
d_'8804''8314''45'isPreorder'45''8801'_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''8314''45'isPreorder'45''8801'_176 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_IsPreorder_70
d_'8804''8314''45'isPreorder'45''8801'_176 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsPreorder_70
v4
  = T_IsPreorder_70 -> T_IsPreorder_70
du_'8804''8314''45'isPreorder'45''8801'_176 T_IsPreorder_70
v4
du_'8804''8314''45'isPreorder'45''8801'_176 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_'8804''8314''45'isPreorder'45''8801'_176 :: T_IsPreorder_70 -> T_IsPreorder_70
du_'8804''8314''45'isPreorder'45''8801'_176 T_IsPreorder_70
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
         ((AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
 -> Maybe AgdaAny -> T__'8804''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny)
-> Maybe AgdaAny -> T__'8804''8314'__20
du_'8804''8314''45'reflexive'45''8801'_100
           ((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_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
           AgdaAny
v1)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8804''8314'__20
 -> T__'8804''8314'__20
 -> T__'8804''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8804''8314'__20
du_'8804''8314''45'trans_40
         ((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_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-isPartialOrder-≡
d_'8804''8314''45'isPartialOrder'45''8801'_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8804''8314''45'isPartialOrder'45''8801'_212 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> T_IsPartialOrder_162
d_'8804''8314''45'isPartialOrder'45''8801'_212 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsPartialOrder_162
v4
  = T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder'45''8801'_212 T_IsPartialOrder_162
v4
du_'8804''8314''45'isPartialOrder'45''8801'_212 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder'45''8801'_212 :: T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder'45''8801'_212 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
      ((T_IsPreorder_70 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsPreorder_70
du_'8804''8314''45'isPreorder'45''8801'_176
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0)))
      AgdaAny
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-isDecPartialOrder-≡
d_'8804''8314''45'isDecPartialOrder'45''8801'_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_'8804''8314''45'isDecPartialOrder'45''8801'_252 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> T_IsDecPartialOrder_206
d_'8804''8314''45'isDecPartialOrder'45''8801'_252 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
                                                  T_IsDecPartialOrder_206
v4
  = T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_'8804''8314''45'isDecPartialOrder'45''8801'_252 T_IsDecPartialOrder_206
v4
du_'8804''8314''45'isDecPartialOrder'45''8801'_252 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_'8804''8314''45'isDecPartialOrder'45''8801'_252 :: T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_'8804''8314''45'isDecPartialOrder'45''8801'_252 T_IsDecPartialOrder_206
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      ((T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder'45''8801'_212
         ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_216
            (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
MAlonzo.Code.Data.Maybe.Properties.du_'8801''45'dec_24
         ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__218 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8804''8314''45'dec_56
         ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__220
            (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-isTotalOrder-≡
d_'8804''8314''45'isTotalOrder'45''8801'_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_'8804''8314''45'isTotalOrder'45''8801'_304 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalOrder_384
-> T_IsTotalOrder_384
d_'8804''8314''45'isTotalOrder'45''8801'_304 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsTotalOrder_384
v4
  = T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder'45''8801'_304 T_IsTotalOrder_384
v4
du_'8804''8314''45'isTotalOrder'45''8801'_304 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder'45''8801'_304 :: T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder'45''8801'_304 T_IsTotalOrder_384
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
      ((T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder'45''8801'_212
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            (T_IsTotalOrder_384 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384
v0)))
      (((AgdaAny -> AgdaAny -> T__'8846'__30)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T__'8846'__30)
-> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30
du_'8804''8314''45'total_72
         ((T_IsTotalOrder_384 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_394 (T_IsTotalOrder_384 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict.≤⁺-isDecTotalOrder-≡
d_'8804''8314''45'isDecTotalOrder'45''8801'_350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_'8804''8314''45'isDecTotalOrder'45''8801'_350 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecTotalOrder_434
-> T_IsDecTotalOrder_434
d_'8804''8314''45'isDecTotalOrder'45''8801'_350 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsDecTotalOrder_434
v4
  = T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_'8804''8314''45'isDecTotalOrder'45''8801'_350 T_IsDecTotalOrder_434
v4
du_'8804''8314''45'isDecTotalOrder'45''8801'_350 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
du_'8804''8314''45'isDecTotalOrder'45''8801'_350 :: T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_'8804''8314''45'isDecTotalOrder'45''8801'_350 T_IsDecTotalOrder_434
v0
  = (T_IsTotalOrder_384
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_434
forall a b. a -> b
coe
      T_IsTotalOrder_384
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
      ((T_IsTotalOrder_384 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder'45''8801'_304
         ((T_IsDecTotalOrder_434 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.d_isTotalOrder_444
            (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
MAlonzo.Code.Data.Maybe.Properties.du_'8801''45'dec_24
         ((T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__446 (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8804''8314''45'dec_56
         ((T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__448
            (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict._._._≈∙_
d__'8776''8729'__420 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__420 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-isPreorder
d_'8804''8314''45'isPreorder_450 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''8314''45'isPreorder_450 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_IsPreorder_70
d_'8804''8314''45'isPreorder_450 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70 -> T_IsPreorder_70
du_'8804''8314''45'isPreorder_450 T_IsPreorder_70
v6
du_'8804''8314''45'isPreorder_450 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_'8804''8314''45'isPreorder_450 :: T_IsPreorder_70 -> T_IsPreorder_70
du_'8804''8314''45'isPreorder_450 T_IsPreorder_70
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'isEquivalence_108
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'8804''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8804''8314'__20
du_'8804''8314''45'reflexive_158
         ((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_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8804''8314'__20
 -> T__'8804''8314'__20
 -> T__'8804''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8804''8314'__20
du_'8804''8314''45'trans_40
         ((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_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-isPartialOrder
d_'8804''8314''45'isPartialOrder_486 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8804''8314''45'isPartialOrder_486 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPartialOrder_162
-> T_IsPartialOrder_162
d_'8804''8314''45'isPartialOrder_486 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPartialOrder_162
v6
  = T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder_486 T_IsPartialOrder_162
v6
du_'8804''8314''45'isPartialOrder_486 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder_486 :: T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder_486 T_IsPartialOrder_162
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
      ((T_IsPreorder_70 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsPreorder_70
du_'8804''8314''45'isPreorder_450
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8804''8314'__20
 -> T__'8804''8314'__20
 -> T__'8776''8729'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'8804''8314'__20
-> T__'8776''8729'__20
du_'8804''8314''45'antisym_166
         ((T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-isDecPartialOrder
d_'8804''8314''45'isDecPartialOrder_526 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_'8804''8314''45'isDecPartialOrder_526 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecPartialOrder_206
-> T_IsDecPartialOrder_206
d_'8804''8314''45'isDecPartialOrder_526 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecPartialOrder_206
v6
  = T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_'8804''8314''45'isDecPartialOrder_526 T_IsDecPartialOrder_206
v6
du_'8804''8314''45'isDecPartialOrder_526 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_'8804''8314''45'isDecPartialOrder_526 :: T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_'8804''8314''45'isDecPartialOrder_526 T_IsDecPartialOrder_206
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      ((T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder_486
         ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_216
            (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'dec_66
         ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__218 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8804''8314''45'dec_56
         ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__220
            (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-isTotalOrder
d_'8804''8314''45'isTotalOrder_578 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_'8804''8314''45'isTotalOrder_578 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsTotalOrder_384
-> T_IsTotalOrder_384
d_'8804''8314''45'isTotalOrder_578 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsTotalOrder_384
v6
  = T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder_578 T_IsTotalOrder_384
v6
du_'8804''8314''45'isTotalOrder_578 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder_578 :: T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder_578 T_IsTotalOrder_384
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
      ((T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_'8804''8314''45'isPartialOrder_486
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            (T_IsTotalOrder_384 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384
v0)))
      (((AgdaAny -> AgdaAny -> T__'8846'__30)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T__'8846'__30)
-> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30
du_'8804''8314''45'total_72
         ((T_IsTotalOrder_384 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_394 (T_IsTotalOrder_384 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384
v0)))
-- Relation.Binary.Construct.Add.Supremum.NonStrict._.≤⁺-isDecTotalOrder
d_'8804''8314''45'isDecTotalOrder_624 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_'8804''8314''45'isDecTotalOrder_624 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecTotalOrder_434
-> T_IsDecTotalOrder_434
d_'8804''8314''45'isDecTotalOrder_624 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsDecTotalOrder_434
v6
  = T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_'8804''8314''45'isDecTotalOrder_624 T_IsDecTotalOrder_434
v6
du_'8804''8314''45'isDecTotalOrder_624 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
du_'8804''8314''45'isDecTotalOrder_624 :: T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_'8804''8314''45'isDecTotalOrder_624 T_IsDecTotalOrder_434
v0
  = (T_IsTotalOrder_384
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_434
forall a b. a -> b
coe
      T_IsTotalOrder_384
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
      ((T_IsTotalOrder_384 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_'8804''8314''45'isTotalOrder_578
         ((T_IsDecTotalOrder_434 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.d_isTotalOrder_444
            (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'dec_66
         ((T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__446 (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8804''8314''45'dec_56
         ((T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__448
            (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v0)))