# Library UniMath.Induction.W.Core

The W-type associated to (A, B) is the initial algebra of the associated polynomial functor. See the comment in Induction.M.Core as to why we can't use category-theoretic terminology.

Section W.
Context {A : UU} (B : A UU).
Local Notation F := (polynomial_functor A B).

The "recursion principle": there exists a morphism into any other algebra.
(The first two rules in Proposition 5.8 in Awodey, Gambino, and Sojakova)
Definition is_preinitial (X : algebra_ob F) :=
(Y : algebra_ob F), algebra_mor F X Y.

The "homotopy-initiality principle": there is exactly one morphism into any other algebra.
(Definition 5.6 in Awodey, Gambino, and Sojakova)
Definition is_initial (X : algebra_ob F) :=
(Y : algebra_ob F), iscontr (algebra_mor F X Y).

Definition isaprop_is_initial (X : algebra_ob F) : isaprop (is_initial X).
Proof.
apply impred.
intro.
apply isapropiscontr.
Defined.

Lemma is_preinitial_to_is_initial (X : algebra_ob F) :
is_preinitial X ( Y, isaprop (algebra_mor F X Y)) is_initial X.
Proof.
exact (λ is_pre is_prop Y, iscontraprop1 (is_prop Y) (is_pre Y)).
Defined.

Definition W := (X : algebra_ob F), is_initial X.
Definition W_algebra : W algebra_ob F := pr1.
Definition W_is_initial : (w : W), is_initial (pr1 w) := pr2.
Coercion W_algebra : W >-> algebra_ob.
End W.

Arguments isaprop_is_initial {_ _} _.
Arguments is_preinitial {_ _} _.
Arguments is_initial {_ _} _.