{-# 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.NonStrictToStrict 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.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d__'8777'__20 ::
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 -> ()
d__'8777'__20 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8777'__20 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
d__'60'__26 ::
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 -> ()
d__'60'__26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__26 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_'60''8658''8804'_32 ::
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.Sigma.T_Σ_14 -> AgdaAny
d_'60''8658''8804'_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
d_'60''8658''8804'_32 ~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 ~AgdaAny
v6 ~AgdaAny
v7 T_Σ_14
v8
= T_Σ_14 -> AgdaAny
du_'60''8658''8804'_32 T_Σ_14
v8
du_'60''8658''8804'_32 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
du_'60''8658''8804'_32 :: T_Σ_14 -> AgdaAny
du_'60''8658''8804'_32 T_Σ_14
v0
= (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v0)
d_'60''8658''8777'_38 ::
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.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''8658''8777'_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
d_'60''8658''8777'_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
d_'8804''8743''8777''8658''60'_44 ::
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 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''8743''8777''8658''60'_44 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
d_'8804''8743''8777''8658''60'_44 ~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 ~AgdaAny
v6 ~AgdaAny
v7
= AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
du_'8804''8743''8777''8658''60'_44
du_'8804''8743''8777''8658''60'_44 ::
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''8743''8777''8658''60'_44 :: AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
du_'8804''8743''8777''8658''60'_44
= (AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
d_'60''8658''8817'_50 ::
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 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''8658''8817'_50 :: 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
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
d_'60''8658''8817'_50 = 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
-> T_Σ_14
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
d_'8804''8658''8815'_64 ::
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.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8804''8658''8815'_64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
d_'8804''8658''8815'_64 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
d_'8816''8658''62'_76 ::
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) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8816''8658''62'_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
d_'8816''8658''62'_76 ~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 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny -> T_Irrelevant_20
v11
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
du_'8816''8658''62'_76 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny -> T_Irrelevant_20
v11
du_'8816''8658''62'_76 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8816''8658''62'_76 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
du_'8816''8658''62'_76 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny -> T_Irrelevant_20
v5
= let v6 :: t
v6 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny
v3 AgdaAny
v4 in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v6 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v8 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Irrelevant_20
v5 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v3 AgdaAny
v8))))
T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'8814''8658''8805'_126 ::
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.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny
d_'8814''8658''8805'_126 :: 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 -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> (T_Σ_14 -> T_Irrelevant_20)
-> AgdaAny
d_'8814''8658''8805'_126 ~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 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8846'__30
v9 AgdaAny
v10
AgdaAny
v11 ~T_Σ_14 -> T_Irrelevant_20
v12
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8814''8658''8805'_126 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8846'__30
v9 AgdaAny
v10 AgdaAny
v11
du_'8814''8658''8805'_126 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
AgdaAny -> AgdaAny -> AgdaAny
du_'8814''8658''8805'_126 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8814''8658''8805'_126 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> T__'8846'__30
v3 AgdaAny
v4 AgdaAny
v5
= let v6 :: t
v6 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v4 AgdaAny
v5 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v7 :: t
v7 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v3 AgdaAny
v5 AgdaAny
v4 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v6 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v8 T_Reflects_16
v9
-> let v10 :: b
v10
= case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v10 -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
v10
T__'8846'__30
_ -> b
forall a. a
MAlonzo.RTE.mazUnreachableError in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then let v11 :: b
v11
= case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11 -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
v11
T__'8846'__30
_ -> b
forall a. a
MAlonzo.RTE.mazUnreachableError in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v9 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v12
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v5 AgdaAny
v12)
T_Reflects_16
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
else (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
-> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v9 of
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
T_Reflects_16
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10
T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
d_'60''45'irrefl_196 ::
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 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''45'irrefl_196 :: 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
-> T_Σ_14
-> T_Irrelevant_20
d_'60''45'irrefl_196 = 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
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
d_'60''45'trans_202 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
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_'60''45'trans_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPartialOrder_174
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'60''45'trans_202 ~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_IsPartialOrder_174
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 T_Σ_14
v11
= T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'60''45'trans_202 T_IsPartialOrder_174
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10 T_Σ_14
v11
du_'60''45'trans_202 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
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_'60''45'trans_202 :: T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'60''45'trans_202 T_IsPartialOrder_174
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T_Σ_14
v4 T_Σ_14
v5
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v5 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (T_IsPartialOrder_174 -> T_IsPartialOrder_174
forall a b. a -> b
coe T_IsPartialOrder_174
v0))
AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v6 AgdaAny
v8)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v10 ->
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
v7
((T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 T_IsPartialOrder_174
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6
((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
(T_IsPartialOrder_174 -> T_IsPartialOrder_174
forall a b. a -> b
coe T_IsPartialOrder_174
v0))
AgdaAny
v2 AgdaAny
v3 AgdaAny
v1 AgdaAny
v8
((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_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
(T_IsPartialOrder_174 -> T_IsPartialOrder_174
forall a b. a -> b
coe T_IsPartialOrder_174
v0))
AgdaAny
v3 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_174 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
(T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0)))
AgdaAny
v1 AgdaAny
v3 AgdaAny
v10))))))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60''45''8804''45'trans_256 ::
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 -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45''8804''45'trans_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
d_'60''45''8804''45'trans_256 ~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 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 T_Σ_14
v13 AgdaAny
v14
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_'60''45''8804''45'trans_256 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 T_Σ_14
v13 AgdaAny
v14
du_'60''45''8804''45'trans_256 ::
(AgdaAny -> 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.Agda.Builtin.Sigma.T_Σ_14 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45''8804''45'trans_256 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
-> T_Σ_14
du_'60''45''8804''45'trans_256 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T_Σ_14
v7 AgdaAny
v8
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v9 AgdaAny
v10
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v9 AgdaAny
v8)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v11 ->
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v4 AgdaAny
v5 AgdaAny
v9 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v5 AgdaAny
v6 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v6 AgdaAny
v11) AgdaAny
v8))))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8804''45''60''45'trans_274 ::
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 -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''45''60''45'trans_274 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'8804''45''60''45'trans_274 ~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 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9
AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 T_Σ_14
v13
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
du_'8804''45''60''45'trans_274 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 T_Σ_14
v13
du_'8804''45''60''45'trans_274 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''45''60''45'trans_274 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
du_'8804''45''60''45'trans_274 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T_Σ_14
v7
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v10 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v4 AgdaAny
v5 AgdaAny
v8 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v4 AgdaAny
v3 AgdaAny
v5 AgdaAny
v10 AgdaAny
v6))))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60''45'asym_290 ::
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 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''45'asym_290 :: 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
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'60''45'asym_290 = 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
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
d_'60''45'resp'737''45''8776'_300 ::
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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
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'_300 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'737''45''8776'_300 ~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 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8
AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_Σ_14
v12
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
du_'60''45'resp'737''45''8776'_300 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_Σ_14
v12
du_'60''45'resp'737''45''8776'_300 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
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'_300 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
du_'60''45'resp'737''45''8776'_300 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T_Σ_14
v6
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v6 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v9 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8 ((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
v3 AgdaAny
v4 AgdaAny
v2 AgdaAny
v5 AgdaAny
v9)))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60''45'resp'691''45''8776'_312 ::
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 -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
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'_312 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'691''45''8776'_312 ~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 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8
AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 T_Σ_14
v13
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
du_'60''45'resp'691''45''8776'_312 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 T_Σ_14
v13
du_'60''45'resp'691''45''8776'_312 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
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'_312 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
du_'60''45'resp'691''45''8776'_312 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T_Σ_14
v7
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v10 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v5 AgdaAny
v4 AgdaAny
v10 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6))))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60''45'resp'45''8776'_328 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'45''8776'_328 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> T_Σ_14
d_'60''45'resp'45''8776'_328 ~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_IsEquivalence_26
v6 T_Σ_14
v7
= T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'45''8776'_328 T_IsEquivalence_26
v6 T_Σ_14
v7
du_'60''45'resp'45''8776'_328 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'resp'45''8776'_328 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'45''8776'_328 T_IsEquivalence_26
v0 T_Σ_14
v1
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14)
-> 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
-> T_Σ_14
-> T_Σ_14
du_'60''45'resp'691''45''8776'_312
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14)
-> 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
-> T_Σ_14
-> T_Σ_14
du_'60''45'resp'737''45''8776'_300
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60''45'trichotomous_352 ::
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.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_'60''45'trichotomous_352 :: 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 -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T_Tri_158
d_'60''45'trichotomous_352 ~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 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8846'__30
v9
AgdaAny
v10 AgdaAny
v11
= (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T_Tri_158
du_'60''45'trichotomous_352 AgdaAny -> AgdaAny -> T_Dec_20
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v9 AgdaAny
v10 AgdaAny
v11
du_'60''45'trichotomous_352 ::
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
du_'60''45'trichotomous_352 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T_Tri_158
du_'60''45'trichotomous_352 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny
v2 AgdaAny
v3
= let v4 :: t
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v2 AgdaAny
v3 in
AgdaAny -> T_Tri_158
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v4 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v7
-> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v7
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6)
(let v7 :: t
v7 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny
v2 AgdaAny
v3 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v8
-> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8) AgdaAny
forall a. a
erased)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v8
-> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8) AgdaAny
forall a. a
erased)
T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'60''45'decidable_434 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'60''45'decidable_434 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_'60''45'decidable_434 ~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 AgdaAny -> AgdaAny -> T_Dec_20
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7 AgdaAny
v8 AgdaAny
v9
= (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'60''45'decidable_434 AgdaAny -> AgdaAny -> T_Dec_20
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7 AgdaAny
v8 AgdaAny
v9
du_'60''45'decidable_434 ::
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'60''45'decidable_434 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'60''45'decidable_434 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3)
((T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_'172''63'_70
((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v2 AgdaAny
v3))
d_'60''45'isStrictPartialOrder_444 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_444 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPartialOrder_174
-> T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_444 ~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_IsPartialOrder_174
v6
= T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_444 T_IsPartialOrder_174
v6
du_'60''45'isStrictPartialOrder_444 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_444 :: T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_444 T_IsPartialOrder_174
v0
= (T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_290)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
(T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
((T_IsPartialOrder_174 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0)))
((T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'60''45'trans_202 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0))
((T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'resp'45''8776'_328
((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_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0)))
((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_118
((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
(T_IsPartialOrder_174 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_174
v0))))
d_'60''45'isDecStrictPartialOrder_490 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_336
d_'60''45'isDecStrictPartialOrder_490 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecPartialOrder_224
-> T_IsDecStrictPartialOrder_336
d_'60''45'isDecStrictPartialOrder_490 ~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_IsDecPartialOrder_224
v6
= T_IsDecPartialOrder_224 -> T_IsDecStrictPartialOrder_336
du_'60''45'isDecStrictPartialOrder_490 T_IsDecPartialOrder_224
v6
du_'60''45'isDecStrictPartialOrder_490 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_336
du_'60''45'isDecStrictPartialOrder_490 :: T_IsDecPartialOrder_224 -> T_IsDecStrictPartialOrder_336
du_'60''45'isDecStrictPartialOrder_490 T_IsDecPartialOrder_224
v0
= (T_IsStrictPartialOrder_290
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecStrictPartialOrder_336)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecStrictPartialOrder_336
forall a b. a -> b
coe
T_IsStrictPartialOrder_290
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecStrictPartialOrder_336
MAlonzo.Code.Relation.Binary.Structures.C_IsDecStrictPartialOrder'46'constructor_18663
((T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_444
((T_IsDecPartialOrder_224 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecPartialOrder_224 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_234
(T_IsDecPartialOrder_224 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_224
v0)))
((T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__236 (T_IsDecPartialOrder_224 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_224
v0))
(((AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_'60''45'decidable_434
((T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__236 (T_IsDecPartialOrder_224 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_224
v0))
((T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__238
(T_IsDecPartialOrder_224 -> AgdaAny
forall a b. a -> b
coe T_IsDecPartialOrder_224
v0)))
d_'60''45'isStrictTotalOrder'8321'_548 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'8321'_548 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsTotalOrder_404
-> T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'8321'_548 ~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 AgdaAny -> AgdaAny -> T_Dec_20
v6
T_IsTotalOrder_404
v7
= (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsTotalOrder_404 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8321'_548 AgdaAny -> AgdaAny -> T_Dec_20
v6 T_IsTotalOrder_404
v7
du_'60''45'isStrictTotalOrder'8321'_548 ::
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8321'_548 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsTotalOrder_404 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8321'_548 AgdaAny -> AgdaAny -> T_Dec_20
v0 T_IsTotalOrder_404
v1
= (T_IsStrictPartialOrder_290
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
T_IsStrictPartialOrder_290
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_24953
((T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_444
((T_IsTotalOrder_404 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsTotalOrder_404 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_412
(T_IsTotalOrder_404 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_404
v1)))
(((AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T_Tri_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T_Tri_158
du_'60''45'trichotomous_352 ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0)
((T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_404 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_414 (T_IsTotalOrder_404 -> AgdaAny
forall a b. a -> b
coe T_IsTotalOrder_404
v1)))
d_'60''45'isStrictTotalOrder'8322'_602 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'8322'_602 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecTotalOrder_460
-> T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'8322'_602 ~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_IsDecTotalOrder_460
v6
= T_IsDecTotalOrder_460 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8322'_602 T_IsDecTotalOrder_460
v6
du_'60''45'isStrictTotalOrder'8322'_602 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8322'_602 :: T_IsDecTotalOrder_460 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8322'_602 T_IsDecTotalOrder_460
v0
= ((AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsTotalOrder_404 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsTotalOrder_404 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder'8321'_548
((T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecTotalOrder_460 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__472 (T_IsDecTotalOrder_460 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_460
v0))
((T_IsDecTotalOrder_460 -> T_IsTotalOrder_404) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecTotalOrder_460 -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Structures.d_isTotalOrder_470
(T_IsDecTotalOrder_460 -> AgdaAny
forall a b. a -> b
coe T_IsDecTotalOrder_460
v0))