{-# 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.On 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.Empty
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Induction.WellFounded
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

-- Relation.Binary.Construct.On._.implies
d_implies_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  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
d_implies_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_implies_38 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_implies_38 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_implies_38 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_implies_38 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_implies_38 AgdaAny -> AgdaAny
v0 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
v1
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v4) AgdaAny
v2 AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5) AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Construct.On._.reflexive
d_reflexive_44 ::
  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
d_reflexive_44 :: 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
d_reflexive_44 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_reflexive_44 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v7 AgdaAny
v8
du_reflexive_44 ::
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_reflexive_44 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_reflexive_44 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny
v1
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
         (\ AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3) AgdaAny
v2 AgdaAny
v2)
-- Relation.Binary.Construct.On._.irreflexive
d_irreflexive_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_irreflexive_52 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_irreflexive_52 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Construct.On._.symmetric
d_symmetric_58 ::
  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
d_symmetric_58 :: 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
d_symmetric_58 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_symmetric_58 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_symmetric_58 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_symmetric_58 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_symmetric_58 AgdaAny -> AgdaAny
v0 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
v1
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v4) AgdaAny
v2 AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5) AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Construct.On._.transitive
d_transitive_64 ::
  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
d_transitive_64 :: 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_transitive_64 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 AgdaAny -> 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_transitive_64 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_transitive_64 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_transitive_64 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_transitive_64 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
         (\ AgdaAny
v5 AgdaAny
v6 -> AgdaAny
v5) AgdaAny
v2 AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v5 AgdaAny
v6 -> AgdaAny
v6) AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v5 AgdaAny
v6 -> AgdaAny
v6) AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)
-- Relation.Binary.Construct.On._.antisymmetric
d_antisymmetric_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  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_antisymmetric_72 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> 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_antisymmetric_72 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisymmetric_72 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_antisymmetric_72 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisymmetric_72 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisymmetric_72 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v4) AgdaAny
v2 AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5) AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Construct.On._.asymmetric
d_asymmetric_78 ::
  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) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asymmetric_78 :: 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 -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asymmetric_78 = 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 -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Construct.On._.respects
d_respects_86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  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
d_respects_86 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_respects_86 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_respects_86 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_respects_86 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_respects_86 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_respects_86 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v4) AgdaAny
v2 AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5) AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Construct.On._.respects₂
d_respects'8322'_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  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_respects'8322'_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_respects'8322'_94 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_Σ_14
v9
  = (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_respects'8322'_94 AgdaAny -> AgdaAny
v4 T_Σ_14
v9
du_respects'8322'_94 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_respects'8322'_94 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_respects'8322'_94 AgdaAny -> AgdaAny
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (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
forall a b. a -> b
coe
                (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
                   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     AgdaAny
v2
                     (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
                        (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v7) AgdaAny
v4 AgdaAny
v5)
                     (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
                        (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v7) AgdaAny
v5 AgdaAny
v6)
                     (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
                        (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v8) AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6)))
             ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
                   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     AgdaAny
v3
                     (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
                        (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v8) AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v4)
                     (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v0
                        (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v7) AgdaAny
v5 AgdaAny
v6)
                     (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
                        (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v8) AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6)))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.On._.decidable
d_decidable_102 ::
  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.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decidable_102 :: 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_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_decidable_102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 AgdaAny -> AgdaAny -> T_Dec_32
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T_Dec_32
v7 AgdaAny
v8 AgdaAny
v9
du_decidable_102 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_decidable_102 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Dec_32
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
-- Relation.Binary.Construct.On._.total
d_total_112 ::
  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.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_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 -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_total_112 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 AgdaAny -> AgdaAny -> T__'8846'__30
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_total_112 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T__'8846'__30
v7 AgdaAny
v8 AgdaAny
v9
du_total_112 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_total_112 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_total_112 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
-- Relation.Binary.Construct.On._.trichotomous
d_trichotomous_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  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_136) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
d_trichotomous_124 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Tri_136
d_trichotomous_124 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny -> T_Tri_136
v9 AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Tri_136
du_trichotomous_124 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T_Tri_136
v9 AgdaAny
v10 AgdaAny
v11
du_trichotomous_124 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
du_trichotomous_124 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Tri_136
du_trichotomous_124 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Tri_136
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
-- Relation.Binary.Construct.On._.accessible
d_accessible_136 ::
  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 ->
  MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
  MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_accessible_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_136 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Relation.Binary.Construct.On._.wellFounded
