dsimp [Functor.comp, Functor.id]
α : Type u
inst✝ : Category α
⊢ singletonF ⋙ joinF = 𝟭 (List α)
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor X),
        map := fun {X Y} f ↦ Prefunctor.map joinF.toPrefunctor (Prefunctor.map singletonF.toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }