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