C D F G (A : @AdjunctionUnitCounit C D F G) : AdjunctionUnit F G. Proof. exists (unit A). intros c d f. apply contr_inhabited_hprop; [ apply hprop_allpath | (exists (counit A d o F _1 f)); abstract unit_counit_of_t ]. intros [? ?] [? ?]. apply path_sigma_uncurried. let A := match goal with |- @sig ?A ?P => constr:(A) end in let H := fresh in assert (H : A); [ | exists H; exact (center _) ]. simpl. let x := match goal with |- ?x = ?y => constr:(x) end in let y := match goal with |- ?x = ?y => constr:(y) end in rewrite <- (right_identity _ _ _ x), <- (right_identity _ _ _ y), <- !(unit_counit_equation_1 A), <- ?associativity; repeat simpl rewrite <- (commutes (counit A)); (try_associativity_quick rewrite <- !composition_of); repeat apply ap; etransitivity; [ | symmetry ]; eassumption. 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.