proposition: Lemma adjunction_unit__of__adjunction_hom_helper (A : AdjunctionHom F G) (c : C) (d : D) (f : morphism C c (G d)) : IsHProp {g : morphism D (F c) d & G _1 g o A (c, F c) 1 = f}.
proof: Proof. apply hprop_allpath. intros [g0 H0] [g1 H1]; apply path_sigma_hprop; simpl. destruct H1. rewrite !adjunction_naturality in H0. rewrite !right_identity in H0. change (idmap g0 = idmap g1). rewrite <- (ap10 (@left_inverse _ _ _ (A (c, d)) _)). simpl rewrite H0. let k := constr:(ap10 (@left_inverse _ _ _ (A (c, d)) _)) in simpl rewrite k. reflexivity. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Adjoint.UnitCounit Adjoint.UnitCounitCoercions Adjoint.Hom Category.Morphisms Functor.Composition.Core FunctorCategory.Morphisms Functor.Identity SetCategory.Morphisms Basics.Trunc Types.Sigma HoTT.Tactics Equivalences