{-# 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.Strict 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.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Maybe.Properties
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict
import qualified MAlonzo.Code.Relation.Binary.Definitions
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.Strict._<⁺_
d__'60''8314'__20 :: p -> p -> p -> p -> p -> p -> ()
d__'60''8314'__20 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T__'60''8314'__20
  = C_'91'_'93'_26 AgdaAny | C_'91'_'93''60''8868''8314'_30
-- Relation.Binary.Construct.Add.Supremum.Strict.[<]-injective
d_'91''60''93''45'injective_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T__'60''8314'__20 -> AgdaAny
d_'91''60''93''45'injective_36 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'60''8314'__20
-> AgdaAny
d_'91''60''93''45'injective_36 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__'60''8314'__20
v6
  = T__'60''8314'__20 -> AgdaAny
du_'91''60''93''45'injective_36 T__'60''8314'__20
v6
du_'91''60''93''45'injective_36 :: T__'60''8314'__20 -> AgdaAny
du_'91''60''93''45'injective_36 :: T__'60''8314'__20 -> AgdaAny
du_'91''60''93''45'injective_36 T__'60''8314'__20
v0
  = case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v0 of
      C_'91'_'93'_26 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
      T__'60''8314'__20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-asym
d_'60''8314''45'asym_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'60''8314'__20 ->
  T__'60''8314'__20 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''8314''45'asym_40 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T_'8869'_4
d_'60''8314''45'asym_40 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-trans
d_'60''8314''45'trans_48 ::
  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__'60''8314'__20 -> T__'60''8314'__20 -> T__'60''8314'__20
d_'60''8314''45'trans_48 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'trans_48 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 Maybe AgdaAny
v7 T__'60''8314'__20
v8 T__'60''8314'__20
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans_48 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 Maybe AgdaAny
v7 T__'60''8314'__20
v8 T__'60''8314'__20
v9
du_'60''8314''45'trans_48 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'60''8314'__20 -> T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'trans_48 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans_48 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'60''8314'__20
v4 T__'60''8314'__20
v5
  = case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v4 of
      C_'91'_'93'_26 AgdaAny
v8
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v9
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                      -> case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v5 of
                           C_'91'_'93'_26 AgdaAny
v13
                             -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                                  MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v14
                                    -> (AgdaAny -> T__'60''8314'__20) -> AgdaAny -> T__'60''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'60''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
v9 AgdaAny
v10 AgdaAny
v14 AgdaAny
v8 AgdaAny
v13)
                                  Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                             -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                           T__'60''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'60''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-dec
d_'60''8314''45'dec_62 ::
  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_'60''8314''45'dec_62 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Dec_32
d_'60''8314''45'dec_62 ~()
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_'60''8314''45'dec_62 AgdaAny -> AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
du_'60''8314''45'dec_62 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'60''8314''45'dec_62 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'60''8314''45'dec_62 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
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 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__'60''8314'__20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'60''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
v3 AgdaAny
v4)
             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__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30))
             Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2)
             ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
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
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-irrelevant
d_'60''8314''45'irrelevant_80 ::
  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__'60''8314'__20 ->
  T__'60''8314'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8314''45'irrelevant_80 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
d_'60''8314''45'irrelevant_80 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.Strict._._._≤⁺_
d__'8804''8314'__102 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d__'8804''8314'__102 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-transʳ
d_'60''8314''45'trans'691'_154 ::
  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 -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.T__'8804''8314'__20 ->
  T__'60''8314'__20 -> T__'60''8314'__20
d_'60''8314''45'trans'691'_154 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'trans'691'_154 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9
                               T__'8804''8314'__20
v10 T__'60''8314'__20
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans'691'_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9 T__'8804''8314'__20
v10 T__'60''8314'__20
v11
du_'60''8314''45'trans'691'_154 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.T__'8804''8314'__20 ->
  T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'trans'691'_154 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8804''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans'691'_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'8804''8314'__20
v4 T__'60''8314'__20
v5
  = case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v4 of
      MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.C_'91'_'93'_26 AgdaAny
v8
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v9
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                      -> case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v5 of
                           C_'91'_'93'_26 AgdaAny
v13
                             -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                                  MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v14
                                    -> (AgdaAny -> T__'60''8314'__20) -> AgdaAny -> T__'60''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'60''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
v9 AgdaAny
v10 AgdaAny
v14 AgdaAny
v8 AgdaAny
v13)
                                  Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                             -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                           T__'60''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8804''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-transˡ
d_'60''8314''45'trans'737'_168 ::
  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 -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.T__'8804''8314'__20 ->
  T__'60''8314'__20
d_'60''8314''45'trans'737'_168 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'8804''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'trans'737'_168 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9
                               T__'60''8314'__20
