(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Forall Types.Sigma.

(** * Theorems about W-types (well-founded trees) *)

Inductive W (A : Type) (B : A -> Type) : Type :=
  w_sup (x : A) : (B x -> W A B) -> W A B.

Definition w_label {A B} (w : W A B) : A :=
  match w with
  | w_sup x y => x
  end.

Definition w_arg {A B} (w : W A B) : B (w_label w) -> W A B :=
  match w with
  | w_sup x y => y
  end.

Definition issig_W (A : Type) (B : A -> Type)
  : _ <~> W A B := ltac:(issig).

(** ** Paths *)

Definition equiv_path_wtype {A B} (z z' : W A B)
  : (w_label z;w_arg z) = (w_label z';w_arg z') :> {a : _ & B a -> W A B} <~> z = z'
  := (equiv_ap' (issig_W A B)^-1%equiv z z')^-1%equiv.

Definition equiv_path_wtype' {A B} (z z' : W A B)
  : {p : w_label z = w_label z' & w_arg z = w_arg z' o transport B p}
    <~> z = z'.
A: Type
B: A -> Type
z, z': W A B
{p : w_label z = w_label z' &
w_arg z = w_arg z' o transport B p} <~> z = z'
Proof.
A: Type
B: A -> Type
z, z': W A B
{p : w_label z = w_label z' &
w_arg z = w_arg z' o transport B p} <~> z = z'
  refine (equiv_path_wtype _ _ oE equiv_path_sigma _ _ _ oE _).
A: Type
B: A -> Type
z, z': W A B
{p : w_label z = w_label z' &
w_arg z =
(fun x : B (w_label z) => w_arg z' (transport B p x))} <~>
{p : (w_label z; w_arg z).1 = (w_label z'; w_arg z').1
&
transport (fun a : A => B a -> W A B) p
  (w_label z; w_arg z).2 = (w_label z'; w_arg z').2}
  apply equiv_functor_sigma_id.
A: Type
B: A -> Type
z, z': W A B
forall a : w_label z = w_label z',
w_arg z =
(fun x : B (w_label z) => w_arg z' (transport B a x)) <~>
transport (fun a0 : A => B a0 -> W A B) a
  (w_label z; w_arg z).2 = (w_label z'; w_arg z').2
  destruct z as [z1 z2], z' as [z1' z2'].
A: Type
B: A -> Type
z1: A
z2: B z1 -> W A B
z1': A
z2': B z1' -> W A B
forall
a : w_label (w_sup A B z1 z2) =
    w_label (w_sup A B z1' z2'),
w_arg (w_sup A B z1 z2) =
(fun x : B (w_label (w_sup A B z1 z2)) =>
 w_arg (w_sup A B z1' z2') (transport B a x)) <~>
transport (fun a0 : A => B a0 -> W A B) a
  (w_label (w_sup A B z1 z2); w_arg (w_sup A B z1 z2)).2 =
(w_label (w_sup A B z1' z2');
w_arg (w_sup A B z1' z2')).2
  cbn; intros p.
A: Type
B: A -> Type
z1: A
z2: B z1 -> W A B
z1': A
z2': B z1' -> W A B
p: z1 = z1'
z2 = (fun x : B z1 => z2' (transport B p x)) <~>
transport (fun a : A => B a -> W A B) p z2 = z2'
  destruct p.
A: Type
B: A -> Type
z1: A
z2, z2': B z1 -> W A B
z2 = (fun x : B z1 => z2' (transport B 1 x)) <~>
transport (fun a : A => B a -> W A B) 1 z2 = z2'
  reflexivity.
Defined.

(** ** W-types preserve truncation *)

Global Instance istrunc_wtype `{Funext}
  {A B} {n : trunc_index} `{IsTrunc n.+1 A}
: IsTrunc n.+1 (W A B) | 100.
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
IsTrunc n.+1 (W A B)
Proof.
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
IsTrunc n.+1 (W A B)
  apply istrunc_S.
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
forall x y : W A B, IsTrunc n (x = y)
  intros z; induction z as [a w].
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
a: A
w: B a -> W A B
X: forall (b : B a) (y : W A B), IsTrunc n (w b = y)
forall y : W A B, IsTrunc n (w_sup A B a w = y)
  intro y; destruct y as [a0 w0].
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
a: A
w: B a -> W A B
X: forall (b : B a) (y : W A B), IsTrunc n (w b = y)
a0: A
w0: B a0 -> W A B
IsTrunc n (w_sup A B a w = w_sup A B a0 w0)
  nrefine (istrunc_equiv_istrunc _ (equiv_path_wtype' _ _)).
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
a: A
w: B a -> W A B
X: forall (b : B a) (y : W A B), IsTrunc n (w b = y)
a0: A
w0: B a0 -> W A B
IsTrunc n
  {p
  : w_label (w_sup A B a w) =
    w_label (w_sup A B a0 w0) &
  w_arg (w_sup A B a w) =
  (fun x : B (w_label (w_sup A B a w)) =>
   w_arg (w_sup A B a0 w0) (transport B p x))}
  rapply istrunc_sigma.
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
a: A
w: B a -> W A B
X: forall (b : B a) (y : W A B), IsTrunc n (w b = y)
a0: A
w0: B a0 -> W A B
forall
a1 : w_label (w_sup A B a w) =
     w_label (w_sup A B a0 w0),
IsTrunc n
  (w_arg (w_sup A B a w) =
   (fun x : B (w_label (w_sup A B a w)) =>
    w_arg (w_sup A B a0 w0) (transport B a1 x)))
  cbn; intro p.
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
a: A
w: B a -> W A B
X: forall (b : B a) (y : W A B), IsTrunc n (w b = y)
a0: A
w0: B a0 -> W A B
p: a = a0
IsTrunc n (w = (fun x : B a => w0 (transport B p x)))
  destruct p.
H: Funext
A: Type
B: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 A
a: A
w: B a -> W A B
X: forall (b : B a) (y : W A B), IsTrunc n (w b = y)
w0: B a -> W A B
IsTrunc n (w = (fun x : B a => w0 (transport B 1 x)))
  apply (istrunc_equiv_istrunc _ (equiv_path_forall _ _)).
Defined.