Coreflective subcategory (source code)

= Coreflective subcategory
{title2=$I\dashv q$}

A full subcategory is coreflective when its inclusion $I$ has a right adjoint $q$. The counit $IqX\to X$ is universal for maps to $X$ from objects of the subcategory. The <comonad> $Iq$ is idempotent. For a finite-limit-closed coreflective subcategory of a <topos>, its coalgebra construction can prove that the subcategory is itself a topos.