@joey From a logical point of view, in everyday maths, we say lot "assuming x is an element of A, ..." or "let x be an element of A ..." and carry on the rest of the argument. The fact that slicing a topos/LCCC is still a topos/LCCC makes this way of working possible: let A be an object of C, "assuming x : A" in the internal logic of C means switching from C to C/A, and the new category C/A is still a topos/LCCC, so we can continue using the same kind of logic. Also, the weakening functor p* : C -> C/A is a logical/LCC functor, so our existing structures in C are still available after "assuming x : A". For example, an exponential B^C in C after weakening is isomorphic to the exponential (p* B)^(p* C) in C/A.
For this reason, when using the internal language of topos/LCCC informally, you see people say things like "if x : A ⊢ f : B(x) and a : A then f(a) : B(a)", mentioning only the local new assumption x : A, rather than "if Γ, x : A ⊢ f : B(x) and Γ ⊢ a : A then Γ ⊢ f(a) : B(a)" that explicitly track all the assumptions. This is possible because of the fundamental lemma of topos/LCCCs—they are stable under "making assumptions".
Add comment