I am a bit confused about the interpretation of "implication" in the standard treatment of categorical logic, for example in [Bart Jacobs 1999] "Categorical Logic and Type Theory".
(A). On the one hand, the book says that "terms give rise to morphisms between contexts, this is the canonical way to produce a category from types" (p.5) Under this interpretation, type contexts are the objects in the category, also called indices, such that fibers can be built over indices. Under the Curry-Howard isomorphism, this arrow would correspond to an implication $\Rightarrow$ in logic.
(B). On the other hand, "each fiber category $P(I)$ is a Boolean algebra... with propositional connectives such as $\wedge, \vee, \top, \bot, \neg$ in (Boolean) logic" (p.12, ibid). This seems to be the approach used by Lawvere when he formulated the notion of topos, with the sub-object classifier $\Omega$. Under this interpretation, one can also create the (Boolean) logic implication operator $A \Rightarrow B$ defined as $\neg A \vee B$ (in Boolean algebra, but one can also do similarly in Heyting algebra). Would this $\Rightarrow$ be in conflict with the $\Rightarrow$ in (A)?
Edit: More specifically, if there is an arrow $A \Rightarrow B$ in the fiber, as in (B), how does it correspond (via Curry-Howard) to some type or term in the base category?