proposition: Lemma M_coalg_eq : ∏ X Y : M B, M_coalgebra B X = M_coalgebra B Y.
proof: Proof. intros X Y. pose (π1eq := (M_carriers_eq X Y)). pose (f := pr1 ((pr2 Y) (M_coalgebra B X))). apply (total2_paths_f π1eq). 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 : X → F X} {g : Y → F Y} (p : X = Y), (forall (x : X), transportf F p (f x) = g (transportf (idfun UU) p x)) → transportf (λ X, X → F X) p f = g). { intros ? ? ? ? ? p H. induction p. unfold transportf. apply funextfun. exact H. } 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), transportf (idfun UU) π1eq x = (pr1 f) x). { intro. refine (toforallpaths _ _ _ _ x0). refine ((weqpath_transport (M_carriers_iso _ Y)) @ _). reflexivity. } assert (lemma2 : transportf F π1eq = F* (pr1 f)). { refine (!(arr_transport _ _ π1eq) @ _). apply maponpaths. unfold π1eq, M_carriers_eq. refine ((weqpath_transport (M_carriers_iso _ _)) @ _). reflexivity. } refine (_ @ !(maponpaths ψ (lemma1 x))). refine (toforallpaths _ (transportf F π1eq) (F* (pr1 f)) lemma2 (θ x) @ _). apply (toforallpaths _ (F* (pr1 f) ∘ θ) (ψ ∘ pr1 f)). exact (pr2 f). Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorCoalgebras_legacy UniMath.CategoryTheory.Categories.Type.Core UniMath.Induction.PolynomialFunctors UniMath.Induction.M.Core