Definition monoid_free_forgetful_counit : nat_trans (functor_composite monoid_forgetful_functor monoid_free_functor ) (functor_identity _). Proof. use make_nat_trans. - intro. use tpair. + intro; apply iterop_list_mon; assumption. + split. * intros ? ?; apply iterop_list_mon_concatenate. * reflexivity. - intros ? ? f; apply monoidfun_paths. apply funextfun; intro; simpl in *. apply (iterop_list_mon_map f). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Free_Monoids_and_Groups. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core.