小编Bob*_*Bob的帖子

如何将州monad S -> (A, S)与costate comonad 结合起来(E->A, E)？

我试图与这两个明显的组合S -> ((E->A, E), S)和(E->S->(A, S), E)后来在这两种情况下,我不知道如何定义的操作(return,extract,...等等)的组合.

在 Cubical Agda 的标准库中，有一些有限的多重集，我在下面重现了它们的优雅定义：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude

infixr 20 _?_

data FMSet (A : Set) : Set where
  []    : FMSet A
  _?_   : (x : A) ? (xs : FMSet A) ? FMSet A
  comm  : ? x y xs ? x ? y ? xs ? y ? x ? xs
  trunc : isSet (FMSet A)

_++_ : ? {A : Set} -> FMSet A ? FMSet A ? FMSet A …

我有一个 DER 格式的 base64 编码的公钥。在Python中，如何将其转换为COSE密钥？

这是我失败的尝试：

from base64 import b64decode
from cose.keys import CoseKey

pubkeyder = "...=="
decCborData.key = CoseKey.decode(b64decode(pubkeyder))

在下面的代码中,如何替换put 1某些在该状态下插入非确定性1或2的代码？

import Control.Monad.List
import Control.Monad.Trans.State

test :: StateT Int [] Int
test = do
  put 1
  v <- get
  return v

我可以定义以下归纳类型：

Inductive T : Type -> Type :=
| c1 : forall (A : Type), A -> T A
| c2 : T unit.

但随后该命令Check (c1 (T nat))失败并显示以下消息：该术语T nat具有类型，Type@{max(Set, Top.3+1)}而预期具有类型Type@{Top.3}（宇宙不一致）。

我怎样才能调整上面的归纳定义，以便c1 (T nat)不会导致宇宙不一致，并且不设置宇宙多态性？

以下工作，但我更喜欢不添加平等的解决方案：

Inductive T (A : Type) : Type :=
| c1 : A -> T A
| c2' : A = unit -> T A.

Definition c2 : T unit := c2' unit eq_refl.

Check (c1 (T …

是否可以证明 John Major 等式的功能可扩展性（可能依赖于安全公理）？

Goal forall A (P:A->Type) (Q:A->Type)
(f:forall a, P a) (g:forall a, Q a),
(forall a, JMeq (f a) (g a)) -> JMeq f g.

如果不是，将其假设为公理是否安全？

如何在（纯）构造演算中定义递归函数？我在那里没有看到任何固定点组合器。

假设我有

• 共生 D
• 单子 T
• 一个l : D T -> T DcomonadD对 monad的分配法则T。

我如何定义 comonad D T？

以下代码旨在将布尔型的Church编码打印为Haskell的Bool：

{-#LANGUAGE FlexibleInstances #-}

instance Show (t -> t -> t) where
  show b = show $ b True False

导致此错误：

<interactive>:4:21: error:
• Couldn't match expected type ‘t’ with actual type ‘Bool’
  ‘t’ is a rigid type variable bound by
    the instance declaration at <interactive>:3:10-27
• In the first argument of ‘b’, namely ‘True’
  In the second argument of ‘($)’, namely ‘b True False’
  In the expression: show $ b True False
• Relevant bindings include
    b …