Definition restricted_adjunction_right_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 d'; pose (d := precategory_object_from_sub_precategory_object _ _ d'). use tpair. + exact (G d). + cbn. use make_is_z_isomorphism. * exact (post_whisker ε G _). * assert (HH : η (G d) · (post_whisker ε G) d = identity (G d)). { apply (triangle_id_right_ad are). } assert (inv : ∑ h, is_inverse_in_precat (post_whisker ε G d) h). { use tpair. - exact (# G (inv_from_z_iso (make_z_iso' _ (pr2 d')))). - apply (functor_is_inverse_in_precat_inv_from_z_iso G (make_z_iso' _ (pr2 d'))). } split. -- exact HH. -- pose (eq := left_inverse_of_iso_is_inverse ((post_whisker ε G) d)). specialize (eq (pr1 inv) (pr2 inv) (η (G d)) HH). refine (maponpaths (fun z => _ · z) eq @ _). apply is_inverse_in_precat1. exact (pr2 inv). - * intros ? ? f; cbn. use tpair. -- exact (# G (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.