{-# 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.Properties.Poset where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Consequences
import qualified MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
import qualified MAlonzo.Code.Relation.Binary.Properties.Preorder
import qualified MAlonzo.Code.Relation.Binary.Structures
d__'8777'__50 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> ()
d__'8777'__50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8777'__50 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_invIsPreorder_136 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_invIsPreorder_136 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_IsPreorder_70
d_invIsPreorder_136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 = T_Poset_282 -> T_IsPreorder_70
du_invIsPreorder_136 T_Poset_282
v3
du_invIsPreorder_136 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_invIsPreorder_136 :: T_Poset_282 -> T_IsPreorder_70
du_invIsPreorder_136 T_Poset_282
v0
= (T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_invIsPreorder_64
((T_Poset_282 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d_invPreorder_138 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_invPreorder_138 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_Preorder_132
d_invPreorder_138 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 = T_Poset_282 -> T_Preorder_132
du_invPreorder_138 T_Poset_282
v3
du_invPreorder_138 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_invPreorder_138 :: T_Poset_282 -> T_Preorder_132
du_invPreorder_138 T_Poset_282
v0
= (T_Preorder_132 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
T_Preorder_132 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_invPreorder_66
((T_Poset_282 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d__'8805'__140 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> ()
d__'8805'__140 :: T_Poset_282 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8805'__140 = T_Poset_282 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
d_'8805''45'isPartialOrder_146 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8805''45'isPartialOrder_146 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_IsPartialOrder_162
d_'8805''45'isPartialOrder_146 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282 -> T_IsPartialOrder_162
du_'8805''45'isPartialOrder_146 T_Poset_282
v3
du_'8805''45'isPartialOrder_146 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_'8805''45'isPartialOrder_146 :: T_Poset_282 -> T_IsPartialOrder_162
du_'8805''45'isPartialOrder_146 T_Poset_282
v0
= (T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Properties.Preorder.du_invIsPreorder_64
((T_Poset_282 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)))
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
(T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
(T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> T_Poset_282
forall a b. a -> b
coe T_Poset_282
v0))
AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3))
d_'8805''45'poset_148 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_'8805''45'poset_148 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_Poset_282
d_'8805''45'poset_148 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 = T_Poset_282 -> T_Poset_282
du_'8805''45'poset_148 T_Poset_282
v3
du_'8805''45'poset_148 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_'8805''45'poset_148 :: T_Poset_282 -> T_Poset_282
du_'8805''45'poset_148 T_Poset_282
v0
= (T_IsPartialOrder_162 -> T_Poset_282) -> AgdaAny -> T_Poset_282
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_282 -> T_IsPartialOrder_162
du_'8805''45'isPartialOrder_146 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d_antisym_152 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
= T_Poset_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_152 T_Poset_282
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
du_antisym_152 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_152 :: T_Poset_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_152 T_Poset_282
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
= (T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
(T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> T_Poset_282
forall a b. a -> b
coe T_Poset_282
v0))
AgdaAny
v1 AgdaAny
v2 AgdaAny
v4 AgdaAny
v3
d_refl_154 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny
d_refl_154 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> AgdaAny -> AgdaAny
d_refl_154 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 = T_Poset_282 -> AgdaAny -> AgdaAny
du_refl_154 T_Poset_282
v3
du_refl_154 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny
du_refl_154 :: T_Poset_282 -> AgdaAny -> AgdaAny
du_refl_154 T_Poset_282
v0
= let v1 :: t
v1 = (T_Poset_282 -> T_Poset_282) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_282 -> T_Poset_282
du_'8805''45'poset_148 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0) in
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v2 :: T_IsPartialOrder_162
v2
= T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(AgdaAny -> T_Poset_282
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsPreorder_70 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
(T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v2))))
d_reflexive_156 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
= T_Poset_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_156 T_Poset_282
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
du_reflexive_156 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_156 :: T_Poset_282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_156 T_Poset_282
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
(T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
((T_Poset_282 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)))
AgdaAny
v2 AgdaAny
v1
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
(T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
((T_IsPartialOrder_162 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))))
AgdaAny
v1 AgdaAny
v2 AgdaAny
v3)
d_trans_158 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_158 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_158 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
= T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_158 T_Poset_282
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
du_trans_158 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_158 :: T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_158 T_Poset_282
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
= (T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
((T_Poset_282 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)))
AgdaAny
v3 AgdaAny
v2 AgdaAny
v1 AgdaAny
v5 AgdaAny
v4
d__'8816'__160 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> ()
d__'8816'__160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8816'__160 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_'8816''45'resp'737''45''8776'_166 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8816''45'resp'737''45''8776'_166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
d_'8816''45'resp'737''45''8776'_166 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
d_'8816''45'resp'691''45''8776'_172 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8816''45'resp'691''45''8776'_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
d_'8816''45'resp'691''45''8776'_172 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
d__'60'__178 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny -> AgdaAny -> ()
d__'60'__178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__178 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_'60''45'isStrictPartialOrder_180 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_180 T_Poset_282
v3
du_'60''45'isStrictPartialOrder_180 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_180 :: T_Poset_282 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_180 T_Poset_282
v0
= (T_IsPartialOrder_162 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'60''45'isStrictPartialOrder_438
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d_'60''45'strictPartialOrder_182 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_'60''45'strictPartialOrder_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> T_StrictPartialOrder_472
d_'60''45'strictPartialOrder_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_182 T_Poset_282
v3
du_'60''45'strictPartialOrder_182 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_182 :: T_Poset_282 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_182 T_Poset_282
v0
= (T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe
T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_8957
((T_Poset_282 -> T_IsStrictPartialOrder_266) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_282 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_180 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d_asym_186 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_asym_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_'8869'_4
d_asym_186 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_'8869'_4
forall a. a
erased
d_irrefl_188 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_'8869'_4
d_irrefl_188 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_'8869'_4
forall a. a
erased
d_'60''45'resp'45''8776'_190 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'45''8776'_190 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_Σ_14
d_'60''45'resp'45''8776'_190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282 -> T_Σ_14
du_'60''45'resp'45''8776'_190 T_Poset_282
v3
du_'60''45'resp'45''8776'_190 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'45''8776'_190 :: T_Poset_282 -> T_Σ_14
du_'60''45'resp'45''8776'_190 T_Poset_282
v0
= (T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
((T_Poset_282 -> T_IsStrictPartialOrder_266) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_282 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_180 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d_'60''45'resp'691''45''8776'_192 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'691''45''8776'_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'691''45''8776'_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'691''45''8776'_192 T_Poset_282
v3
du_'60''45'resp'691''45''8776'_192 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'691''45''8776'_192 :: T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'691''45''8776'_192 T_Poset_282
v0
= let v1 :: t
v1 = (T_Poset_282 -> T_StrictPartialOrder_472) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_282 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_182 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0) in
AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
((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.du_'60''45'resp'691''45''8776'_304
((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
d_'60''45'resp'737''45''8776'_194 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'737''45''8776'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'737''45''8776'_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'737''45''8776'_194 T_Poset_282
v3
du_'60''45'resp'737''45''8776'_194 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'737''45''8776'_194 :: T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'737''45''8776'_194 T_Poset_282
v0
= let v1 :: t
v1 = (T_Poset_282 -> T_StrictPartialOrder_472) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_282 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_182 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0) in
AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
((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.du_'60''45'resp'737''45''8776'_306
((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
d_trans_196 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_trans_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_trans_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 = T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_trans_196 T_Poset_282
v3
du_trans_196 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_trans_196 :: T_Poset_282
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_trans_196 T_Poset_282
v0
= (T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282
((T_Poset_282 -> T_IsStrictPartialOrder_266) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_282 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_180 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))
d_'60''8658''8777'_202 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''8658''8777'_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_'8869'_4
d_'60''8658''8777'_202 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
d_'8804''8743''8777''8658''60'_208 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''8743''8777''8658''60'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> T_Σ_14
d_'8804''8743''8777''8658''60'_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Poset_282
v3 ~AgdaAny
v4 ~AgdaAny
v5
= AgdaAny -> (AgdaAny -> T_'8869'_4) -> T_Σ_14
du_'8804''8743''8777''8658''60'_208
du_'8804''8743''8777''8658''60'_208 ::
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''8743''8777''8658''60'_208 :: AgdaAny -> (AgdaAny -> T_'8869'_4) -> T_Σ_14
du_'8804''8743''8777''8658''60'_208
= (AgdaAny -> (AgdaAny -> T_'8869'_4) -> T_Σ_14)
-> AgdaAny -> (AgdaAny -> T_'8869'_4) -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> (AgdaAny -> T_'8869'_4) -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict.du_'8804''8743''8777''8658''60'_44
d_'60''8658''8817'_214 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''8658''8817'_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_'8869'_4
d_'60''8658''8817'_214 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
d_'8804''8658''8815'_220 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8804''8658''8815'_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_'8869'_4
d_'8804''8658''8815'_220 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_'8869'_4
forall a. a
erased
d_mono'8658'cong_224 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono'8658'cong_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_mono'8658'cong_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 AgdaAny -> AgdaAny
v4
= T_Poset_282
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_224 T_Poset_282
v3 AgdaAny -> AgdaAny
v4
du_mono'8658'cong_224 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_mono'8658'cong_224 :: T_Poset_282
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_224 T_Poset_282
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Consequences.du_mono'8658'cong_226
(let v2 :: t
v2
= (T_Poset_282 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)))))
((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))))
((T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_antimono'8658'cong_228 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antimono'8658'cong_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antimono'8658'cong_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 AgdaAny -> AgdaAny
v4
= T_Poset_282
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_228 T_Poset_282
v3 AgdaAny -> AgdaAny
v4
du_antimono'8658'cong_228 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antimono'8658'cong_228 :: T_Poset_282
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_228 T_Poset_282
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Consequences.du_antimono'8658'cong_240
(let v2 :: t
v2
= (T_Poset_282 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe
T_Poset_282 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.du_preorder_326 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)))))
((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0))))
((T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
d_invIsPartialOrder_230 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_invIsPartialOrder_230 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_IsPartialOrder_162
d_invIsPartialOrder_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282 -> T_IsPartialOrder_162
du_invIsPartialOrder_230 T_Poset_282
v3
du_invIsPartialOrder_230 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_invIsPartialOrder_230 :: T_Poset_282 -> T_IsPartialOrder_162
du_invIsPartialOrder_230 T_Poset_282
v0
= (T_Poset_282 -> T_IsPartialOrder_162)
-> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe T_Poset_282 -> T_IsPartialOrder_162
du_'8805''45'isPartialOrder_146 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)
d_invPoset_232 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_invPoset_232 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Poset_282 -> T_Poset_282
d_invPoset_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3 = T_Poset_282 -> T_Poset_282
du_invPoset_232 T_Poset_282
v3
du_invPoset_232 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_invPoset_232 :: T_Poset_282 -> T_Poset_282
du_invPoset_232 T_Poset_282
v0 = (T_Poset_282 -> T_Poset_282) -> AgdaAny -> T_Poset_282
forall a b. a -> b
coe T_Poset_282 -> T_Poset_282
du_'8805''45'poset_148 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)
d_strictPartialOrder_234 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_strictPartialOrder_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_282
-> T_StrictPartialOrder_472
d_strictPartialOrder_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Poset_282
v3
= T_Poset_282 -> T_StrictPartialOrder_472
du_strictPartialOrder_234 T_Poset_282
v3
du_strictPartialOrder_234 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_strictPartialOrder_234 :: T_Poset_282 -> T_StrictPartialOrder_472
du_strictPartialOrder_234 T_Poset_282
v0
= (T_Poset_282 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe T_Poset_282 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_182 (T_Poset_282 -> AgdaAny
forall a b. a -> b
coe T_Poset_282
v0)