{-# 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.Closure.Reflexive.Properties where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Sum

-- Relation.Binary.Construct.Closure.Reflexive.Properties._.=[]⇒
d_'61''91''93''8658'_44 ::
  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) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_'61''91''93''8658'_44 :: T_Level_18
-> T_Level_18
-> 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_ReflClosure_30
-> T_ReflClosure_30
d_'61''91''93''8658'_44 ~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 -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10
                        AgdaAny
v11 T_ReflClosure_30
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_'61''91''93''8658'_44 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
du_'61''91''93''8658'_44 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_'61''91''93''8658'_44 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_'61''91''93''8658'_44 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
             AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
             ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6)
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._._~ᵒ_
d__'126''7506'__62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d__'126''7506'__62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'126''7506'__62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.fromSum
d_fromSum_68 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_fromSum_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_ReflClosure_30
d_fromSum_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__'8846'__30
v6 = T__'8846'__30 -> T_ReflClosure_30
du_fromSum_68 T__'8846'__30
v6
du_fromSum_68 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_fromSum_68 :: T__'8846'__30 -> T_ReflClosure_30
du_fromSum_68 T__'8846'__30
v0
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v1
        -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v1
        -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
             AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
             AgdaAny
v1
      T__'8846'__30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.toSum
d_toSum_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T__'8846'__30
d_toSum_76 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 T_ReflClosure_30
v6 = T_ReflClosure_30 -> T__'8846'__30
du_toSum_76 T_ReflClosure_30
v6
du_toSum_76 ::
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_76 :: T_ReflClosure_30 -> T__'8846'__30
du_toSum_76 T_ReflClosure_30
v0
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v0 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
forall a. a
erased
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v3
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
      T_ReflClosure_30
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.⊎⇔Refl
d_'8846''8660'Refl_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_'8846''8660'Refl_84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Equivalence_16
d_'8846''8660'Refl_84 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = T_Equivalence_16
du_'8846''8660'Refl_84
du_'8846''8660'Refl_84 ::
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_'8846''8660'Refl_84 :: T_Equivalence_16
du_'8846''8660'Refl_84
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56
      ((T__'8846'__30 -> T_ReflClosure_30) -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T_ReflClosure_30
du_fromSum_68) ((T_ReflClosure_30 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe T_ReflClosure_30 -> T__'8846'__30
du_toSum_76)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.sym
d_sym_86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_sym_86 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
d_sym_86 ~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 T_ReflClosure_30
v7 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_sym_86 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T_ReflClosure_30
v7
du_sym_86 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_sym_86 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_sym_86 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
             AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
             ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6)
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.trans
d_trans_94 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_trans_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
d_trans_94 ~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 T_ReflClosure_30
v8 T_ReflClosure_30
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
du_trans_94 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 T_ReflClosure_30
v8 T_ReflClosure_30
v9
du_trans_94 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_trans_94 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
du_trans_94 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T_ReflClosure_30
v4 T_ReflClosure_30
v5
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v4 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v5 of
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
               -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
                    T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
             MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v9
               -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
                    AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                    AgdaAny
v9
             T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v8
        -> case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v5 of
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
               -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
                    AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                    AgdaAny
