Remove ported lax comma categories
Remove theorems that don't need to be ported
Remove ported adjoint hom