proposition: Lemma base_category_z_iso_weq (F₀ G₀ : base_category) : z_iso F₀ G₀ ≃ (∏ (x : C), z_iso (F₀ x) (G₀ x)).
proof: Proof. exists (base_category_z_iso_to_z_iso_fam F₀ G₀). use isweq_iso. - apply base_category_z_iso_fam_to_z_iso. - intros x. apply z_iso_eq. apply idpath. - intros x. apply funextsec. intros y. apply z_iso_eq. apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions