rfl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor [] =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor []
no goals