Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
In proposition in the subsection in category theoretic logic a proposition in context is declared to be a -subobject of where is a class of monomorphisms - but the latter link is grey probably indicating that this class shall satisfy some (closure-)properties.
In this section it says the class often is chosen to be just that of all monomorphisms, which other choices do occur in the literature?
In a quasitopos, one sometimes takes the class of strong monomorphisms (which there coincide with the regular ones).
The entry proposition had no pointer back to anything type-theoretic. I have added a brief paragraph.
1 to 3 of 3