I'm not sure about the terminology here. I only learned about weak limits a bit ago. So a weak limit satisfies the existence property but not uniqueness property of a limit.
A "weak topos" ought to have all weak finite limits, a weak function space and a "weak subobject classifier." I can sort of figure out weak terminal objects, products and functions but I'm having trouble figuring out stuff like what a "weak subobject classifier" or "weak equalizer" ought to be.
I feel like a "weak topos" ought to correspond to a dependent type theory lacking functional extensionality and eta laws. Possible "weak natural numbers objects" for "weak W-topoi" ought to lack inductive principles for inductive types." I'm not sure but I think the same idea for coinductive types corresponds to equality not being the same as bisimilarity. This feels a lot to me like the impredicative Calculus of Constructions with Church encodings of inductive types.
In dependent type theory the subobject classifier usually corresponds to an proof irrelevant impredicative sort. I think the appropriate eta law here might correspond to propositional extensionality but I'm not sure.
Figuring out what laws not to assume for equalizers seems much harder for me. In type theory equalizers correspond to subset types $\{ x \mid f(x) = g(x) \}$. Thinking of this as a tuple of a value and a proof eta expansion is just $(\pi_1(e), \pi_2(e))$. I still have trouble thinking through what it means for equalizers though.
I think another problem might be that the weight of being a "weak topos" might enforce uniqueness for some things anyway. Not at all sure though.
I think maybe a more concrete way to think about things might be in terms of a sort of "category of weak presheafs." I'm not sure what a "free weak cocompletion" ought to be. You could probably come up with a category WeakSet to have WeakSet-valued presheafs but I have a hunch a better point of view might be from the equivalence with discrete fibrations. I'm not at all sure what a "weak discrete fibration" ought to be though.
Do these ideas sound familiar or sane? Where can I learn more about weak limits or this sort of stuff.