v10 T__'8804''8314'__20
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'8804''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans'737'_168 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9 T__'60''8314'__20
v10 T__'8804''8314'__20
v11
du_'60''8314''45'trans'737'_168 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.T__'8804''8314'__20 ->
  T__'60''8314'__20
du_'60''8314''45'trans'737'_168 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'8804''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans'737'_168 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'60''8314'__20
v4 T__'8804''8314'__20
v5
  = case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v4 of
      C_'91'_'93'_26 AgdaAny
v8
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v9
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                      -> case T__'8804''8314'__20 -> T__'8804''8314'__20
forall a b. a -> b
coe T__'8804''8314'__20
v5 of
                           MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.C_'91'_'93'_26 AgdaAny
v13
                             -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                                  MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v14
                                    -> (AgdaAny -> T__'60''8314'__20) -> AgdaAny -> T__'60''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'60''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
v9 AgdaAny
v10 AgdaAny
v14 AgdaAny
v8 AgdaAny
v13)
                                  Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T__'8804''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict.C__'8804''8868''8314'_30
                             -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                           T__'8804''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
        -> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'60''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__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30)
      T__'60''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-cmp-≡
d_'60''8314''45'cmp'45''8801'_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
d_'60''8314''45'cmp'45''8801'_184 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Tri_136
d_'60''8314''45'cmp'45''8801'_184 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> T_Tri_136
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136
du_'60''8314''45'cmp'45''8801'_184 AgdaAny -> AgdaAny -> T_Tri_136
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
du_'60''8314''45'cmp'45''8801'_184 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
du_'60''8314''45'cmp'45''8801'_184 :: (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136
du_'60''8314''45'cmp'45''8801'_184 AgdaAny -> AgdaAny -> T_Tri_136
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
               -> let v5 :: t
v5 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v3 AgdaAny
v4 in
                  AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v6
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                              ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'60''8314'__20
C_'91'_'93'_26 AgdaAny
v6)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v7
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
forall a. a
erased
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v8
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                              ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'60''8314'__20
C_'91'_'93'_26 AgdaAny
v8)
                       T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                    (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30)
             Maybe AgdaAny
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> 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
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                    (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
forall a. a
erased
             Maybe AgdaAny
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-irrefl-≡
d_'60''8314''45'irrefl'45''8801'_240 ::
  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 -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'60''8314'__20 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''8314''45'irrefl'45''8801'_240 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T_'8869'_4)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'60''8314'__20
-> T_'8869'_4
d_'60''8314''45'irrefl'45''8801'_240 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T_'8869'_4)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'60''8314'__20
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-respˡ-≡
d_'60''8314''45'resp'737''45''8801'_246 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'60''8314'__20 -> T__'60''8314'__20
d_'60''8314''45'resp'737''45''8801'_246 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'60''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'resp'737''45''8801'_246 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~Maybe AgdaAny
v4 ~Maybe AgdaAny
v5 ~Maybe AgdaAny
v6
                                        ~T__'8801'__12
v7 T__'60''8314'__20
v8
  = T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8801'_246 T__'60''8314'__20
v8
du_'60''8314''45'resp'737''45''8801'_246 ::
  T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8801'_246 :: T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8801'_246 T__'60''8314'__20
v0 = T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v0
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-respʳ-≡
d_'60''8314''45'resp'691''45''8801'_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'60''8314'__20 -> T__'60''8314'__20
d_'60''8314''45'resp'691''45''8801'_250 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'60''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'resp'691''45''8801'_250 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~Maybe AgdaAny
v4 ~Maybe AgdaAny
v5 ~Maybe AgdaAny
v6
                                        ~T__'8801'__12
v7 T__'60''8314'__20
v8
  = T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8801'_250 T__'60''8314'__20
v8
du_'60''8314''45'resp'691''45''8801'_250 ::
  T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8801'_250 :: T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8801'_250 T__'60''8314'__20
v0 = T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v0
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-resp-≡
d_'60''8314''45'resp'45''8801'_254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''8314''45'resp'45''8801'_254 :: () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14
d_'60''8314''45'resp'45''8801'_254 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = T_Σ_14
du_'60''8314''45'resp'45''8801'_254
du_'60''8314''45'resp'45''8801'_254 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''8314''45'resp'45''8801'_254 :: T_Σ_14
du_'60''8314''45'resp'45''8801'_254
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Relation.Binary.Construct.Add.Supremum.Strict._._._≈∙_
d__'8776''8729'__266 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__266 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-cmp
d_'60''8314''45'cmp_296 ::
  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 -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
