<p>To answer my own question, the paper <a href="https://www.researchgate.net/publication/322191243_Generic_derivation_of_induction_for_impredicative_encodings_in_Cedille" rel="nofollow noreferrer">Generic derivation of induction for impredicative encodings in Cedille</a> shows a type for induction on a fixpoint type. It can look like:</p>

<pre><code>ind : ∀F T (P : Fix F -&gt; *). ((h : F (Σ (Fix F) P)) -&gt; P (in (map fst h))) -&gt; (x : Fix F) -&gt; P x
</code></pre>

<p>With <code>Σ</code> being the dependent product and <code>map</code> the functor map of <code>F</code>.</p>

CC BY-SA 4.0
2020-02-11T11:34:26.500Z
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.
Labbekak
CC BY-SA 4.0
2020-01-31T20:16:57.653Z
2020-01-31T20:16:57.653Z
Labbekak
<p>To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming <code>F</code> is a <code>Functor</code>):</p>

<pre><code>Fix : (* -&gt; *) -&gt; *
in  : ∀F. F (Fix F) -&gt; Fix F
out : ∀F. Fix F -&gt; F (Fix F)
</code></pre>

<p>We can then write down the type of case discrimination and folding:</p>

<pre><code>case : ∀F T. (F (Fix F) -&gt; T) -&gt; Fix F -&gt; T
fold : ∀F T. (F T -&gt; T) -&gt; Fix F -&gt; T
</code></pre>

<p>But what is the type of induction (if there is one)? I've gotten this far:</p>

<pre><code>ind : ∀F T (P : Fix F -&gt; *). (∀(h : Fix F). P h -&gt; P ???) -&gt; (x : Fix F) -&gt; P x
</code></pre>

<p>Assuming the rest is correct, what should be in the place of <code>???</code>?
Alternatively, what is the type of dependent case discrimination?</p>

CC BY-SA 4.0
2020-01-28T17:42:32.213Z
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
CC BY-SA 4.0
2020-01-28T17:43:14.127Z
If we let $F(X) = X \to \mathsf{Empty}$, what is $\mathsf{Fix}(F)$?
Andrej Bauer
CC BY-SA 4.0
2020-01-28T17:53:44.137Z
If we constrain F in some way (for example strictly positive occurrences of X), can we then state a induction principle?
Labbekak
CC BY-SA 4.0
2020-01-28T20:37:44.963Z
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
CC BY-SA 4.0
2020-01-28T20:44:58.017Z
Okay interesting, but then could you write down the type of `induction` for all `Fix F`? Or you could write down `induction` for a specific `F` in `Fix F` only?
Labbekak
CC BY-SA 4.0
2020-01-28T20:45:27.147Z
@cody: right, and we don't need any strict positivity, just covariance, in order to *phraase* the induction principle.
Andrej Bauer
<type-theory><dependent-type><typed-lambda-calculus><calculus-of-constructions>
Type of induction principle for fixpoint types
Labbekak
# Type of induction principle for fixpoint types

(Asked by: username_0 on 2020-01-28)

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?

**Tags:** type-theory, dependent-type, typed-lambda-calculus, calculus-of-constructions
> **Comments:**
> **username_1**: 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.  
> **username_1**: If we let $F(X) = X \to \mathsf{Empty}$, what is $\mathsf{Fix}(F)$?  
> **username_0**: If we constrain F in some way (for example strictly positive occurrences of X), can we then state a induction principle?  
> **username_2**: 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.  
> **username_0**: Okay interesting, but then could you write down the type of `induction` for all `Fix F`? Or you could write down `induction` for a specific `F` in `Fix F` only?  
> **username_1**: @cody: right, and we don't need any strict positivity, just covariance, in order to *phraase* the induction principle.  

---

## 1 answers

### Answer by username_0 on 2020-01-31. Score: 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.

> **Comments:**
> **username_0**: 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.  

---

