Definition base_category_z_iso_fam_to_z_iso (F₀ G₀ : base_category) : (∏ (x : C), z_iso (F₀ x) (G₀ x)) → z_iso F₀ G₀. Proof. intros γ. exists γ, (λ x, inv_from_z_iso (γ x)). split. - apply funextsec. intros x. cbn. apply z_iso_inv_after_z_iso. - apply funextsec. intros x. cbn. apply z_iso_after_z_iso_inv. 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.