d_wellFounded_146 ::
  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 -> MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
  AgdaAny -> MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_wellFounded_146 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_146 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Relation.Binary.Construct.On._.isEquivalence
d_isEquivalence_166 ::
  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.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_IsEquivalence_26
d_isEquivalence_166 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 AgdaAny -> AgdaAny
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsEquivalence_26
v7
  = (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 AgdaAny -> AgdaAny
v5 T_IsEquivalence_26
v7
du_isEquivalence_166 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_166 :: (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 AgdaAny -> AgdaAny
v0 T_IsEquivalence_26
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_reflexive_44 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
      (((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
du_symmetric_58 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_transitive_64 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1)))
-- Relation.Binary.Construct.On._.isDecEquivalence
d_isDecEquivalence_186 ::
  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.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
d_isDecEquivalence_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 AgdaAny -> AgdaAny
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 T_IsDecEquivalence_44
v7
  = (AgdaAny -> AgdaAny)
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_isDecEquivalence_186 AgdaAny -> AgdaAny
v5 T_IsDecEquivalence_44
v7
du_isDecEquivalence_186 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_isDecEquivalence_186 :: (AgdaAny -> AgdaAny)
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_isDecEquivalence_186 AgdaAny -> AgdaAny
v0 T_IsDecEquivalence_44
v1
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3075
      (((AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
            (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v1)))
-- Relation.Binary.Construct.On._.isPreorder
d_isPreorder_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPreorder_70
-> T_IsPreorder_70
d_isPreorder_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsPreorder_70
v9
  = (AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_228 AgdaAny -> AgdaAny
v6 T_IsPreorder_70
v9
du_isPreorder_228 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_228 :: (AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_228 AgdaAny -> AgdaAny
v0 T_IsPreorder_70
v1
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      (((AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
      (((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
du_implies_38 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_transitive_64 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v1)))
-- Relation.Binary.Construct.On._.isPartialOrder
d_isPartialOrder_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsPartialOrder_162 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_isPartialOrder_264 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPartialOrder_162
-> T_IsPartialOrder_162
d_isPartialOrder_264 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsPartialOrder_162
v9
  = (AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_isPartialOrder_264 AgdaAny -> AgdaAny
v6 T_IsPartialOrder_162
v9
du_isPartialOrder_264 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_isPartialOrder_264 :: (AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_isPartialOrder_264 AgdaAny -> AgdaAny
v0 T_IsPartialOrder_162
v1
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
      (((AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_228 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
      (((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_antisymmetric_72 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v1)))
-- Relation.Binary.Construct.On._.isDecPartialOrder
d_isDecPartialOrder_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsDecPartialOrder_206 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_isDecPartialOrder_304 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecPartialOrder_206
-> T_IsDecPartialOrder_206
d_isDecPartialOrder_304 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsDecPartialOrder_206
v9
  = (AgdaAny -> AgdaAny)
-> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_isDecPartialOrder_304 AgdaAny -> AgdaAny
v6 T_IsDecPartialOrder_206
v9
du_isDecPartialOrder_304 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_isDecPartialOrder_304 :: (AgdaAny -> AgdaAny)
-> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_isDecPartialOrder_304 AgdaAny -> AgdaAny
v0 T_IsDecPartialOrder_206
v1
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      (((AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_isPartialOrder_264 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecPartialOrder_206 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_216
            (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__218 (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecPartialOrder_206 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__220
            (T_IsDecPartialOrder_206 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_206
v1)))
-- Relation.Binary.Construct.On._.isStrictPartialOrder
d_isStrictPartialOrder_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_isStrictPartialOrder_356 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266
d_isStrictPartialOrder_356 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsStrictPartialOrder_266
v9
  = (AgdaAny -> AgdaAny)
-> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_isStrictPartialOrder_356 AgdaAny -> AgdaAny
v6 T_IsStrictPartialOrder_266
v9
du_isStrictPartialOrder_356 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
du_isStrictPartialOrder_356 :: (AgdaAny -> AgdaAny)
-> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_isStrictPartialOrder_356 AgdaAny -> AgdaAny
v0 T_IsStrictPartialOrder_266
v1
  = (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
      (((AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((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
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_transitive_64 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((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
v1)))
      (((AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_respects'8322'_94 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v1)))
-- Relation.Binary.Construct.On._.isTotalOrder
d_isTotalOrder_394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsTotalOrder_384 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_isTotalOrder_394 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsTotalOrder_384
-> T_IsTotalOrder_384
d_isTotalOrder_394 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsTotalOrder_384
v9
  = (AgdaAny -> AgdaAny) -> T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_isTotalOrder_394 AgdaAny -> AgdaAny
v6 T_IsTotalOrder_384
v9
du_isTotalOrder_394 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
du_isTotalOrder_394 :: (AgdaAny -> AgdaAny) -> T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_isTotalOrder_394 AgdaAny -> AgdaAny
v0 T_IsTotalOrder_384
v1
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
      (((AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_isPartialOrder_264 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsTotalOrder_384 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
            (T_IsTotalOrder_384 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_total_112 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsTotalOrder_384 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_394 (T_IsTotalOrder_384 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_384
v1)))
-- Relation.Binary.Construct.On._.isDecTotalOrder
d_isDecTotalOrder_440 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsDecTotalOrder_434 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_isDecTotalOrder_440 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecTotalOrder_434
-> T_IsDecTotalOrder_434
d_isDecTotalOrder_440 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsDecTotalOrder_434
v9
  = (AgdaAny -> AgdaAny)
-> T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_isDecTotalOrder_440 AgdaAny -> AgdaAny
v6 T_IsDecTotalOrder_434
v9
du_isDecTotalOrder_440 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
du_isDecTotalOrder_440 :: (AgdaAny -> AgdaAny)
-> T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_isDecTotalOrder_440 AgdaAny -> AgdaAny
v0 T_IsDecTotalOrder_434
v1
  = (T_IsTotalOrder_384
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_434
forall a b. a -> b
coe
      T_IsTotalOrder_384
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
      (((AgdaAny -> AgdaAny) -> T_IsTotalOrder_384 -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_isTotalOrder_394 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecTotalOrder_434 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.d_isTotalOrder_444
            (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__446 (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_decidable_102 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecTotalOrder_434 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__448
            (T_IsDecTotalOrder_434 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_434
v1)))
-- Relation.Binary.Construct.On._.isStrictTotalOrder
d_isStrictTotalOrder_500 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
d_isStrictTotalOrder_500 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsStrictTotalOrder_502
d_isStrictTotalOrder_500 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 T_IsStrictTotalOrder_502
v9
  = (AgdaAny -> AgdaAny)
-> T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_isStrictTotalOrder_500 AgdaAny -> AgdaAny
v6 T_IsStrictTotalOrder_502
v9
du_isStrictTotalOrder_500 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
du_isStrictTotalOrder_500 :: (AgdaAny -> AgdaAny)
-> T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_isStrictTotalOrder_500 AgdaAny -> AgdaAny
v0 T_IsStrictTotalOrder_502
v1
  = (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
      (((AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((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
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_transitive_64 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((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
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny
 -> AgdaAny
 -> T_Tri_136)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Tri_136
du_trichotomous_124 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((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
v1)))
-- Relation.Binary.Construct.On.preorder
d_preorder_554 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_132 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_554 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_132
-> (AgdaAny -> AgdaAny)
-> T_Preorder_132
d_preorder_554 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Preorder_132
v5 AgdaAny -> AgdaAny
v6 = T_Preorder_132 -> (AgdaAny -> AgdaAny) -> T_Preorder_132
du_preorder_554 T_Preorder_132
v5 AgdaAny -> AgdaAny
v6
du_preorder_554 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_554 :: T_Preorder_132 -> (AgdaAny -> AgdaAny) -> T_Preorder_132
du_preorder_554 T_Preorder_132
v0 AgdaAny -> AgdaAny
v1
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      (((AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70
du_isPreorder_228 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Relation.Binary.Construct.On.setoid
d_setoid_562 ::
  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_Setoid_44 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_562 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (AgdaAny -> AgdaAny)
-> T_Setoid_44
d_setoid_562 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4 AgdaAny -> AgdaAny
v5 = T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Setoid_44
du_setoid_562 T_Setoid_44
v4 AgdaAny -> AgdaAny
v5
du_setoid_562 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_setoid_562 :: T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Setoid_44
du_setoid_562 T_Setoid_44
v0 AgdaAny -> AgdaAny
v1
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26
du_isEquivalence_166 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
-- Relation.Binary.Construct.On.decSetoid
d_decSetoid_570 ::
  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_DecSetoid_84 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_decSetoid_570 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_DecSetoid_84
-> (AgdaAny -> AgdaAny)
-> T_DecSetoid_84
d_decSetoid_570 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_DecSetoid_84
v4 AgdaAny -> AgdaAny
v5 = T_DecSetoid_84 -> (AgdaAny -> AgdaAny) -> T_DecSetoid_84
du_decSetoid_570 T_DecSetoid_84
v4 AgdaAny -> AgdaAny
v5
du_decSetoid_570 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
du_decSetoid_570 :: T_DecSetoid_84 -> (AgdaAny -> AgdaAny) -> T_DecSetoid_84
du_decSetoid_570 T_DecSetoid_84
v0 AgdaAny -> AgdaAny
v1
  = (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1385
      (((AgdaAny -> AgdaAny)
 -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_isDecEquivalence_186 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
            (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0)))
-- Relation.Binary.Construct.On.poset
d_poset_578 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_282 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_poset_578 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> (AgdaAny -> AgdaAny)
-> T_Poset_282
d_poset_578 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Poset_282
v5 AgdaAny -> AgdaAny
v6 = T_Poset_282 -> (AgdaAny -> AgdaAny) -> T_Poset_282
du_poset_578 T_Poset_282
v5 AgdaAny -> AgdaAny
v6
du_poset_578 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_poset_578 :: T_Poset_282 -> (AgdaAny -> AgdaAny) -> T_Poset_282
du_poset_578 T_Poset_282
v0 AgdaAny -> AgdaAny
v1
  = (T_IsPartialOrder_162 -> T_Poset_282) -> AgdaAny -> T_Poset_282
forall a b. a -> b
coe
      T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
      (((AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162 -> T_IsPartialOrder_162
du_isPartialOrder_264 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
            (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)))
-- Relation.Binary.Construct.On.decPoset
d_decPoset_586 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_DecPoset_360 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
d_decPoset_586 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_DecPoset_360
-> (AgdaAny -> AgdaAny)
-> T_DecPoset_360
d_decPoset_586 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_DecPoset_360
v5 AgdaAny -> AgdaAny
v6 = T_DecPoset_360 -> (AgdaAny -> AgdaAny) -> T_DecPoset_360
du_decPoset_586 T_DecPoset_360
v5 AgdaAny -> AgdaAny
v6
du_decPoset_586 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
du_decPoset_586 :: T_DecPoset_360 -> (AgdaAny -> AgdaAny) -> T_DecPoset_360
du_decPoset_586 T_DecPoset_360
v0 AgdaAny -> AgdaAny
v1
  = (T_IsDecPartialOrder_206 -> T_DecPoset_360)
-> AgdaAny -> T_DecPoset_360
forall a b. a -> b
coe
      T_IsDecPartialOrder_206 -> T_DecPoset_360
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_6777
      (((AgdaAny -> AgdaAny)
 -> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206
du_isDecPartialOrder_304 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_DecPoset_360 -> T_IsDecPartialOrder_206) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecPoset_360 -> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Bundles.d_isDecPartialOrder_382
            (T_DecPoset_360 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_360
v0)))
-- Relation.Binary.Construct.On.strictPartialOrder
d_strictPartialOrder_594 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_472 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_strictPartialOrder_594 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_472
-> (AgdaAny -> AgdaAny)
-> T_StrictPartialOrder_472
d_strictPartialOrder_594 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_StrictPartialOrder_472
v5 AgdaAny -> AgdaAny
v6
  = T_StrictPartialOrder_472
-> (AgdaAny -> AgdaAny) -> T_StrictPartialOrder_472
du_strictPartialOrder_594 T_StrictPartialOrder_472
v5 AgdaAny -> AgdaAny
v6
du_strictPartialOrder_594 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_strictPartialOrder_594 :: T_StrictPartialOrder_472
-> (AgdaAny -> AgdaAny) -> T_StrictPartialOrder_472
du_strictPartialOrder_594 T_StrictPartialOrder_472
v0 AgdaAny -> AgdaAny
v1
  = (T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_8957
      (((AgdaAny -> AgdaAny)
 -> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_isStrictPartialOrder_356 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
            (T_StrictPartialOrder_472 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_472
v0)))
-- Relation.Binary.Construct.On.totalOrder
d_totalOrder_602 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_652 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652
d_totalOrder_602 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> T_TotalOrder_652
d_totalOrder_602 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_TotalOrder_652
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> T_TotalOrder_652
du_totalOrder_602 T_TotalOrder_652
v5 AgdaAny -> AgdaAny
v6
du_totalOrder_602 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652
du_totalOrder_602 :: T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> T_TotalOrder_652
du_totalOrder_602 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = (T_IsTotalOrder_384 -> T_TotalOrder_652)
-> AgdaAny -> T_TotalOrder_652
forall a b. a -> b
coe
      T_IsTotalOrder_384 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Bundles.C_TotalOrder'46'constructor_12489
      (((AgdaAny -> AgdaAny) -> T_IsTotalOrder_384 -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsTotalOrder_384 -> T_IsTotalOrder_384
du_isTotalOrder_394 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_TotalOrder_652 -> T_IsTotalOrder_384) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)))
-- Relation.Binary.Construct.On.decTotalOrder
d_decTotalOrder_610 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_740 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
d_decTotalOrder_610 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_DecTotalOrder_740
-> (AgdaAny -> AgdaAny)
-> T_DecTotalOrder_740
d_decTotalOrder_610 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_DecTotalOrder_740
v5 AgdaAny -> AgdaAny
v6
  = T_DecTotalOrder_740 -> (AgdaAny -> AgdaAny) -> T_DecTotalOrder_740
du_decTotalOrder_610 T_DecTotalOrder_740
v5 AgdaAny -> AgdaAny
v6
du_decTotalOrder_610 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
du_decTotalOrder_610 :: T_DecTotalOrder_740 -> (AgdaAny -> AgdaAny) -> T_DecTotalOrder_740
du_decTotalOrder_610 T_DecTotalOrder_740
v0 AgdaAny -> AgdaAny
v1
  = (T_IsDecTotalOrder_434 -> T_DecTotalOrder_740)
-> AgdaAny -> T_DecTotalOrder_740
forall a b. a -> b
coe
      T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_14337
      (((AgdaAny -> AgdaAny)
 -> T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsDecTotalOrder_434 -> T_IsDecTotalOrder_434
du_isDecTotalOrder_440 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_DecTotalOrder_740 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecTotalOrder_740 -> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Bundles.d_isDecTotalOrder_762
            (T_DecTotalOrder_740 -> AgdaAny
forall a b. a -> b
coe T_DecTotalOrder_740
v0)))
-- Relation.Binary.Construct.On.strictTotalOrder
d_strictTotalOrder_618 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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_864 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_strictTotalOrder_618 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny)
-> T_StrictTotalOrder_864
d_strictTotalOrder_618 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_StrictTotalOrder_864
v5 AgdaAny -> AgdaAny
v6
  = T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny) -> T_StrictTotalOrder_864
du_strictTotalOrder_618 T_StrictTotalOrder_864
v5 AgdaAny -> AgdaAny
v6
du_strictTotalOrder_618 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
du_strictTotalOrder_618 :: T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny) -> T_StrictTotalOrder_864
du_strictTotalOrder_618 T_StrictTotalOrder_864
v0 AgdaAny -> AgdaAny
v1
  = (T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864)
-> AgdaAny -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_16739
      (((AgdaAny -> AgdaAny)
 -> T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_isStrictTotalOrder_500 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
            (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)))