fact: Definition retraction_is_retraction : retraction_section · retraction_retraction = identity A := pr22 H.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors