feat(category_theory/lifting_properties): create a new file about lifting properties (#6852)
This file introduces lifting properties, establishes a few basic properties, and constructs a subcategory spanned by morphisms having a right lifting property.