{-# 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
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
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
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
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
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)
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
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
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
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)
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))
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)
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
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
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
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
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))
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
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))
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
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)
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)))
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)))
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)))