Some of my mathlib contributions

• Quasi-categories and inner anodyne extensions. Inner fibrations, inner and strong inner anodyne extensions; interactions with pushout-products, including the result that the internal hom into a quasi-category is a quasi-category. Inner fibrations, inner anodyne extensions, pushout-products and functor quasi-categories.
• Simplicial sets and subcomplexes. Products of simplicial sets and subcomplexes, and the relationship between subcomplexes and pushout-products. Monoidal category structure on simplicial sets, pushout-products of simplicial sets.
• Leibniz constructions and parametrized adjunctions. General pushout-products and pullback-homs, Leibniz bifunctors, Leibniz adjunctions, and the corresponding equivalences of lifting properties. Leibniz constructions, lifting properties of pushout-products, pushout-products and pullback-homs.
• Monoidal arrow categories. Monoidal and monoidal-closed structures on arrow categories induced by pushout-products and pullback-homs, including braided and symmetric structures. Monoidal arrow categories.
• Lifting properties and retracts. Left and right lifting properties for classes of morphisms; their stability under retracts, base and cobase change, products, coproducts, and composition; and categorical retracts of objects and arrows. Left and right lifting properties, categorical retracts, morphism properties stable under retracts.
• Adhesive categories and subobjects. Infrastructure for adhesive categories and binary coproducts of subobjects in an adhesive category, including the result that pushout-products of monomorphisms are monomorphisms. Adhesive categories, subobjects in adhesive categories.
• Enriched functor categories and functors to Type. Explicit product and coproduct constructions for type-valued functors, internal homs and enrichment of functor categories over type-valued functors, and the monoidal-closed structure on categories of functors to Type. Products and coproducts of type-valued functors, internal homs and enrichment of functor categories, monoidal-closed functor categories.
• Pivotal and spherical categories. Pivotal categories, spherical categories, and the spherical structure on symmetric rigid categories.
• Monoidal quotient categories. The construction of monoidal structures on quotient categories.
• Subobjects in abelian categories. Modularity of subobject lattices, the correspondence theorem for subobjects, the second isomorphism theorem for subobjects.