{-# 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.PropositionalEquality.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.Equality
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
d_trans'45'refl'691'_24 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'refl'691'_24 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'refl'691'_24 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_trans'45'assoc_40 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'assoc_40 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'assoc_40 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_trans'45'sym'737'_48 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'sym'737'_48 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'sym'737'_48 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_trans'45'sym'691'_56 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'sym'691'_56 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'sym'691'_56 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_trans'45'injective'737'_70 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'injective'737'_70 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'injective'737'_70 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_trans'45'injective'691'_84 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'injective'691'_84 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'injective'691'_84 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_cong'45'id_94 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'45'id_94 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'45'id_94 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_cong'45''8728'_106 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'45''8728'_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_cong'45''8728'_106 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_trans'45'cong_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'cong_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'cong_120 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_cong'8322''45'refl'737'_134 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'8322''45'refl'737'_134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'8322''45'refl'737'_134 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_cong'8322''45'refl'691'_148 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'8322''45'refl'691'_148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'8322''45'refl'691'_148 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_subst'45'injective_170 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'injective_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'injective_170 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_subst'45'subst_182 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'subst_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45'subst_182 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_subst'45'subst'45'sym_188 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'subst'45'sym_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45'subst'45'sym_188 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_subst'45'sym'45'subst_194 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'sym'45'subst_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45'sym'45'subst_194 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_subst'45''8728'_208 ::
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) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45''8728'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45''8728'_208 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_subst'45'application_240 ::
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) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'application_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'application_240 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_isEquivalence_242 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_242 :: T_Level_18 -> T_Level_18 -> T_IsEquivalence_26
d_isEquivalence_242 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsEquivalence_26
du_isEquivalence_242
du_isEquivalence_242 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_242 :: T_IsEquivalence_26
du_isEquivalence_242
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
d_isDecEquivalence_244 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_244 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecEquivalence_44
d_isDecEquivalence_244 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 = (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
du_isDecEquivalence_244 AgdaAny -> AgdaAny -> T_Dec_32
v2
du_isDecEquivalence_244 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_isDecEquivalence_244 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
du_isDecEquivalence_244 AgdaAny -> AgdaAny -> T_Dec_32
v0
= (T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3075
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
du_isEquivalence_242) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0)
d_isPreorder_248 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_248 :: T_Level_18 -> T_Level_18 -> T_IsPreorder_70
d_isPreorder_248 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsPreorder_70
du_isPreorder_248
du_isPreorder_248 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_248 :: T_IsPreorder_70
du_isPreorder_248
= (T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
du_isEquivalence_242) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) AgdaAny
forall a. a
erased
d_setoid_250 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_250 :: T_Level_18 -> T_Level_18 -> T_Setoid_44
d_setoid_250 ~T_Level_18
v0 ~T_Level_18
v1 = T_Setoid_44
du_setoid_250
du_setoid_250 :: MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_setoid_250 :: T_Setoid_44
du_setoid_250
= (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
du_isEquivalence_242)
d_decSetoid_254 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_decSetoid_254 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecSetoid_84
d_decSetoid_254 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 = (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecSetoid_84
du_decSetoid_254 AgdaAny -> AgdaAny -> T_Dec_32
v2
du_decSetoid_254 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
du_decSetoid_254 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecSetoid_84
du_decSetoid_254 AgdaAny -> AgdaAny -> T_Dec_32
v0
= (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1385
(((AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
du_isDecEquivalence_244 ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0))
d_preorder_258 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_258 :: T_Level_18 -> T_Level_18 -> T_Preorder_132
d_preorder_258 ~T_Level_18
v0 ~T_Level_18
v1 = T_Preorder_132
du_preorder_258
du_preorder_258 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_258 :: T_Preorder_132
du_preorder_258
= (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
(T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
du_isPreorder_248)