proposition: Lemma W_alg_eq : ∏ X Y : W B, W_algebra B X = W_algebra B Y.
proof: Proof. intros X Y. pose (f := pr1 ((pr2 X) (W_algebra B Y))). pose (pr1eq := (W_carriers_eq X Y)). apply (total2_paths_f pr1eq). pose (is_final_X := pr2 X). pose (is_final_Y := pr2 Y). pose (θ := pr2 (pr1 X)). pose (ψ := pr2 (pr1 Y)). assert (trans_fun : forall {X Y : UU} {F : UU → UU} {f : F X → X} {g : F Y → Y} (p : X = Y), (forall (x : F X), g (transportf F p x) = (transportf (idfun UU) p (f x))) → transportf (λ X, F X → X) p f = g). { intros ? ? ? ? ? p H. induction p. apply funextfun. intro x. exact (!H x). } apply trans_fun. intro x. assert (arr_transport : forall {X Y : UU} (p : X = Y), F* (transportf (idfun _) p) = transportf F p). { intros ? ? p. induction p. reflexivity. } assert (lemma1 : forall x : pr1 (pr1 X), (pr1 f) x = transportf (idfun UU) pr1eq x ). { intro. refine (toforallpaths _ _ _ _ x0). refine (_ @ !(weqpath_transport (W_carriers_iso X Y))). reflexivity. } assert (lemma2 : transportf F pr1eq = F* (pr1 f)). { refine (!(arr_transport _ _ pr1eq) @ _). apply maponpaths. unfold pr1eq, W_carriers_eq. refine ((weqpath_transport (W_carriers_iso X Y)) @ _). reflexivity. } refine (_ @ lemma1 (θ x)). refine (maponpaths ψ (toforallpaths _ _ _ lemma2 x) @ _). apply (toforallpaths _ (λ x, ψ (F* (pr1 f) x)) (pr1 f ∘ θ)). exact (!pr2 f). Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core