proposition: Lemma restricted_adjunction_equivalence : equivalence_of_cats (full_subcat_nat_trans_is_z_iso η) (full_subcat_nat_trans_is_z_iso ε).
proof: Proof. exists (adjunction_data_from_is_left_adjoint are_adjoints_restricted_adjunction). split. - intro a. pose (isomor := make_z_iso' _ (pr2 a) : z_iso (pr1 a) (pr1 (right_adjoint are_adjoints_restricted_adjunction (left_adjoint are_adjoints_restricted_adjunction a)))). apply (iso_in_precat_is_iso_in_subcat C _ _ _ isomor). - intro b. cbn. pose (isomor := make_z_iso' _ (pr2 b) : z_iso (pr1 (left_adjoint are_adjoints_restricted_adjunction (right_adjoint are_adjoints_restricted_adjunction b))) (pr1 b)). apply (iso_in_precat_is_iso_in_subcat _ _ _ _ isomor). Defined.
imports: UniMath.Foundations.Preamble UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Subcategory.Full UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.whiskering