{ CO : forall x, morphism D (F x) (G x) | forall s d (m : morphism C s d), CO d o F _1 m = G _1 m o CO s } <~> NaturalTransformation F G. Proof. let build := constr:(@Build_NaturalTransformation _ _ F G) in let pr1 := constr:(@components_of _ _ F G) in let pr2 := constr:(@commutes _ _ F G) in apply (equiv_adjointify (fun u => build u.1 u.2) (fun v => (pr1 v; pr2 v))); hnf; [ intros []; intros; simpl; expand; f_ap; exact (center _) | intros; apply eta_sigma ]. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Equivalences HoTT.Types Trunc Basics.Tactics.