+ eapply if_comp.
+ apply (if_associativity (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) F
+ (retraction_retraction F)).
+ eapply if_comp; [ idtac | apply if_right_identity ].
+ apply (if_respects
+ (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
+ (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
+ (F >>>> retraction_retraction F)
+ (functor_id _)).
+ apply (if_id _).