Commit 2024-11-28 16:12 2f728e97

View on Github →

chore: split Prefunctor out of Quiver (#19525)

Estimated changes

deleted def Prefunctor.comp
deleted theorem Prefunctor.comp_assoc
deleted theorem Prefunctor.comp_id
deleted theorem Prefunctor.congr_map
deleted theorem Prefunctor.ext
deleted def Prefunctor.id
deleted theorem Prefunctor.id_comp
deleted theorem Prefunctor.mk_map
deleted theorem Prefunctor.mk_obj
deleted structure Prefunctor
added def Prefunctor.comp
added theorem Prefunctor.comp_assoc
added theorem Prefunctor.comp_id
added theorem Prefunctor.congr_map
added theorem Prefunctor.ext
added def Prefunctor.id
added theorem Prefunctor.id_comp
added theorem Prefunctor.mk_map
added theorem Prefunctor.mk_obj
added structure Prefunctor