d_'60''8314''45'cmp_296 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Tri_136
d_'60''8314''45'cmp_296 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> T_Tri_136
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8
  = (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136
du_'60''8314''45'cmp_296 AgdaAny -> AgdaAny -> T_Tri_136
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8
du_'60''8314''45'cmp_296 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
du_'60''8314''45'cmp_296 :: (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136
du_'60''8314''45'cmp_296 AgdaAny -> AgdaAny -> T_Tri_136
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
               -> let v5 :: t
v5 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v3 AgdaAny
v4 in
                  AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v6
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                              ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'60''8314'__20
C_'91'_'93'_26 AgdaAny
v6)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v7
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158
                              ((AgdaAny -> T__'8776''8729'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'91'_'93'_28
                                 AgdaAny
v7)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v8
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                              ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'60''8314'__20
C_'91'_'93'_26 AgdaAny
v8)
                       T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                    (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30)
             Maybe AgdaAny
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> 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
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                    (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158
                    (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)
             Maybe AgdaAny
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-irrefl
d_'60''8314''45'irrefl_354 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'60''8314'__20 -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''8314''45'irrefl_354 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T_'8869'_4
d_'60''8314''45'irrefl_354 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-respˡ-≈⁺
d_'60''8314''45'resp'737''45''8776''8314'_362 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'60''8314'__20 -> T__'60''8314'__20
d_'60''8314''45'resp'737''45''8776''8314'_362 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'resp'737''45''8776''8314'_362 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4
                                              ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9 T__'8776''8729'__20
v10 T__'60''8314'__20
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8776''8314'_362
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9 T__'8776''8729'__20
v10 T__'60''8314'__20
v11
du_'60''8314''45'resp'737''45''8776''8314'_362 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8776''8314'_362 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8776''8314'_362 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'8776''8729'__20
v4 T__'60''8314'__20
v5
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v4 of
      T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'8729''8776''8729'_22
        -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v5
      MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'91'_'93'_28 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 Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                      -> case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v5 of
                           C_'91'_'93'_26 AgdaAny
v13
                             -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
                                  MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v14
                                    -> (AgdaAny -> T__'60''8314'__20) -> AgdaAny -> T__'60''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'60''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
v14 AgdaAny
v9 AgdaAny
v10 AgdaAny
v8 AgdaAny
v13)
                                  Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                             -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
C_'91'_'93''60''8868''8314'_30
                           T__'60''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8776''8729'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-respʳ-≈⁺
d_'60''8314''45'resp'691''45''8776''8314'_380 ::
  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 -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'60''8314'__20 -> T__'60''8314'__20
d_'60''8314''45'resp'691''45''8776''8314'_380 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_'60''8314''45'resp'691''45''8776''8314'_380 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4
                                              ~AgdaAny -> AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9 T__'8776''8729'__20
v10 T__'60''8314'__20
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8776''8314'_380
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 Maybe AgdaAny
v9 T__'8776''8729'__20
v10 T__'60''8314'__20
v11
du_'60''8314''45'resp'691''45''8776''8314'_380 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  T__'60''8314'__20 -> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8776''8314'_380 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8776''8314'_380 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'8776''8729'__20
v4 T__'60''8314'__20
v5
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v4 of
      T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'8729''8776''8729'_22
        -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v5
      MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.C_'91'_'93'_28 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 Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                      -> case T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v5 of
                           C_'91'_'93'_26 AgdaAny
v13
                             -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
                                  MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v14
                                    -> (AgdaAny -> T__'60''8314'__20) -> AgdaAny -> T__'60''8314'__20
forall a b. a -> b
coe AgdaAny -> T__'60''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
v14 AgdaAny
v9 AgdaAny
v10 AgdaAny
v8 AgdaAny
v13)
                                  Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T__'60''8314'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8776''8729'__20
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-resp-≈⁺
d_'60''8314''45'resp'45''8776''8314'_392 ::
  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.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''8314''45'resp'45''8776''8314'_392 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Σ_14
-> T_Σ_14
d_'60''8314''45'resp'45''8776''8314'_392 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5
  = T_Σ_14 -> T_Σ_14
du_'60''8314''45'resp'45''8776''8314'_392
du_'60''8314''45'resp'45''8776''8314'_392 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''8314''45'resp'45''8776''8314'_392 :: T_Σ_14 -> T_Σ_14
du_'60''8314''45'resp'45''8776''8314'_392
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'resp'691''45''8776''8314'_380)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'resp'737''45''8776''8314'_362))
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-isStrictPartialOrder-≡
d_'60''8314''45'isStrictPartialOrder'45''8801'_394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'60''8314''45'isStrictPartialOrder'45''8801'_394 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266
d_'60''8314''45'isStrictPartialOrder'45''8801'_394 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
                                                   T_IsStrictPartialOrder_266
v4
  = T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder'45''8801'_394 T_IsStrictPartialOrder_266
