Library UniMath.Induction.W.Wtypes

Axiomatic definition of a W-type.

Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi 2019-2024.

Derived from the code in the GitHub repository https://github.com/HoTT/Archive/tree/master/LICS2012 , which accompanies the paper "_Inductive Types in Homotopy Type Theory_", by S. Awodey, N. Gambino and K. Sojakova.

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.Notations.
Require Import UniMath.MoreFoundations.PartA.

Axiomatic definition of a W-Type.

Definition Wtype (A: UU) (B: ∏ x: A , UU): UU
  := ∑ (U: UU)
       (w_sup: ∏ (x : A) (f : B x → U ), U)
       (w_ind: ∏ (P : U → UU) (e_s : ∏ (x: A) (f: B x → U) (IH: ∏ u: B x , P (f u)), P (w_sup x f)) (w: U ), P w ),
       (∏ (P : U → UU)
          (e_s : ∏ (x: A) (f: B x → U) (IH: ∏ u: B x , P (f u)), P (w_sup x f))
          (x : A) (f : B x → U )
        , w_ind P e_s (w_sup x f) = e_s x f (λ u , w_ind P e_s (f u))).

Coercion w_carrier {A: UU} {B: ∏ x: A , UU} (W: Wtype A B): UU := pr1 W.

Section W.

Constructor.

Definition makeWtype {A: UU} {B: ∏ x: A , UU}
  (U: UU)
  (w_sup: ∏ (x : A) (f : B x → U ), U)
  (w_ind: ∏ (P : U → UU) (e_s : ∏ (x: A) (f: B x → U) (IH: ∏ u: B x , P (f u)), P (w_sup x f)) (w: U ), P w)
  (w_beta: ∏ (P : U → UU)
    (e_s : ∏ (x: A) (f: B x → U) (IH: ∏ u: B x , P (f u)), P (w_sup x f))
    (x : A) (f : B x → U )
    , w_ind P e_s (w_sup x f) = e_s x f (λ u , w_ind P e_s (f u)))
  : Wtype A B
  := (U ,,w_sup ,,w_ind ,,w_beta).

Context {A: UU} {B: ∏ x: A , UU} {W: Wtype A B}.

Accessors.

Definition w_sup := pr12 W.

Definition w_ind := pr122 W.

Definition w_beta := pr222 W.

Derived rules.

First-order eta rule.

Definition w_eta_1 (P: W → UU) (e_s: ∏ (x: A) (f: B x → W) (IH: ∏ u: B x , P (f u)), P (w_sup x f))
                   (h: ∏ x: W , P x) (p_s: ∏ (x: A) (f: B x → W ), h (w_sup x f) = (e_s x f (λ b , h (f b))))
  : ∏ (w : W ), h w = w_ind P e_s w.
Proof.
  refine (w_ind _ _).
  intros.
  cbn.
  cbn in IH.
  etrans.
  - apply p_s.
  - etrans.
    all: revgoals.
    * apply pathsinv0.
      apply w_beta.
    * apply maponpaths.
      apply funextsec.
      intro.
      apply IH.
Defined.

Second-order eta rule.

Definition w_eta_2 (P: W → UU) (e_s: ∏ (x: A) (f: B x → W) (IH: ∏ u: B x , P (f u)), P (w_sup x f))
                               (h: ∏ x: W , P x) (p_s: ∏ (x: A) (f: B x → W ), h (w_sup x f) = (e_s x f (λ b , h (f b))))
  : ∏ (x : A) (f : B x → W )
      , w_eta_1 P e_s h p_s (w_sup x f) @ w_beta P e_s x f
        = p_s x f @ maponpaths (e_s x f) (funextsec _ _ _ (fun b => w_eta_1 P e_s h p_s (f b))).
Proof.
  intros.
  apply hornRotation_rr.
  etrans.
  - apply (w_beta (λ w , h w = w_ind P e_s w)).
  - apply path_assoc.
Defined.

End W.