Given the following definition of ordinals how would you define a nice induction principle over them?

```
CoInductive stream A := {
head: A ;
tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).
```

Given the following definition of ordinals how would you define a nice induction principle over them?

```
CoInductive stream A := {
head: A ;
tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).
```

I couldn’t figure out how to use `Fixpoint`

through coinductive types either, but if you replace `stream A`

with `nat -> A`

it’s possible to define

```
Fixpoint ord_ind (P : ord -> Prop)
(HO : P O)
(HS : forall n, P n -> P (S n))
(HSup : forall f, (forall i, P (f i)) -> P (Sup f))
: forall n, P n.
```

Ah well that was what I was planning on avoiding.

And I don’t think there is way to define an isomorphism between

```
Inductive ord := O | S (n: ord) | Lim (p: nat -> ord).
```

And the other representation without extensionality which I was maybe thinking of assuming but it’d be nice not to have to use

Full context for an induction principle which doesn’t quite go through.

See also How is coinduction the dual of induction? – Blog – Joachim Breitner's Homepage