{ retraction_section_fobj : C -> D
; retraction_section : Functor C D retraction_section_fobj
; retraction_retraction_fobj : D -> C
; retraction_retraction : Functor D C retraction_retraction_fobj
; retraction_composes : retraction_section >>>> retraction_retraction ≃ functor_id _
}.
{ retraction_section_fobj : C -> D
; retraction_section : Functor C D retraction_section_fobj
; retraction_retraction_fobj : D -> C
; retraction_retraction : Functor D C retraction_retraction_fobj
; retraction_composes : retraction_section >>>> retraction_retraction ≃ functor_id _
}.