Coq defining a hierarchy of collections of integers with infinitely many "levels"

Question

I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic).

It's straightforward to formalize something resembling second-order arithmetic or something resembling higher-order arithmetic in Coq if there are a fixed number of possible levels.

I'm curious if there's a way to define such a notion, though, for an infinite number of levels.

Require Import BinNums.

Definition col (X : Type) : Type := X -> bool.

(* This is bad because it only goes up to 2 levels *)
Inductive col_hierarchy_bad_1 : Type :=
| catom : N -> col_hierarchy_bad_1
| ccol1 : (col N) -> col_hierarchy_bad_1
| ccol2 : (col (col N)) -> col_hierarchy_bad_1.

(* This attempt doesn't even compile. I'm trying to decorate "col_hierarchy"
   with the kind of thing it contains and then later figure out how to stitch
   the different col_hierarchies together into a single type. *)
(*
Inductive col_hierarchy_bad_2 (contents : Type) : Type :=
| catom : N -> col_hierarchy_bad_2 N
| ccol : forall T : Type, (col_hierarchy_bad_2 T -> col_hierarchy_bad_2 (col T)). 
*)

Answer 1

A simple way is to define the type in terms of the Peano natural numbers nat.

Require Import BinNums Arith.

Definition col (X : Type) : Type := X -> bool.

Fixpoint col_repeat (n : nat) (X : Type) : Type :=
match n with
| O => X
| S n => col (col_repeat n X)
end.

Inductive col_hierarchy : Type :=
| ccoln (n : nat) : col_repeat n N -> col_hierarchy.

This way, ccoln 0 corresponds to your catom, ccoln 1 to ccol1, and so on, and ccoln n is defined for every natural number n.

Answer 2

Your definition is awkward because of strict positivity requirements in inductive datatypes.

Your definition of col is really a decidable subset and there exists an alternative strictly positive encoding of subsets in terms of the image of a function.

Inductive hierarchy: nat -> Type :=
| catom: N -> hierarchy 0
| cimage {n} (X: Set): (X -> hierarchy n) -> hierarchy (S n).

The decidable hierarchy consists of

Fixpoint decidable {n} (h: hierarchy) : Type :=
  match h with
  | catom _ => unit
  | cimage X P => (forall y. {exists x. P x = y} + {~exists x. P x = y}) * forall x. decidable (P x)
  end.

A little mucky but I thought it was worth mentioning. The image strictly positive encoding trick is often useful for some constructions.