Lemma base_category_z_iso_weq (F₀ G₀ : base_category) : z_iso F₀ G₀ ≃ (∏ (x : C), z_iso (F₀ x) (G₀ x)). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.