proposition: Lemma finalcoalgebra_is_z_iso : is_z_isomorphism α.
proof: Proof. use make_is_z_isomorphism. - exact α'. - split. + exact αα'_idA. + exact α'α_idFA. Defined.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total