Lean4
/-- The adjunction between forming the free category on a reflexive quiver, and forgetting a category
to a reflexive quiver.
-/
nonrec def adj : Cat.freeRefl.{max u v, u} ⊣ ReflQuiv.forget :=
Adjunction.mkOfUnitCounit
{ unit :=
{ app _ := adj.unit.app _
naturality _ _ _ := rfl }
counit :=
{ app _ := adj.counit.app _
naturality _ _ F := Quotient.lift_unique' _ _ _ (Quiv.adj.counit.naturality F) }
left_triangle := by
ext V
apply Cat.FreeRefl.lift_unique'
dsimp
conv => rhs; rw [Cat.id_eq_id]; apply Functor.comp_id
simp only [id_comp]
rw [Cat.comp_eq_comp, ← Functor.assoc]
change (Cat.FreeRefl.quotientFunctor _ ⋙ Cat.freeReflMap _) ⋙ _ = _
rw [Cat.freeReflMap_naturality, Functor.assoc]
dsimp only [Cat.freeRefl, Cat.free_obj, Cat.of_α, of_val, forget_obj, adj.unit.app_toPrefunctor]
rw [adj.counit.comp_app_eq]
dsimp only [Cat.of_α]
rw [Cat.freeMap_comp, Functor.assoc, Quiv.pathComposition_naturality]
rw [← Functor.assoc]
have := Quiv.freeMap_pathsOf_pathComposition
simp only at this
rw [this]
exact Functor.id_comp _
right_triangle := by
ext C
dsimp
exact forgetToQuiv_faithful _ _ (Quiv.adj.right_triangle_components C) }
