To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F
is a Functor
):
Fix : (* -> *) -> *
in : ∀F. F (Fix F) -> Fix F
out : ∀F. Fix F -> F (Fix F)
We can then write down the type of case discrimination and folding:
case : ∀F T. (F (Fix F) -> T) -> Fix F -> T
fold : ∀F T. (F T -> T) -> Fix F -> T
But what is the type of induction (if there is one)? I've gotten this far:
ind : ∀F T (P : Fix F -> *). (∀(h : Fix F). P h -> P ???) -> (x : Fix F) -> P x
Assuming the rest is correct, what should be in the place of ???
?
Alternatively, what is the type of dependent case discrimination?
lift_fiber : forall A : *, (A -> *) -> (F A -> *)
. This is certainly enough to express what you need. $\endgroup$