Definition restricted_adjunction_left_adjoint : functor (full_subcat_nat_trans_is_z_iso η) (full_subcat_nat_trans_is_z_iso ε). Proof. use make_functor; [use make_functor_data|split]. - * intros c'; pose (c := precategory_object_from_sub_precategory_object _ _ c'). use tpair. -- exact (F c). -- cbn. use make_is_z_isomorphism. ++ exact (post_whisker η F _). ++ assert (HH : (post_whisker η F) c · ε (F c) = identity (F c)). { apply (triangle_id_left_ad are). } assert (inv : ∑ h, is_inverse_in_precat ((post_whisker η F) c) h). { use tpair. - exact (# F (inv_from_z_iso (make_z_iso' _ (pr2 c')))). - cbn. apply (functor_is_inverse_in_precat_inv_from_z_iso F (make_z_iso' _ (pr2 c'))). } split. ** pose (eq := right_inverse_of_iso_is_inverse ((post_whisker η F) c) ). specialize (eq (pr1 inv) (pr2 inv) (ε (F c)) HH). refine (maponpaths (fun z => z · _) eq @ _). apply is_inverse_in_precat1. apply is_inverse_in_precat_inv. exact (pr2 inv). ** exact HH. - intros ? ? f; cbn. use tpair. + exact (# F (precategory_morphism_from_sub_precategory_morphism _ _ _ _ f)). + exact tt. - intro; cbn. apply subtypePath; [intro; apply propproperty|]. apply functor_id. - intros ? ? ? ? ?; cbn. apply subtypePath; [intro; apply propproperty|]. apply functor_comp. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Propositions. 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.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering.