{-# 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.Flip.EqAndOrd where

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

-- Relation.Binary.Construct.Flip.EqAndOrd._.refl
d_refl_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_refl_44 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_refl_44 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny
v4 AgdaAny
v5 = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_refl_44 AgdaAny -> AgdaAny
v4 AgdaAny
v5
du_refl_44 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_refl_44 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_refl_44 AgdaAny -> AgdaAny
v0 AgdaAny
v1 = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1
-- Relation.Binary.Construct.Flip.EqAndOrd._.sym
d_sym_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sym_48 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_48 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_sym_48 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_48 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_48 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v1
-- Relation.Binary.Construct.Flip.EqAndOrd._.trans
d_trans_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_52 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_52 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_trans_52 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_52 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_52 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = (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
v3 AgdaAny
v2 AgdaAny
v1 AgdaAny
v5 AgdaAny
v4
-- Relation.Binary.Construct.Flip.EqAndOrd._.asym
d_asym_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_asym_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_asym_56 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Construct.Flip.EqAndOrd._.total
d_total_60 ::
  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) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_total_60 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T__'8846'__30
v4 AgdaAny
v5 AgdaAny
v6 = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_60 AgdaAny -> AgdaAny -> T__'8846'__30
v4 AgdaAny
v5 AgdaAny
v6
du_total_60 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_total_60 :: (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_60 AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v2 AgdaAny
v1
-- Relation.Binary.Construct.Flip.EqAndOrd._.resp
d_resp_72 ::
  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 -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp_72 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp_72 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp_72 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_resp_72 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp_72 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp_72 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v2 AgdaAny
v4)
-- Relation.Binary.Construct.Flip.EqAndOrd._.max
d_max_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_max_82 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_max_82 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 AgdaAny -> AgdaAny
v5 = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_max_82 AgdaAny -> AgdaAny
v5
du_max_82 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_max_82 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_max_82 AgdaAny -> AgdaAny
v0 = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0
-- Relation.Binary.Construct.Flip.EqAndOrd._.min
d_min_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_min_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_min_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 AgdaAny -> AgdaAny
v5 = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_min_88 AgdaAny -> AgdaAny
v5
du_min_88 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_min_88 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_min_88 AgdaAny -> AgdaAny
v0 = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0
-- Relation.Binary.Construct.Flip.EqAndOrd._.reflexive
d_reflexive_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_106 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_reflexive_106 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_106 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_106 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)
-- Relation.Binary.Construct.Flip.EqAndOrd._.irrefl
d_irrefl_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_irrefl_112 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Construct.Flip.EqAndOrd._.antisym
d_antisym_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_122 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_122 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_122 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_antisym_122 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_122 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_122 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3
-- Relation.Binary.Construct.Flip.EqAndOrd._.compare
d_compare_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_compare_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny
-> AgdaAny
-> T_Tri_158
d_compare_126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Tri_158
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T_Tri_158
du_compare_126 AgdaAny -> AgdaAny -> T_Tri_158
v6 AgdaAny
v7 AgdaAny
v8
du_compare_126 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
du_compare_126 :: (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T_Tri_158
du_compare_126 AgdaAny -> AgdaAny -> T_Tri_158
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_Tri_158
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v4
           -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v4
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v5
           -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v5
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v6
           -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v6
         T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Construct.Flip.EqAndOrd._.resp₂
d_resp'8322'_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_resp'8322'_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_resp'8322'_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_Σ_14
v6 = T_Σ_14 -> T_Σ_14
du_resp'8322'_188 T_Σ_14
v6
du_resp'8322'_188 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_resp'8322'_188 :: T_Σ_14 -> T_Σ_14
du_resp'8322'_188 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> (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
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Flip.EqAndOrd._.dec
d_dec_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dec_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_dec_206 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Dec_20
v6 AgdaAny
v7 AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
du_dec_206 AgdaAny -> AgdaAny -> T_Dec_20
v6 AgdaAny
v7 AgdaAny
v8
du_dec_206 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dec_206 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
du_dec_206 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v2 AgdaAny
v1
-- Relation.Binary.Construct.Flip.EqAndOrd.isEquivalence
d_isEquivalence_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsEquivalence_28
d_isEquivalence_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsEquivalence_28
v4 = T_IsEquivalence_28 -> T_IsEquivalence_28
du_isEquivalence_210 T_IsEquivalence_28
v4
du_isEquivalence_210 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_isEquivalence_210 :: T_IsEquivalence_28 -> T_IsEquivalence_28
du_isEquivalence_210 T_IsEquivalence_28
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
      (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_refl_44
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_48
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_52
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isDecEquivalence
d_isDecEquivalence_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
d_isDecEquivalence_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecEquivalence_48
-> T_IsDecEquivalence_48
d_isDecEquivalence_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsDecEquivalence_48
v4
  = T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_isDecEquivalence_232 T_IsDecEquivalence_48
v4
du_isDecEquivalence_232 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
du_isDecEquivalence_232 :: T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_isDecEquivalence_232 T_IsDecEquivalence_48
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_48)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_48
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Structures.C_constructor_70
      ((T_IsEquivalence_28 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28
du_isEquivalence_210
         ((T_IsDecEquivalence_48 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_54
            (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
du_dec_206
         ((T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__56 (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isPreorder
d_isPreorder_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_isPreorder_258 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPreorder_76
-> T_IsPreorder_76
d_isPreorder_258 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsPreorder_76
v6 = T_IsPreorder_76 -> T_IsPreorder_76
du_isPreorder_258 T_IsPreorder_76
v6
du_isPreorder_258 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_isPreorder_258 :: T_IsPreorder_76 -> T_IsPreorder_76
du_isPreorder_258 T_IsPreorder_76
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
         (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_106
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
               (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0)))
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_52
         ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isTotalPreorder
d_isTotalPreorder_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalPreorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalPreorder_132
d_isTotalPreorder_304 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsTotalPreorder_132
-> T_IsTotalPreorder_132
d_isTotalPreorder_304 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsTotalPreorder_132
v6
  = T_IsTotalPreorder_132 -> T_IsTotalPreorder_132
du_isTotalPreorder_304 T_IsTotalPreorder_132
v6
du_isTotalPreorder_304 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalPreorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalPreorder_132
du_isTotalPreorder_304 :: T_IsTotalPreorder_132 -> T_IsTotalPreorder_132
du_isTotalPreorder_304 T_IsTotalPreorder_132
v0
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalPreorder_132)
-> AgdaAny -> AgdaAny -> T_IsTotalPreorder_132
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalPreorder_132
MAlonzo.Code.Relation.Binary.Structures.C_constructor_178
      ((T_IsPreorder_76 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76
du_isPreorder_258
         ((T_IsTotalPreorder_132 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalPreorder_132 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_140 (T_IsTotalPreorder_132 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_132
v0)))
      (((AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_60
         ((T_IsTotalPreorder_132 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_132 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_142 (T_IsTotalPreorder_132 -> AgdaAny
forall a b. a -> b
coe T_IsTotalPreorder_132
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isPartialOrder
d_isPartialOrder_350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_isPartialOrder_350 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPartialOrder_248
-> T_IsPartialOrder_248
d_isPartialOrder_350 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsPartialOrder_248
v6
  = T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_isPartialOrder_350 T_IsPartialOrder_248
v6
du_isPartialOrder_350 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_isPartialOrder_350 :: T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_isPartialOrder_350 T_IsPartialOrder_248
v0
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      ((T_IsPreorder_76 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76
du_isPreorder_258
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_122
         ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isTotalOrder
d_isTotalOrder_398 ::
  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_488 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488
d_isTotalOrder_398 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsTotalOrder_488
-> T_IsTotalOrder_488
d_isTotalOrder_398 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsTotalOrder_488
v6
  = T_IsTotalOrder_488 -> T_IsTotalOrder_488
du_isTotalOrder_398 T_IsTotalOrder_488
v6
du_isTotalOrder_398 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488
du_isTotalOrder_398 :: T_IsTotalOrder_488 -> T_IsTotalOrder_488
du_isTotalOrder_398 T_IsTotalOrder_488
v0
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_488)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_488
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Structures.C_constructor_540
      ((T_IsPartialOrder_248 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_isPartialOrder_350
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            (T_IsTotalOrder_488 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_488
v0)))
      (((AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_60
         ((T_IsTotalOrder_488 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_488 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_498 (T_IsTotalOrder_488 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_488
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isDecTotalOrder
d_isDecTotalOrder_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_IsDecTotalOrder_546 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546
d_isDecTotalOrder_450 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecTotalOrder_546
-> T_IsDecTotalOrder_546
d_isDecTotalOrder_450 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsDecTotalOrder_546
v6
  = T_IsDecTotalOrder_546 -> T_IsDecTotalOrder_546
du_isDecTotalOrder_450 T_IsDecTotalOrder_546
v6
du_isDecTotalOrder_450 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546
du_isDecTotalOrder_450 :: T_IsDecTotalOrder_546 -> T_IsDecTotalOrder_546
du_isDecTotalOrder_450 T_IsDecTotalOrder_546
v0
  = (T_IsTotalOrder_488
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_546
forall a b. a -> b
coe
      T_IsTotalOrder_488
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
MAlonzo.Code.Relation.Binary.Structures.C_constructor_618
      ((T_IsTotalOrder_488 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalOrder_488 -> T_IsTotalOrder_488
du_isTotalOrder_398
         ((T_IsDecTotalOrder_546 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_546 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Structures.d_isTotalOrder_556
            (T_IsDecTotalOrder_546 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_546
v0)))
      ((T_IsDecTotalOrder_546 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecTotalOrder_546 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__558 (T_IsDecTotalOrder_546 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_546
v0))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
du_dec_206
         ((T_IsDecTotalOrder_546 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_546 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__560
            (T_IsDecTotalOrder_546 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_546
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isStrictPartialOrder
d_isStrictPartialOrder_518 ::
  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_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_isStrictPartialOrder_518 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370
d_isStrictPartialOrder_518 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictPartialOrder_370
v6
  = T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_isStrictPartialOrder_518 T_IsStrictPartialOrder_370
v6
du_isStrictPartialOrder_518 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
du_isStrictPartialOrder_518 :: T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_isStrictPartialOrder_518 T_IsStrictPartialOrder_370
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_370)
-> T_IsEquivalence_28
-> AgdaAny
-> AgdaAny
-> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.C_constructor_412
      (T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
         (T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_52
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0)))
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14
du_resp'8322'_188
         ((T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.isStrictTotalOrder
d_isStrictTotalOrder_556 ::
  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_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
d_isStrictTotalOrder_556 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_624
-> T_IsStrictTotalOrder_624
d_isStrictTotalOrder_556 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictTotalOrder_624
v6
  = T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
du_isStrictTotalOrder_556 T_IsStrictTotalOrder_624
v6
du_isStrictTotalOrder_556 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
du_isStrictTotalOrder_556 :: T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
du_isStrictTotalOrder_556 T_IsStrictTotalOrder_624
v0
  = (T_IsStrictPartialOrder_370
 -> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_624
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Structures.C_constructor_680
      ((T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_isStrictPartialOrder_518
         ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
            (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
      (((AgdaAny -> AgdaAny -> T_Tri_158)
 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T_Tri_158
du_compare_126
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.setoid
d_setoid_612 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_setoid_612 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Setoid_46
d_setoid_612 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 = T_Setoid_46 -> T_Setoid_46
du_setoid_612 T_Setoid_46
v2
du_setoid_612 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_setoid_612 :: T_Setoid_46 -> T_Setoid_46
du_setoid_612 T_Setoid_46
v0
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      ((T_IsEquivalence_28 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28
du_isEquivalence_210
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.decSetoid
d_decSetoid_644 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
d_decSetoid_644 :: T_Level_18 -> T_Level_18 -> T_DecSetoid_90 -> T_DecSetoid_90
d_decSetoid_644 ~T_Level_18
v0 ~T_Level_18
v1 T_DecSetoid_90
v2 = T_DecSetoid_90 -> T_DecSetoid_90
du_decSetoid_644 T_DecSetoid_90
v2
du_decSetoid_644 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
du_decSetoid_644 :: T_DecSetoid_90 -> T_DecSetoid_90
du_decSetoid_644 T_DecSetoid_90
v0
  = (T_IsDecEquivalence_48 -> T_DecSetoid_90)
-> AgdaAny -> T_DecSetoid_90
forall a b. a -> b
coe
      T_IsDecEquivalence_48 -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_134
      ((T_IsDecEquivalence_48 -> T_IsDecEquivalence_48)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_isDecEquivalence_232
         ((T_DecSetoid_90 -> T_IsDecEquivalence_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_90 -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_106
            (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.preorder
d_preorder_682 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_preorder_682 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_Preorder_142
d_preorder_682 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3 = T_Preorder_142 -> T_Preorder_142
du_preorder_682 T_Preorder_142
v3
du_preorder_682 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_preorder_682 :: T_Preorder_142 -> T_Preorder_142
du_preorder_682 T_Preorder_142
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_IsPreorder_76 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76
du_isPreorder_258
         ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.totalPreorder
d_totalPreorder_760 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240
d_totalPreorder_760 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_240
-> T_TotalPreorder_240
d_totalPreorder_760 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalPreorder_240
v3 = T_TotalPreorder_240 -> T_TotalPreorder_240
du_totalPreorder_760 T_TotalPreorder_240
v3
du_totalPreorder_760 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240
du_totalPreorder_760 :: T_TotalPreorder_240 -> T_TotalPreorder_240
du_totalPreorder_760 T_TotalPreorder_240
v0
  = (T_IsTotalPreorder_132 -> T_TotalPreorder_240)
-> AgdaAny -> T_TotalPreorder_240
forall a b. a -> b
coe
      T_IsTotalPreorder_132 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_334
      ((T_IsTotalPreorder_132 -> T_IsTotalPreorder_132)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalPreorder_132 -> T_IsTotalPreorder_132
du_isTotalPreorder_304
         ((T_TotalPreorder_240 -> T_IsTotalPreorder_132)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_IsTotalPreorder_132
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_262
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.poset
d_poset_844 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_poset_844 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_492 -> T_Poset_492
d_poset_844 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_492
v3 = T_Poset_492 -> T_Poset_492
du_poset_844 T_Poset_492
v3
du_poset_844 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_poset_844 :: T_Poset_492 -> T_Poset_492
du_poset_844 T_Poset_492
v0
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      ((T_IsPartialOrder_248 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_isPartialOrder_350
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
            (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.totalOrder
d_totalOrder_928 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986
d_totalOrder_928 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_TotalOrder_986 -> T_TotalOrder_986
d_totalOrder_928 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> T_TotalOrder_986
du_totalOrder_928 T_TotalOrder_986
v3
du_totalOrder_928 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986
du_totalOrder_928 :: T_TotalOrder_986 -> T_TotalOrder_986
du_totalOrder_928 T_TotalOrder_986
v0
  = (T_IsTotalOrder_488 -> T_TotalOrder_986)
-> AgdaAny -> T_TotalOrder_986
forall a b. a -> b
coe
      T_IsTotalOrder_488 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1090
      ((T_IsTotalOrder_488 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalOrder_488 -> T_IsTotalOrder_488
du_isTotalOrder_398
         ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.decTotalOrder
d_decTotalOrder_1022 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098
d_decTotalOrder_1022 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_DecTotalOrder_1098
-> T_DecTotalOrder_1098
d_decTotalOrder_1022 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_DecTotalOrder_1098
v3 = T_DecTotalOrder_1098 -> T_DecTotalOrder_1098
du_decTotalOrder_1022 T_DecTotalOrder_1098
v3
du_decTotalOrder_1022 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098
du_decTotalOrder_1022 :: T_DecTotalOrder_1098 -> T_DecTotalOrder_1098
du_decTotalOrder_1022 T_DecTotalOrder_1098
v0
  = (T_IsDecTotalOrder_546 -> T_DecTotalOrder_1098)
-> AgdaAny -> T_DecTotalOrder_1098
forall a b. a -> b
coe
      T_IsDecTotalOrder_546 -> T_DecTotalOrder_1098
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1272
      ((T_IsDecTotalOrder_546 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecTotalOrder_546 -> T_IsDecTotalOrder_546
du_isDecTotalOrder_450
         ((T_DecTotalOrder_1098 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecTotalOrder_1098 -> T_IsDecTotalOrder_546
MAlonzo.Code.Relation.Binary.Bundles.d_isDecTotalOrder_1120
            (T_DecTotalOrder_1098 -> AgdaAny
forall a b. a -> b
coe T_DecTotalOrder_1098
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.strictPartialOrder
d_strictPartialOrder_1134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_strictPartialOrder_1134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_760
-> T_StrictPartialOrder_760
d_strictPartialOrder_1134 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_760
v3
  = T_StrictPartialOrder_760 -> T_StrictPartialOrder_760
du_strictPartialOrder_1134 T_StrictPartialOrder_760
v3
du_strictPartialOrder_1134 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
du_strictPartialOrder_1134 :: T_StrictPartialOrder_760 -> T_StrictPartialOrder_760
du_strictPartialOrder_1134 T_StrictPartialOrder_760
v0
  = (T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760)
-> AgdaAny -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_842
      ((T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_isStrictPartialOrder_518
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (T_StrictPartialOrder_760 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_760
v0)))
-- Relation.Binary.Construct.Flip.EqAndOrd.strictTotalOrder
d_strictTotalOrder_1204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
d_strictTotalOrder_1204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_StrictTotalOrder_1280
d_strictTotalOrder_1204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3
  = T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_strictTotalOrder_1204 T_StrictTotalOrder_1280
v3
du_strictTotalOrder_1204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
du_strictTotalOrder_1204 :: T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_strictTotalOrder_1204 T_StrictTotalOrder_1280
v0
  = (T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280)
-> AgdaAny -> T_StrictTotalOrder_1280
forall a b. a -> b
coe
      T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1386
      ((T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
du_isStrictTotalOrder_556
         ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
            (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))