I tried to do some Polynominal endofunctor stuff in a slightly more syntactic way. Unfortunately I don't think it quite works.

syntactic.v

Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.

Inductive U :=
| const (A: Type)

| id
(* | compose (τ0 τ1: U) *)

| empty
| sum (τ0 τ1: U)

| unit
| prod (τ0 τ1: U)

| Σ {A: Type} (τ: A → U)
| Π {A: Type} (τ: A → U)
.

Implicit Type τ: U.

(* Infix "∘" := compose (at level 30). *)
Infix "+" := sum.
Infix "*" := prod.

Inductive El {X: Type}: U → Type :=
| pure: X → El id

(* Not sure how this might work *)
(* | join {τ1 τ2} {A: Type}: @El A τ1 → (A → El τ2) → El (τ1 ∘ τ2) *)
(* | join {τ1 τ2}: @El (El τ2) τ1 → El (τ1 ∘ τ2) *)

| k {A}: A → El (const A)

| i1 {τ1 τ2}: El τ1 → El (τ1 + τ2)
| i2 {τ1 τ2}: El τ2 → El (τ1 + τ2)

| tt: El unit
| fanout {τ1 τ2}: El τ1 → El τ2 → El (τ1 * τ2)

| ex {A} {τ: A → U} (x: A): El (τ x) → El (Σ τ)
| Λ {A} {τ: A → U}: (∀ (x: A), El (τ x)) → El (Π τ)
.

Arguments El: clear implicits.

Definition unpure {A} (x: El A id): A :=
  match x with
  | pure x => x
  end.

Fixpoint map {P A B} (f: A → B) (x: El A P) {struct x}: El B P :=
  match x with
  | pure x => pure (f x)

  | k x => k x
  | i1 x' => i1 (map f x')
  | i2 x' => i2 (map f x')

  | tt => tt
  | fanout x y => fanout (map f x) (map f y)

  | ex x y => ex x (map f y)
  | Λ x => Λ (λ y, map f (x y))
  end.

(* FIXME implement join? *)

Definition cases {A τ1 τ2 B} (x: El A (τ1 + τ2)) (f: El A τ1 → B) (g: El A τ2 → B): B.
Proof.
  dependent destruction x.
  - exact (f x).
  - exact (g x).
Defined.

Inductive W {P} :=
| roll: El W P → W.
Arguments W: clear implicits.

Definition unroll {P} (x: W P): El (W P) P :=
  match x with
  | roll x => x
  end.

(* Fixpoint fold {P A}(f: El A P → A) (x: W P) {struct x}: A. *)
(* Proof. *)
(*   destruct x. *)
(*   refine (f _). *)
(*   refine (map (fold _ _ f) e). *)
(* Defined. *)

(* Definition nat_schema := unit + id. *)
(* Definition nat := W nat_schema. *)

(* Definition O: nat := roll (i1 tt). *)
(* Definition S (x: nat): nat := roll (i2 (pure x)). *)

(* Fixpoint add (x y: nat) {struct x}: nat := *)
(*   cases (unroll x) *)
(*     (λ _, y) *)
(*     (λ x', S (add (unpure x') y)). *)

ugly.v

Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.

Module Import Poly.
  Inductive U :=
  | const (A: Type)

  | id
  (* | compose (τ0 τ1: U) *)

  | empty
  | sum (τ0 τ1: U)

  | unit
  | prod (τ0 τ1: U)

  | Σ {A: Type} (τ: A → U)
  | Π {A: Type} (τ: A → U)
  .

  Implicit Type τ: U.

  (* Infix "∘" := compose (at level 30). *)
  Infix "+" := sum.
  Infix "*" := prod.

  Inductive S: U → Type :=
  | pure: S id

  | k {A}: A → S (const A)

  | i1 {τ1 τ2}: S τ1 → S (τ1 + τ2)
  | i2 {τ1 τ2}: S τ2 → S (τ1 + τ2)

  | tt: S unit
  | fanout {τ1 τ2}: S τ1 → S τ2 → S (τ1 * τ2)

  | ex {A} {τ: A → U} (x: A): S (τ x) → S (Σ τ)
  | Λ {A} {τ: A → U}: (∀ (x: A), S (τ x)) → S (Π τ)
  .

  Inductive π: ∀ {τ: U}, S τ → Type :=
  | π_pure: π pure
  | π_fanout_1 {τ1 τ2} {x: S τ1} {y: S τ2}: π x → π (fanout x y)
  | π_fanout_2 {τ1 τ2} {x: S τ1} {y: S τ2}: π y → π (fanout x y)

  | π_i1 {τ1 τ2} {x: S τ1}: π x → @π (τ1 + τ2) (i1 x)
  | π_i2 {τ1 τ2} {x: S τ2}: π x → @π (τ1 + τ2) (i2 x)

  | π_ex {A} {τ: A → U} {x: A} {y: S (τ x)}: π y → π (ex x y)
  | π_Λ {A} {τ: A → U} {x: ∀ y, S (τ y)} y: π (x y) → π (Λ x)
  .

  Inductive W {τ} :=
  | roll (x: S τ): (π x → W) → W.
  Arguments W: clear implicits.

  Definition tag {τ} (x: W τ): S τ :=
    match x with
    | roll x _ => x
    end.

  Definition field {τ} (x: W τ): π (tag x) → W τ :=
    match x with
    | roll _ f => f
    end.
End Poly.

Definition nat_schema := unit + id.
Definition nat := W nat_schema.

Definition unπ_tt {A} (x: π tt): A.
Proof.
  dependent destruction x.
Defined.

Definition unπ_i1 {τ1 τ2} {x: S τ1} (y: @π (τ1 + τ2) (i1 x)): π x.
Proof.
  dependent destruction y.
  auto.
Defined.

Definition unπ_i2 {τ1 τ2} {x: S τ2} (y: @π (τ1 + τ2) (i2 x)): π x.
Proof.
  dependent destruction y.
  auto.
Defined.

Definition O: nat := roll (i1 tt) (λ x, unπ_tt (unπ_i1 x)).
Definition S (x: nat): nat := roll (i2 pure) (λ _, x).