Definition base_category_z_iso_to_z_iso_fam (F₀ G₀ : base_category) : z_iso F₀ G₀ → (∏ (x : C), z_iso (F₀ x) (G₀ x)). Proof. intros [γ Hγ]. destruct Hγ as [θ [Hγθ Hθγ]]. intros x. exists (γ x), (θ x). split. - apply (toforallpaths _ _ _ Hγθ). - apply (toforallpaths _ _ _ Hθγ). 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.