Definition lan_after_pre_comp_iso (P : [C'', D]) : z_iso (lan_functor HD F' (pre_comp_functor F' P)) P. Proof. refine (iso_from_fully_faithful_reflection (fully_faithful_from_equivalence _ _ _ Hequiv) _). apply (functor_on_z_iso (pre_comp_functor F)). exact (z_iso_inv (pre_comp_after_lan_iso _ HF' _ _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.LeftKanExtension. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.AlgebraicTheories.FundamentalTheorem.SurjectivePrecomposition. Section AdjointEquivalenceFromComp. End AdjointEquivalenceFromComp.