Lean4
/-- The equivalence of categories `LightProfinite ≌ LightDiagram` -/
noncomputable def equivDiagram : LightProfinite.{u} ≌ LightDiagram.{u}
where
functor := lightProfiniteToLightDiagram
inverse := lightDiagramToLightProfinite
unitIso := Iso.refl _
counitIso :=
NatIso.ofComponents (fun _ ↦ lightDiagramToProfinite.preimageIso (Iso.refl _))
(by
intro _ _ f
simp only [Functor.comp_obj, lightDiagramToLightProfinite_obj, lightProfiniteToLightDiagram_obj, Functor.id_obj,
Functor.comp_map, lightDiagramToLightProfinite_map, lightProfiniteToLightDiagram_map,
lightDiagramToProfinite_obj, Functor.preimageIso_hom, Iso.refl_hom, Functor.id_map]
erw [lightDiagramToProfinite.preimage_id, lightDiagramToProfinite.preimage_id, Category.comp_id f])
functor_unitIso_comp _ := by simpa using lightDiagramToProfinite.preimage_id
