Results needed for topos theory

[plt-amy]

I'm writing up the beginnings of a section on topos theory at https://github.com/plt-amy/1lab/tree/feature/topoi (specific definition used: A topos is a lex reflective subcategory of a category of presheaves) and ran into a bunch of results we do not have yet. Tracking them here:

• Monadic adjunctions create limits (more generally, C^M is complete when C is)
• Reflective subcategory inclusions are monadic functors
• Limit respects natural isomorphism (i.e. for F ≅ G, we have Limit F → Limit G)
• Reflective subcategories are exponential ideals when the reflector is lex (Elephant, prop A4.3.1)
• Left adjoints preserve colimits (dualises right adjoints preserve limits, which we already have)
• Slices of presheaf categories are presheaf categories: PSh(C)/F ≅ PSh(∫ F)
• Sliced adjoint functors
• Equivalent characterisations of reflective subcategories: right adjoint is fully faithful ←→ counit is a natural isomorphism
• Colimits in functor categories (dualising limits in functor categories, which we already have)