CODEWITHSUNDEEP
coq
Hexirp
Hexirp

Reputation: 420

Can I define an equivalent to this using the Axiom command?

mu can not be defined.

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

However, the Axiom command can be used to pseudo-define 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).

Can I do the same for higher_path and higher_path_argument? Even after using several techniques, it still seems to be impossible.

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.

Upvotes: 0

Views: 61

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

You will have to start with

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

then higher_path_argument_beta which you will have to use in the higher_path_beta to compute the type. You will however end up with something really verbose however.

Upvotes: 1

Related Questions