∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u_1)) (X : FintypeCatᵒᵖ),
  (fun g => g ∘ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X).unop)) =
    CategoryTheory.CategoryStruct.id
      ((Opposite.unop X).carrier →
        F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op { carrier := PUnit.{u_1 + 1}, str := PUnit.fintype })))