proposition: Lemma equiv_sig_adjunction : adjunction_sig <~> (F -| G).
proof: Proof. issig. Defined.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core Functor.Identity Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths Types Trunc Basics.Tactics