agda 相关问题

Agda是一种依赖类型的全功能编程语言和证明助手。

我有两个密切相关的问题：首先，如何在 Agda 中建模/表示 Haskell 的 Arrow 类？类箭头 a 哪里 arr :: (b -> c) -> a b c (>>...

haskell agda arrow-abstraction

回答 2 投票 0

所以我正在 Agda 中实现一些（大部分）HoTT 定义。为了检查类型是否是我定义的集合： isSet : ∀ (A : 集合) → 集合 isSet A = ∀ {x y : A} (p q : (x eq y)) → (p eq) 这个证明...

agda cubical-type-theory

回答 1 投票 0

Coq/Proof General 中类似 Agda 的编程？

与 Agda 不同，Coq 倾向于将证明与函数分开。 Coq 提供的策略非常适合编写证明，但我想知道是否有办法复制一些 Agda 模式功能。具体...

coq agda dependent-type proof-general coqide

回答 2 投票 0

如何通知 Agda 类型检查器两个类型确实相等？

这是一个最小的（非）工作示例。中缀 4 _≡_ data _≡_ {a} {A : 设置 a} (x : A) : A → 设置 a 其中参考：x == x {-# 内在平等 _≡_ #-} 数据类型₁：设置在哪里 id：类型₁ 非...

types equality agda dependent-type

回答 1 投票 0

如何证明 Agda 中广义组合的伪结合性？

我一直在尝试翻译论文“Continuation-Passing Style, Defunctionization, Accumulations, and Associativity”，可以在这里找到：https://arxiv.org/ftp/arxiv/papers/2111/2111.10...

composition agda associativity agda-stdlib

回答 1 投票 0

定义 HIT 操作

我是一个简单的人，并没有真正理解Cubical Agda的所有来龙去脉。我尝试阅读它的文档和 HoTT，但很快就停止了关注正在发生的事情。我是什么

agda

回答 1 投票 0

Agda 的类别库？

是否有任何“推荐”库可以在 Agda 中提供易于使用的基本范畴论形式化？ Agda 标准库似乎在这方面提供的很少。我在找...

standard-library agda category-theory

回答 2 投票 0

`agda-mode`找不到可执行文件

我通过Cabal在Codespaces中安装了Agda，安装似乎运行良好，我也可以在集成终端中使用Agda，但是扩展agda-mode给了我这个错误：连接错误：无法...

ubuntu vscode-extensions agda codespaces

回答 1 投票 0

Agda：证明 ØAny≃AllØ

我想证明 Ø任何≃全部Ø : ∀ {A : 集合} → {P : A → 集合} → (xs : 列表 A) → (Ø_ ∘ 任意 P) xs ≃ 全部 (Ø_ ∘ P) xs 我已经定义了到 [] t = [] 到 (x :: xs) v = (v ∘ 这里) ∷ 到 xs (v ∘ 那里) 来自 [] ...

agda

回答 1 投票 0

Agda：证明 ØAny≃AllØ，FromTo 基本情况

遵循 PLFA，我试图证明这一点 Ø任何≃全部Ø : ∀ {A : 集合} → {P : A → 集合} → (xs : 列表 A) → (Ø_ ∘ 任意 P) xs ≃ 全部 (Ø_ ∘ P) xs 我的问题是从到 : ∀ {A : 集合} → {P : A → 集合} → (x...

agda

回答 1 投票 0

在证明身份时使用论证具有一定的模式

从PLFA我试图证明All-++-≃，也就是说， All-++-≃ : ∀ {A : 集合} {P : A → 集合} (xs ys : 列表 A) → 所有 P (xs ++ ys) ≃ (所有 P xs × 所有 P ys) 我的问题是从到 : ∀ {A : 设置...

agda

回答 2 投票 0

不安全的强制和更高效的Agda代码（-ftrust-me-im-agda）

在 Agda 邮件列表上，Conor McBride 问道：有什么办法可以得到像假设一样的操作 trustFromJust :: 也许 x -> x 它实际上并没有检查 Just 和 G...