Type of induction principle for fixpoint types

Question

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?

The word induction is used when we construct an inductive type, i.e., the smallest or initial fixed point of a type constructor $F$. However, a general type constructor need not have an initial or smallest fixed point, and therefore no reasonable induction principle can be stated in general. — Andrej Bauer, Jan 28 '20 at 17:42
If we let $F(X) = X \to \mathsf{Empty}$, what is $\mathsf{Fix}(F)$? — Andrej Bauer, Jan 28 '20 at 17:43
If we constrain F in some way (for example strictly positive occurrences of X), can we then state a induction principle? — Labbekak, Jan 28 '20 at 17:53
I think you need an additional constraint over $F$, namely that it is behaves well over "fibrations", i.e. that there is some function lift_fiber : forall A : *, (A -> *) -> (F A -> *). This is certainly enough to express what you need. — cody, Jan 28 '20 at 20:37
@cody: right, and we don't need any strict positivity, just covariance, in order to phraase the induction principle. — Andrej Bauer, Jan 28 '20 at 20:45

Labbekak · Accepted Answer · 2020-01-31 20:16:57Z

2

To answer my own question, the paper Generic derivation of induction for impredicative encodings in Cedille shows a type for induction on a fixpoint type. It can look like:

ind : ∀F T (P : Fix F -> *). ((h : F (Σ (Fix F) P)) -> P (in (map fst h))) -> (x : Fix F) -> P x

With Σ being the dependent product and map the functor map of F.

answered Jan 31 '20 at 20:16

Labbekak

6913 silver badges9 bronze badges

$\begingroup$ Just a note, having this Fix type is not enough to derive induction for inductive datatypes like Nat or List. You'd also need an induction principle for F. If F is constructed from unit, sums and products then you'd need induction principles for those. $\endgroup$
– Labbekak
Feb 11 '20 at 11:34

Add a comment |

1 Answer 1