{B C D : Type} `{Is01Cat B, Is01Cat C, Is01Cat D} `{IsPointed B, IsPointed C, IsPointed D} (F : B -->* C) (G : C -->* D) : B -->* D. Proof. snrapply Build_BasepointPreservingFunctor. - exact (G o F). - exact _. - exact (bp_pointed G $o fmap G (bp_pointed F)). Defined.
Require Import Basics.Overture Basics.Tactics.