# Library Containers.W_with_Conversion

Require Export HoTT.

Context {uv : Univalence}.
Axiom A : Type.
Axiom B : A Type.
Axiom W : Type.
Axiom sup : a, (B a W) W.
Axiom W_rect :
P : Type,
( a, ( b : B a, P) P)
W P.
Axiom W_rect_β : P step a f,
W_rect P step (sup a f) = step a (W_rect P step o f).

Definition W' :=
{w : W &
{rect : P, ( a, (B a P) P) P &
(fun P stepW_rect P step w) = rect}}.

Definition sup' : a, (B a W') W'.
Proof.
intros a f.
(sup a (pr1 o f)).
serapply existT.
- exact (fun P stepstep a (fun b(f b).2.1 P step)).
- hnf.
apply path_forall; intros P.
apply path_forall; intros step.
apply (transitivity (W_rect_β P step a (pr1 o f))).
f_ap.
apply path_forall; intros b.
exact (ap10 (apD10 (f b).2.2 P) step).
Defined.

Definition label' (w : W') : A.
Proof.
destruct w as [w [rect p] ].
exact (rect A (fun a IHa)).
Defined.

Goal a f, label' (sup' a f) = a.
Proof.
reflexivity.
Defined.

Definition W_rect'
(P : Type) (step : a, ( b : B a, P) P) (w : W') :
P :=
(w.2.1 P step).

Goal P step a f,
W_rect' P step (sup' a f) = step a (W_rect' P step o f).
Proof.
reflexivity.
Qed.

Lemma W'_equiv_W : W' <~> W.
Proof.
- exact pr1.
- intros w.
w.
(fun P stepW_rect P step w).
reflexivity.
- intros w.
reflexivity.
- intros [w [rect p] ].
destruct p.
reflexivity.
Defined.

Lemma W'_is_W : W' = W.
Proof.
apply path_universe_uncurried.
apply W'_equiv_W.
Defined.

Goal transport (fun X a, (B a X) X) W'_is_W sup' = sup.
Proof.
apply path_forall; intros a. apply path_forall; intros f.
rewrite transport_forall_constant. rewrite transport_arrow.
unfold W'_is_W. rewrite transport_path_universe_uncurried.
simpl; f_ap.
apply path_forall; intros b.
rewrite transport_arrow_fromconst.
rewrite transport_path_universe_V_uncurried.
reflexivity.
Qed.

Goal transport (fun X P, ( a, (B a P) P) X P)
W'_is_W
W_rect' =
W_rect.
Proof.
apply path_forall; intros P. apply path_forall; intros step.
apply path_forall; intros w.
rewrite transport_forall_constant. rewrite transport_arrow_fromconst.
rewrite transport_arrow_toconst.
unfold W'_is_W. rewrite transport_path_universe_V_uncurried.
reflexivity.
Qed.