v4
du_'60''8314''45'isStrictPartialOrder'45''8801'_394 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder'45''8801'_394 :: T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder'45''8801'_394 T_IsStrictPartialOrder_266
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_13145
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans_48
         ((T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'60''8314''45'resp'45''8801'_254)
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-isDecStrictPartialOrder-≡
d_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314
d_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> T_IsDecStrictPartialOrder_314
d_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 ~()
v0 ~()
v1 ~()
v2
                                                      ~AgdaAny -> AgdaAny -> ()
v3 T_IsDecStrictPartialOrder_314
v4
  = T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
du_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 T_IsDecStrictPartialOrder_314
v4
du_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314
du_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 :: T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
du_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecStrictPartialOrder_314)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecStrictPartialOrder_314
MAlonzo.Code.Relation.Binary.Structures.C_IsDecStrictPartialOrder'46'constructor_17873
      ((T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder'45''8801'_394
         ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_324
            (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
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_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__326 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
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_'60''8314''45'dec_62
         ((T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'60''63'__328 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Construct.Add.Supremum.Strict.<⁺-isStrictTotalOrder-≡
d_'60''8314''45'isStrictTotalOrder'45''8801'_482 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
d_'60''8314''45'isStrictTotalOrder'45''8801'_482 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictTotalOrder_502
-> T_IsStrictTotalOrder_502
d_'60''8314''45'isStrictTotalOrder'45''8801'_482 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsStrictTotalOrder_502
v4
  = T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''8314''45'isStrictTotalOrder'45''8801'_482 T_IsStrictTotalOrder_502
v4
du_'60''8314''45'isStrictTotalOrder'45''8801'_482 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
du_'60''8314''45'isStrictTotalOrder'45''8801'_482 :: T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''8314''45'isStrictTotalOrder'45''8801'_482 T_IsStrictTotalOrder_502
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_23999
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans_48
         ((T_IsStrictTotalOrder_502
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_514 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> T_Tri_136)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136
du_'60''8314''45'cmp'45''8801'_184
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
-- Relation.Binary.Construct.Add.Supremum.Strict._._._≈∙_
d__'8776''8729'__544 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__544 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-isStrictPartialOrder
d_'60''8314''45'isStrictPartialOrder_574 ::
  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_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'60''8314''45'isStrictPartialOrder_574 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266
d_'60''8314''45'isStrictPartialOrder_574 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictPartialOrder_266
v6
  = T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder_574 T_IsStrictPartialOrder_266
v6
du_'60''8314''45'isStrictPartialOrder_574 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder_574 :: T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder_574 T_IsStrictPartialOrder_266
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_13145
      ((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_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans_48
         ((T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      ((T_Σ_14 -> T_Σ_14) -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14
du_'60''8314''45'resp'45''8776''8314'_392
         (T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
            (T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-isDecStrictPartialOrder
d_'60''8314''45'isDecStrictPartialOrder_612 ::
  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_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314
d_'60''8314''45'isDecStrictPartialOrder_612 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecStrictPartialOrder_314
-> T_IsDecStrictPartialOrder_314
d_'60''8314''45'isDecStrictPartialOrder_612 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5
                                            T_IsDecStrictPartialOrder_314
v6
  = T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
du_'60''8314''45'isDecStrictPartialOrder_612 T_IsDecStrictPartialOrder_314
v6
du_'60''8314''45'isDecStrictPartialOrder_612 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314
du_'60''8314''45'isDecStrictPartialOrder_612 :: T_IsDecStrictPartialOrder_314 -> T_IsDecStrictPartialOrder_314
du_'60''8314''45'isDecStrictPartialOrder_612 T_IsDecStrictPartialOrder_314
v0
  = (T_IsStrictPartialOrder_266
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecStrictPartialOrder_314)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecStrictPartialOrder_314
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecStrictPartialOrder_314
MAlonzo.Code.Relation.Binary.Structures.C_IsDecStrictPartialOrder'46'constructor_17873
      ((T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''8314''45'isStrictPartialOrder_574
         ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_324
            (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
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_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__326 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
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_'60''8314''45'dec_62
         ((T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'60''63'__328 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Construct.Add.Supremum.Strict._.<⁺-isStrictTotalOrder
d_'60''8314''45'isStrictTotalOrder_662 ::
  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_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
d_'60''8314''45'isStrictTotalOrder_662 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictTotalOrder_502
-> T_IsStrictTotalOrder_502
d_'60''8314''45'isStrictTotalOrder_662 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictTotalOrder_502
v6
  = T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''8314''45'isStrictTotalOrder_662 T_IsStrictTotalOrder_502
v6
du_'60''8314''45'isStrictTotalOrder_662 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
du_'60''8314''45'isStrictTotalOrder_662 :: T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''8314''45'isStrictTotalOrder_662 T_IsStrictTotalOrder_502
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_23999
      ((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_IsStrictTotalOrder_502 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_512
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_'60''8314''45'trans_48
         ((T_IsStrictTotalOrder_502
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_514 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> T_Tri_136)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Tri_136)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_136
du_'60''8314''45'cmp_296
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))