proposition: Lemma W_carriers_iso : ∏ X Y : W B, (alg_carrier F X) ≃ (alg_carrier F Y).
proof: Proof. intros X Y. pose (X_mor_Y := iscontrpr1 (pr2 X Y)). pose (Y_mor_X := iscontrpr1 (pr2 Y X)). apply (weq_iso (mor_from_algebra_mor _ _ _ X_mor_Y) (mor_from_algebra_mor _ _ _ Y_mor_X)). - intro x. apply (toforallpaths _ (Y_mor_X ∘ X_mor_Y) (idfun _)). refine (base_paths (algebra_mor_comp _ _ _ _ X_mor_Y Y_mor_X) (algebra_mor_id F X) _). apply (proofirrelevancecontr (pr2 X X)). - intro y. apply (toforallpaths _ (X_mor_Y ∘ Y_mor_X) (idfun _)). refine (base_paths (algebra_mor_comp _ _ _ _ Y_mor_X X_mor_Y) (algebra_mor_id F Y) _). apply (proofirrelevancecontr (pr2 Y Y)). 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