Lean4
/-- The functor sending a reflexive quiver to the free category it generates, a quotient of
its path category -/
@[simps!]
def freeRefl : ReflQuiv.{v, u} ⥤ Cat.{max u v, u}
where
obj V := Cat.of (FreeRefl V)
map F := freeReflMap F
map_id
X :=
by
refine (Quotient.lift_unique _ _ _ _ ((Functor.comp_id _).trans <| (Functor.id_comp _).symm.trans ?_)).symm
congr 1
exact (free.map_id X.toQuiv).symm
map_comp {X Y Z} f
g := by
apply (Quotient.lift_unique _ _ _ _ _).symm
change FreeRefl.quotientFunctor _ ⋙ _ = _
rw [Cat.comp_eq_comp, ← Functor.assoc, freeReflMap_naturality, Functor.assoc, freeReflMap_naturality, ←
Functor.assoc]
have : freeMap (f ≫ g).toPrefunctor = freeMap f.toPrefunctor ⋙ freeMap g.toPrefunctor := by rw [← freeMap_comp]; rfl
rw [this]