v8
             MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v11
               -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
                    AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                    ((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
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v8 AgdaAny
v11)
             T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.antisym
d_antisym_114 ::
  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 -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny
d_antisym_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> AgdaAny
d_antisym_114 ~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 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
v7 AgdaAny
v8 ~AgdaAny
v9 T_ReflClosure_30
v10 T_ReflClosure_30
v11
  = (AgdaAny -> AgdaAny)
-> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny
du_antisym_114 AgdaAny -> AgdaAny
v6 AgdaAny
v8 T_ReflClosure_30
v10 T_ReflClosure_30
v11
du_antisym_114 ::
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny
du_antisym_114 :: (AgdaAny -> AgdaAny)
-> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny
du_antisym_114 AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_ReflClosure_30
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v2 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
               -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1
             MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v9
               -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_24
             T_ReflClosure_30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ReflClosure_30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.total
d_total_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_total_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Tri_136
v4 AgdaAny
v5 AgdaAny
v6 = (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_140 AgdaAny -> AgdaAny -> T_Tri_136
v4 AgdaAny
v5 AgdaAny
v6
du_total_140 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_total_140 :: (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_140 AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v4
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                ((AgdaAny -> T_ReflClosure_30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                   AgdaAny
v4)
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v5
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                (T_ReflClosure_30 -> AgdaAny
forall a b. a -> b
coe
                   T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36)
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v6
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                ((AgdaAny -> T_ReflClosure_30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                   AgdaAny
v6)
         T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.dec
d_dec_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dec_174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_dec_174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Dec_32
v4 AgdaAny -> AgdaAny -> T_Dec_32
v5 AgdaAny
v6 AgdaAny
v7 = (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_174 AgdaAny -> AgdaAny -> T_Dec_32
v4 AgdaAny -> AgdaAny -> T_Dec_32
v5 AgdaAny
v6 AgdaAny
v7
du_dec_174 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dec_174 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_174 AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny -> AgdaAny -> T_Dec_32
v1 AgdaAny
v2 AgdaAny
v3
  = (T_Equivalence_16 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      T_Equivalence_16 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.du_map_14
      (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
du_'8846''8660'Refl_84)
      ((T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Sum.du__'8846''45'dec__32
         ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v1 AgdaAny
v2 AgdaAny
v3))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.decidable
d_decidable_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decidable_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_decidable_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Tri_136
v4 AgdaAny
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_decidable_184 AgdaAny -> AgdaAny -> T_Tri_136
v4 AgdaAny
v5 AgdaAny
v6
du_decidable_184 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_decidable_184 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_decidable_184 AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v4
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                   ((AgdaAny -> T_ReflClosure_30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                      AgdaAny
v4))
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v5
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                   (T_ReflClosure_30 -> AgdaAny
forall a b. a -> b
coe
                      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36))
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v6
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
         T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._..extendedlambda0
d_'46'extendedlambda0_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda0_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> (T__'8801'__12 -> T_'8869'_4)
-> AgdaAny
-> T_ReflClosure_30
-> T_'8869'_4
d_'46'extendedlambda0_220 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> (T__'8801'__12 -> T_'8869'_4)
-> AgdaAny
-> T_ReflClosure_30
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.respˡ
d_resp'737'_226 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
d_resp'737'_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
d_resp'737'_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
du_resp'737'_226 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
du_resp'737'_226 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T_ReflClosure_30
v4
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v4 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny
v6)
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v7
        -> (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
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v7
      T_ReflClosure_30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.respʳ
d_resp'691'_234 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
d_resp'691'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
d_resp'691'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'691'_234
du_resp'691'_234 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
du_resp'691'_234 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'691'_234 = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.resp
d_resp_250 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
d_resp_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
d_resp_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 T_ReflClosure_30
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny
du_resp_250 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 T_ReflClosure_30
v9
du_resp_250 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
du_resp_250 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny
du_resp_250 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> AgdaAny
v5)
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> (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
v6
      T_ReflClosure_30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.resp₂
d_resp'8322'_270 ::
  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'_270 :: 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'_270 ~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 -> T_Σ_14
du_resp'8322'_270
du_resp'8322'_270 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_resp'8322'_270 :: T_Σ_14 -> T_Σ_14
du_resp'8322'_270
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'691'_234))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._._~ᵒ_
d__'126''7506'__282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d__'126''7506'__282 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'126''7506'__282 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isPreorder
d_isPreorder_284 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_284 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
d_isPreorder_284 ~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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
du_isPreorder_284 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4
du_isPreorder_284 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_284 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
du_isPreorder_284 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> T_ReflClosure_30 -> AgdaAny
forall a b. a -> b
coe T_ReflClosure_30
du_'46'extendedlambda0_288)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> T_ReflClosure_30
 -> T_ReflClosure_30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
du_trans_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._..extendedlambda0
d_'46'extendedlambda0_288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_'46'extendedlambda0_288 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_ReflClosure_30
d_'46'extendedlambda0_288 ~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 ~T__'8801'__12
v7
  = T_ReflClosure_30
du_'46'extendedlambda0_288
du_'46'extendedlambda0_288 ::
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_'46'extendedlambda0_288 :: T_ReflClosure_30
du_'46'extendedlambda0_288
  = T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isPartialOrder
d_isPartialOrder_290 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_isPartialOrder_290 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_266
-> T_IsPartialOrder_162
d_isPartialOrder_290 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsStrictPartialOrder_266
v4 = T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_isPartialOrder_290 T_IsStrictPartialOrder_266
v4
du_isPartialOrder_290 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_isPartialOrder_290 :: T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_isPartialOrder_290 T_IsStrictPartialOrder_266
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> 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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
du_isPreorder_284
         ((T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> ((AgdaAny -> AgdaAny)
 -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny
du_antisym_114 AgdaAny
forall a. a
erased AgdaAny
v1 AgdaAny
v3 AgdaAny
v4)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isDecPartialOrder
d_isDecPartialOrder_328 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_isDecPartialOrder_328 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecStrictPartialOrder_314
-> T_IsDecPartialOrder_206
d_isDecPartialOrder_328 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsDecStrictPartialOrder_314
v4
  = T_IsDecStrictPartialOrder_314 -> T_IsDecPartialOrder_206
du_isDecPartialOrder_328 T_IsDecStrictPartialOrder_314
v4
du_isDecPartialOrder_328 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_isDecPartialOrder_328 :: T_IsDecStrictPartialOrder_314 -> T_IsDecPartialOrder_206
du_isDecPartialOrder_328 T_IsDecStrictPartialOrder_314
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      ((T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_isPartialOrder_290
         ((T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_324
            (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
      ((T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__326 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_174
         ((T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__326 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0))
         ((T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_314 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'60''63'__328 (T_IsDecStrictPartialOrder_314 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_314
v0)))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isTotalOrder
d_isTotalOrder_378 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_isTotalOrder_378 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsTotalOrder_384
d_isTotalOrder_378 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsStrictTotalOrder_502
v4 = T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384
du_isTotalOrder_378 T_IsStrictTotalOrder_502
v4
du_isTotalOrder_378 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
du_isTotalOrder_378 :: T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384
du_isTotalOrder_378 T_IsStrictTotalOrder_502
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
      ((T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_isPartialOrder_290
         ((T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.du_isStrictPartialOrder_540
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_140
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isDecTotalOrder
d_isDecTotalOrder_430 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_isDecTotalOrder_430 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsDecTotalOrder_434
d_isDecTotalOrder_430 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsStrictTotalOrder_502
v4
  = T_IsStrictTotalOrder_502 -> T_IsDecTotalOrder_434
du_isDecTotalOrder_430 T_IsStrictTotalOrder_502
v4
du_isDecTotalOrder_430 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
du_isDecTotalOrder_430 :: T_IsStrictTotalOrder_502 -> T_IsDecTotalOrder_434
du_isDecTotalOrder_430 T_IsStrictTotalOrder_502
v0
  = (T_IsTotalOrder_384
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_434
forall a b. a -> b
coe
      T_IsTotalOrder_384
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
      ((T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384
du_isTotalOrder_378 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
      ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__518 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_174
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__518 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__520
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))