(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. 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.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Adjoint.UnitCounit Adjoint.UnitCounitCoercions Adjoint.Hom. Require Import Category.Morphisms. Require Import Functor.Composition.Core. Require Import FunctorCategory.Morphisms. Require Import Functor.Identity. Require Import SetCategory.Morphisms. Require Import Basics.Trunc Types.Sigma HoTT.Tactics Equivalences.