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 step ⇒ W_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 step ⇒ step 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 IH ⇒ a)).
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.
  serapply equiv_adjointify.
  - exact pr1.
  - intros w.
    ∃ w.
    ∃ (fun P step ⇒ W_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.