(A : AdjunctionUnit F G) : AdjunctionUnitCounit F G. Proof. exists A.1 (counit_natural_transformation__of__adjunction_unit A); simpl; intros; try match goal with | [ |- context[?x.1] ] => exact x.2 end; []. abstract (to_unit_counit_nt zig__of__adjunction_unit ltac:(fun H => try_associativity_quick rewrite <- H)). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Adjoint.UnitCounit Adjoint.Dual. Require Import Functor.Composition.Core Functor.Identity. Require Import HoTT.Tactics Basics.Trunc Types.Sigma. Require Import Basics.Tactics.