Really confused here. I thought induction was not derivable. Not sure how that applies to anafunctions?

impredicative_induction.v

Require Import Coq.Unicode.Utf8.

(* ana is short for anafunction, not really a better name *)
Definition ana A := { P: A → Prop | exists! a: A, P a }.

Definition map {A B} (f: A → B) (x: ana A): ana B.
Proof.
  exists (λ b, ∃ a, proj1_sig x a ∧ f a = b).
  destruct x as [? [a p]].
  exists (f a).
  cbn.
  split.
  - exists a.
    split.
    2: reflexivity.
    destruct p.
    auto.
  - intro y.
    intros [a' [? q]].
    replace a' with a in q.
    1: auto.
    eapply p.
    auto.
Defined.

Definition pure {A} (x: A): ana A.
Proof.
  exists (eq x).
  exists x.
  split.
  1: reflexivity.
  auto.
Defined.

Definition bind {A B} (f: A → ana B) (x: ana A): ana B.
Proof.
  exists (λ b, ∃ a, proj1_sig x a ∧ proj1_sig (f a) b).
  destruct x as [? [a p]].
  destruct (proj2_sig (f a)) as [y q].
  exists y.
  cbn.
  split.
  - exists a.
    split.
    + destruct p.
      auto.
    + destruct q.
      auto.
  - intro y'.
    intros [a' [r s]].
    destruct q.
    destruct p.
    eapply H0.
    replace a' with a in s.
    1: auto.
    apply H2.
    eauto.
Defined.

Definition nat: Type := ∀ N, ana N → (N → ana N) → ana N.

Definition O: nat.
Proof.
  intros N O S.
  exact O.
Defined.

Definition S (n: nat): nat.
Proof.
  intros N O S.
  exact (bind S (n N O S)).
Defined.

(* Recursor + eta laws is equivalent in power to induction correct? *)
Definition fold N O' S' (n: nat) := n N O' S'.

Lemma fold_O N O' S': fold N O' S' O = O'.
Proof.
  cbn in *.
  reflexivity.
Qed.

Lemma fold_S N O' S' (n: nat):
  ∀ m,
  proj1_sig (bind S' (fold N O' S' n)) m ↔
  proj1_sig (fold N O' S' (S n)) m.
Proof.
  intro m.
  cbn.
  split.
  - intro.
    auto.
  - intro.
    auto.
Defined.