F' o F -| G o G'. Proof. exists compose_unit compose_counit; simpl; abstract ( repeat match goal with | _ => intro | _ => reflexivity | _ => progress rewrite ?identity_of, ?left_identity, ?right_identity | _ => rewrite <- ?composition_of, unit_counit_equation_1 | _ => rewrite <- ?composition_of, unit_counit_equation_2 | [ A : _ -| _ |- _ = 1%morphism ] => (etransitivity; [ | apply (unit_counit_equation_1 A) ]; try_associativity_quick f_ap) | [ A : _ -| _ |- _ = 1%morphism ] => (etransitivity; [ | apply (unit_counit_equation_2 A) ]; try_associativity_quick f_ap) | _ => repeat (try_associativity_quick rewrite <- !composition_of); progress repeat apply ap; rewrite ?composition_of | [ |- context[components_of ?T] ] => (try_associativity_quick simpl rewrite <- (commutes T)); try_associativity_quick (apply concat_right_identity || apply concat_left_identity) | [ |- context[components_of ?T] ] => (try_associativity_quick simpl rewrite (commutes T)); try_associativity_quick (apply concat_right_identity || apply concat_left_identity) end ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import Functor.Identity. Require Import Adjoint.UnitCounit Adjoint.Core. Require Import HoTT.Tactics. Require Import Basics.Tactics.