Definition LRB_lunitor_nat_z_iso_pre (x y : B) : nat_z_iso (η_{x,y} ∙ (bindelta_pair_functor (constant_functor (R (hom x y)) (R (hom x x)) (η (hom x x) (id₁ x))) (functor_identity (R (hom x y))) ∙ LRB_composition x x y)) (η_{x,y} ∙ functor_identity (R (hom x y))). Proof. transparent assert (p : (nat_z_iso (η_{x,y} ∙ (bindelta_pair_functor (constant_functor (R (hom x y)) (R (hom x x)) (η (hom x x) (id₁ x))) (functor_identity (R (hom x y))) )) (bindelta_pair_functor (constant_functor (hom x y) (hom x x) (id₁ x)) (functor_identity (hom x y)) ∙ (pair_functor (η (hom x x)) (η_{x,y})))) ). { use make_nat_z_iso. - use make_nat_trans. + intro ; apply identity. + intro ; intros. cbn. do 3 rewrite id_left. rewrite id_right. apply maponpaths_2. apply (! functor_id (η (hom x x)) _). - intro ; apply (identity_is_z_iso (C := _ ⊠ _)). } use (nat_z_iso_comp (nat_z_iso_functor_comp_assoc _ _ _)). use (nat_z_iso_comp (post_whisker_nat_z_iso p _) _). use (nat_z_iso_comp (nat_z_iso_inv (nat_z_iso_functor_comp_assoc _ _ _))). use (nat_z_iso_comp (pre_whisker_nat_z_iso _ _) _). 2: apply lift_functor_along_comm. use (nat_z_iso_comp _ (nat_z_iso_inv (functor_commutes_with_id _))). use (nat_z_iso_comp (nat_z_iso_functor_comp_assoc _ _ _)). use post_whisker_nat_z_iso. use make_nat_z_iso. - apply lunitor_transf. - intro ; apply is_z_iso_lunitor. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RezkCompletions.RezkCompletions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.YonedaLemma. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Properties. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.