我可以使用Axiom命令定义一个等价的吗?

Question

mu不能定义

Definiton mu (A : Type) (f : A -> A) : A := f (mu A f).

但是，Axiom命令可以用来伪定义mu。

Axiom mu : forall A : Type, (A -> A) -> A.
Axiom mu_beta : forall (A : Type) (f : A -> A), mu A f = f (mu A f).

我可以对higher_path和higher_path_argument做同样的事情吗?即使使用了几种技术，这似乎仍然是不可能的。

Definition higher_path
: forall n : nat, higher_path_argument n -> Type
:= fun n : nat =>
match n with
| O => fun x : higher_path_argument 0 => x
| S n_p =>
fun x : higher_path_argument (S n_p) =>
match x with
| existT _ x_a x_b =>
match x_b with
| pair x_b_a x_b_b => x_b_a = x_b_b :> higher_path n_p x_a
end
end
end.
Definition higher_path_argument
: nat -> Type
:= fun n : nat =>
match n with
| O => Type
| S n_p =>
sigT
(A := higher_path_argument n_p)
(fun x_p => prod (higher_path n_p x_p) (higher_path n_p x_p))
end.

Answer 1

你必须从

开始

Axiom higher_path_argument : nat -> Type.
Axiom higher_path : forall n : nat, higher_path_argument n -> Type.

然后higher_path_argument_beta，你将不得不在higher_path_beta中使用计算的类型。然而，你最终会得到一些非常冗长的东西。