proposition: Lemma equiv_hom_set_adjunction (c : C) (d : D) : morphism C c (G d) <~> morphism D (F c) d.
proof: Proof. refine (equiv_adjointify (fun f => (@center _ (T.2 _ _ f)).1) (fun g => G _1 g o T.1 c) _ _); intro. - match goal with | [ |- @pr1 ?A ?P ?x = ?y ] => change (x.1 = (exist P y idpath).1) end. apply (ap pr1). apply contr. - match goal with | [ |- context[?x.1] ] => apply x.2 end. Defined.
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