I've been using the book "Topoi: A Categorial Analysis of Logic" by Robert Goldblatt. I found it intuitive and fun, but I feel like some parts are missing. For instance, I struggled to prove $a^1 \cong a$, and it seems like I wasn't the only one. In fact, Goldblatt's book produces the concept of Cartesian Closed Categories without first introducing Yoneda's lemma, let alone functors! (Note, though, that functors are introduced in chapter 9 and Yoneda's lemma is introduced in chapter 16).
At this point, I'm struggling again to prove something like $ev\circ \langle \lceil f\rceil, x\rangle = f \circ x$, and I have a feeling that it's for the same reason as the difficulty with proving stuff about exponents; namely, adjoints, functors, Yoneda's lemma, and much of the rigorous material of category theory is sorta glossed over in favor of a more intuitive approach.
I'm looking for those missing tools to solve some of the exercises in this book. I like the pace of "Topoi," and its exposition is pleasant, so I'd like to stick with it if at all possible, but are there any references that might be helpful as I'm learning?
You might find the following helpful:
which is at a pretty introductory level and perhaps goes slower over some key explanations than e.g. Leinster's wonderful book or even than Goldblatt. (It is stalled work-in-progress, set aside while I finish another project, and so comes with the usual "caveat lector" warning.)